1structure daisyLib :> daisyLib = 2struct 3 4open HolKernel Parse boolLib bossLib daisyTheory; 5 6fun run_daisy path func = let 7 val str = ``p_str "test" ^func`` 8 |> EVAL |> concl |> rand |> stringSyntax.fromHOLstring 9 val output_filename = path ^ "/Program" 10 val filename = output_filename ^ ".scala" 11 val f = TextIO.openOut filename 12 val _ = TextIO.output (f,str) 13 val _ = TextIO.closeOut f 14 val _ = OS.Process.system("cd "^path^" && ./daisy " ^ filename ^ " > /dev/null") 15 val f = TextIO.openIn output_filename 16 val str = (case TextIO.inputLine(f) of SOME str => str) 17 val _ = TextIO.closeIn f 18 val cs = explode " ,\n[]" 19 val strs = String.tokens (fn c => mem c cs) str 20 val err = el 3 strs |> stringSyntax.fromMLstring 21 val lower = el 5 strs |> stringSyntax.fromMLstring 22 val upper = el 6 strs |> stringSyntax.fromMLstring 23 val tm = ``rosa_correctness fp64_conf ^func 0 [(^err,^lower,^upper)]`` 24 in mk_oracle_thm "Daisy" ([],tm) end 25 26(* 27 28EXAMPLE: 29 30open daisyLib daisyTheory 31 32val func = ``(Func ["x"] [Assert (Cons (LessEq (X (Const "-1")) (X (Var "x")))); 33 Assert (Cons (LessEq (X (Var "x")) (X (Const "1"))))] 34 (NonRec (Simple (Exp (X (Var "x"))))))``; 35show_tags := true; 36val path = "/Users/mom22/tools/daisy"; 37 38 run_daisy path func 39 40*) 41 42end 43