1.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Mon Feb 18 18:34:55 2013 +0100
     1.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Tue Feb 19 13:21:49 2013 +0100
     1.3 @@ -28,6 +28,7 @@
     1.4  val do_it = false (* switch to "true" to generate the files *)
     1.5  val params = Sledgehammer_Isar.default_params @{context} []
     1.6  val range = (1, NONE)
     1.7 +val linearize = false
     1.8  val dir = "List"
     1.9  val prefix = "/tmp/" ^ dir ^ "/"
    1.10  val prob_dir = prefix ^ "mash_problems"
    1.11 @@ -42,7 +43,7 @@
    1.12  
    1.13  ML {*
    1.14  if do_it then
    1.15 -  evaluate_mash_suggestions @{context} params range
    1.16 +  evaluate_mash_suggestions @{context} params range linearize
    1.17        [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
    1.18        (SOME prob_dir)
    1.19        (prefix ^ "mepo_suggestions")

     2.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Mon Feb 18 18:34:55 2013 +0100
     2.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Tue Feb 19 13:21:49 2013 +0100
     2.3 @@ -33,6 +33,7 @@
     2.4  val prover = hd provers
     2.5  val range = (1, NONE)
     2.6  val step = 1
     2.7 +val linearize = false
     2.8  val max_suggestions = 1024
     2.9  val dir = "List"
    2.10  val prefix = "/tmp/" ^ dir ^ "/"
    2.11 @@ -47,21 +48,22 @@
    2.12  
    2.13  ML {*
    2.14  if do_it then
    2.15 -  generate_accessibility @{context} thys false (prefix ^ "mash_accessibility")
    2.16 +  generate_accessibility @{context} thys linearize
    2.17 +      (prefix ^ "mash_accessibility")
    2.18  else
    2.19    ()
    2.20  *}
    2.21  
    2.22  ML {*
    2.23  if do_it then
    2.24 -  generate_features @{context} prover thys false (prefix ^ "mash_features")
    2.25 +  generate_features @{context} prover thys (prefix ^ "mash_features")
    2.26  else
    2.27    ()
    2.28  *}
    2.29  
    2.30  ML {*
    2.31  if do_it then
    2.32 -  generate_isar_dependencies @{context} thys false
    2.33 +  generate_isar_dependencies @{context} thys linearize
    2.34        (prefix ^ "mash_dependencies")
    2.35  else
    2.36    ()
    2.37 @@ -70,7 +72,7 @@
    2.38  ML {*
    2.39  if do_it then
    2.40    generate_isar_commands @{context} prover (range, step) thys
    2.41 -      (prefix ^ "mash_commands")
    2.42 +      linearize (prefix ^ "mash_commands")
    2.43  else
    2.44    ()
    2.45  *}
    2.46 @@ -78,7 +80,7 @@
    2.47  ML {*
    2.48  if do_it then
    2.49    generate_mepo_suggestions @{context} params (range, step) thys
    2.50 -      max_suggestions (prefix ^ "mepo_suggestions")
    2.51 +      linearize max_suggestions (prefix ^ "mepo_suggestions")
    2.52  else
    2.53    ()
    2.54  *}
    2.55 @@ -93,7 +95,7 @@
    2.56  
    2.57  ML {*
    2.58  if do_it then
    2.59 -  generate_prover_dependencies @{context} params range thys false
    2.60 +  generate_prover_dependencies @{context} params range thys linearize
    2.61        (prefix ^ "mash_prover_dependencies")
    2.62  else
    2.63    ()
    2.64 @@ -102,7 +104,7 @@
    2.65  ML {*
    2.66  if do_it then
    2.67    generate_prover_commands @{context} params (range, step) thys
    2.68 -      (prefix ^ "mash_prover_commands")
    2.69 +      linearize (prefix ^ "mash_prover_commands")
    2.70  else
    2.71    ()
    2.72  *}

     3.1 --- a/src/HOL/TPTP/mash_eval.ML	Mon Feb 18 18:34:55 2013 +0100
     3.2 +++ b/src/HOL/TPTP/mash_eval.ML	Tue Feb 19 13:21:49 2013 +0100
     3.3 @@ -16,8 +16,9 @@
     3.4    val MeSh_ProverN : string
     3.5    val IsarN : string
     3.6    val evaluate_mash_suggestions :
     3.7 -    Proof.context -> params -> int * int option -> string list -> string option
     3.8 -    -> string -> string -> string -> string -> string -> string -> unit
     3.9 +    Proof.context -> params -> int * int option -> bool -> string list
    3.10 +    -> string option -> string -> string -> string -> string -> string -> string
    3.11 +    -> unit
    3.12  end;
    3.13  
    3.14  structure MaSh_Eval : MASH_EVAL =
    3.15 @@ -39,7 +40,7 @@
    3.16  fun in_range (from, to) j =
    3.17    j >= from andalso (to = NONE orelse j <= the to)
    3.18  
    3.19 -fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
    3.20 +fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name
    3.21          mepo_file_name mash_isar_file_name mash_prover_file_name
    3.22          mesh_isar_file_name mesh_prover_file_name report_file_name =
    3.23    let

     4.1 --- a/src/HOL/TPTP/mash_export.ML	Mon Feb 18 18:34:55 2013 +0100
     4.2 +++ b/src/HOL/TPTP/mash_export.ML	Tue Feb 19 13:21:49 2013 +0100
     4.3 @@ -12,21 +12,21 @@
     4.4    val generate_accessibility :
     4.5      Proof.context -> theory list -> bool -> string -> unit
     4.6    val generate_features :
     4.7 -    Proof.context -> string -> theory list -> bool -> string -> unit
     4.8 +    Proof.context -> string -> theory list -> string -> unit
     4.9    val generate_isar_dependencies :
    4.10      Proof.context -> theory list -> bool -> string -> unit
    4.11    val generate_prover_dependencies :
    4.12      Proof.context -> params -> int * int option -> theory list -> bool -> string
    4.13      -> unit
    4.14    val generate_isar_commands :
    4.15 -    Proof.context -> string -> (int * int option) * int -> theory list -> string
    4.16 -    -> unit
    4.17 +    Proof.context -> string -> (int * int option) * int -> theory list -> bool
    4.18 +    -> string -> unit
    4.19    val generate_prover_commands :
    4.20 -    Proof.context -> params -> (int * int option) * int -> theory list -> string
    4.21 -    -> unit
    4.22 +    Proof.context -> params -> (int * int option) * int -> theory list -> bool
    4.23 +    -> string -> unit
    4.24    val generate_mepo_suggestions :
    4.25 -    Proof.context -> params -> (int * int option) * int -> theory list -> int
    4.26 -    -> string -> unit
    4.27 +    Proof.context -> params -> (int * int option) * int -> theory list -> bool
    4.28 +    -> int -> string -> unit
    4.29    val generate_mesh_suggestions : int -> string -> string -> string -> unit
    4.30  end;
    4.31  
    4.32 @@ -51,28 +51,30 @@
    4.33      |> sort (crude_thm_ord o pairself snd)
    4.34    end
    4.35  
    4.36 -fun generate_accessibility ctxt thys include_thys file_name =
    4.37 +fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
    4.38 +
    4.39 +fun generate_accessibility ctxt thys linearize file_name =
    4.40    let
    4.41      val path = file_name |> Path.explode
    4.42      val _ = File.write path ""
    4.43 -    fun do_fact fact prevs =
    4.44 +    fun do_fact (parents, fact) prevs =
    4.45        let
    4.46 -        val s = encode_str fact ^ ": " ^ encode_strs prevs ^ "\n"
    4.47 +        val parents = if linearize then prevs else parents
    4.48 +        val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n"
    4.49          val _ = File.append path s
    4.50        in [fact] end
    4.51      val facts =
    4.52        all_facts ctxt
    4.53 -      |> not include_thys ? filter_out (has_thys thys o snd)
    4.54 -      |> map (snd #> nickname_of_thm)
    4.55 +      |> filter_out (has_thys thys o snd)
    4.56 +      |> attach_parents_to_facts []
    4.57 +      |> map (apsnd (nickname_of_thm o snd))
    4.58    in fold do_fact facts []; () end
    4.59  
    4.60 -fun generate_features ctxt prover thys include_thys file_name =
    4.61 +fun generate_features ctxt prover thys file_name =
    4.62    let
    4.63      val path = file_name |> Path.explode
    4.64      val _ = File.write path ""
    4.65 -    val facts =
    4.66 -      all_facts ctxt
    4.67 -      |> not include_thys ? filter_out (has_thys thys o snd)
    4.68 +    val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
    4.69      fun do_fact ((_, stature), th) =
    4.70        let
    4.71          val name = nickname_of_thm th
    4.72 @@ -109,20 +111,22 @@
    4.73      | NONE => (omitted_marker, [])
    4.74    end
    4.75  
    4.76 -fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
    4.77 +fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize
    4.78                                           file_name =
    4.79    let
    4.80      val path = file_name |> Path.explode
    4.81 -    val facts =
    4.82 -      all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
    4.83 +    val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
    4.84      val name_tabs = build_name_tables nickname_of_thm facts
    4.85      fun do_fact (j, (_, th)) =
    4.86        if in_range range j then
    4.87          let
    4.88            val name = nickname_of_thm th
    4.89            val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
    4.90 +          val access_facts =
    4.91 +            if linearize then take (j - 1) facts
    4.92 +            else facts |> filter_accessible_from th
    4.93            val (marker, deps) =
    4.94 -            smart_dependencies_of ctxt params_opt facts name_tabs th NONE
    4.95 +            smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE
    4.96          in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end
    4.97        else
    4.98          ""
    4.99 @@ -142,25 +146,29 @@
   4.100    is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
   4.101  
   4.102  fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
   4.103 -                                     file_name =
   4.104 +                                     linearize file_name =
   4.105    let
   4.106      val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
   4.107      val path = file_name |> Path.explode
   4.108      val facts = all_facts ctxt
   4.109      val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
   4.110      val name_tabs = build_name_tables nickname_of_thm facts
   4.111 -    fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
   4.112 +    fun do_fact (j, ((name, (parents, ((_, stature), th))), prevs)) =
   4.113        if in_range range j then
   4.114          let
   4.115            val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
   4.116            val feats =
   4.117              features_of ctxt prover (theory_of_thm th) stature [prop_of th]
   4.118            val isar_deps = isar_dependencies_of name_tabs th
   4.119 +          val access_facts =
   4.120 +            (if linearize then take (j - 1) new_facts
   4.121 +             else new_facts |> filter_accessible_from th) @ old_facts
   4.122            val (marker, deps) =
   4.123 -            smart_dependencies_of ctxt params_opt facts name_tabs th
   4.124 +            smart_dependencies_of ctxt params_opt access_facts name_tabs th
   4.125                                    (SOME isar_deps)
   4.126 +          val parents = if linearize then prevs else parents
   4.127            val core =
   4.128 -            encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
   4.129 +            encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
   4.130              encode_features (sort_wrt fst feats)
   4.131            val query =
   4.132              if is_bad_query ctxt ho_atp step j th isar_deps then ""
   4.133 @@ -170,10 +178,12 @@
   4.134          in query ^ update end
   4.135        else
   4.136          ""
   4.137 -    val parents =
   4.138 +    val new_facts =
   4.139 +      new_facts |> attach_parents_to_facts old_facts
   4.140 +                |> map (`(nickname_of_thm o snd o snd))
   4.141 +    val hd_prevs =
   4.142        map (nickname_of_thm o snd) (the_list (try List.last old_facts))
   4.143 -    val new_facts = new_facts |> map (`(nickname_of_thm o snd))
   4.144 -    val prevss = fst (split_last (parents :: map (single o fst) new_facts))
   4.145 +    val prevss = fst (split_last (hd_prevs :: map (single o fst) new_facts))
   4.146      val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
   4.147    in File.write_list path lines end
   4.148  
   4.149 @@ -184,7 +194,7 @@
   4.150    generate_isar_or_prover_commands ctxt prover (SOME params)
   4.151  
   4.152  fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
   4.153 -                              (range, step) thys max_suggs file_name =
   4.154 +                              (range, step) thys linearize max_suggs file_name =
   4.155    let
   4.156      val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
   4.157      val path = file_name |> Path.explode
   4.158 @@ -206,6 +216,7 @@
   4.159              let
   4.160                val suggs =
   4.161                  old_facts
   4.162 +                |> linearize ? filter_accessible_from th
   4.163                  |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
   4.164                         max_suggs NONE hyp_ts concl_t
   4.165                  |> map (nickname_of_thm o snd)

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 18 18:34:55 2013 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Feb 19 13:21:49 2013 +0100
     5.3 @@ -56,6 +56,7 @@
     5.4      ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
     5.5      -> 'a list
     5.6    val crude_thm_ord : thm * thm -> order
     5.7 +  val thm_less : thm * thm -> bool
     5.8    val goal_of_thm : theory -> thm -> thm
     5.9    val run_prover_for_mash :
    5.10      Proof.context -> params -> string -> fact list -> thm -> prover_result
    5.11 @@ -80,6 +81,8 @@
    5.12    val mash_learn_proof :
    5.13      Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
    5.14      -> unit
    5.15 +  val attach_parents_to_facts :
    5.16 +    ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list
    5.17    val mash_learn :
    5.18      Proof.context -> params -> fact_override -> thm list -> bool -> unit
    5.19    val is_mash_enabled : unit -> bool
    5.20 @@ -902,6 +905,8 @@
    5.21          (true, "")
    5.22        end)
    5.23  
    5.24 +(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
    5.25 +
    5.26  fun chunks_and_parents_for chunks th =
    5.27    let
    5.28      fun insert_parent new parents =
    5.29 @@ -925,27 +930,30 @@
    5.30    in
    5.31      fold_rev do_chunk chunks ([], [])
    5.32      |>> cons []
    5.33 +    ||> map nickname_of_thm
    5.34    end
    5.35  
    5.36 -fun attach_parents_to_facts facts =
    5.37 -  let
    5.38 -    fun do_facts _ _ [] = []
    5.39 -      | do_facts _ parents [fact] = [(parents, fact)]
    5.40 -      | do_facts chunks parents ((fact as (_, th)) :: (facts as (_, th') :: _)) =
    5.41 -        let
    5.42 -          val chunks = app_hd (cons th) chunks
    5.43 -          val (chunks', parents') =
    5.44 -            (if thm_less_eq (th, th') andalso
    5.45 -                thy_name_of_thm th = thy_name_of_thm th' then
    5.46 -               (chunks, [th])
    5.47 -             else
    5.48 -               chunks_and_parents_for chunks th')
    5.49 -            ||> map nickname_of_thm
    5.50 -        in (parents, fact) :: do_facts chunks' parents' facts end
    5.51 -  in
    5.52 -    facts |> sort (crude_thm_ord o pairself snd)
    5.53 -          |> do_facts [[]] []
    5.54 -  end
    5.55 +fun attach_parents_to_facts _ [] = []
    5.56 +  | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
    5.57 +    let
    5.58 +      fun do_facts _ [] = []
    5.59 +        | do_facts (_, parents) [fact] = [(parents, fact)]
    5.60 +        | do_facts (chunks, parents)
    5.61 +                   ((fact as (_, th)) :: (facts as (_, th') :: _)) =
    5.62 +          let
    5.63 +            val chunks = app_hd (cons th) chunks
    5.64 +            val chunks_and_parents' =
    5.65 +              if thm_less_eq (th, th') andalso
    5.66 +                 thy_name_of_thm th = thy_name_of_thm th' then
    5.67 +                (chunks, [nickname_of_thm th])
    5.68 +              else
    5.69 +                chunks_and_parents_for chunks th'
    5.70 +          in (parents, fact) :: do_facts chunks_and_parents' facts end
    5.71 +    in
    5.72 +      old_facts @ facts
    5.73 +      |> do_facts (chunks_and_parents_for [[]] th)
    5.74 +      |> drop (length old_facts)
    5.75 +    end
    5.76  
    5.77  fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
    5.78  
    5.79 @@ -1046,12 +1054,12 @@
    5.80              0
    5.81            else
    5.82              let
    5.83 -              val facts =
    5.84 +              val new_facts =
    5.85                  facts |> attach_parents_to_facts
    5.86                        |> filter_out (is_in_access_G o snd)
    5.87                val (learns, (n, _, _)) =
    5.88                  ([], (0, next_commit_time (), false))
    5.89 -                |> fold learn_new_fact facts
    5.90 +                |> fold learn_new_fact new_facts
    5.91              in commit true learns [] []; n end
    5.92          fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
    5.93            | relearn_old_fact ((_, (_, status)), th)