# HG changeset patch # User blanchet # Date 1341991949 -7200 # Node ID 6a8d1879816167d944be6a471be7d0e8f9411acf # Parent 0016290f904c3222502403aa1fe906ed6fe3deb9 rationalized output diff -r 0016290f904c -r 6a8d18798161 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 09:32:29 2012 +0200 @@ -14,6 +14,7 @@ val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order val dependencies_of : string list -> thm -> string list + val goal_of_thm : thm -> thm val meng_paulson_facts : Proof.context -> string -> int -> real * real -> thm -> int -> (((unit -> string) * stature) * thm) list diff -r 0016290f904c -r 6a8d18798161 src/HOL/TPTP/mash_import.ML --- a/src/HOL/TPTP/mash_import.ML Tue Jul 10 23:36:03 2012 +0200 +++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 09:32:29 2012 +0200 @@ -15,6 +15,8 @@ structure MaSh_Import : MASH_IMPORT = struct +open MaSh_Export + val unescape_meta = let fun un accum [] = String.implode (rev accum) @@ -63,16 +65,15 @@ fun with_index facts s = (find_index (fn ((s', _), _) => s = s') facts + 1, s) fun index_string (j, s) = s ^ "@" ^ string_of_int j - fun print_result label facts {outcome, run_time, used_facts, ...} = - tracing (" " ^ label ^ ": " ^ - (if is_none outcome then - "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ - space_implode " " - (used_facts |> map (with_index facts o fst) - |> sort (int_ord o pairself fst) - |> map index_string) - else - "Failure: " ^ space_implode " " (map (fst o fst) facts) )) + fun str_of_res label facts {outcome, run_time, used_facts, ...} = + " " ^ label ^ ": " ^ + (if is_none outcome then + "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ + space_implode " " (used_facts |> map (with_index facts o fst) + |> sort (int_ord o pairself fst) + |> map index_string) + else + "Failure: " ^ space_implode " " (map (fst o fst) facts)) fun run_sh heading facts goal = let val problem = @@ -81,14 +82,11 @@ val prover = Sledgehammer_Run.get_minimizing_prover ctxt Sledgehammer_Provers.Normal prover_name - in - prover params (K (K (K ""))) problem - |> tap (print_result heading facts) - end + val res as {outcome, ...} = prover params (K (K (K ""))) problem + in (str_of_res heading facts res, is_none outcome) end fun solve_goal name suggs = let val name = of_fact_name name - val _ = tracing ("Goal: " ^ name) val th = case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of SOME (_, th) => th @@ -104,12 +102,12 @@ i facts val mash_facts = sugg_facts hyp_ts concl_t facts suggs val hybrid_facts = hybrid_facts meng_facts mash_facts + val (dep_s, dep_ok) = run_sh "Dependencies" deps_facts goal + val (meng_s, meng_ok) = run_sh "Meng & Paulson" meng_facts goal + val (mash_s, mash_ok) = run_sh "MaSh" mash_facts goal + val (hybrid_s, hybrid_ok) = run_sh "Hybrid" hybrid_facts goal in - run_sh "Dependencies" deps_facts goal; - run_sh "Meng & Paulson" meng_facts goal; - run_sh "MaSh" mash_facts goal; - run_sh "Hybrid" hybrid_facts goal; - () + tracing (cat_lines ["Goal: ", name, dep_s, meng_s, mash_s, hybrid_s]) end val explode_suggs = space_explode " " #> filter_out (curry (op =) "") fun do_line line =