# HG changeset patch
# User blanchet
# Date 1361276509 -3600
# Node ID 962190eab40dfa116ca828e505a1ec85f82389ed
# Parent  d0fa18638478e3f88a6c21facdee14290d40034c
provide two modes for MaSh driver: linearized or real visibility

diff -r d0fa18638478 -r 962190eab40d src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Tue Feb 19 13:21:49 2013 +0100
@@ -28,6 +28,7 @@
 val do_it = false (* switch to "true" to generate the files *)
 val params = Sledgehammer_Isar.default_params @{context} []
 val range = (1, NONE)
+val linearize = false
 val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
 val prob_dir = prefix ^ "mash_problems"
@@ -42,7 +43,7 @@
 
 ML {*
 if do_it then
-  evaluate_mash_suggestions @{context} params range
+  evaluate_mash_suggestions @{context} params range linearize
       [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
       (SOME prob_dir)
       (prefix ^ "mepo_suggestions")
diff -r d0fa18638478 -r 962190eab40d src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Tue Feb 19 13:21:49 2013 +0100
@@ -33,6 +33,7 @@
 val prover = hd provers
 val range = (1, NONE)
 val step = 1
+val linearize = false
 val max_suggestions = 1024
 val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
@@ -47,21 +48,22 @@
 
 ML {*
 if do_it then
-  generate_accessibility @{context} thys false (prefix ^ "mash_accessibility")
+  generate_accessibility @{context} thys linearize
+      (prefix ^ "mash_accessibility")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_features @{context} prover thys false (prefix ^ "mash_features")
+  generate_features @{context} prover thys (prefix ^ "mash_features")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_isar_dependencies @{context} thys false
+  generate_isar_dependencies @{context} thys linearize
       (prefix ^ "mash_dependencies")
 else
   ()
@@ -70,7 +72,7 @@
 ML {*
 if do_it then
   generate_isar_commands @{context} prover (range, step) thys
-      (prefix ^ "mash_commands")
+      linearize (prefix ^ "mash_commands")
 else
   ()
 *}
@@ -78,7 +80,7 @@
 ML {*
 if do_it then
   generate_mepo_suggestions @{context} params (range, step) thys
-      max_suggestions (prefix ^ "mepo_suggestions")
+      linearize max_suggestions (prefix ^ "mepo_suggestions")
 else
   ()
 *}
@@ -93,7 +95,7 @@
 
 ML {*
 if do_it then
-  generate_prover_dependencies @{context} params range thys false
+  generate_prover_dependencies @{context} params range thys linearize
       (prefix ^ "mash_prover_dependencies")
 else
   ()
@@ -102,7 +104,7 @@
 ML {*
 if do_it then
   generate_prover_commands @{context} params (range, step) thys
-      (prefix ^ "mash_prover_commands")
+      linearize (prefix ^ "mash_prover_commands")
 else
   ()
 *}
diff -r d0fa18638478 -r 962190eab40d src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Tue Feb 19 13:21:49 2013 +0100
@@ -16,8 +16,9 @@
   val MeSh_ProverN : string
   val IsarN : string
   val evaluate_mash_suggestions :
-    Proof.context -> params -> int * int option -> string list -> string option
-    -> string -> string -> string -> string -> string -> string -> unit
+    Proof.context -> params -> int * int option -> bool -> string list
+    -> string option -> string -> string -> string -> string -> string -> string
+    -> unit
 end;
 
 structure MaSh_Eval : MASH_EVAL =
@@ -39,7 +40,7 @@
 fun in_range (from, to) j =
   j >= from andalso (to = NONE orelse j <= the to)
 
-fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
+fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name
         mepo_file_name mash_isar_file_name mash_prover_file_name
         mesh_isar_file_name mesh_prover_file_name report_file_name =
   let
diff -r d0fa18638478 -r 962190eab40d src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Tue Feb 19 13:21:49 2013 +0100
@@ -12,21 +12,21 @@
   val generate_accessibility :
     Proof.context -> theory list -> bool -> string -> unit
   val generate_features :
-    Proof.context -> string -> theory list -> bool -> string -> unit
+    Proof.context -> string -> theory list -> string -> unit
   val generate_isar_dependencies :
     Proof.context -> theory list -> bool -> string -> unit
   val generate_prover_dependencies :
     Proof.context -> params -> int * int option -> theory list -> bool -> string
     -> unit
   val generate_isar_commands :
-    Proof.context -> string -> (int * int option) * int -> theory list -> string
-    -> unit
+    Proof.context -> string -> (int * int option) * int -> theory list -> bool
+    -> string -> unit
   val generate_prover_commands :
-    Proof.context -> params -> (int * int option) * int -> theory list -> string
-    -> unit
+    Proof.context -> params -> (int * int option) * int -> theory list -> bool
+    -> string -> unit
   val generate_mepo_suggestions :
-    Proof.context -> params -> (int * int option) * int -> theory list -> int
-    -> string -> unit
+    Proof.context -> params -> (int * int option) * int -> theory list -> bool
+    -> int -> string -> unit
   val generate_mesh_suggestions : int -> string -> string -> string -> unit
 end;
 
@@ -51,28 +51,30 @@
     |> sort (crude_thm_ord o pairself snd)
   end
 
-fun generate_accessibility ctxt thys include_thys file_name =
+fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
+
+fun generate_accessibility ctxt thys linearize file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    fun do_fact fact prevs =
+    fun do_fact (parents, fact) prevs =
       let
-        val s = encode_str fact ^ ": " ^ encode_strs prevs ^ "\n"
+        val parents = if linearize then prevs else parents
+        val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n"
         val _ = File.append path s
       in [fact] end
     val facts =
       all_facts ctxt
-      |> not include_thys ? filter_out (has_thys thys o snd)
-      |> map (snd #> nickname_of_thm)
+      |> filter_out (has_thys thys o snd)
+      |> attach_parents_to_facts []
+      |> map (apsnd (nickname_of_thm o snd))
   in fold do_fact facts []; () end
 
-fun generate_features ctxt prover thys include_thys file_name =
+fun generate_features ctxt prover thys file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val facts =
-      all_facts ctxt
-      |> not include_thys ? filter_out (has_thys thys o snd)
+    val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
     fun do_fact ((_, stature), th) =
       let
         val name = nickname_of_thm th
@@ -109,20 +111,22 @@
     | NONE => (omitted_marker, [])
   end
 
-fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
+fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize
                                          file_name =
   let
     val path = file_name |> Path.explode
-    val facts =
-      all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
+    val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
     val name_tabs = build_name_tables nickname_of_thm facts
     fun do_fact (j, (_, th)) =
       if in_range range j then
         let
           val name = nickname_of_thm th
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
+          val access_facts =
+            if linearize then take (j - 1) facts
+            else facts |> filter_accessible_from th
           val (marker, deps) =
-            smart_dependencies_of ctxt params_opt facts name_tabs th NONE
+            smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE
         in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end
       else
         ""
@@ -142,25 +146,29 @@
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
 
 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
-                                     file_name =
+                                     linearize file_name =
   let
     val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
     val facts = all_facts ctxt
     val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
     val name_tabs = build_name_tables nickname_of_thm facts
-    fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
+    fun do_fact (j, ((name, (parents, ((_, stature), th))), prevs)) =
       if in_range range j then
         let
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val feats =
             features_of ctxt prover (theory_of_thm th) stature [prop_of th]
           val isar_deps = isar_dependencies_of name_tabs th
+          val access_facts =
+            (if linearize then take (j - 1) new_facts
+             else new_facts |> filter_accessible_from th) @ old_facts
           val (marker, deps) =
-            smart_dependencies_of ctxt params_opt facts name_tabs th
+            smart_dependencies_of ctxt params_opt access_facts name_tabs th
                                   (SOME isar_deps)
+          val parents = if linearize then prevs else parents
           val core =
-            encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
+            encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
             encode_features (sort_wrt fst feats)
           val query =
             if is_bad_query ctxt ho_atp step j th isar_deps then ""
@@ -170,10 +178,12 @@
         in query ^ update end
       else
         ""
-    val parents =
+    val new_facts =
+      new_facts |> attach_parents_to_facts old_facts
+                |> map (`(nickname_of_thm o snd o snd))
+    val hd_prevs =
       map (nickname_of_thm o snd) (the_list (try List.last old_facts))
-    val new_facts = new_facts |> map (`(nickname_of_thm o snd))
-    val prevss = fst (split_last (parents :: map (single o fst) new_facts))
+    val prevss = fst (split_last (hd_prevs :: map (single o fst) new_facts))
     val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
   in File.write_list path lines end
 
@@ -184,7 +194,7 @@
   generate_isar_or_prover_commands ctxt prover (SOME params)
 
 fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
-                              (range, step) thys max_suggs file_name =
+                              (range, step) thys linearize max_suggs file_name =
   let
     val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
@@ -206,6 +216,7 @@
             let
               val suggs =
                 old_facts
+                |> linearize ? filter_accessible_from th
                 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
                        max_suggs NONE hyp_ts concl_t
                 |> map (nickname_of_thm o snd)
diff -r d0fa18638478 -r 962190eab40d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 18 18:34:55 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Feb 19 13:21:49 2013 +0100
@@ -56,6 +56,7 @@
     ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
     -> 'a list
   val crude_thm_ord : thm * thm -> order
+  val thm_less : thm * thm -> bool
   val goal_of_thm : theory -> thm -> thm
   val run_prover_for_mash :
     Proof.context -> params -> string -> fact list -> thm -> prover_result
@@ -80,6 +81,8 @@
   val mash_learn_proof :
     Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     -> unit
+  val attach_parents_to_facts :
+    ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list
   val mash_learn :
     Proof.context -> params -> fact_override -> thm list -> bool -> unit
   val is_mash_enabled : unit -> bool
@@ -902,6 +905,8 @@
         (true, "")
       end)
 
+(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
+
 fun chunks_and_parents_for chunks th =
   let
     fun insert_parent new parents =
@@ -925,27 +930,30 @@
   in
     fold_rev do_chunk chunks ([], [])
     |>> cons []
+    ||> map nickname_of_thm
   end
 
-fun attach_parents_to_facts facts =
-  let
-    fun do_facts _ _ [] = []
-      | do_facts _ parents [fact] = [(parents, fact)]
-      | do_facts chunks parents ((fact as (_, th)) :: (facts as (_, th') :: _)) =
-        let
-          val chunks = app_hd (cons th) chunks
-          val (chunks', parents') =
-            (if thm_less_eq (th, th') andalso
-                thy_name_of_thm th = thy_name_of_thm th' then
-               (chunks, [th])
-             else
-               chunks_and_parents_for chunks th')
-            ||> map nickname_of_thm
-        in (parents, fact) :: do_facts chunks' parents' facts end
-  in
-    facts |> sort (crude_thm_ord o pairself snd)
-          |> do_facts [[]] []
-  end
+fun attach_parents_to_facts _ [] = []
+  | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
+    let
+      fun do_facts _ [] = []
+        | do_facts (_, parents) [fact] = [(parents, fact)]
+        | do_facts (chunks, parents)
+                   ((fact as (_, th)) :: (facts as (_, th') :: _)) =
+          let
+            val chunks = app_hd (cons th) chunks
+            val chunks_and_parents' =
+              if thm_less_eq (th, th') andalso
+                 thy_name_of_thm th = thy_name_of_thm th' then
+                (chunks, [nickname_of_thm th])
+              else
+                chunks_and_parents_for chunks th'
+          in (parents, fact) :: do_facts chunks_and_parents' facts end
+    in
+      old_facts @ facts
+      |> do_facts (chunks_and_parents_for [[]] th)
+      |> drop (length old_facts)
+    end
 
 fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
 
@@ -1046,12 +1054,12 @@
             0
           else
             let
-              val facts =
+              val new_facts =
                 facts |> attach_parents_to_facts
                       |> filter_out (is_in_access_G o snd)
               val (learns, (n, _, _)) =
                 ([], (0, next_commit_time (), false))
-                |> fold learn_new_fact facts
+                |> fold learn_new_fact new_facts
             in commit true learns [] []; n end
         fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
           | relearn_old_fact ((_, (_, status)), th)