--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 16:10:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 16:26:43 2014 +0100
@@ -352,35 +352,35 @@
|> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
*)
|> isar_proof true params assms lems
- |> postprocess_remove_unreferenced_steps I
- |> relabel_proof_canonically
- |> `(proof_preplay_data debug ctxt metis_type_enc metis_lam_trans do_preplay
- preplay_timeout)
+ |> postprocess_isar_proof_remove_unreferenced_steps I
+ |> relabel_isar_proof_canonically
+ |> `(preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
+ preplay_timeout)
val (play_outcome, isar_proof) =
isar_proof
- |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0) preplay_data
+ |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
+ preplay_data
|> try0_isar ? try0_isar_proof preplay_timeout preplay_data
- |> postprocess_remove_unreferenced_steps (try0_isar ? minimal_deps_of_step preplay_data)
+ |> postprocess_isar_proof_remove_unreferenced_steps
+ (try0_isar ? minimize_isar_step_dependencies preplay_data)
|> `overall_preplay_outcome
||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
val isar_text =
- string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
+ string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
in
(case isar_text of
"" =>
- if isar_proofs = SOME true then
- "\nNo structured proof available (proof too simple)."
- else
- ""
+ if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
+ else ""
| _ =>
let
val msg =
(if verbose then
- let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in
- [string_of_int num_steps ^ " step" ^ plural_s num_steps]
- end
+ let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in
+ [string_of_int num_steps ^ " step" ^ plural_s num_steps]
+ end
else
[]) @
(if do_preplay then [string_of_play_outcome play_outcome] else [])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 16:10:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 16:26:43 2014 +0100
@@ -9,12 +9,12 @@
When configuring the pretty printer appropriately, the constraints will show up as type annotations
when printing the term. This allows the term to be printed and reparsed without a change of types.
-NOTE: Terms should be unchecked before calling annotate_types to avoid awkward syntax.
+Note: Terms should be unchecked before calling "annotate_types_in_term" to avoid awkward syntax.
*)
signature SLEDGEHAMMER_ISAR_ANNOTATE =
sig
- val annotate_types : Proof.context -> term -> term
+ val annotate_types_in_term : Proof.context -> term -> term
end;
structure Sledgehammer_Isar_Annotate : SLEDGEHAMMER_ISAR_ANNOTATE =
@@ -197,7 +197,7 @@
end
(* (7) Annotate *)
-fun annotate_types ctxt t =
+fun annotate_types_in_term ctxt t =
let
val t' = generalize_types ctxt t
val subst = match_types ctxt t' t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 16:10:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 16:26:43 2014 +0100
@@ -9,9 +9,9 @@
signature SLEDGEHAMMER_ISAR_COMPRESS =
sig
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
- type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
+ type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val compress_proof : real -> preplay_data -> isar_proof -> isar_proof
+ val compress_isar_proof : real -> isar_preplay_data -> isar_proof -> isar_proof
end;
structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
@@ -95,8 +95,8 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
-fun compress_proof compress_isar
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data) proof =
+fun compress_isar_proof compress_isar
+ ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
if compress_isar <= 1.0 then
proof
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 16:10:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 16:26:43 2014 +0100
@@ -7,12 +7,13 @@
signature SLEDGEHAMMER_ISAR_MINIMIZE =
sig
- type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
type isar_step = Sledgehammer_Isar_Proof.isar_step
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
+ type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val minimal_deps_of_step : preplay_data -> isar_step -> isar_step
- val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
+ val minimize_isar_step_dependencies : isar_preplay_data -> isar_step -> isar_step
+ val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
+ isar_proof
end;
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
@@ -24,8 +25,8 @@
val slack = seconds 0.1
-fun minimal_deps_of_step (_ : preplay_data) (step as Let _) = step
- | minimal_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
+ | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
(case get_preplay_outcome l of
Played time =>
@@ -46,7 +47,7 @@
end
| _ => step (* don't touch steps that time out or fail *))
-fun postprocess_remove_unreferenced_steps postproc_step =
+fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
let
val add_lfs = fold (Ord_List.insert label_ord)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 16:10:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 16:26:43 2014 +0100
@@ -14,14 +14,14 @@
val trace : bool Config.T
- type preplay_data =
+ type isar_preplay_data =
{get_preplay_outcome: label -> play_outcome,
set_preplay_outcome: label -> play_outcome -> unit,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
- val proof_preplay_data : bool -> Proof.context -> string -> string -> bool -> Time.time ->
- isar_proof -> preplay_data
+ val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
+ isar_proof -> isar_preplay_data
end;
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
@@ -147,7 +147,7 @@
(*** proof preplay interface ***)
-type preplay_data =
+type isar_preplay_data =
{get_preplay_outcome: label -> play_outcome,
set_preplay_outcome: label -> play_outcome -> unit,
preplay_quietly: Time.time -> isar_step -> play_outcome,
@@ -184,14 +184,14 @@
calculation.
Precondition: The proof must be labeled canonically; cf.
- "Slegehammer_Proof.relabel_proof_canonically". *)
-fun proof_preplay_data debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
+ "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 *)
{get_preplay_outcome = K (Played Time.zeroTime),
set_preplay_outcome = K (K ()),
preplay_quietly = K (K (Played Time.zeroTime)),
- overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_data
+ overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
else
let
val ctxt = enrich_context_with_local_facts proof ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 16:10:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 16:26:43 2014 +0100
@@ -40,11 +40,10 @@
structure Canonical_Label_Tab : TABLE
- (** canonical proof labels: 1, 2, 3, ... in postorder **)
val canonical_label_ord : (label * label) -> order
- val relabel_proof_canonically : isar_proof -> isar_proof
+ val relabel_isar_proof_canonically : isar_proof -> isar_proof
- val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
+ val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
end;
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
@@ -112,14 +111,14 @@
type key = label
val ord = canonical_label_ord)
-fun relabel_proof_canonically proof =
+fun relabel_isar_proof_canonically proof =
let
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
handle Option.Option =>
- raise Fail "Sledgehammer_Isar_Proof: relabel_proof_canonically"
+ raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically"
fun do_assm (l, t) state =
let
@@ -149,7 +148,7 @@
val indent_size = 2
-fun string_of_proof ctxt type_enc lam_trans i n proof =
+fun string_of_isar_proof ctxt type_enc lam_trans i n proof =
let
(* Make sure only type constraints inserted by the type annotation code are printed. *)
val ctxt =
@@ -183,7 +182,7 @@
fun add_term term (s, ctxt) =
(s ^ (term
|> singleton (Syntax.uncheck_terms ctxt)
- |> annotate_types ctxt
+ |> annotate_types_in_term ctxt
|> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
|> simplify_spaces
|> maybe_quote),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 16:10:39 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 16:26:43 2014 +0100
@@ -9,9 +9,9 @@
signature SLEDGEHAMMER_ISAR_TRY0 =
sig
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
- type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
+ type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
- val try0_isar_proof : Time.time -> preplay_data -> isar_proof -> isar_proof
+ val try0_isar_proof : Time.time -> isar_preplay_data -> isar_proof -> isar_proof
end;
structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
@@ -30,7 +30,7 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data)
+ ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
(step as Prove (_, _, l, _, _, _)) =
let
val timeout =