author blanchet Mon, 03 Feb 2014 11:37:48 +0100 changeset 55279 df41d34d1324 parent 55278 73372494fd80 child 55280 f0187a12b8f2
tuned data structure
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 11:30:53 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 11:37:48 2014 +0100
@@ -230,9 +230,9 @@
val skolem = is_skolemize_rule rule

fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
-              fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
+              fun steps_of_rest l step = isar_steps outer (SOME l) (step :: accum) infs

-              val deps = fold add_fact_of_dependencies gamma no_facts
+              val deps = fold add_fact_of_dependencies gamma ([], [])
val meths =
(if skolem then skolem_methods
else if is_arith_rule rule then arith_methods
@@ -246,13 +246,14 @@
[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] (no_facts, meths)] infs
+                      isar_steps outer (SOME l) [prove [subproof] (([], []), meths)] infs
end
else
-                    do_rest l (prove [] by)
-                | _ => do_rest l (prove [] by))
+                    steps_of_rest l (prove [] by)
+                | _ => steps_of_rest l (prove [] by))
else
-                do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
+                steps_of_rest l
+                  (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
end
| isar_steps outer predecessor accum (Cases cases :: infs) =
let```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:30:53 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:37:48 2014 +0100
@@ -169,7 +169,7 @@
outcome as Played _ => SOME (meth, outcome)
| _ => NONE)

-    val meths = snd (byline_of_isar_step step)
+    val meths = proof_methods_of_isar_step step
in
the_list (Par_List.get_some try_method meths)
end```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 11:30:53 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 11:37:48 2014 +0100
@@ -33,7 +33,6 @@
(facts * proof_method list)

val no_label : label
-  val no_facts : facts

val label_ord : label * label -> order
val string_of_label : label -> string
@@ -43,7 +42,8 @@
val steps_of_isar_proof : isar_proof -> isar_step list

val label_of_isar_step : isar_step -> label option
-  val byline_of_isar_step : isar_step -> facts * proof_method list
+  val facts_of_isar_step : isar_step -> facts
+  val proof_methods_of_isar_step : isar_step -> proof_method list

val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
@@ -98,7 +98,6 @@
(facts * proof_method list)

val no_label = ("", ~1)
-val no_facts = ([],[])

val label_ord = pairself swap #> prod_ord int_ord fast_string_ord

@@ -127,8 +126,11 @@
fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
| subproofs_of_isar_step _ = NONE

-fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = byline
-  | byline_of_isar_step _ = (([], []), [])
+fun facts_of_isar_step (Prove (_, _, _, _, _, (facts, _))) = facts
+  | facts_of_isar_step _ = ([], [])
+
+fun proof_methods_of_isar_step (Prove (_, _, _, _, _, (_, meths))) = meths
+  | proof_methods_of_isar_step _ = []

fun fold_isar_step f step =
fold (steps_of_isar_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
@@ -169,8 +171,7 @@
fun kill_useless_labels_in_isar_proof proof =
let
val used_ls =
-      fold_isar_steps (byline_of_isar_step #> (fn ((ls, _), _) => union (op =) ls | _ => I))
-        (steps_of_isar_proof proof) []
+      fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []

fun kill_label l = if member (op =) used_ls l then l else no_label

@@ -188,34 +189,34 @@
fun next_label l (next, subst) =
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end

-    fun do_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by
+    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 do_assm (l, t) state =
+    fun relabel_assm (l, t) state =
let
val (l, state) = next_label l state
in ((l, t), state) end

-    fun do_proof (Proof (fix, assms, steps)) state =
+    fun relabel_proof (Proof (fix, assms, steps)) state =
let
-        val (assms, state) = fold_map do_assm assms state
-        val (steps, state) = fold_map do_step steps state
+        val (assms, state) = fold_map relabel_assm assms state
+        val (steps, state) = fold_map relabel_step steps state
in
(Proof (fix, assms, steps), state)
end

-    and do_step (step as Let _) state = (step, state)
-      | do_step (Prove (qs, fix, l, t, subproofs, by)) state=
+    and relabel_step (step as Let _) state = (step, state)
+      | relabel_step (Prove (qs, fix, l, t, subproofs, by)) state=
let
-          val by = do_byline by state
-          val (subproofs, state) = fold_map do_proof subproofs state
+          val by = relabel_byline by 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)
end
in
-    fst (do_proof proof (0, []))
+    fst (relabel_proof proof (0, []))
end

val assume_prefix = "a"```