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";›
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