# HG changeset patch
# User blanchet
# Date 1359651245 -3600
# Node ID 4f694d52bf625fa9f8c2868876f16d5bdb61d4dc
# Parent  0ecffccf93596707741cdcf1d472acd3b24cdf06
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices

diff -r 0ecffccf9359 -r 4f694d52bf62 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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
@@ -473,12 +473,13 @@
           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 =
+          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
-          |> #1 (*###*)
-          |> tap (fn facts =>
+          |> tap (fn (facts, _, _) => (* FIXME *)
                      "Line " ^ str0 (Position.line_of pos) ^ ": " ^
                      (if null facts then
                         "Found no relevant facts."
@@ -490,7 +491,8 @@
         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, facts = facts}
+           subgoal_count = Sledgehammer_Util.subgoal_count st,
+           fact_triple = fact_triple}
       in prover params (K (K (K ""))) problem end)) ()
       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate
diff -r 0ecffccf9359 -r 4f694d52bf62 src/HOL/TPTP/sledgehammer_tactics.ML
--- 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
@@ -45,7 +45,7 @@
       |> #1
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       facts = facts}
+       fact_triple = (facts, facts, facts)}
   in
     (case prover params (K (K (K ""))) problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
diff -r 0ecffccf9359 -r 4f694d52bf62 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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
@@ -532,7 +532,7 @@
   let
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
-       facts = facts}
+       fact_triple = (facts, facts, facts)}
   in
     get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
                                problem
diff -r 0ecffccf9359 -r 4f694d52bf62 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- 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,
-       facts = facts}
+       fact_triple = (facts, facts, facts)}
     val result as {outcome, used_facts, run_time, ...} =
       prover params (K (K (K ""))) problem
   in
@@ -267,7 +267,8 @@
 
 fun maybe_minimize ctxt mode do_learn name
         (params as {verbose, isar_proofs, minimize, ...})
-        ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
+        ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...}
+         : prover_problem)
         (result as {outcome, used_facts, run_time, preplay, message,
                     message_tail} : prover_result) =
   if is_some outcome orelse null used_facts then
diff -r 0ecffccf9359 -r 4f694d52bf62 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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,11 +68,11 @@
      goal : thm,
      subgoal : int,
      subgoal_count : int,
-     facts : fact list}
+     fact_triple : fact list * fact list * fact list}
 
   type prover_result =
     {outcome : failure option,
-     used_facts : (string * stature) list,
+     used_facts : (string * stature) list, (* FIXME: store triple component *)
      run_time : Time.time,
      preplay : play Lazy.lazy,
      message : play -> string,
@@ -354,7 +354,7 @@
    goal : thm,
    subgoal : int,
    subgoal_count : int,
-   facts : fact list}
+   fact_triple : fact list * fact list * fact list}
 
 type prover_result =
   {outcome : failure option,
@@ -630,7 +630,8 @@
                     max_new_mono_instances, isar_proofs, isar_shrink,
                     slice, timeout, preplay_timeout, ...})
         minimize_command
-        ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
+        ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *)
+          ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -1057,7 +1058,8 @@
 
 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
         minimize_command
-        ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
+        ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *)
+         ...} : prover_problem) =
   let
     val ctxt = Proof.context_of state
     val num_facts = length facts
@@ -1099,7 +1101,8 @@
 fun run_reconstructor mode name
         (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
         minimize_command
-        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
+        ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...}
+         : prover_problem) =
   let
     val reconstr =
       if name = metisN then
diff -r 0ecffccf9359 -r 4f694d52bf62 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- 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
@@ -65,7 +65,8 @@
 fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
                               timeout, expect, ...})
                   mode minimize_command only learn
-                  {state, goal, subgoal, subgoal_count, facts} name =
+                  {state, goal, subgoal, subgoal_count,
+                   fact_triple as (facts, _, _)} name =
   let
     val ctxt = Proof.context_of state
     val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
@@ -79,10 +80,12 @@
     val problem =
       {state = state, goal = goal, subgoal = subgoal,
        subgoal_count = subgoal_count,
-       facts = facts
-               |> not (Sledgehammer_Provers.is_ho_atp ctxt name)
-                  ? filter_out (curry (op =) Induction o snd o snd o fst)
-               |> take num_facts}
+       fact_triple =
+         fact_triple
+         |> triple_self ((not (is_ho_atp ctxt name)
+                          ? filter_out (fn ((_, (_, Induction)), _) => true
+                                         | _ => false))
+                         #> take num_facts)}
     fun print_used_facts used_facts =
       tag_list 1 facts
       |> map (fn (j, fact) => fact |> apsnd (K j))
@@ -177,7 +180,7 @@
       val ctxt = Proof.context_of state
       val {facts = chained, goal, ...} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
-      val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+      val ho_atp = exists (is_ho_atp ctxt) provers
       val reserved = reserved_isar_keyword_table ()
       val css = clasimpset_rule_table_of ctxt
       val all_facts =
@@ -191,7 +194,7 @@
       val (smts, (ueq_atps, full_atps)) =
         provers |> List.partition (is_smt_prover ctxt)
                 ||> List.partition (is_unit_equational_atp ctxt)
-      fun get_facts label is_appropriate_prop provers =
+      fun get_fact_triple label is_appropriate_prop provers =
         let
           val max_max_facts =
             case max_facts of
@@ -207,8 +210,7 @@
               | NONE => I)
           |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
                             hyp_ts concl_t
-          |> #1 (*###*)
-          |> tap (fn facts =>
+          |> tap (fn (facts, _, _) => (* FIXME *)
                      if verbose then
                        label ^ plural_s (length provers) ^ ": " ^
                        (if null facts then
@@ -223,11 +225,10 @@
         end
       fun launch_provers state label is_appropriate_prop provers =
         let
-          val facts = get_facts label is_appropriate_prop provers
-          val num_facts = length facts
+          val fact_triple = get_fact_triple label is_appropriate_prop provers
           val problem =
             {state = state, goal = goal, subgoal = i, subgoal_count = n,
-             facts = facts}
+             fact_triple = fact_triple}
           fun learn prover =
             mash_learn_proof ctxt params prover (prop_of goal) all_facts
           val launch = launch_prover params mode minimize_command only learn
diff -r 0ecffccf9359 -r 4f694d52bf62 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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,6 +11,7 @@
   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
@@ -43,6 +44,8 @@
 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)