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