generate Meng--Paulson facts for evaluation purposes
authorblanchet
Tue, 10 Jul 2012 23:36:03 +0200
changeset 48239 0016290f904c
parent 48238 c9454e434665
child 48240 6a8d18798161
generate Meng--Paulson facts for evaluation purposes
src/HOL/TPTP/ATP_Theory_Export.thy
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/MaSh_Import.thy
src/HOL/TPTP/mash_export.ML
src/HOL/TPTP/mash_import.ML
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Jul 10 23:36:03 2012 +0200
@@ -5,7 +5,7 @@
 header {* ATP Theory Exporter *}
 
 theory ATP_Theory_Export
-imports "~~/src/HOL/Sledgehammer2d" (*###*) Complex_Main
+imports Complex_Main
 uses "atp_theory_export.ML"
 begin
 
@@ -16,7 +16,7 @@
 
 ML {*
 val do_it = false; (* switch to "true" to generate the files *)
-val thy = @{theory Complex_Main};
+val thy = @{theory};
 val ctxt = @{context}
 *}
 
--- a/src/HOL/TPTP/MaSh_Export.thy	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Tue Jul 10 23:36:03 2012 +0200
@@ -9,16 +9,23 @@
 uses "mash_export.ML"
 begin
 
+sledgehammer_params [provers = e, max_relevant = 500]
+
 ML {*
 open MaSh_Export
 *}
 
 ML {*
-val do_it = false (* switch to "true" to generate the files *)
+val do_it = false (* switch to "true" to generate the files *);
 val thy = @{theory List}
 *}
 
 ML {*
+if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions"
+else ()
+*}
+
+ML {*
 if do_it then generate_mash_commands thy "/tmp/mash_commands"
 else ()
 *}
@@ -38,8 +45,4 @@
 else ()
 *}
 
-ML {*
-find_index (curry (op =) 22) [0, 0, 9, 1, 2, 3]
-*}
-
 end
--- a/src/HOL/TPTP/MaSh_Import.thy	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy	Tue Jul 10 23:36:03 2012 +0200
@@ -9,6 +9,10 @@
 uses "mash_import.ML"
 begin
 
+sledgehammer_params
+  [max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
+
 declare [[sledgehammer_instantiate_inducts]]
 
 ML {*
@@ -16,12 +20,12 @@
 *}
 
 ML {*
-val do_it = true (* switch to "true" to generate the files *);
-val thy = @{theory List}
+val do_it = false (* switch to "true" to generate the files *);
+val thy = @{theory Nat}
 *}
 
 ML {*
-if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions2"
+if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions"
 else ()
 *}
 
--- a/src/HOL/TPTP/mash_export.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -14,10 +14,16 @@
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
   val dependencies_of : string list -> thm -> string list
+  val meng_paulson_facts :
+    Proof.context -> string -> int -> real * real -> thm -> int
+    -> (((unit -> string) * stature) * thm) list
+    -> ((string * stature) * thm) list
   val generate_mash_accessibility : theory -> bool -> string -> unit
   val generate_mash_features : theory -> bool -> string -> unit
   val generate_mash_dependencies : theory -> bool -> string -> unit
   val generate_mash_commands : theory -> string -> unit
+  val generate_meng_paulson_suggestions :
+    Proof.context -> theory -> string -> unit
 end;
 
 structure MaSh_Export : MASH_EXPORT =
@@ -192,6 +198,32 @@
 val dependencies_of =
   map fact_name_of oo theorems_mentioned_in_proof_term o SOME
 
+val freezeT = Type.legacy_freeze_type
+
+fun freeze (t $ u) = freeze t $ freeze u
+  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
+  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
+  | freeze (Const (s, T)) = Const (s, freezeT T)
+  | freeze (Free (s, T)) = Free (s, freezeT T)
+  | freeze t = t
+
+val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init
+
+fun meng_paulson_facts ctxt prover_name max_relevant relevance_thresholds
+                       goal i =
+  let
+    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+    val is_built_in_const =
+      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
+    val relevance_fudge =
+      Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
+    val relevance_override = {add = [], del = [], only = false}
+  in
+    Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+        max_relevant is_built_in_const relevance_fudge relevance_override []
+        hyp_ts concl_t
+  end
+
 fun generate_mash_accessibility thy include_thy file_name =
   let
     val path = file_name |> Path.explode
@@ -210,10 +242,8 @@
         val thy = theory_of_thm (hd ths)
         val parents = parent_thms thy_ths thy
         val ths = ths |> map (fact_name_of o Thm.get_name_hint)
-        val _ = fold do_thm ths parents
-      in () end
-    val _ = List.app (do_thy o snd) thy_ths
-  in () end
+      in fold do_thm ths parents; () end
+  in List.app (do_thy o snd) thy_ths end
 
 fun generate_mash_features thy include_thy file_name =
   let
@@ -228,8 +258,7 @@
         val feats = features_of thy (status, th)
         val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
       in File.append path s end
-    val _ = List.app do_fact facts
-  in () end
+  in List.app do_fact facts end
 
 fun generate_mash_dependencies thy include_thy file_name =
   let
@@ -246,8 +275,7 @@
         val deps = dependencies_of all_names th
         val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
       in File.append path s end
-    val _ = List.app do_thm ths
-  in () end
+  in List.app do_thm ths end
 
 fun generate_mash_commands thy file_name =
   let
@@ -274,7 +302,38 @@
       in [name] end
     val thy_ths = old_facts |> thms_by_thy
     val parents = parent_thms thy_ths thy
-    val _ = fold do_fact new_facts parents
-  in () end
+  in fold do_fact new_facts parents; () end
+
+fun generate_meng_paulson_suggestions ctxt thy file_name =
+  let
+    val {provers, max_relevant, relevance_thresholds, ...} =
+      Sledgehammer_Isar.default_params ctxt []
+    val prover_name = hd provers
+    val path = file_name |> Path.explode
+    val _ = File.write path ""
+    val facts = non_tautological_facts_of thy
+    val (new_facts, old_facts) =
+      facts |> List.partition (has_thy thy o snd)
+            |>> sort (thm_ord o pairself snd)
+    val i = 1
+    fun do_fact (fact as (_, th)) old_facts =
+      let
+        val name = Thm.get_name_hint th
+        val goal = goal_of_thm th
+        val kind = Thm.legacy_get_kind th
+        val _ =
+          if kind <> "" then
+            let
+              val suggs =
+                old_facts
+                |> meng_paulson_facts ctxt prover_name (the max_relevant)
+                                      relevance_thresholds goal i
+                |> map (fact_name_of o Thm.get_name_hint o snd)
+              val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
+            in File.append path s end
+          else
+            ()
+      in fact :: old_facts end
+  in fold do_fact new_facts old_facts; () end
 
 end;
--- a/src/HOL/TPTP/mash_import.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/mash_import.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -28,63 +28,23 @@
 
 val of_fact_name = unescape_meta
 
-val freezeT = Type.legacy_freeze_type;
-
-fun freeze (t $ u) = freeze t $ freeze u
-  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
-  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
-  | freeze (Const (s, T)) = Const (s, freezeT T)
-  | freeze (Free (s, T)) = Free (s, freezeT T)
-  | freeze t = t
-
-val prover_name = ATP_Systems.spassN
-val max_relevant = 40
-val slack_max_relevant = 2 * max_relevant
-val timeout = 5
+val max_relevant_slack = 2
 
 fun import_and_evaluate_mash_suggestions ctxt thy file_name =
   let
-    val params as {relevance_thresholds, ...} =
-      Sledgehammer_Isar.default_params ctxt
-         [("strict", "true"),
-          ("slice", "false"),
-          ("type_enc", "poly_guards??"),
-          ("timeout", string_of_int timeout),
-          ("preplay_timeout", "0"),
-          ("minimize", "true")]
-    val is_built_in_const =
-      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
-    val relevance_fudge =
-      Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
-    val relevance_override = {add = [], del = [], only = false}
+    val params as {provers, max_relevant, relevance_thresholds, ...} =
+      Sledgehammer_Isar.default_params ctxt []
+    val prover_name = hd provers
     val path = file_name |> Path.explode
     val lines = path |> File.read_lines
     val facts = non_tautological_facts_of thy
     val all_names = facts |> map (Thm.get_name_hint o snd)
     val i = 1
-    fun run_sh facts goal =
-      let
-        val facts =
-          facts |> take max_relevant
-                |> map Sledgehammer_Provers.Untranslated_Fact
-        val problem =
-          {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1,
-           facts = facts}
-        val prover =
-          Sledgehammer_Run.get_minimizing_prover ctxt
-              Sledgehammer_Provers.Normal prover_name
-      in prover params (K (K (K ""))) problem end
-    fun meng_facts goal =
-      let val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i in
-        Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
-            slack_max_relevant is_built_in_const relevance_fudge
-            relevance_override [] hyp_ts concl_t
-      end
     fun find_sugg facts sugg =
       find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
     fun sugg_facts hyp_ts concl_t facts =
       map_filter (find_sugg facts o of_fact_name)
-      #> take slack_max_relevant
+      #> take (max_relevant_slack * the max_relevant)
       #> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t
       #> map (apfst (apfst (fn name => name ())))
     fun hybrid_facts fs1 fs2 =
@@ -98,12 +58,12 @@
       in
         union fact_eq fs1 fs2
         |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
-        |> take max_relevant
+        |> take (the max_relevant)
       end
     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_res label facts {outcome, run_time, used_facts, ...} =
+    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 ^ "): " ^
@@ -113,6 +73,18 @@
                                   |> map index_string)
                 else
                   "Failure: " ^ space_implode " " (map (fst o fst) facts) ))
+    fun run_sh heading facts goal =
+      let
+        val problem =
+          {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1,
+           facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+        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
     fun solve_goal name suggs =
       let
         val name = of_fact_name name
@@ -122,22 +94,22 @@
             SOME (_, th) => th
           | NONE => error ("No fact called \"" ^ name ^ "\"")
         val deps = dependencies_of all_names th
-        val goal = th |> prop_of |> freeze |> cterm_of thy |> Goal.init
+        val goal = goal_of_thm th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
         val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
         val deps_facts = sugg_facts hyp_ts concl_t facts deps
-        val meng_facts = meng_facts goal facts
+        val meng_facts =
+          meng_paulson_facts ctxt prover_name
+              (max_relevant_slack * the max_relevant) relevance_thresholds goal
+              i facts
         val mash_facts = sugg_facts hyp_ts concl_t facts suggs
         val hybrid_facts = hybrid_facts meng_facts mash_facts
-        val deps_res = run_sh deps_facts goal
-        val meng_res = run_sh meng_facts goal
-        val mash_res = run_sh mash_facts goal
-        val hybrid_res = run_sh hybrid_facts goal
       in
-        print_res "Dependencies" deps_facts deps_res;
-        print_res "Meng & Paulson" meng_facts meng_res;
-        print_res "MaSh" mash_facts mash_res;
-        print_res "Hybrid" hybrid_facts hybrid_res
+        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;
+        ()
       end
     val explode_suggs = space_explode " " #> filter_out (curry (op =) "")
     fun do_line line =