# HG changeset patch # User blanchet # Date 1391370831 -3600 # Node ID cfd276a7dbebd2ca90abb5dedfffd81486bfc8d5 # Parent 0dc4993b4f560aeafd2e36e8847eb6d1a59e9eee unform treatment of preplay_timeout = 0 and > 0 diff -r 0dc4993b4f56 -r cfd276a7dbeb src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 02 20:53:51 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 02 20:53:51 2014 +0100 @@ -137,6 +137,7 @@ val do_preplay = preplay_timeout <> Time.zeroTime val try0_isar = try0_isar andalso do_preplay + val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev @@ -279,8 +280,8 @@ |> relabel_isar_proof_canonically val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} = - preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay - preplay_timeout isar_proof + preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans preplay_timeout + isar_proof fun str_of_preplay_outcome outcome = if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" @@ -299,8 +300,7 @@ val (play_outcome, isar_proof) = isar_proof |> tap (trace_isar_proof "Original") - |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0) - preplay_data + |> compress_isar_proof compress_isar preplay_data |> tap (trace_isar_proof "Compressed") |> try0_isar ? try0_isar_proof preplay_timeout preplay_data |> tap (trace_isar_proof "Tried0") diff -r 0dc4993b4f56 -r cfd276a7dbeb src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100 @@ -21,7 +21,7 @@ preplay_quietly: Time.time -> isar_step -> play_outcome, overall_preplay_outcome: isar_proof -> play_outcome} - val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time -> + val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> Time.time -> isar_proof -> isar_preplay_data end; @@ -172,67 +172,60 @@ Precondition: The proof must be labeled canonically; cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *) -fun preplay_data_of_isar_proof 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 *) - {set_preplay_outcomes = K (K ()), - preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))), - preplay_quietly = K (K (Played Time.zeroTime)), - overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data - else - let - val ctxt = enrich_context_with_local_facts proof ctxt +fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans preplay_timeout proof = + let + val ctxt = enrich_context_with_local_facts proof ctxt - fun preplay quietly timeout meth step = - preplay_raw debug type_enc lam_trans ctxt timeout meth step - 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) - else - (); - Play_Failed) + fun preplay quietly timeout meth step = + preplay_raw debug type_enc lam_trans ctxt timeout meth step + 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) + else + (); + Play_Failed) - (* preplay steps treating exceptions like timeouts *) - fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) = - preplay true timeout meth step - | preplay_quietly _ _ = Played Time.zeroTime + (* preplay steps treating exceptions like timeouts *) + fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) = + preplay true timeout meth step + | preplay_quietly _ _ = Played Time.zeroTime - val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty + val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty + + fun set_preplay_outcomes l meths_outcomes = + preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes) + (!preplay_tab) - fun set_preplay_outcomes l meths_outcomes = - preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes) - (!preplay_tab) + fun preplay_outcome l meth = + (case Canonical_Label_Tab.lookup (!preplay_tab) l of + SOME meths_outcomes => + (case AList.lookup (op =) meths_outcomes meth of + SOME outcome => outcome + | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method") + | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label") - fun preplay_outcome l meth = - (case Canonical_Label_Tab.lookup (!preplay_tab) l of - SOME meths_outcomes => - (case AList.lookup (op =) meths_outcomes meth of - SOME outcome => outcome - | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method") - | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label") - - fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) = - Lazy.force (preplay_outcome l meth) - | result_of_step _ = Played Time.zeroTime + fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) = + Lazy.force (preplay_outcome l meth) + | result_of_step _ = Played Time.zeroTime - fun overall_preplay_outcome (Proof (_, _, steps)) = - fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime) + fun overall_preplay_outcome (Proof (_, _, steps)) = + fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime) - fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = - preplay_tab := Canonical_Label_Tab.update (l, map (fn meth => - (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths) - (!preplay_tab) - | reset_preplay_outcomes _ = () + fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = + preplay_tab := Canonical_Label_Tab.update (l, map (fn meth => + (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths) + (!preplay_tab) + | reset_preplay_outcomes _ = () - val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) () - in - {set_preplay_outcomes = set_preplay_outcomes, - preplay_outcome = preplay_outcome, - preplay_quietly = preplay_quietly, - overall_preplay_outcome = overall_preplay_outcome} - end + val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) () + in + {set_preplay_outcomes = set_preplay_outcomes, + preplay_outcome = preplay_outcome, + preplay_quietly = preplay_quietly, + overall_preplay_outcome = overall_preplay_outcome} + end end;