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