1(* this is an -*- sml -*- file *)
2val _ = HOL_Interactive.toggle_quietdec();
3
4val _ = loadPath :=
5            (concat [Globals.HOLDIR, "/examples/separationLogic/src"]) ::
6            (concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot"]) ::
7            !loadPath;
8
9val _ = map load ["holfootParser", "holfoot_pp_print", "holfootLib"];
10open holfootParser;
11open holfoot_pp_print;
12open holfootLib;
13
14open separationLogicTheory vars_as_resourceTheory holfootTheory generalHelpersTheory;
15
16use (Globals.HOLDIR ^ "/tools/hol-mode.sml");
17
18val _ = Feedback.set_trace "Unicode" 0;
19val _ = Feedback.set_trace "PPBackEnd use annotations" 0;
20val _ = Feedback.set_trace "PPBackEnd use styles" 1;
21val _ = Feedback.set_trace "PPBackEnd show types" 0;
22val _ = Feedback.set_trace "metis" 0;
23
24val examplesDir =
25    concat [Globals.HOLDIR,
26            "/examples/separationLogic/src/holfoot/EXAMPLES"];
27
28
29(*testing*)
30val _ = holfoot_auto_verify_spec (examplesDir ^ "/automatic/list.sf")
31val _ = holfoot_verify_spec (examplesDir ^ "/automatic/mergesort.sf") [];
32
33
34use (Globals.HOLDIR ^ "/tools/Holmake/QuoteFilter.sml");
35
36val _ = HOL_Interactive.toggle_quietdec();
37
38(* save state *)
39val state_file = "holfoot.state"
40val _ = PolyML.SaveState.saveState state_file;
41