# HG changeset patch
# User blanchet
# Date 1341868992 -7200
# Node ID 9075d4636dd86a54a9bd8bd30df256e50696a56b
# Parent  46e56c617dc1f4bb19b9fb4a5383d8d739d56941
generate problem file

diff -r 46e56c617dc1 -r 9075d4636dd8 src/HOL/TPTP/ATP_Theory_Export.thy
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Mon Jul 09 23:23:12 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Mon Jul 09 23:23:12 2012 +0200
@@ -16,13 +16,13 @@
 
 ML {*
 val do_it = true (* false ### *); (* switch to "true" to generate the files *)
-val thy = @{theory Groups}; (* @{theory Complex_Main}; ### *)
+val thy = @{theory Nat}; (* @{theory Complex_Main}; ### *)
 val ctxt = @{context}
 *}
 
 ML {*
 if do_it then
-  "/tmp/mash_accessibility.out"
+  "/tmp/mash_sample_problem.out"
   |> generate_mash_accessibility_file_for_theory thy
 else
   ()
@@ -30,8 +30,16 @@
 
 ML {*
 if do_it then
+  "/tmp/mash_accessibility.out"
+  |> generate_mash_accessibility_file_for_theory thy false
+else
+  ()
+*}
+
+ML {*
+if do_it then
   "/tmp/mash_features.out"
-  |> generate_mash_feature_file_for_theory ctxt thy
+  |> generate_mash_feature_file_for_theory thy false
 else
   ()
 *}
@@ -39,7 +47,7 @@
 ML {*
 if do_it then
   "/tmp/mash_dependencies.out"
-  |> generate_mash_dependency_file_for_theory thy
+  |> generate_mash_dependency_file_for_theory thy false
 else
    ()
 *}
diff -r 46e56c617dc1 -r 9075d4636dd8 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 09 23:23:12 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 09 23:23:12 2012 +0200
@@ -12,10 +12,12 @@
 
   val theorems_mentioned_in_proof_term :
     string list option -> thm -> string list
-  val generate_mash_accessibility_file_for_theory : theory -> string -> unit
-  val generate_mash_feature_file_for_theory :
-    Proof.context -> theory -> string -> unit
-  val generate_mash_dependency_file_for_theory : theory -> string -> unit
+  val generate_mash_accessibility_file_for_theory :
+    theory -> bool -> string -> unit
+  val generate_mash_feature_file_for_theory : theory -> bool -> string -> unit
+  val generate_mash_dependency_file_for_theory :
+    theory -> bool -> string -> unit
+  val generate_mash_problem_file_for_theory : theory -> string -> unit
   val generate_tptp_inference_file_for_theory :
     Proof.context -> theory -> atp_format -> string -> string -> unit
 end;
@@ -43,6 +45,12 @@
 
 val fact_name_of = escape_meta
 val thy_name_of = escape_meta
+val const_name_of = prefix const_prefix o escape_meta
+val type_name_of = prefix type_const_prefix o escape_meta
+
+val thy_name_of_thm = theory_of_thm #> Context.theory_name
+
+fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
 
 fun facts_of thy =
   let val ctxt = Proof_Context.init_global thy in
@@ -86,23 +94,47 @@
          |> map fact_name_of
   in names end
 
-fun interesting_const_names ctxt =
-  let val thy = Proof_Context.theory_of ctxt in
+fun interesting_const_names thy =
+  let val ctxt = Proof_Context.init_global thy in
     Sledgehammer_Filter.const_names_in_fact thy
         (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN)
+    #> map const_name_of
   end
 
+fun interesting_type_names t =
+  let
+    val bad = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
+    fun maybe_add_type (Type (s, Ts)) =
+        (not (member (op =) bad s) ? insert (op =) s)
+        #> fold maybe_add_type Ts
+      | maybe_add_type _ = I
+  in [] |> fold_types maybe_add_type t |> map type_name_of end
+
 fun theory_ord p =
   if Theory.eq_thy p then EQUAL
   else if Theory.subthy p then LESS
   else if Theory.subthy (swap p) then GREATER
   else EQUAL
 
-fun generate_mash_accessibility_file_for_theory thy file_name =
+val thm_ord = theory_ord o pairself theory_of_thm
+
+fun parent_thms thy_ths thy =
+  Theory.parents_of thy
+  |> map (thy_name_of o Context.theory_name)
+  |> map_filter (AList.lookup (op =) thy_ths)
+  |> map List.last
+  |> map (fact_name_of o Thm.get_name_hint)
+
+val thms_by_thy =
+  map (snd #> `thy_name_of_thm)
+  #> AList.group (op =)
+  #> sort (thm_ord o pairself (hd o snd))
+  #> map (apsnd (sort thm_ord))
+
+fun generate_mash_accessibility_file_for_theory thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val thy_name_of_thm = theory_of_thm #> Context.theory_name
     fun do_thm th prevs =
       let
         val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
@@ -110,19 +142,12 @@
       in [th] end
     val thy_ths =
       facts_of thy
-      |> map (snd #> `thy_name_of_thm)
-      |> AList.group (op =)
-      |> sort (theory_ord o pairself (theory_of_thm o hd o snd))
-      |> map (apsnd (sort (theory_ord o pairself theory_of_thm)))
+      |> not include_thy ? filter_out (has_thy thy o snd)
+      |> thms_by_thy
     fun do_thy ths =
       let
         val thy = theory_of_thm (hd ths)
-        val parents =
-          Theory.parents_of thy
-          |> map (thy_name_of o Context.theory_name)
-          |> map_filter (AList.lookup (op =) thy_ths)
-          |> map List.last
-          |> map (fact_name_of o Thm.get_name_hint)
+        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
@@ -130,52 +155,92 @@
   in () end
 
 (* TODO: Add types, subterms *)
-fun generate_mash_feature_file_for_theory ctxt thy file_name =
+fun features_of thy (status, th) =
+  let
+    val is_skolem =
+      String.isSubstring Sledgehammer_Filter.pseudo_skolem_prefix
+    fun fix_abs s =
+      if String.isSubstring Sledgehammer_Filter.pseudo_abs_name s then "abs"
+      else s
+    val prop = Thm.prop_of th
+  in
+    interesting_const_names thy prop @ interesting_type_names prop
+    |> (fn features =>
+           case List.partition is_skolem features of
+             (_, []) => ["likely_tautology"]
+           | ([], features) => features
+           | (_, features) => "skolem" :: features)
+    |> map fix_abs
+    |> (case status of
+          General => I
+        | Induction => cons "induction"
+        | Intro => cons "intro"
+        | Inductive => cons "inductive"
+        | Elim => cons "elim"
+        | Simp => cons "simp"
+        | Def => cons "def")
+  end
+
+fun generate_mash_feature_file_for_theory thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val axioms = Theory.all_axioms_of thy |> map fst
-    val facts = facts_of thy
+    val facts = facts_of thy |> not include_thy ? filter_out (has_thy thy o snd)
     fun do_fact ((_, (_, status)), th) =
       let
-        val is_boring =
-          String.isSubstring Sledgehammer_Filter.pseudo_skolem_prefix
         val name = Thm.get_name_hint th
-        val features =
-          map (prefix const_prefix o escape_meta)
-              (interesting_const_names ctxt (Thm.prop_of th))
-          |> (fn features =>
-                 features |> forall is_boring features
-                             ? cons "likely_tautology")
-          |> (member (op =) axioms name ? cons "axiom")
-          |> (case status of
-                General => I
-              | Induction => cons "induction"
-              | Intro => cons "intro"
-              | Inductive => cons "inductive"
-              | Elim => cons "elim"
-              | Simp => cons "simp"
-              | Def => cons "def")
-        val s = fact_name_of name ^ ": " ^ space_implode " " features ^ "\n"
+        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
 
-fun generate_mash_dependency_file_for_theory thy file_name =
+val dependencies_of = theorems_mentioned_in_proof_term o SOME
+
+fun generate_mash_dependency_file_for_theory thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val ths = facts_of thy |> map snd
+    val ths =
+      facts_of thy |> not include_thy ? filter_out (has_thy thy o snd)
+                   |> map snd
     val all_names = map Thm.get_name_hint ths
     fun do_thm th =
       let
         val name = Thm.get_name_hint th
-        val ths = theorems_mentioned_in_proof_term (SOME all_names) th
-        val s = fact_name_of name ^ ": " ^ space_implode " " ths ^ "\n"
+        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
 
+fun generate_mash_problem_file_for_theory thy file_name =
+  let
+    val path = file_name |> Path.explode
+    val _ = File.write path ""
+    val facts = facts_of thy
+    val (new_facts, old_facts) =
+      facts |> List.partition (has_thy thy o snd)
+            |>> sort (thm_ord o pairself snd)
+    val all_names = map (Thm.get_name_hint o snd) facts
+    fun do_fact ((_, (_, status)), th) prevs =
+      let
+        val name = Thm.get_name_hint th
+        val feats = features_of thy (status, th)
+        val deps = dependencies_of all_names th
+        val th = fact_name_of name
+        val s =
+          th ^ ": " ^
+          space_implode " " prevs ^ "; " ^
+          space_implode " " feats ^ "; " ^
+          space_implode " " deps ^ "\n"
+        val _ = File.append path s
+      in [th] 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
+
 fun inference_term [] = NONE
   | inference_term ss =
     ATerm (("inference", []),