--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 21:55:57 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 22:16:16 2013 +0100
@@ -77,8 +77,13 @@
|> lam_trans <> metis_default_lam_trans ? cons lam_trans
in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
+fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
+ | term_name' t = ""
+
+fun lambda' v = Term.lambda_name (term_name' v, v)
+
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t
+fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t
fun make_tfree ctxt w =
let val ww = "'" ^ w in
@@ -123,10 +128,10 @@
| add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ _ = I
-fun repair_variable_name f s =
+fun repair_var_name s =
let
fun subscript_name s n = s ^ nat_subscript n
- val s = String.map f s
+ val s = String.map Char.toLower s
in
case space_explode "_" s of
[_] => (case take_suffix Char.isDigit (String.explode s) of
@@ -235,6 +240,8 @@
end
| NONE => (* a free or schematic variable *)
let
+ fun fresh_up s =
+ [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
val term_ts = map (do_term [] NONE) us
val ts = term_ts @ extra_ts
val T =
@@ -248,8 +255,10 @@
case unprefix_and_unascii schematic_var_prefix s of
SOME s => Var ((s, var_index), T)
| NONE =>
- Var ((s |> textual ? repair_variable_name Char.toLower,
- var_index), T)
+ if textual andalso not (is_tptp_variable s) then
+ Free (s |> textual ? (repair_var_name #> fresh_up), T)
+ else
+ Var ((s |> textual ? repair_var_name, var_index), T)
in list_comb (t, ts) end
in do_term [] end
@@ -294,7 +303,7 @@
(* FIXME: TFF *)
#>> quantify_over_var
(case q of AForall => forall_of | AExists => exists_of)
- (s |> textual ? repair_variable_name Char.toLower)
+ (s |> textual ? repair_var_name)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Jan 02 21:55:57 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Jan 02 22:16:16 2013 +0100
@@ -41,7 +41,6 @@
val direct_graph : direct_sequent list -> direct_graph
val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof
val succedent_of_cases : (clause * direct_inference list) list -> clause
- val chain_direct_proof : direct_proof -> direct_proof
val string_of_direct_proof : direct_proof -> string
end;
@@ -186,19 +185,6 @@
in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end
in redirect [] axioms seqs end
-val chain_direct_proof =
- let
- fun chain_inf cl0 (seq as Have (cs, c)) =
- seq
- | chain_inf _ (Cases cases) = Cases (map chain_case cases)
- and chain_case (c, is) = (c, chain_proof (SOME c) is)
- and chain_proof _ [] = []
- | chain_proof (SOME prev) (i :: is) =
- chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is
- | chain_proof _ (i :: is) =
- i :: chain_proof (SOME (succedent_of_inference i)) is
- in chain_proof NONE end
-
fun indent 0 = ""
| indent n = " " ^ indent (n - 1)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jan 02 21:55:57 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jan 02 22:16:16 2013 +0100
@@ -17,6 +17,8 @@
Fix of (string * typ) list |
Let of term * term |
Assume of label * term |
+ Obtain of
+ isar_qualifier list * (string * typ) list * label * term * byline |
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
@@ -27,7 +29,7 @@
val metis_steps_total : isar_step list -> int
end
-structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
+structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
struct
type label = string * int
@@ -39,6 +41,7 @@
Fix of (string * typ) list |
Let of term * term |
Assume of label * term |
+ Obtain of isar_qualifier list * (string * typ) list * label * term * byline |
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
@@ -46,12 +49,14 @@
fun string_for_label (s, num) = s ^ string_of_int num
-val inc = curry op+
-fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0
-fun metis_steps_total proof =
- fold (fn Prove (_,_,_, By_Metis _) => inc 1
- | Prove (_,_,_, Case_Split (cases, _)) =>
- inc (fold (inc o metis_steps_total) cases 1)
+fun metis_steps_top_level proof =
+ fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I)
+ proof 0
+fun metis_steps_total proof =
+ fold (fn Obtain _ => Integer.add 1
+ | Prove (_, _, _, By_Metis _) => Integer.add 1
+ | Prove (_, _, _, Case_Split (cases, _)) =>
+ Integer.add (fold (Integer.add o metis_steps_total) cases 1)
| _ => I) proof 0
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 21:55:57 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 22:16:16 2013 +0100
@@ -150,13 +150,13 @@
else
isa_ext
-val leo2_ext = "extcnf_equal_neg"
-val leo2_unfold_def = "unfold_def"
+val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
+val leo2_unfold_def_rule = "unfold_def"
fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) =
- (if rule = leo2_ext then
+ (if rule = leo2_extcnf_equal_neg_rule then
insert (op =) (ext_name ctxt, (Global, General))
- else if rule = leo2_unfold_def then
+ else if rule = leo2_unfold_def_rule then
(* LEO 1.3.3 does not record definitions properly, leading to missing
dependencies in the TSTP proof. Remove the next line once this is
fixed. *)
@@ -389,19 +389,18 @@
Inference_Step (name, role, t, rule, []) :: lines
else
map (replace_dependencies_in_line (name, [])) lines
- | add_line _ (Inference_Step (name, role, t, rule, deps)) lines =
+ | add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines =
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
- Inference_Step (name, role, t, rule, deps) :: lines
+ line :: lines
(* Is there a repetition? If so, replace later line by earlier one. *)
else case take_prefix (not o is_same_inference t) lines of
(* FIXME: Doesn't this code risk conflating proofs involving different
types? *)
- (_, []) => Inference_Step (name, role, t, rule, deps) :: lines
- | (pre, Inference_Step (name', role, t', rule, _) :: post) =>
- Inference_Step (name, role, t', rule, deps) ::
- pre @ map (replace_dependencies_in_line (name', [name])) post
- | _ => raise Fail "unexpected inference"
+ (_, []) => line :: lines
+ | (pre, Inference_Step (name', _, _, _, _) :: post) =>
+ line :: pre @ map (replace_dependencies_in_line (name', [name])) post
+ | _ => raise Fail "unexpected inference"
val waldmeister_conjecture_num = "1.0.0.0"
@@ -431,6 +430,12 @@
fun is_bad_free frees (Free x) = not (member (op =) frees x)
| is_bad_free _ _ = false
+val e_skolemize_rule = "skolemize"
+val vampire_skolemisation_rule = "skolemisation"
+
+val is_skolemize_rule =
+ member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
+
fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
(j, line :: map (replace_dependencies_in_line (name, [])) lines)
| add_desired_line fact_names frees
@@ -438,6 +443,7 @@
(j + 1,
if is_fact fact_names ss orelse
is_conjecture ss orelse
+ is_skolemize_rule rule orelse
(* the last line must be kept *)
j = 0 orelse
(not (is_only_type_information t) andalso
@@ -467,13 +473,16 @@
if member (op =) qs Show then "thus" else "hence"
else
if member (op =) qs Show then "show" else "have")
+ fun do_obtain qs xs =
+ (if member (op =) qs Then then "then " else "") ^ "obtain " ^
+ (space_implode " " (map fst xs)) ^ " where"
val do_term =
annotate_types ctxt
#> with_vanilla_print_mode (Syntax.string_of_term ctxt)
#> simplify_spaces
#> maybe_quote
val reconstr = Metis (type_enc, lam_trans)
- fun do_facts ind (ls, ss) =
+ fun do_metis ind (ls, ss) =
"\n" ^ do_indent (ind + 1) ^
reconstructor_command reconstr 1 1 [] 0
(ls |> sort_distinct (prod_ord string_ord int_ord),
@@ -484,14 +493,17 @@
do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
| do_step ind (Assume (l, t)) =
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
+ | do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) =
+ do_indent ind ^ do_obtain qs xs ^ " " ^
+ do_label l ^ do_term t ^ do_metis ind facts ^ "\n"
| do_step ind (Prove (qs, l, t, By_Metis facts)) =
do_indent ind ^ do_have qs ^ " " ^
- do_label l ^ do_term t ^ do_facts ind facts ^ "\n"
+ do_label l ^ do_term t ^ do_metis ind facts ^ "\n"
| do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
proofs) ^
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
- do_facts ind facts ^ "\n"
+ do_metis ind facts ^ "\n"
and do_steps prefix suffix ind steps =
let val s = implode (map (do_step ind) steps) in
replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
@@ -509,7 +521,8 @@
(if n <> 1 then "next" else "qed")
in do_proof end
-fun used_labels_of_step (Prove (_, _, _, by)) =
+fun used_labels_of_step (Obtain (_, _, _, _, By_Metis (ls, _))) = ls
+ | used_labels_of_step (Prove (_, _, _, by)) =
(case by of
By_Metis (ls, _) => ls
| Case_Split (proofs, (ls, _)) =>
@@ -522,6 +535,7 @@
val used_ls = used_labels_of proof
fun do_label l = if member (op =) used_ls l then l else no_label
fun do_step (Assume (l, t)) = Assume (do_label l, t)
+ | do_step (Obtain (qs, xs, l, t, by)) = Obtain (qs, xs, do_label l, t, by)
| do_step (Prove (qs, l, t, by)) =
Prove (qs, do_label l, t,
case by of
@@ -535,60 +549,77 @@
val relabel_proof =
let
- fun aux _ _ _ [] = []
- | aux subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
+ fun fresh_label depth (old as (l, subst, next_have)) =
+ if l = no_label then
+ old
+ else
+ let val l' = (prefix_for_depth depth have_prefix, next_have) in
+ (l', (l, l') :: subst, next_have + 1)
+ end
+ fun do_facts subst =
+ apfst (maps (the_list o AList.lookup (op =) subst))
+ fun do_byline subst depth by =
+ case by of
+ By_Metis facts => By_Metis (do_facts subst facts)
+ | Case_Split (proofs, facts) =>
+ Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs,
+ do_facts subst facts)
+ and do_proof _ _ _ [] = []
+ | do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
if l = no_label then
- Assume (l, t) :: aux subst depth (next_assum, next_have) proof
+ Assume (l, t) :: do_proof subst depth (next_assum, next_have) proof
else
let val l' = (prefix_for_depth depth assume_prefix, next_assum) in
Assume (l', t) ::
- aux ((l, l') :: subst) depth (next_assum + 1, next_have) proof
+ do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof
end
- | aux subst depth (next_assum, next_have)
+ | do_proof subst depth (next_assum, next_have)
+ (Obtain (qs, xs, l, t, by) :: proof) =
+ let
+ val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth
+ val by = by |> do_byline subst depth
+ in
+ Obtain (qs, xs, l, t, by) ::
+ do_proof subst depth (next_assum, next_have) proof
+ end
+ | do_proof subst depth (next_assum, next_have)
(Prove (qs, l, t, by) :: proof) =
let
- val (l', subst, next_have) =
- if l = no_label then
- (l, subst, next_have)
- else
- let val l' = (prefix_for_depth depth have_prefix, next_have) in
- (l', (l, l') :: subst, next_have + 1)
- end
- val relabel_facts =
- apfst (maps (the_list o AList.lookup (op =) subst))
- val by =
- case by of
- By_Metis facts => By_Metis (relabel_facts facts)
- | Case_Split (proofs, facts) =>
- Case_Split (map (aux subst (depth + 1) (1, 1)) proofs,
- relabel_facts facts)
+ val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth
+ val by = by |> do_byline subst depth
in
- Prove (qs, l', t, by) :: aux subst depth (next_assum, next_have) proof
+ Prove (qs, l, t, by) ::
+ do_proof subst depth (next_assum, next_have) proof
end
- | aux subst depth nextp (step :: proof) =
- step :: aux subst depth nextp proof
- in aux [] 0 (1, 1) end
+ | do_proof subst depth nextp (step :: proof) =
+ step :: do_proof subst depth nextp proof
+ in do_proof [] 0 (1, 1) end
val chain_direct_proof =
let
- fun succedent_of_step (Prove (_, label, _, _)) = SOME label
- | succedent_of_step (Assume (label, _)) = SOME label
- | succedent_of_step _ = NONE
- fun chain_inf (SOME label0)
- (step as Prove (qs, label, t, By_Metis (lfs, gfs))) =
- if member (op =) lfs label0 then
- Prove (Then :: qs, label, t,
- By_Metis (filter_out (curry (op =) label0) lfs, gfs))
+ fun label_of (Assume (l, _)) = SOME l
+ | label_of (Obtain (_, _, l, _, _)) = SOME l
+ | label_of (Prove (_, l, _, _)) = SOME l
+ | label_of _ = NONE
+ fun chain_step (SOME l0)
+ (step as Obtain (qs, xs, l, t, By_Metis (lfs, gfs))) =
+ if member (op =) lfs l0 then
+ Obtain (Then :: qs, xs, l, t, By_Metis (lfs |> remove (op =) l0, gfs))
else
step
- | chain_inf _ (Prove (qs, label, t, Case_Split (proofs, facts))) =
- Prove (qs, label, t, Case_Split ((map (chain_proof NONE) proofs), facts))
- | chain_inf _ step = step
+ | chain_step (SOME l0)
+ (step as Prove (qs, l, t, By_Metis (lfs, gfs))) =
+ if member (op =) lfs l0 then
+ Prove (Then :: qs, l, t, By_Metis (lfs |> remove (op =) l0, gfs))
+ else
+ step
+ | chain_step _ (Prove (qs, l, t, Case_Split (proofs, facts))) =
+ Prove (qs, l, t, Case_Split ((map (chain_proof NONE) proofs), facts))
+ | chain_step _ step = step
and chain_proof _ [] = []
| chain_proof (prev as SOME _) (i :: is) =
- chain_inf prev i :: chain_proof (succedent_of_step i) is
- | chain_proof _ (i :: is) =
- i :: chain_proof (succedent_of_step i) is
+ chain_step prev i :: chain_proof (label_of i) is
+ | chain_proof _ (i :: is) = i :: chain_proof (label_of i) is
in chain_proof NONE end
type isar_params =
@@ -644,25 +675,32 @@
val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
val axioms = axioms_of_ref_graph ref_graph conjs
val tainted = tainted_atoms_of_ref_graph ref_graph conjs
- val props =
+ val steps =
Symtab.empty
|> fold (fn Definition_Step _ => I (* FIXME *)
- | Inference_Step (name as (s, ss), role, t, _, _) =>
- Symtab.update_new (s,
- if member (op = o apsnd fst) tainted s then
- t |> role <> Conjecture ? s_not
- |> fold exists_of (map Var (Term.add_vars t []))
- else
- t))
+ | Inference_Step (name as (s, ss), role, t, rule, _) =>
+ Symtab.update_new (s, (rule,
+ t |> (if member (op = o apsnd fst) tainted s then
+ (role <> Conjecture ? s_not)
+ #> fold exists_of (map Var (Term.add_vars t []))
+ else
+ I))))
atp_proof
- (* The assumptions and conjecture are props; the rest are bools. *)
+ fun is_clause_skolemize_rule [(s, _)] =
+ Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) =
+ SOME true
+ | is_clause_skolemize_rule _ = false
+ (* The assumptions and conjecture are "prop"s; the other formulas are
+ "bool"s. *)
fun prop_of_clause [name as (s, ss)] =
(case resolve_conjecture ss of
[j] => if j = length hyp_ts then concl_t else nth hyp_ts j
- | _ => the_default @{term False} (Symtab.lookup props s)
- |> HOLogic.mk_Trueprop |> close_form)
+ | _ => the_default ("", @{term False}) (Symtab.lookup steps s)
+ |> snd |> HOLogic.mk_Trueprop |> close_form)
| prop_of_clause names =
- let val lits = map_filter (Symtab.lookup props o fst) names in
+ let
+ val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
+ in
case List.partition (can HOLogic.dest_not) lits of
(negs as _ :: _, pos as _ :: _) =>
HOLogic.mk_imp
@@ -674,12 +712,24 @@
fun maybe_show outer c =
(outer andalso length c = 1 andalso subset (op =) (c, conjs))
? cons Show
- fun do_have outer qs (gamma, c) =
- Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
- By_Metis (fold (add_fact_from_dependencies fact_names) gamma
- ([], [])))
- fun do_inf outer (Have z) = do_have outer [] z
- | do_inf outer (Cases cases) =
+ fun isar_step_of_direct_inf outer (Have (gamma, c)) =
+ let
+ val l = label_of_clause c
+ val t = prop_of_clause c
+ val by =
+ By_Metis (fold (add_fact_from_dependencies fact_names) gamma
+ ([], []))
+ in
+ if is_clause_skolemize_rule c then
+ let
+ val xs =
+ Term.add_frees t []
+ |> filter_out (Variable.is_declared ctxt o fst)
+ in Obtain ([], xs, l, t, by) end
+ else
+ Prove (maybe_show outer c [], l, t, by)
+ end
+ | isar_step_of_direct_inf outer (Cases cases) =
let val c = succedent_of_cases cases in
Prove (maybe_show outer c [Ultimately], label_of_clause c,
prop_of_clause c,
@@ -687,18 +737,18 @@
end
and do_case outer (c, infs) =
Assume (label_of_clause c, prop_of_clause c) ::
- map (do_inf outer) infs
+ map (isar_step_of_direct_inf outer) infs
val (isar_proof, (preplay_fail, ext_time)) =
ref_graph
|> redirect_graph axioms tainted
- |> map (do_inf true)
+ |> map (isar_step_of_direct_inf true)
|> append assms
|> (if not preplay andalso isar_shrink <= 1.0 then
- pair (false, (true, seconds 0.0)) #> swap
+ rpair (false, (true, seconds 0.0))
else
shrink_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout
- (if isar_proofs then isar_shrink else 1000.0))
+ preplay_timeout
+ (if isar_proofs then isar_shrink else 1000.0))
(* |>> reorder_proof_to_minimize_jumps (* ? *) *)
|>> chain_direct_proof
|>> kill_useless_labels_in_proof
@@ -711,22 +761,23 @@
case isar_text of
"" =>
if isar_proofs then
- "\nNo structured proof available (proof too short)."
+ "\nNo structured proof available (proof too simple)."
else
""
| _ =>
- let
- val msg =
- (if preplay then
- [if preplay_fail
- then "may fail"
+ let
+ val msg =
+ (if preplay then
+ [if preplay_fail then "may fail"
else string_from_ext_time ext_time]
- else [])
- @
- (if verbose then
- [let val num_steps = metis_steps_total isar_proof
- in string_of_int num_steps ^ plural_s num_steps end]
- else [])
+ else
+ []) @
+ (if verbose then
+ let val num_steps = metis_steps_total isar_proof in
+ [string_of_int num_steps ^ " step" ^ plural_s num_steps]
+ end
+ else
+ [])
in
"\n\nStructured proof "
^ (commas msg |> not (null msg) ? enclose "(" ")")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Jan 02 21:55:57 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Jan 02 22:16:16 2013 +0100
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_SHRINK =
sig
type isar_step = Sledgehammer_Proof.isar_step
- val shrink_proof :
+ val shrink_proof :
bool -> Proof.context -> string -> string -> bool -> Time.time option
-> real -> isar_step list -> isar_step list * (bool * (bool * Time.time))
end
@@ -58,225 +58,220 @@
(* Main function for shrinking proofs *)
fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
isar_shrink proof =
-let
- (* 60 seconds seems like a good interpreation of "no timeout" *)
- val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
+ let
+ (* 60 seconds seems like a good interpreation of "no timeout" *)
+ val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
+
+ (* handle metis preplay fail *)
+ local
+ open Unsynchronized
+ val metis_fail = ref false
+ in
+ fun handle_metis_fail try_metis () =
+ try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime)
+ fun get_time lazy_time =
+ if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
+ val metis_fail = fn () => !metis_fail
+ end
- (* handle metis preplay fail *)
- local
- open Unsynchronized
- val metis_fail = ref false
- in
- fun handle_metis_fail try_metis () =
- try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime)
- fun get_time lazy_time =
- if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
- val metis_fail = fn () => !metis_fail
- end
-
- (* Shrink top level proof - do not shrink case splits *)
- fun shrink_top_level on_top_level ctxt proof =
- let
- (* proof vector *)
- val proof_vect = proof |> map SOME |> Vector.fromList
- val n = Vector.length proof_vect
- val n_metis = metis_steps_top_level proof
- val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round
+ (* Shrink top level proof - do not shrink case splits *)
+ fun shrink_top_level on_top_level ctxt proof =
+ let
+ (* proof vector *)
+ val proof_vect = proof |> map SOME |> Vector.fromList
+ val n = Vector.length proof_vect
+ val n_metis = metis_steps_top_level proof
+ val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round
- (* table for mapping from (top-level-)label to proof position *)
- fun update_table (i, Assume (label, _)) =
- Label_Table.update_new (label, i)
- | update_table (i, Prove (_, label, _, _)) =
- Label_Table.update_new (label, i)
- | update_table _ = I
- val label_index_table = fold_index update_table proof Label_Table.empty
+ (* table for mapping from (top-level-)label to proof position *)
+ fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i)
+ | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i)
+ | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
+ | update_table _ = I
+ val label_index_table = fold_index update_table proof Label_Table.empty
+ val filter_refs = map_filter (Label_Table.lookup label_index_table)
- (* proof references *)
- fun refs (Prove (_, _, _, By_Metis (lfs, _))) =
- map_filter (Label_Table.lookup label_index_table) lfs
- | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
- map_filter (Label_Table.lookup label_index_table) lfs
- @ maps (maps refs) cases
- | refs _ = []
- val refed_by_vect =
- Vector.tabulate (n, (fn _ => []))
- |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
- |> Vector.map rev (* after rev, indices are sorted in ascending order *)
-
- (* candidates for elimination, use table as priority queue (greedy
- algorithm) *)
- fun add_if_cand proof_vect (i, [j]) =
- (case (the (get i proof_vect), the (get j proof_vect)) of
- (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
- cons (Term.size_of_term t, i)
- | _ => I)
- | add_if_cand _ _ = I
- val cand_tab =
- v_fold_index (add_if_cand proof_vect) refed_by_vect []
- |> Inttab.make_list
+ (* proof references *)
+ fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = filter_refs lfs
+ | refs (Prove (_, _, _, By_Metis (lfs, _))) = filter_refs lfs
+ | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
+ filter_refs lfs @ maps (maps refs) cases
+ | refs _ = []
+ val refed_by_vect =
+ Vector.tabulate (n, (fn _ => []))
+ |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
+ |> Vector.map rev (* after rev, indices are sorted in ascending order *)
- (* Metis Preplaying *)
- fun resolve_fact_names names =
- names
- |>> map string_for_label
- |> op @
- |> maps (thms_of_name ctxt)
+ (* candidates for elimination, use table as priority queue (greedy
+ algorithm) *)
+ (* TODO: consider adding "Obtain" cases *)
+ fun add_if_cand proof_vect (i, [j]) =
+ (case (the (get i proof_vect), the (get j proof_vect)) of
+ (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
+ cons (Term.size_of_term t, i)
+ | _ => I)
+ | add_if_cand _ _ = I
+ val cand_tab =
+ v_fold_index (add_if_cand proof_vect) refed_by_vect []
+ |> Inttab.make_list
- fun try_metis timeout (succedent, Prove (_, _, t, byline)) =
- if not preplay then (fn () => SOME Time.zeroTime) else
- (case byline of
- By_Metis fact_names =>
- let
- val facts = resolve_fact_names fact_names
- val goal =
- Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
- fun tac {context = ctxt, prems = _} =
- Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
- in
- take_time timeout (fn () => goal tac)
- end
- | Case_Split (cases, fact_names) =>
- let
- val facts =
+ (* Metis Preplaying *)
+ fun resolve_fact_names names =
+ names
+ |>> map string_for_label
+ |> op @
+ |> maps (thms_of_name ctxt)
+
+ (* TODO: add "Obtain" case *)
+ fun try_metis timeout (succedent, Prove (_, _, t, byline)) =
+ if not preplay then K (SOME Time.zeroTime) else
+ let
+ val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+ val facts =
+ (case byline of
+ By_Metis fact_names => resolve_fact_names fact_names
+ | Case_Split (cases, fact_names) =>
resolve_fact_names fact_names
@ (case the succedent of
- Prove (_, _, t, _) =>
- Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t
- | Assume (_, t) =>
- Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t
+ Assume (_, t) => make_thm t
+ | Obtain (_, _, _, t, _) => make_thm t
+ | Prove (_, _, t, _) => make_thm t
| _ => error "Internal error: unexpected succedent of case split")
- :: map
- (hd #> (fn Assume (_, a) => Logic.mk_implies(a, t)
- | _ => error "Internal error: malformed case split")
- #> Skip_Proof.make_thm (Proof_Context.theory_of ctxt))
- cases
- val goal =
- Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
- fun tac {context = ctxt, prems = _} =
- Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
- in
- take_time timeout (fn () => goal tac)
- end)
- | try_metis _ _ = (fn () => SOME Time.zeroTime)
+ :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
+ | _ => error "Internal error: malformed case split")
+ #> make_thm)
+ cases)
+ val goal =
+ Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
+ fun tac {context = ctxt, prems = _} =
+ Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
+ in
+ take_time timeout (fn () => goal tac)
+ end
+ | try_metis _ _ = K (SOME Time.zeroTime)
- val try_metis_quietly = the_default NONE oo try oo try_metis
+ val try_metis_quietly = the_default NONE oo try oo try_metis
+
+ (* cache metis preplay times in lazy time vector *)
+ val metis_time =
+ v_map_index
+ (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout
+ o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the)
+ proof_vect
+ fun sum_up_time lazy_time_vector =
+ Vector.foldl
+ ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts))
+ | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout)))
+ o apfst get_time)
+ no_time lazy_time_vector
- (* cache metis preplay times in lazy time vector *)
- val metis_time =
- v_map_index
- (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout
- o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the)
- proof_vect
- fun sum_up_time lazy_time_vector =
- Vector.foldl
- ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts))
- | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout)))
- o apfst get_time)
- no_time lazy_time_vector
+ (* Merging *)
+ (* TODO: consider adding "Obtain" cases *)
+ fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1)))
+ (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =
+ let
+ val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
+ val gfs = union (op =) gfs1 gfs2
+ in Prove (qs2, label2, t, By_Metis (lfs, gfs)) end
+ | merge _ _ = error "Internal error: Unmergeable Isar steps"
- (* Merging *)
- fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1)))
- (Prove (qs2, label2 , t, By_Metis (lfs2, gfs2))) =
- let
- val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
- val gfs = union (op =) gfs1 gfs2
- in Prove (qs2, label2, t, By_Metis (lfs, gfs)) end
- | merge _ _ = error "Internal error: Tring to merge unmergable isar steps"
+ fun try_merge metis_time (s1, i) (s2, j) =
+ (case get i metis_time |> Lazy.force of
+ NONE => (NONE, metis_time)
+ | SOME t1 =>
+ (case get j metis_time |> Lazy.force of
+ NONE => (NONE, metis_time)
+ | SOME t2 =>
+ let
+ val s12 = merge s1 s2
+ val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
+ in
+ case try_metis_quietly timeout (NONE, s12) () of
+ NONE => (NONE, metis_time)
+ | some_t12 =>
+ (SOME s12, metis_time
+ |> replace (Time.zeroTime |> SOME |> Lazy.value) i
+ |> replace (Lazy.value some_t12) j)
- fun try_merge metis_time (s1, i) (s2, j) =
- (case get i metis_time |> Lazy.force of
- NONE => (NONE, metis_time)
- | SOME t1 =>
- (case get j metis_time |> Lazy.force of
- NONE => (NONE, metis_time)
- | SOME t2 =>
+ end))
+
+ fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
+ if Inttab.is_empty cand_tab
+ orelse n_metis' <= target_n_metis
+ orelse (on_top_level andalso n'<3)
+ then
+ (Vector.foldr
+ (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
+ [] proof_vect,
+ sum_up_time metis_time)
+ else
let
- val s12 = merge s1 s2
- val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
+ val (i, cand_tab) = pop_max cand_tab
+ val j = get i refed_by |> the_single
+ val s1 = get i proof_vect |> the
+ val s2 = get j proof_vect |> the
in
- case try_metis_quietly timeout (NONE, s12) () of
- NONE => (NONE, metis_time)
- | some_t12 =>
- (SOME s12, metis_time
- |> replace (Time.zeroTime |> SOME |> Lazy.value) i
- |> replace (Lazy.value some_t12) j)
-
- end))
-
- fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
- if Inttab.is_empty cand_tab
- orelse n_metis' <= target_n_metis
- orelse (on_top_level andalso n'<3)
- then
- (Vector.foldr
- (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
- [] proof_vect,
- sum_up_time metis_time)
- else
- let
- val (i, cand_tab) = pop_max cand_tab
- val j = get i refed_by |> the_single
- val s1 = get i proof_vect |> the
- val s2 = get j proof_vect |> the
- in
- case try_merge metis_time (s1, i) (s2, j) of
- (NONE, metis_time) =>
- merge_steps metis_time proof_vect refed_by cand_tab n' n_metis'
- | (s, metis_time) =>
- let
- val refs = refs s1
- val refed_by = refed_by |> fold
- (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
- val new_candidates =
- fold (add_if_cand proof_vect)
- (map (fn i => (i, get i refed_by)) refs) []
- val cand_tab = add_list cand_tab new_candidates
- val proof_vect = proof_vect |> replace NONE i |> replace s j
- in
- merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) (n_metis' - 1)
+ case try_merge metis_time (s1, i) (s2, j) of
+ (NONE, metis_time) =>
+ merge_steps metis_time proof_vect refed_by cand_tab n' n_metis'
+ | (s, metis_time) =>
+ let
+ val refs = refs s1
+ val refed_by = refed_by |> fold
+ (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
+ val new_candidates =
+ fold (add_if_cand proof_vect)
+ (map (fn i => (i, get i refed_by)) refs) []
+ val cand_tab = add_list cand_tab new_candidates
+ val proof_vect = proof_vect |> replace NONE i |> replace s j
+ in
+ merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
+ (n_metis' - 1)
+ end
end
- end
- in
- merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis
- end
-
- fun shrink_proof' on_top_level ctxt proof =
- let
- (* Enrich context with top-level facts *)
- val thy = Proof_Context.theory_of ctxt
- fun enrich_ctxt (Assume (label, t)) ctxt =
- Proof_Context.put_thms false
- (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt
- | enrich_ctxt (Prove (_, label, t, _)) ctxt =
- Proof_Context.put_thms false
- (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt
- | enrich_ctxt _ ctxt = ctxt
- val rich_ctxt = fold enrich_ctxt proof ctxt
-
- (* Shrink case_splits and top-levl *)
- val ((proof, top_level_time), lower_level_time) =
- proof |> shrink_case_splits rich_ctxt
- |>> shrink_top_level on_top_level rich_ctxt
in
- (proof, ext_time_add lower_level_time top_level_time)
+ merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis
end
- and shrink_case_splits ctxt proof =
- let
- fun shrink_each_and_collect_time shrink candidates =
- let fun f_m cand time = shrink cand ||> ext_time_add time
- in fold_map f_m candidates no_time end
- val shrink_case_split = shrink_each_and_collect_time (shrink_proof' false ctxt)
- fun shrink (Prove (qs, lbl, t, Case_Split (cases, facts))) =
- let val (cases, time) = shrink_case_split cases
- in (Prove (qs, lbl, t, Case_Split (cases, facts)), time) end
- | shrink step = (step, no_time)
- in
- shrink_each_and_collect_time shrink proof
- end
-in
- shrink_proof' true ctxt proof
- |> apsnd (pair (metis_fail () ) )
-end
+ fun do_proof on_top_level ctxt proof =
+ let
+ (* Enrich context with top-level facts *)
+ val thy = Proof_Context.theory_of ctxt
+ (* TODO: add Skolem variables to context? *)
+ fun enrich_with_fact l t =
+ Proof_Context.put_thms false
+ (string_for_label l, SOME [Skip_Proof.make_thm thy t])
+ fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t
+ | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
+ | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
+ | enrich_with_step _ = I
+ val rich_ctxt = fold enrich_with_step proof ctxt
+
+ (* Shrink case_splits and top-levl *)
+ val ((proof, top_level_time), lower_level_time) =
+ proof |> do_case_splits rich_ctxt
+ |>> shrink_top_level on_top_level rich_ctxt
+ in
+ (proof, ext_time_add lower_level_time top_level_time)
+ end
+
+ and do_case_splits ctxt proof =
+ let
+ fun shrink_each_and_collect_time shrink candidates =
+ let fun f_m cand time = shrink cand ||> ext_time_add time
+ in fold_map f_m candidates no_time end
+ val shrink_case_split =
+ shrink_each_and_collect_time (do_proof false ctxt)
+ fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) =
+ let val (cases, time) = shrink_case_split cases
+ in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
+ | shrink step = (step, no_time)
+ in
+ shrink_each_and_collect_time shrink proof
+ end
+ in
+ do_proof true ctxt proof
+ |> apsnd (pair (metis_fail ()))
+ end
end