tuned data structure

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -474,21 +474,20 @@
           Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
               Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
               hyp_ts concl_t
-        val fact_triple =
+        val factss =
           facts
           |> filter (is_appropriate_prop o prop_of o snd)
           |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_facts max_facts)
                  Sledgehammer_Fact.no_fact_override hyp_ts concl_t
-          |> tap (fn fact_triple =>
+          |> tap (fn factss =>
                      "Line " ^ str0 (Position.line_of pos) ^ ": " ^
-                     Sledgehammer_Run.string_of_fact_triple fact_triple
+                     Sledgehammer_Run.string_of_factss factss
                      |> Output.urgent_message)
         val prover = get_prover ctxt prover_name params goal facts
         val problem =
           {state = st', goal = goal, subgoal = i,
-           subgoal_count = Sledgehammer_Util.subgoal_count st,
-           fact_triple = fact_triple}
+           subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
       in prover params (K (K (K ""))) problem end)) ()
       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate

--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -42,15 +42,15 @@
       |> relevant_facts ctxt params name
              (the_default default_max_facts max_facts) fact_override hyp_ts
              concl_t
-      |> #1
+      |> hd |> snd
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       fact_triple = (facts, facts, facts)}
+       factss = [("", facts)]}
   in
     (case prover params (K (K (K ""))) problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
     | _ => NONE)
-      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+    handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
   end
 
 fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -88,7 +88,7 @@
   val mash_weight : real
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
-    -> term -> raw_fact list -> fact list * fact list * fact list
+    -> term -> raw_fact list -> (string * fact list) list
   val kill_learners : unit -> unit
   val running_learners : unit -> unit
 end;
@@ -536,7 +536,7 @@
   let
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
-       fact_triple = (facts, facts, facts)}
+       factss = [("", facts)]}
   in
     get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
                                problem
@@ -1106,10 +1106,10 @@
     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   else if only then
     let val facts = facts |> map fact_of_raw_fact in
-      (facts, facts, facts)
+      [("", facts)]
     end
   else if max_facts <= 0 orelse null facts then
-    ([], [], [])
+    [("", [])]
   else
     let
       fun maybe_learn () =
@@ -1164,8 +1164,9 @@
     in
       case mess of
         [(_, (mepo, _)), (_, (mash, _))] =>
-        (mesh, mepo |> map fst |> add_and_take, mash |> map fst |> add_and_take)
-      | _ => (mesh, mesh, mesh)
+        [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
+         (mashN, mash |> map fst |> add_and_take)]
+      | _ => [("", mesh)]
     end
 
 fun kill_learners () = Async_Manager.kill_threads MaShN "learner"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -81,7 +81,7 @@
        preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
-       fact_triple = (facts, facts, facts)}
+       factss = [("", facts)]}
     val result as {outcome, used_facts, run_time, ...} =
       prover params (K (K (K ""))) problem
   in
@@ -267,8 +267,7 @@
 
 fun maybe_minimize ctxt mode do_learn name
         (params as {verbose, isar_proofs, minimize, ...})
-        ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...}
-         : prover_problem)
+        ({state, subgoal, subgoal_count, ...} : prover_problem)
         (result as {outcome, used_facts, used_from, run_time, preplay, message,
                     message_tail} : prover_result) =
   if is_some outcome orelse null used_facts then
@@ -310,7 +309,7 @@
         if minimize then
           minimize_facts do_learn minimize_name params
               (mode <> Normal orelse not verbose) subgoal subgoal_count state
-              (filter_used_facts true used_facts (map (apsnd single) facts))
+              (filter_used_facts true used_facts (map (apsnd single) used_from))
           |>> Option.map (map fst)
         else
           (SOME used_facts, (preplay, message, ""))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -68,7 +68,7 @@
      goal : thm,
      subgoal : int,
      subgoal_count : int,
-     fact_triple : fact list * fact list * fact list}
+     factss : (string * fact list) list}
 
   type prover_result =
     {outcome : failure option,
@@ -355,7 +355,7 @@
    goal : thm,
    subgoal : int,
    subgoal_count : int,
-   fact_triple : fact list * fact list * fact list}
+   factss : (string * fact list) list}
 
 type prover_result =
   {outcome : failure option,
@@ -632,7 +632,7 @@
                     max_new_mono_instances, isar_proofs, isar_shrink,
                     slice, timeout, preplay_timeout, ...})
         minimize_command
-        ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *)
+        ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *)
           ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
@@ -1064,7 +1064,7 @@
 
 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
         minimize_command
-        ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *)
+        ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *)
          ...} : prover_problem) =
   let
     val ctxt = Proof.context_of state
@@ -1108,7 +1108,7 @@
 fun run_reconstructor mode name
         (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
         minimize_command
-        ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...}
+        ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
          : prover_problem) =
   let
     val reconstr =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -18,7 +18,7 @@
   val noneN : string
   val timeoutN : string
   val unknownN : string
-  val string_of_fact_triple : fact list * fact list * fact list -> string
+  val string_of_factss : (string * fact list) list -> string
   val run_sledgehammer :
     params -> mode -> int -> fact_override
     -> ((string * string list) list -> string -> minimize_command)
@@ -66,9 +66,8 @@
 
 fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
                               timeout, expect, ...})
-                  mode minimize_command only learn
-                  {state, goal, subgoal, subgoal_count,
-                   fact_triple as (facts, _, _)} name =
+        mode minimize_command only learn
+        {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
   let
     val ctxt = Proof.context_of state
     val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
@@ -82,12 +81,12 @@
     val problem =
       {state = state, goal = goal, subgoal = subgoal,
        subgoal_count = subgoal_count,
-       fact_triple =
-         fact_triple
-         |> triple_self ((not (is_ho_atp ctxt name)
-                          ? filter_out (fn ((_, (_, Induction)), _) => true
-                                         | _ => false))
-                         #> take num_facts)}
+       factss =
+         factss
+         |> map (apsnd ((not (is_ho_atp ctxt name)
+                         ? filter_out (fn ((_, (_, Induction)), _) => true
+                                        | _ => false))
+                        #> take num_facts))}
     fun print_used_facts used_facts used_from =
       tag_list 1 used_from
       |> map (fn (j, fact) => fact |> apsnd (K j))
@@ -167,21 +166,22 @@
 
 val auto_try_max_facts_divisor = 2 (* FUDGE *)
 
+fun eq_facts p = eq_list (op = o pairself fst) p
+
 fun string_of_facts facts =
   "Including " ^ string_of_int (length facts) ^
   " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
   (facts |> map (fst o fst) |> space_implode " ") ^ "."
 
-fun eq_facts p = eq_list (op = o pairself fst) p
-
-fun string_of_fact_triple ([], [], []) = "Found no relevant facts."
-  | string_of_fact_triple (mesh, mepo, mash) =
-    if eq_facts (mesh, mepo) andalso eq_facts (mesh, mash) then
-      string_of_facts mesh
-    else
-      MeShN ^ ": " ^ string_of_facts mesh ^ "\n\n" ^
-      MePoN ^ ": " ^ string_of_facts mepo ^ "\n\n" ^
-      MaShN ^ ": " ^ string_of_facts mash
+fun string_of_factss factss =
+  if forall (null o snd) factss then
+    "Found no relevant facts."
+  else case factss of
+    [(_, facts)] => string_of_facts facts
+  | _ =>
+    factss
+    |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
+    |> space_implode "\n\n"
 
 fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
                                  slice, ...})
@@ -213,7 +213,7 @@
       val (smts, (ueq_atps, full_atps)) =
         provers |> List.partition (is_smt_prover ctxt)
                 ||> List.partition (is_unit_equational_atp ctxt)
-      fun get_fact_triple label is_appropriate_prop provers =
+      fun get_factss label is_appropriate_prop provers =
         let
           val max_max_facts =
             case max_facts of
@@ -229,20 +229,20 @@
               | NONE => I)
           |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
                             hyp_ts concl_t
-          |> tap (fn fact_triple =>
+          |> tap (fn factss =>
                      if verbose then
                        label ^ plural_s (length provers) ^ ": " ^
-                       string_of_fact_triple fact_triple
+                       string_of_factss factss
                        |> print
                      else
                        ())
         end
       fun launch_provers state label is_appropriate_prop provers =
         let
-          val fact_triple = get_fact_triple label is_appropriate_prop provers
+          val factss = get_factss label is_appropriate_prop provers
           val problem =
             {state = state, goal = goal, subgoal = i, subgoal_count = n,
-             fact_triple = fact_triple}
+             factss = factss}
           fun learn prover =
             mash_learn_proof ctxt params prover (prop_of goal) all_facts
           val launch = launch_prover params mode minimize_command only learn

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -11,7 +11,6 @@
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
-  val triple_self : ('a -> 'b) -> 'a * 'a * 'a -> 'b * 'b * 'b
   val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
   val infinite_timeout : Time.time
   val time_mult : real -> Time.time -> Time.time
@@ -44,8 +43,6 @@
 val serial_commas = Try.serial_commas
 val simplify_spaces = strip_spaces false (K true)
 
-fun triple_self f (x, y, z) = (f x, f y, f z)
-
 fun with_cleanup clean_up f x =
   Exn.capture f x
   |> tap (fn _ => clean_up x)