Theory Compiler_Test

theory Compiler_Test
imports CakeML_Compiler
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";›

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

cakeml (prog) ‹simple_print›

end