src/holfoot/holfootLib.sml

54 val file = concat [examplesDir, "parallel_mergesort_data.sf"];
55 val file = concat [examplesDir, "mergesort.dsf"];
56 val file = concat [examplesDir, "tree.dsf"];
59 val t = parse_holfoot_file file
2738 fun holfoot_set_goal file =
2739      proofManagerLib.set_goal([], parse_holfoot_file file);
2741 fun holfoot_set_goal_preprocess file =
2742    ((proofManagerLib.set_goal([], parse_holfoot_file file));
2747 fun holfoot_set_goal_procedures file fL =
2748    ((proofManagerLib.set_goal ([], parse_holfoot_file_restrict fL file));
2765 val _ = Feedback.register_btrace ("holfoot print file", print_file);
2802 fun holfoot_verify_spec_internal verbose print_remaining (file, defaultConseqConv_opt, tacL) =
2823                          (if verbose then ("\nparsing file \""^file^"\" ... ") else
2824                                           ("\n"^file^" ... ")) else
2827      val t = parse_holfoot_file file;
2939 fun holfoot_interactive_verify_spec verbose print_err file optL_opt tacL =
2941    val (thm, ok) = holfoot_verify_spec_internal verbose print_err (file,
2950 fun holfoot_verify_spec file optL =
2951   fst (holfoot_interactive_verify_spec true false file (SOME optL) [])
2953 fun holfoot_tac_verify_spec file optL_opt tacL =
2954   fst (holfoot_interactive_verify_spec true false file optL_opt tacL)
2956 fun holfoot_auto_verify_spec file =
2957   fst (holfoot_interactive_verify_spec true true file (SOME [generate_vcs]) [])
2962 (* 27.5 s *) val file = concat [examplesDir, "/automatic/append.dsf"];
2963 (* 27.5 s *) val file = concat [examplesDir, "/automatic/copy.dsf"];
2964 (* 27.5 s *) val file = concat [examplesDir, "/interactive/array.dsf"];
2967 holfoot_set_goal file
2968 holfoot_verify_spec file []
2970 holfoot_set_goal_procedures file ["array_dispose_complicated"]
2973 holfoot_set_goal_procedures file ["array_frame_3"]
2975 holfoot_set_goal_procedures file ["array_frame_5"]
2976 holfoot_set_goal_procedures file ["array_frame_7"]
2977 holfoot_set_goal_procedures file ["array_lookup_1"]
2978 holfoot_set_goal_procedures file ["array_assign_1"]
2981 holfoot_interactive_verify_spec true (true,true,true) ([],[],[]) file
3011 val t = parse_holfoot_file file