# HG changeset patch
# User blanchet
# Date 1391425118 -3600
# Node ID f0187a12b8f200168548ccd48e6769bdeb9051b4
# Parent  df41d34d1324c1d4446709733bca0a12830960b5
tuned data structure

diff -r df41d34d1324 -r f0187a12b8f2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 11:58:38 2014 +0100
@@ -169,7 +169,7 @@
                  else ([], rewrite_methods))
                 ||> massage_meths
             in
-              Prove ([], skos, l, t, [], (([], []), meths))
+              Prove ([], skos, l, t, [], ([], []), meths)
             end)
 
         val bot = atp_proof |> List.last |> #1
@@ -218,7 +218,7 @@
             accum
             |> (if tainted = [] then
                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
-                               ((the_list predecessor, []), massage_meths metislike_methods)))
+                    (the_list predecessor, []), massage_meths metislike_methods))
                 else
                   I)
             |> rev
@@ -229,9 +229,6 @@
               val rule = rule_of_clause_id id
               val skolem = is_skolemize_rule rule
 
-              fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
-              fun steps_of_rest l step = isar_steps outer (SOME l) (step :: accum) infs
-
               val deps = fold add_fact_of_dependencies gamma ([], [])
               val meths =
                 (if skolem then skolem_methods
@@ -239,21 +236,23 @@
                  else if is_datatype_rule rule then datatype_methods
                  else metislike_methods)
                 |> massage_meths
-              val by = (deps, meths)
+
+              fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths)
+              fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
             in
               if is_clause_tainted c then
                 (case gamma of
                   [g] =>
                   if skolem andalso is_clause_tainted g then
                     let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
-                      isar_steps outer (SOME l) [prove [subproof] (([], []), meths)] infs
+                      isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
                     end
                   else
-                    steps_of_rest l (prove [] by)
-                | _ => steps_of_rest l (prove [] by))
+                    steps_of_rest (prove [] deps)
+                | _ => steps_of_rest (prove [] deps))
               else
-                steps_of_rest l
-                  (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
+                steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths)
+                  else prove [] deps)
             end
           | isar_steps outer predecessor accum (Cases cases :: infs) =
             let
@@ -265,7 +264,7 @@
               val step =
                 Prove (maybe_show outer c [], [], l, t,
                   map isar_case (filter_out (null o snd) cases),
-                  ((the_list predecessor, []), massage_meths metislike_methods))
+                  (the_list predecessor, []), massage_meths metislike_methods)
             in
               isar_steps outer (SOME l) (step :: accum) infs
             end
diff -r df41d34d1324 -r f0187a12b8f2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 11:58:38 2014 +0100
@@ -32,7 +32,7 @@
       | collect_steps [] accum = accum
       | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)
     and collect_step (Let _) x = x
-      | collect_step (step as Prove (_, _, l, _, subproofs, _)) x =
+      | collect_step (step as Prove (_, _, l, _, subproofs, _, _)) x =
         (case collect_subproofs subproofs x of
           ([], accu) => ([], accu)
         | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
@@ -55,15 +55,15 @@
       | update_steps (step :: steps) updates = update_step step (update_steps steps updates)
     and update_step step (steps, []) = (step :: steps, [])
       | update_step (step as Let _) (steps, updates) = (step :: steps, updates)
-      | update_step (Prove (qs, xs, l, t, subproofs, by))
-          (steps, updates as Prove (qs', xs', l', t', subproofs', by') :: updates') =
+      | update_step (Prove (qs, xs, l, t, subproofs, facts, meths))
+          (steps, updates as Prove (qs', xs', l', t', subproofs', facts', meths') :: updates') =
         let
           val (subproofs, updates) =
             if l = l' then update_subproofs subproofs' updates'
             else update_subproofs subproofs updates
         in
-          if l = l' then (Prove (qs', xs', l', t', subproofs, by') :: steps, updates)
-          else (Prove (qs, xs, l, t, subproofs, by) :: steps, updates)
+          if l = l' then (Prove (qs', xs', l', t', subproofs, facts', meths') :: steps, updates)
+          else (Prove (qs, xs, l, t, subproofs, facts, meths) :: steps, updates)
         end
     and update_subproofs [] updates = ([], updates)
       | update_subproofs steps [] = (steps, [])
@@ -80,8 +80,8 @@
     | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
   end
 
-fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1)))
-      (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) =
+fun try_merge (Prove (_, [], l1, _, [], (lfs1, gfs1), meths1))
+      (Prove (qs2, fix, l2, t, subproofs, (lfs2, gfs2), meths2)) =
     (case inter (op =) meths1 meths2 of
       [] => NONE
     | meths =>
@@ -89,7 +89,7 @@
         val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
         val gfs = union (op =) gfs1 gfs2
       in
-        SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths)))
+        SOME (Prove (qs2, fix, l2, t, subproofs, (lfs, gfs), meths))
       end)
   | try_merge _ _ = NONE
 
@@ -118,7 +118,7 @@
       val (get_successors, replace_successor) =
         let
           fun add_refs (Let _) = I
-            | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
+            | add_refs (Prove (_, _, v, _, _, (lfs, _), _)) =
               fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs
 
           val tab =
@@ -144,7 +144,7 @@
         if null subs orelse not (compress_further ()) then
           let
             val subproofs = List.revAppend (nontriv_subs, subs)
-            val step = Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))
+            val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)
           in
             set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)];
             step
@@ -154,7 +154,7 @@
             (sub as Proof (_, assms, sub_steps)) :: subs =>
             (let
               (* trivial subproofs have exactly one "Prove" step *)
-              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
+              val [Prove (_, [], l', _, [], (lfs', gfs'), meths')] = sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
               val Played time' = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l'
@@ -163,8 +163,8 @@
               val subs'' = subs @ nontriv_subs
               val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
               val gfs'' = union (op =) gfs' gfs
-              val by = ((lfs'', gfs''), meths(*FIXME*))
-              val step'' = Prove (qs, fix, l, t, subs'', by)
+              val meths'' as _ :: _ = inter (op =) meths' meths
+              val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'')
 
               (* check if the modified step can be preplayed fast enough *)
               val timeout = slackify_merge_timeout (Time.+ (time, time'))
@@ -179,7 +179,7 @@
           | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
 
       fun elim_subproofs (step as Let _) = step
-        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))) =
+        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)) =
           if subproofs = [] then
             step
           else
@@ -208,7 +208,7 @@
           val candidates =
             let
               fun add_cand (_, Let _) = I
-                | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
+                | add_cand (i, Prove (_, _, l, t, _, _, _)) = cons (i, l, size_of_term t)
             in
               (steps
                |> split_last |> fst (* keep last step *)
@@ -217,7 +217,7 @@
 
           fun try_eliminate (i, l, _) labels steps =
             let
-              val ((cand as Prove (_, _, _, _, _, ((lfs, _), _))) :: steps') = drop i steps
+              val ((cand as Prove (_, _, _, _, _, (lfs, _), _)) :: steps') = drop i steps
 
               val succs = collect_successors steps' labels
 
@@ -280,9 +280,9 @@
         steps |> map (fn step => step |> compress_further () ? compress_sub_levels)
               |> compress_further () ? compress_top_level
       and compress_sub_levels (step as Let _) = step
-        | compress_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
+        | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths)) =
           (* compress subproofs *)
-          Prove (qs, xs, l, t, map compress_proof subproofs, by)
+          Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths)
           (* eliminate trivial subproofs *)
           |> compress_further () ? elim_subproofs
     in
diff -r df41d34d1324 -r f0187a12b8f2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 11:58:38 2014 +0100
@@ -25,19 +25,18 @@
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 
-fun keep_fastest_method_of_isar_step preplay_data
-      (Prove (qs, xs, l, t, subproofs, (facts, _))) =
-    Prove (qs, xs, l, t, subproofs, (facts, [fastest_method_of_isar_step preplay_data l]))
+fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, _)) =
+    Prove (qs, xs, l, t, subproofs, facts, [fastest_method_of_isar_step preplay_data l])
   | keep_fastest_method_of_isar_step _ step = step
 
 val slack = seconds 0.1
 
 fun minimize_isar_step_dependencies ctxt preplay_data
-      (step as Prove (qs, xs, l, t, subproofs, ((lfs0, gfs0), meths as meth :: _))) =
+      (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _)) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
       let
-        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
+        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)
 
         fun minimize_facts _ time min_facts [] = (time, min_facts)
           | minimize_facts mk_step time min_facts (f :: facts) =
@@ -76,16 +75,15 @@
         else
           (used, accu))
     and process_used_step step = step |> postproc_step |> process_used_step_subproofs
-    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
+    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) =
       let
         val (used, subproofs) =
           map process_proof subproofs
           |> split_list
           |>> Ord_List.unions label_ord
           |>> fold (Ord_List.insert label_ord) lfs
-        val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
       in
-        (used, step)
+        (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths))
       end
   in
     snd o process_proof
diff -r df41d34d1324 -r f0187a12b8f2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:58:38 2014 +0100
@@ -53,7 +53,7 @@
     fun enrich_with_proof (Proof (_, assms, isar_steps)) =
       enrich_with_assms assms #> fold enrich_with_step isar_steps
     and enrich_with_step (Let _) = I
-      | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
+      | enrich_with_step (Prove (_, _, l, t, subproofs, _, _)) =
         enrich_with_fact l t #> fold enrich_with_proof subproofs
   in
     enrich_with_proof proof ctxt
@@ -88,7 +88,7 @@
 
     val concl = 
       (case try List.last steps of
-        SOME (Prove (_, [], _, t, _, _)) => t
+        SOME (Prove (_, [], _, t, _, _, _)) => t
       | _ => raise Fail "preplay error: malformed subproof")
 
     val var_idx = maxidx_of_term concl + 1
@@ -122,8 +122,7 @@
     | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth
-    (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
+fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
   let
     val goal =
       (case xs of
@@ -186,7 +185,7 @@
     Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
 
 fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
-      (step as Prove (_, _, l, _, _, (_, meths))) meths_outcomes0 =
+      (step as Prove (_, _, l, _, _, _, meths)) meths_outcomes0 =
     let
       fun lazy_preplay meth =
         Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
@@ -229,7 +228,7 @@
   #> get_best_method_outcome Lazy.force
   #> fst
 
-fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) =
+fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) =
     Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))
   | forced_outcome_of_step _ _ = Played Time.zeroTime
 
diff -r df41d34d1324 -r f0187a12b8f2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 11:58:38 2014 +0100
@@ -29,8 +29,8 @@
     Proof of (string * typ) list * (label * term) list * isar_step list
   and isar_step =
     Let of term * term |
-    Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
-      (facts * proof_method list)
+    Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
+      * facts * proof_method list
 
   val no_label : label
 
@@ -94,8 +94,8 @@
   Proof of (string * typ) list * (label * term) list * isar_step list
 and isar_step =
   Let of term * term |
-  Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
-    (facts * proof_method list)
+  Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
+    * facts * proof_method list
 
 val no_label = ("", ~1)
 
@@ -120,16 +120,16 @@
 
 fun steps_of_isar_proof (Proof (_, _, steps)) = steps
 
-fun label_of_isar_step (Prove (_, _, l, _, _, _)) = SOME l
+fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l
   | label_of_isar_step _ = NONE
 
-fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
+fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _, _)) = SOME subproofs
   | subproofs_of_isar_step _ = NONE
 
-fun facts_of_isar_step (Prove (_, _, _, _, _, (facts, _))) = facts
+fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _)) = facts
   | facts_of_isar_step _ = ([], [])
 
-fun proof_methods_of_isar_step (Prove (_, _, _, _, _, (_, meths))) = meths
+fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths)) = meths
   | proof_methods_of_isar_step _ = []
 
 fun fold_isar_step f step =
@@ -140,8 +140,8 @@
   let
     fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
     and map_step (step as Let _) = f step
-      | map_step (Prove (qs, xs, l, t, subproofs, by)) =
-        f (Prove (qs, xs, l, t, map map_proof subproofs, by))
+      | map_step (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+        f (Prove (qs, xs, l, t, map map_proof subproofs, facts, meths))
   in map_proof end
 
 val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
@@ -156,9 +156,9 @@
 fun chain_qs_lfs NONE lfs = ([], lfs)
   | chain_qs_lfs (SOME l0) lfs =
     if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
-fun chain_isar_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
+fun chain_isar_step lbl (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) =
     let val (qs', lfs) = chain_qs_lfs lbl lfs in
-      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, ((lfs, gfs), meths))
+      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, (lfs, gfs), meths)
     end
   | chain_isar_step _ step = step
 and chain_isar_steps _ [] = []
@@ -175,8 +175,8 @@
 
     fun kill_label l = if member (op =) used_ls l then l else no_label
 
-    fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
-        Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
+    fun kill_step (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+        Prove (qs, xs, kill_label l, t, map kill_proof subproofs, facts, meths)
       | kill_step step = step
     and kill_proof (Proof (fix, assms, steps)) =
       Proof (fix, map (apfst kill_label) assms, map kill_step steps)
@@ -189,14 +189,13 @@
     fun next_label l (next, subst) =
       let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
 
-    fun relabel_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by
-    handle Option.Option =>
-      raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically"
+    fun relabel_facts (lfs, gfs) (_, subst) =
+      (map (AList.lookup (op =) subst #> the) lfs, gfs)
+      handle Option.Option =>
+        raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically"
 
     fun relabel_assm (l, t) state =
-      let
-        val (l, state) = next_label l state
-      in ((l, t), state) end
+      next_label l state |> (fn (l, state) => ((l, t), state))
 
     fun relabel_proof (Proof (fix, assms, steps)) state =
       let
@@ -206,15 +205,15 @@
         (Proof (fix, assms, steps), state)
       end
 
-    and relabel_step (step as Let _) state = (step, state)
-      | relabel_step (Prove (qs, fix, l, t, subproofs, by)) state=
+    and relabel_step (Prove (qs, fix, l, t, subproofs, facts, meths)) state =
         let
-          val by = relabel_byline by state
+          val facts = relabel_facts facts state
           val (subproofs, state) = fold_map relabel_proof subproofs state
           val (l, state) = next_label l state
         in
-          (Prove (qs, fix, l, t, subproofs, by), state)
+          (Prove (qs, fix, l, t, subproofs, facts, meths), state)
         end
+      | relabel_step step state = (step, state)
   in
     fst (relabel_proof proof (0, []))
   end
@@ -242,13 +241,13 @@
     fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
 
     fun relabel_steps _ _ _ [] = []
-      | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
+      | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, facts, meths) :: steps) =
         let
           val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
           val sub = relabel_proofs subst depth sub
-          val by = apfst (relabel_facts subst) by
+          val facts = relabel_facts subst facts
         in
-          Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
+          Prove (qs, xs, l, t, sub, facts, meths) :: relabel_steps subst depth next steps
         end
       | relabel_steps subst depth next (step :: steps) =
         step :: relabel_steps subst depth next steps
@@ -367,7 +366,7 @@
         add_str (of_indent ind ^ "let ")
         #> add_term t1 #> add_str " = " #> add_term t2
         #> add_str "\n"
-      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), meths as meth :: _))) =
+      | add_step ind (Prove (qs, xs, l, t, subproofs, (ls, ss), meths as meth :: _)) =
         add_step_pre ind qs subproofs
         #> (case xs of
              [] => add_str (of_have qs (length subproofs) ^ " ")
@@ -387,7 +386,7 @@
     (* One-step Metis proofs are pointless; better use the one-liner directly. *)
     (case proof of
       Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
-    | Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method _ :: _))]) => ""
+    | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _)]) => ""
     | _ =>
       (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
       of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^