Theory Compiler_Test

theory Compiler_Test
imports "../CakeML_Compiler"
begin

definition default_loc :: locs where
"default_loc =
  ( locn.row = 0, locn.col = 0, locn.offset = 0 ,
    locn.row = 0, locn.col = 0, locn.offset = 0 )"

definition simple_print :: Ast.prog where
"simple_print =
  [Ast.Tdec (Ast.Dlet default_loc Ast.Pany (Ast.App Ast.Opapp [Ast.Var (Short ''print''), Ast.Lit (Ast.StrLit ''hi'')]))]"

cakeml (literal) ‹print "hi1";›
cakeml (literal) ‹print "hi2";›

MLval out = CakeML_Compiler.eval_source CakeML_Compiler.Literal val x = 3 + 4; print (Int.toString x);›;
  @{assert} (out = "7")

cakeml (prog) simple_print

end