--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Sun Dec 15 22:03:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 08:35:03 2013 +0100
@@ -13,28 +13,25 @@
eqtype preplay_time
- datatype preplay_result =
- PplFail of exn |
- PplSucc of preplay_time
+ type preplay_result
- val trace : bool Config.T
- val zero_preplay_time : preplay_time
- val some_preplay_time : preplay_time
- val add_preplay_time : preplay_time -> preplay_time -> preplay_time
- val string_of_preplay_time : preplay_time -> string
+ val trace: bool Config.T
+ val zero_preplay_time: preplay_time
+ val some_preplay_time: preplay_time
+ val add_preplay_time: preplay_time -> preplay_time -> preplay_time
+ val string_of_preplay_time: preplay_time -> string
type preplay_interface =
- { get_preplay_result : label -> preplay_result,
- set_preplay_result : label -> preplay_result -> unit,
- get_preplay_time : label -> preplay_time,
- set_preplay_time : label -> preplay_time -> unit,
- preplay_quietly : Time.time -> isar_step -> preplay_time,
- (* the returned flag signals a preplay failure *)
- overall_preplay_stats : isar_proof -> preplay_time * bool }
+ {get_preplay_result: label -> preplay_result,
+ set_preplay_result: label -> preplay_result -> unit,
+ get_preplay_time: label -> preplay_time,
+ set_preplay_time: label -> preplay_time -> unit,
+ preplay_quietly: Time.time -> isar_step -> preplay_time,
+ (* the returned flag signals a preplay failure *)
+ overall_preplay_stats: isar_proof -> preplay_time * bool}
- val proof_preplay_interface :
- bool -> Proof.context -> string -> string -> bool -> Time.time
- -> isar_proof -> preplay_interface
+ val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
+ isar_proof -> preplay_interface
end;
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
@@ -53,8 +50,8 @@
type preplay_time = bool * Time.time
datatype preplay_result =
- PplFail of exn |
- PplSucc of preplay_time
+ Preplay_Success of preplay_time |
+ Preplay_Failure of exn
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *)
@@ -63,199 +60,181 @@
val string_of_preplay_time = ATP_Util.string_of_ext_time
-(* preplay tracing *)
fun preplay_trace ctxt assms concl time =
let
val ctxt = ctxt |> Config.put show_markup true
val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str
val nr_of_assms = length assms
- val assms = assms |> map (Display.pretty_thm ctxt)
- |> (fn [] => Pretty.str ""
- | [a] => a
- | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms) (* Syntax.pretty_term!? *)
+ val assms = assms
+ |> map (Display.pretty_thm ctxt)
+ |> (fn [] => Pretty.str ""
+ | [a] => a
+ | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms) (* Syntax.pretty_term!? *)
val concl = concl |> Syntax.pretty_term ctxt
- val trace_list = [] |> cons concl
- |> nr_of_assms>0 ? cons (Pretty.str "\<Longrightarrow>")
- |> cons assms
- |> cons time
+ val trace_list = []
+ |> cons concl
+ |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>")
+ |> cons assms
+ |> cons time
val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
- in tracing (Pretty.string_of pretty_trace) end
+ in
+ tracing (Pretty.string_of pretty_trace)
+ end
-(* timing *)
fun take_time timeout tac arg =
- let
- val timing = Timing.start ()
- in
+ let val timing = Timing.start () in
(TimeLimit.timeLimit timeout tac arg;
- Timing.result timing |> #cpu |> pair false)
+ Timing.result timing |> #cpu |> pair false)
handle TimeLimit.TimeOut => (true, timeout)
end
-(* lookup facts in context *)
fun resolve_fact_names ctxt names =
(names
- |>> map string_of_label
- |> op @
- |> maps (thms_of_name ctxt))
+ |>> map string_of_label
+ |> op @
+ |> maps (thms_of_name ctxt))
handle ERROR msg => error ("preplay error: " ^ msg)
-(* turn terms/proofs into theorems *)
-fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
let
+ val thy = Proof_Context.theory_of ctxt
+
val concl =
(case try List.last steps of
SOME (Prove (_, [], _, t, _, _)) => t
| _ => raise Fail "preplay error: malformed subproof")
+
val var_idx = maxidx_of_term concl + 1
- fun var_of_free (x, T) = Var((x, var_idx), T)
- val substitutions =
- map (`var_of_free #> swap #> apfst Free) fixed_frees
+ fun var_of_free (x, T) = Var ((x, var_idx), T)
+ val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees
in
Logic.list_implies (assms |> map snd, concl)
- |> subst_free substitutions
- |> thm_of_term ctxt
+ |> subst_free subst
+ |> Skip_Proof.make_thm thy
end
-(* mapping from proof methods to tactics *)
fun tac_of_method method type_enc lam_trans ctxt facts =
- case method of
+ (case method of
MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
| _ =>
- Method.insert_tac facts
- THEN' (case method of
- SimpM => Simplifier.asm_full_simp_tac
- | AutoM => Clasimp.auto_tac #> K
- | FastforceM => Clasimp.fast_force_tac
- | ForceM => Clasimp.force_tac
- | ArithM => Arith_Data.arith_tac
- | BlastM => blast_tac
- | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
+ Method.insert_tac facts THEN'
+ (case method of
+ SimpM => Simplifier.asm_full_simp_tac
+ | AutoM => Clasimp.auto_tac #> K
+ | FastforceM => Clasimp.fast_force_tac
+ | ForceM => Clasimp.force_tac
+ | ArithM => Arith_Data.arith_tac
+ | BlastM => blast_tac
+ | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt)
-
-(* main function for preplaying isar_steps; may throw exceptions *)
+(* main function for preplaying Isar steps; may throw exceptions *)
fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
| preplay_raw debug type_enc lam_trans ctxt timeout
- (Prove (_, xs, _, t, subproofs, (fact_names, proof_method))) =
- let
- val (prop, obtain) =
- (case xs of
- [] => (t, false)
- | _ =>
- (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
- (see ~~/src/Pure/Isar/obtain.ML) *)
- let
- val thesis = Term.Free ("thesis", HOLogic.boolT)
- val thesis_prop = thesis |> HOLogic.mk_Trueprop
- val frees = map Term.Free xs
+ (step as Prove (_, xs, _, t, subproofs, (fact_names, meth))) =
+ let
+ val prop =
+ (case xs of
+ [] => t
+ | _ =>
+ (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
+ (cf. "~~/src/Pure/Isar/obtain.ML") *)
+ let
+ val thesis = Term.Free ("thesis", HOLogic.boolT)
+ val thesis_prop = thesis |> HOLogic.mk_Trueprop
+ val frees = map Term.Free xs
- (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
- val inner_prop =
- fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
-
- (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
- val prop =
+ (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
+ val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
+ in
+ (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
- in
- (prop, true)
- end)
- val facts =
- map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
- val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
- |> Config.put Lin_Arith.verbose debug
- |> obtain ? Config.put Metis_Tactic.new_skolem true
- val goal =
- Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop
- fun tac {context = ctxt, prems = _} =
- HEADGOAL (tac_of_method proof_method type_enc lam_trans ctxt facts)
- fun run_tac () = goal tac
- handle ERROR msg => error ("Preplay error: " ^ msg)
- val preplay_time = take_time timeout run_tac ()
- in
- (* tracing *)
- (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time
- else ();
- preplay_time)
- end
+ end)
+
+ val facts = map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
+
+ val ctxt = ctxt
+ |> Config.put Metis_Tactic.verbose debug
+ |> Config.put Lin_Arith.verbose debug
+ |> use_metis_new_skolem step ? Config.put Metis_Tactic.new_skolem true
+
+ val goal = Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop
+
+ fun tac {context = ctxt, ...} = HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts)
+ fun run_tac () = goal tac handle ERROR msg => error ("Preplay error: " ^ msg)
+
+ val preplay_time = take_time timeout run_tac ()
+ in
+ (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time else ();
+ preplay_time)
+ end
(*** proof preplay interface ***)
type preplay_interface =
-{ get_preplay_result : label -> preplay_result,
- set_preplay_result : label -> preplay_result -> unit,
- get_preplay_time : label -> preplay_time,
- set_preplay_time : label -> preplay_time -> unit,
- preplay_quietly : Time.time -> isar_step -> preplay_time,
- (* the returned flag signals a preplay failure *)
- overall_preplay_stats : isar_proof -> preplay_time * bool }
+ {get_preplay_result: label -> preplay_result,
+ set_preplay_result: label -> preplay_result -> unit,
+ get_preplay_time: label -> preplay_time,
+ set_preplay_time: label -> preplay_time -> unit,
+ preplay_quietly: Time.time -> isar_step -> preplay_time,
+ (* the returned flag signals a preplay failure *)
+ overall_preplay_stats: isar_proof -> preplay_time * bool}
-
-(* enriches context with local proof facts *)
-fun enrich_context proof ctxt =
+fun enrich_context_with_local_facts proof ctxt =
let
val thy = Proof_Context.theory_of ctxt
fun enrich_with_fact l t =
- Proof_Context.put_thms false
- (string_of_label l, SOME [Skip_Proof.make_thm thy t])
+ Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
val enrich_with_assms = fold (uncurry enrich_with_fact)
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_fact l t #> fold enrich_with_proof subproofs
+ enrich_with_fact l t #> fold enrich_with_proof subproofs
in
enrich_with_proof proof ctxt
end
-
-(* Given a proof, produces an imperative preplay interface with a shared table
- mapping from labels to preplay results.
- The preplay results are caluclated lazyly and cached to avoid repeated
+(* Given a proof, produces an imperative preplay interface with a shared table mapping from labels
+ to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated
calculation.
- PRECONDITION: the proof must be labeled canocially, see
- Slegehammer_Proof.relabel_proof_canonically
-*)
-
-fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
- preplay_timeout proof : preplay_interface =
+ Precondition: The proof must be labeled canocially; cf.
+ "Slegehammer_Proof.relabel_proof_canonically". *)
+fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
if not do_preplay then
(* the dont_preplay option pretends that everything works just fine *)
- { get_preplay_result = K (PplSucc zero_preplay_time),
- set_preplay_result = K (K ()),
- get_preplay_time = K zero_preplay_time,
- set_preplay_time = K (K ()),
- preplay_quietly = K (K zero_preplay_time),
- overall_preplay_stats = K (zero_preplay_time, false)}
+ {get_preplay_result = K (Preplay_Success zero_preplay_time),
+ set_preplay_result = K (K ()),
+ get_preplay_time = K zero_preplay_time,
+ set_preplay_time = K (K ()),
+ preplay_quietly = K (K zero_preplay_time),
+ overall_preplay_stats = K (zero_preplay_time, false)} : preplay_interface
else
let
- (* add local proof facts to context *)
- val ctxt = enrich_context proof ctxt
+ val ctxt = enrich_context_with_local_facts proof ctxt
fun preplay quietly timeout step =
preplay_raw debug type_enc lam_trans ctxt timeout step
- |> PplSucc
+ |> Preplay_Success
handle exn =>
- if Exn.is_interrupt exn then
- reraise exn
- else if not quietly andalso debug then
- (warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n "
- ^ @{make_string} exn);
- PplFail exn)
- else
- PplFail exn
+ if Exn.is_interrupt exn then
+ reraise exn
+ else if not quietly andalso debug then
+ (warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^
+ @{make_string} exn);
+ Preplay_Failure exn)
+ else
+ Preplay_Failure exn
(* preplay steps treating exceptions like timeouts *)
fun preplay_quietly timeout step =
(case preplay true timeout step of
- PplSucc preplay_time => preplay_time
- | PplFail _ => (true, timeout))
+ Preplay_Success preplay_time => preplay_time
+ | Preplay_Failure _ => (true, timeout))
val preplay_tab =
let
@@ -263,46 +242,41 @@
case label_of_step step of
NONE => tab
| SOME l =>
- Canonical_Lbl_Tab.update_new
- (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy)
- tab
- handle Canonical_Lbl_Tab.DUP _ =>
- raise Fail "Sledgehammer_Preplay: preplay time table"
+ Canonical_Lbl_Tab.update_new
+ (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab
+ handle Canonical_Lbl_Tab.DUP _ => raise Fail "Sledgehammer_Preplay: preplay time table"
in
Canonical_Lbl_Tab.empty
|> fold_isar_steps add_step_to_tab (steps_of_proof proof)
|> Unsynchronized.ref
end
- fun get_preplay_result lbl =
- Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
- handle Option.Option =>
- raise Fail "Sledgehammer_Preplay: preplay time table"
+ fun get_preplay_result l =
+ Canonical_Lbl_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
+ handle Option.Option => raise Fail "Sledgehammer_Preplay: preplay time table"
- fun set_preplay_result lbl result =
- preplay_tab :=
- Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab)
+ fun set_preplay_result l result =
+ preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
- fun get_preplay_time lbl =
- case get_preplay_result lbl of
- PplSucc preplay_time => preplay_time
- | PplFail _ => some_preplay_time (* best approximation possible *)
+ fun get_preplay_time l =
+ (case get_preplay_result l of
+ Preplay_Success preplay_time => preplay_time
+ | Preplay_Failure _ => some_preplay_time)
- fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time)
+ fun set_preplay_time l time = set_preplay_result l (Preplay_Success time)
- fun overall_preplay_stats (Proof(_, _, steps)) =
+ fun overall_preplay_stats (Proof (_, _, steps)) =
let
fun result_of_step step =
try (label_of_step #> the #> get_preplay_result) step
- |> the_default (PplSucc zero_preplay_time)
+ |> the_default (Preplay_Success zero_preplay_time)
fun do_step step =
(case result_of_step step of
- PplSucc preplay_time => apfst (add_preplay_time preplay_time)
- | PplFail _ => apsnd (K true))
+ Preplay_Success preplay_time => apfst (add_preplay_time preplay_time)
+ | Preplay_Failure _ => apsnd (K true))
in
fold_isar_steps do_step steps (zero_preplay_time, false)
end
-
in
{get_preplay_result = get_preplay_result,
set_preplay_result = set_preplay_result,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sun Dec 15 22:03:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 08:35:03 2013 +0100
@@ -172,8 +172,8 @@
|> maybe_quote),
ctxt |> Variable.auto_fixes term)
- fun by_method method = "by " ^
- (case method of
+ fun by_method meth = "by " ^
+ (case meth of
SimpM => "simp"
| AutoM => "auto"
| FastforceM => "fastforce"
@@ -187,16 +187,15 @@
"using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
fun of_method ls ss MetisM =
- reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
- | of_method ls ss method =
- using_facts ls ss ^ by_method method
+ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
+ | of_method ls ss meth = using_facts ls ss ^ by_method meth
- fun of_byline ind options (ls, ss) method =
+ fun of_byline ind options (ls, ss) meth =
let
val ls = ls |> sort_distinct label_ord
val ss = ss |> sort_distinct string_ord
in
- "\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss method
+ "\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss meth
end
fun of_free (s, T) =
@@ -219,10 +218,10 @@
fun add_assms ind assms = fold (add_assm ind) assms
- fun add_step_post ind l t facts method options =
+ fun add_step_post ind l t facts meth options =
add_suffix (of_label l)
#> add_term t
- #> add_suffix (of_byline ind options facts method ^ "\n")
+ #> add_suffix (of_byline ind options facts meth ^ "\n")
fun of_subproof ind ctxt proof =
let
@@ -251,23 +250,21 @@
#> add_suffix " = "
#> add_term t2
#> add_suffix "\n"
- | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, method))) =
+ | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, meth))) =
(case xs of
[] => (* have *)
add_step_pre ind qs subproofs
#> add_suffix (of_prove qs (length subproofs) ^ " ")
- #> add_step_post ind l t facts method ""
+ #> add_step_post ind l t facts meth ""
| _ => (* obtain *)
add_step_pre ind qs subproofs
#> add_suffix (of_obtain qs (length subproofs) ^ " ")
#> add_frees xs
#> add_suffix " where "
- (* The new skolemizer puts the arguments in the same order as the
- ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML"
- regarding Vampire). *)
- #> add_step_post ind l t facts method
- (if exists (fn (_, T) => length (binder_types T) > 1) xs
- andalso method = MetisM then
+ (* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire --
+ but see also "atp_proof_reconstruct.ML" regarding Vampire). *)
+ #> add_step_post ind l t facts meth
+ (if use_metis_new_skolem step then
"using [[metis_new_skolem]] "
else
""))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Sun Dec 15 22:03:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 16 08:35:03 2013 +0100
@@ -45,6 +45,7 @@
val subproofs_of_step : isar_step -> isar_proof list option
val byline_of_step : isar_step -> (facts * proof_method) option
val proof_method_of_step : isar_step -> proof_method option
+ val use_metis_new_skolem : isar_step -> bool
val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
val fold_isar_steps :
@@ -59,7 +60,6 @@
val relabel_proof_canonically : isar_proof -> isar_proof
structure Canonical_Lbl_Tab : TABLE
-
end;
structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
@@ -110,6 +110,10 @@
fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method
| proof_method_of_step _ = NONE
+fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth))) =
+ meth = MetisM andalso exists (fn (_, T) => length (binder_types T) > 1) xs
+ | use_metis_new_skolem _ = false
+
fun fold_isar_steps f = fold (fold_isar_step f)
and fold_isar_step f step s =
fold (steps_of_proof #> fold_isar_steps f)