# HG changeset patch # User blanchet # Date 1387179303 -3600 # Node ID 0ef52f40d419623f355aeb0921b0eec5adc2245a # Parent a1ac3eaa0d111bbfc3c2799a8977fd839c3391ca use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning diff -r a1ac3eaa0d11 -r 0ef52f40d419 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- 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 ";" "\" "\" assms) (* Syntax.pretty_term!? *) + val assms = assms + |> map (Display.pretty_thm ctxt) + |> (fn [] => Pretty.str "" + | [a] => a + | assms => Pretty.enum ";" "\" "\" assms) (* Syntax.pretty_term!? *) val concl = concl |> Syntax.pretty_term ctxt - val trace_list = [] |> cons concl - |> nr_of_assms>0 ? cons (Pretty.str "\") - |> cons assms - |> cons time + val trace_list = [] + |> cons concl + |> nr_of_assms > 0 ? cons (Pretty.str "\") + |> 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, diff -r a1ac3eaa0d11 -r 0ef52f40d419 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- 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 "")) diff -r a1ac3eaa0d11 -r 0ef52f40d419 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- 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)