--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jul 08 14:24:36 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 09 18:44:59 2013 +0200
@@ -462,7 +462,7 @@
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime,
- preplay = Lazy.value (Sledgehammer_Reconstruct.Failed_to_Play
+ preplay = Lazy.value (Sledgehammer_Reconstructor.Failed_to_Play
Sledgehammer_Provers.plain_metis),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
--- a/src/HOL/Sledgehammer.thy Mon Jul 08 14:24:36 2013 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Jul 09 18:44:59 2013 +0200
@@ -14,9 +14,11 @@
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML"
ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_print.ML"
ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Mon Jul 08 14:24:36 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Tue Jul 09 18:44:59 2013 +0200
@@ -36,6 +36,7 @@
val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
val ((v', s''), _) = post_traverse_term_type' f env v s'
in f (u' $ v') T s'' end
+ handle Bind => raise Fail "Sledgehammer_Annotate: post_traverse_term_type'"
fun post_traverse_term_type f s t =
post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jul 08 14:24:36 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Jul 09 18:44:59 2013 +0200
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_MINIMIZE =
sig
type stature = ATP_Problem_Generate.stature
- type play = Sledgehammer_Reconstruct.play
+ type play = Sledgehammer_Reconstructor.play
type mode = Sledgehammer_Provers.mode
type params = Sledgehammer_Provers.params
type prover = Sledgehammer_Provers.prover
@@ -38,6 +38,7 @@
open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact
+open Sledgehammer_Reconstructor
open Sledgehammer_Reconstruct
open Sledgehammer_Provers
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Tue Jul 09 18:44:59 2013 +0200
@@ -0,0 +1,246 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Basic mapping from proof data structures to proof strings.
+*)
+
+signature SLEDGEHAMMER_PRINT =
+sig
+ type isar_proof = Sledgehammer_Proof.isar_proof
+ type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type one_line_params = Sledgehammer_Reconstructor.one_line_params
+
+ val string_of_reconstructor : reconstructor -> string
+
+ val one_line_proof_text : int -> one_line_params -> string
+
+ val string_of_proof :
+ Proof.context -> string -> string -> int -> int -> isar_proof -> string
+end;
+
+structure Sledgehammer_Print : SLEDGEHAMMER_PRINT =
+struct
+
+open ATP_Util
+open ATP_Proof
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Proof
+open Sledgehammer_Annotate
+
+
+(** reconstructors **)
+
+fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
+ metis_call type_enc lam_trans
+ | string_of_reconstructor SMT = smtN
+
+
+
+(** one-liner reconstructor proofs **)
+
+fun show_time NONE = ""
+ | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
+
+(* FIXME: Various bugs, esp. with "unfolding"
+fun unusing_chained_facts _ 0 = ""
+ | unusing_chained_facts used_chaineds num_chained =
+ if length used_chaineds = num_chained then ""
+ else if null used_chaineds then "(* using no facts *) "
+ else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
+*)
+
+fun apply_on_subgoal _ 1 = "by "
+ | apply_on_subgoal 1 _ = "apply "
+ | apply_on_subgoal i n =
+ "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
+
+fun using_labels [] = ""
+ | using_labels ls =
+ "using " ^ space_implode " " (map string_of_label ls) ^ " "
+
+fun command_call name [] =
+ name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+
+fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
+ (* unusing_chained_facts used_chaineds num_chained ^ *)
+ using_labels ls ^ apply_on_subgoal i n ^
+ command_call (string_of_reconstructor reconstr) ss
+
+fun try_command_line banner time command =
+ banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
+
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command ss =
+ case minimize_command ss of
+ "" => ""
+ | command =>
+ "\nTo minimize: " ^ Active.sendback_markup command ^ "."
+
+fun split_used_facts facts =
+ facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
+ |> pairself (sort_distinct (string_ord o pairself fst))
+
+fun one_line_proof_text num_chained
+ (preplay, banner, used_facts, minimize_command, subgoal,
+ subgoal_count) =
+ let
+ val (chained, extra) = split_used_facts used_facts
+ val (failed, reconstr, ext_time) =
+ case preplay of
+ Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
+ | Trust_Playable (reconstr, time) =>
+ (false, reconstr,
+ case time of
+ NONE => NONE
+ | SOME time =>
+ if time = Time.zeroTime then NONE else SOME (true, time))
+ | Failed_to_Play reconstr => (true, reconstr, NONE)
+ val try_line =
+ ([], map fst extra)
+ |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
+ num_chained
+ |> (if failed then
+ enclose "One-line proof reconstruction failed: "
+ ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
+ \solve this.)"
+ else
+ try_command_line banner ext_time)
+ in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
+
+
+
+
+(** detailed Isar proofs **)
+
+val indent_size = 2
+
+fun string_of_proof ctxt type_enc lam_trans i n proof =
+ let
+ val ctxt =
+ (* make sure type constraint are actually printed *)
+ ctxt |> Config.put show_markup false
+ (* make sure only type constraints inserted by sh_annotate are printed *)
+ |> Config.put Printer.show_type_emphasis false
+ |> Config.put show_types false
+ |> Config.put show_sorts false
+ |> Config.put show_consts false
+ val register_fixes = map Free #> fold Variable.auto_fixes
+ fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
+ fun of_indent ind = replicate_string (ind * indent_size) " "
+ fun of_moreover ind = of_indent ind ^ "moreover\n"
+ fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
+ fun of_obtain qs nr =
+ (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
+ "ultimately "
+ else if nr=1 orelse member (op =) qs Then then
+ "then "
+ else
+ "") ^ "obtain"
+ fun of_show_have qs = if member (op =) qs Show then "show" else "have"
+ fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
+ fun of_prove qs nr =
+ if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
+ "ultimately " ^ of_show_have qs
+ else if nr=1 orelse member (op =) qs Then then
+ of_thus_hence qs
+ else
+ of_show_have qs
+ fun add_term term (s, ctxt) =
+ (s ^ (term
+ |> singleton (Syntax.uncheck_terms ctxt)
+ |> annotate_types ctxt
+ |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
+ |> simplify_spaces
+ |> maybe_quote),
+ ctxt |> Variable.auto_fixes term)
+ val reconstr = Metis (type_enc, lam_trans)
+ fun of_metis ind options (ls, ss) =
+ "\n" ^ of_indent (ind + 1) ^ options ^
+ reconstructor_command reconstr 1 1 [] 0
+ (ls |> sort_distinct (prod_ord string_ord int_ord),
+ ss |> sort_distinct string_ord)
+ fun of_free (s, T) =
+ maybe_quote s ^ " :: " ^
+ maybe_quote (simplify_spaces (with_vanilla_print_mode
+ (Syntax.string_of_typ ctxt) T))
+ fun add_frees xs (s, ctxt) =
+ (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
+ fun add_fix _ [] = I
+ | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
+ #> add_frees xs
+ #> add_suffix "\n"
+ fun add_assm ind (l, t) =
+ add_suffix (of_indent ind ^ "assume " ^ of_label l)
+ #> add_term t
+ #> add_suffix "\n"
+ fun add_assms ind assms = fold (add_assm ind) assms
+ fun add_step_post ind l t facts options =
+ add_suffix (of_label l)
+ #> add_term t
+ #> add_suffix (of_metis ind options facts ^ "\n")
+ fun of_subproof ind ctxt proof =
+ let
+ val ind = ind + 1
+ val s = of_proof ind ctxt proof
+ val prefix = "{ "
+ val suffix = " }"
+ in
+ replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
+ String.extract (s, ind * indent_size,
+ SOME (size s - ind * indent_size - 1)) ^
+ suffix ^ "\n"
+ end
+ and of_subproofs _ _ _ [] = ""
+ | of_subproofs ind ctxt qs subproofs =
+ (if member (op =) qs Then then of_moreover ind else "") ^
+ space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
+ and add_step_pre ind qs subproofs (s, ctxt) =
+ (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
+ and add_step ind (Let (t1, t2)) =
+ add_suffix (of_indent ind ^ "let ")
+ #> add_term t1
+ #> add_suffix " = "
+ #> add_term t2
+ #> add_suffix "\n"
+ | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis facts)) =
+ (case xs of
+ [] => (* have *)
+ add_step_pre ind qs subproofs
+ #> add_suffix (of_prove qs (length subproofs) ^ " ")
+ #> add_step_post ind l t facts ""
+ | _ => (* 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
+ (if exists (fn (_, T) => length (binder_types T) > 1) xs then
+ "using [[metis_new_skolem]] "
+ else
+ ""))
+ and add_steps ind = fold (add_step ind)
+ and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
+ ("", ctxt)
+ |> add_fix ind xs
+ |> add_assms ind assms
+ |> add_steps ind steps
+ |> fst
+ in
+ (* One-step proofs are pointless; better use the Metis one-liner
+ directly. *)
+ case proof of
+ Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => ""
+ | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
+ of_indent 0 ^ (if n <> 1 then "next" else "qed")
+ end
+
+ end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jul 08 14:24:36 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jul 09 18:44:59 2013 +0200
@@ -12,9 +12,9 @@
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
- type reconstructor = Sledgehammer_Reconstruct.reconstructor
- type play = Sledgehammer_Reconstruct.play
- type minimize_command = Sledgehammer_Reconstruct.minimize_command
+ type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type play = Sledgehammer_Reconstructor.play
+ type minimize_command = Sledgehammer_Reconstructor.minimize_command
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
@@ -150,6 +150,8 @@
open Metis_Tactic
open Sledgehammer_Util
open Sledgehammer_Fact
+open Sledgehammer_Reconstructor
+open Sledgehammer_Print
open Sledgehammer_Reconstruct
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Jul 08 14:24:36 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Jul 09 18:44:59 2013 +0200
@@ -9,26 +9,13 @@
sig
type 'a proof = 'a ATP_Proof.proof
type stature = ATP_Problem_Generate.stature
-
- datatype reconstructor =
- Metis of string * string |
- SMT
+ type one_line_params = Sledgehammer_Print.one_line_params
- datatype play =
- Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option |
- Failed_to_Play of reconstructor
-
- type minimize_command = string list -> string
- type one_line_params =
- play * string * (string * stature) list * minimize_command * int * int
type isar_params =
bool * bool * Time.time option * bool * real * string Symtab.table
* (string * stature) list vector * (string * term) list * int Symtab.table
* string proof * thm
- val smtN : string
- val string_of_reconstructor : reconstructor -> string
val lam_trans_of_atp_proof : string proof -> string -> string
val is_typed_helper_used_in_atp_proof : string proof -> bool
val used_facts_in_atp_proof :
@@ -37,7 +24,6 @@
val used_facts_in_unsound_atp_proof :
Proof.context -> (string * stature) list vector -> 'a proof ->
string list option
- val one_line_proof_text : int -> one_line_params -> string
val isar_proof_text :
Proof.context -> bool option -> isar_params -> one_line_params -> string
val proof_text :
@@ -54,8 +40,10 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
+open Sledgehammer_Reconstructor
open Sledgehammer_Proof
open Sledgehammer_Annotate
+open Sledgehammer_Print
open Sledgehammer_Compress
structure String_Redirect = ATP_Proof_Redirect(
@@ -65,25 +53,6 @@
open String_Redirect
-
-(** reconstructors **)
-
-datatype reconstructor =
- Metis of string * string |
- SMT
-
-datatype play =
- Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option |
- Failed_to_Play of reconstructor
-
-val smtN = "smt"
-
-fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
- metis_call type_enc lam_trans
- | string_of_reconstructor SMT = smtN
-
-
(** fact extraction from ATP proofs **)
fun find_first_in_list_vector vec key =
@@ -189,83 +158,6 @@
end
-(** one-liner reconstructor proofs **)
-
-fun show_time NONE = ""
- | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
-
-(* FIXME: Various bugs, esp. with "unfolding"
-fun unusing_chained_facts _ 0 = ""
- | unusing_chained_facts used_chaineds num_chained =
- if length used_chaineds = num_chained then ""
- else if null used_chaineds then "(* using no facts *) "
- else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
-*)
-
-fun apply_on_subgoal _ 1 = "by "
- | apply_on_subgoal 1 _ = "apply "
- | apply_on_subgoal i n =
- "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
-
-fun using_labels [] = ""
- | using_labels ls =
- "using " ^ space_implode " " (map string_of_label ls) ^ " "
-
-fun command_call name [] =
- name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
- | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-
-fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
- (* unusing_chained_facts used_chaineds num_chained ^ *)
- using_labels ls ^ apply_on_subgoal i n ^
- command_call (string_of_reconstructor reconstr) ss
-
-fun try_command_line banner time command =
- banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
-
-fun minimize_line _ [] = ""
- | minimize_line minimize_command ss =
- case minimize_command ss of
- "" => ""
- | command =>
- "\nTo minimize: " ^ Active.sendback_markup command ^ "."
-
-fun split_used_facts facts =
- facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
- |> pairself (sort_distinct (string_ord o pairself fst))
-
-type minimize_command = string list -> string
-type one_line_params =
- play * string * (string * stature) list * minimize_command * int * int
-
-fun one_line_proof_text num_chained
- (preplay, banner, used_facts, minimize_command, subgoal,
- subgoal_count) =
- let
- val (chained, extra) = split_used_facts used_facts
- val (failed, reconstr, ext_time) =
- case preplay of
- Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
- | Trust_Playable (reconstr, time) =>
- (false, reconstr,
- case time of
- NONE => NONE
- | SOME time =>
- if time = Time.zeroTime then NONE else SOME (true, time))
- | Failed_to_Play reconstr => (true, reconstr, NONE)
- val try_line =
- ([], map fst extra)
- |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
- num_chained
- |> (if failed then
- enclose "One-line proof reconstruction failed: "
- ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
- \solve this.)"
- else
- try_command_line banner ext_time)
- in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
-
-
(** Isar proof construction and manipulation **)
val assume_prefix = "a"
@@ -429,131 +321,6 @@
else
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
-val indent_size = 2
-
-fun string_of_proof ctxt type_enc lam_trans i n proof =
- let
- val ctxt =
- (* make sure type constraint are actually printed *)
- ctxt |> Config.put show_markup false
- (* make sure only type constraints inserted by sh_annotate are printed *)
- |> Config.put Printer.show_type_emphasis false
- |> Config.put show_types false
- |> Config.put show_sorts false
- |> Config.put show_consts false
- val register_fixes = map Free #> fold Variable.auto_fixes
- fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
- fun of_indent ind = replicate_string (ind * indent_size) " "
- fun of_moreover ind = of_indent ind ^ "moreover\n"
- fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
- fun of_obtain qs nr =
- (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
- "ultimately "
- else if nr=1 orelse member (op =) qs Then then
- "then "
- else
- "") ^ "obtain"
- fun of_show_have qs = if member (op =) qs Show then "show" else "have"
- fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
- fun of_prove qs nr =
- if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
- "ultimately " ^ of_show_have qs
- else if nr=1 orelse member (op =) qs Then then
- of_thus_hence qs
- else
- of_show_have qs
- fun add_term term (s, ctxt) =
- (s ^ (term
- |> singleton (Syntax.uncheck_terms ctxt)
- |> annotate_types ctxt
- |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
- |> simplify_spaces
- |> maybe_quote),
- ctxt |> Variable.auto_fixes term)
- val reconstr = Metis (type_enc, lam_trans)
- fun of_metis ind options (ls, ss) =
- "\n" ^ of_indent (ind + 1) ^ options ^
- reconstructor_command reconstr 1 1 [] 0
- (ls |> sort_distinct (prod_ord string_ord int_ord),
- ss |> sort_distinct string_ord)
- fun of_free (s, T) =
- maybe_quote s ^ " :: " ^
- maybe_quote (simplify_spaces (with_vanilla_print_mode
- (Syntax.string_of_typ ctxt) T))
- fun add_frees xs (s, ctxt) =
- (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
- fun add_fix _ [] = I
- | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
- #> add_frees xs
- #> add_suffix "\n"
- fun add_assm ind (l, t) =
- add_suffix (of_indent ind ^ "assume " ^ of_label l)
- #> add_term t
- #> add_suffix "\n"
- fun add_assms ind assms = fold (add_assm ind) assms
- fun add_step_post ind l t facts options =
- add_suffix (of_label l)
- #> add_term t
- #> add_suffix (of_metis ind options facts ^ "\n")
- fun of_subproof ind ctxt proof =
- let
- val ind = ind + 1
- val s = of_proof ind ctxt proof
- val prefix = "{ "
- val suffix = " }"
- in
- replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
- String.extract (s, ind * indent_size,
- SOME (size s - ind * indent_size - 1)) ^
- suffix ^ "\n"
- end
- and of_subproofs _ _ _ [] = ""
- | of_subproofs ind ctxt qs subproofs =
- (if member (op =) qs Then then of_moreover ind else "") ^
- space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
- and add_step_pre ind qs subproofs (s, ctxt) =
- (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
- and add_step ind (Let (t1, t2)) =
- add_suffix (of_indent ind ^ "let ")
- #> add_term t1
- #> add_suffix " = "
- #> add_term t2
- #> add_suffix "\n"
- | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By_Metis facts)) =
- (case xs of
- [] => (* have *)
- add_step_pre ind qs subproofs
- #> add_suffix (of_prove qs (length subproofs) ^ " ")
- #> add_step_post ind l t facts ""
- | _ => (* 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
- (if exists (fn (_, T) => length (binder_types T) > 1) xs then
- "using [[metis_new_skolem]] "
- else
- ""))
- and add_steps ind = fold (add_step ind)
- and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
- ("", ctxt)
- |> add_fix ind xs
- |> add_assms ind assms
- |> add_steps ind steps
- |> fst
- in
- (* One-step proofs are pointless; better use the Metis one-liner
- directly. *)
- case proof of
- Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => ""
- | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
- of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
- of_indent 0 ^ (if n <> 1 then "next" else "qed")
- end
val add_labels_of_proof =
steps_of_proof #> fold_isar_steps
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Tue Jul 09 18:44:59 2013 +0200
@@ -0,0 +1,52 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Reconstructors.
+*)
+
+signature SLEDGEHAMMER_RECONSTRUCTOR =
+sig
+
+ type stature = ATP_Problem_Generate.stature
+
+ datatype reconstructor =
+ Metis of string * string |
+ SMT
+
+ datatype play =
+ Played of reconstructor * Time.time |
+ Trust_Playable of reconstructor * Time.time option |
+ Failed_to_Play of reconstructor
+
+ type minimize_command = string list -> string
+
+ type one_line_params =
+ play * string * (string * stature) list * minimize_command * int * int
+
+ val smtN : string
+
+end
+
+structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
+struct
+
+open ATP_Problem_Generate
+
+datatype reconstructor =
+ Metis of string * string |
+ SMT
+
+datatype play =
+ Played of reconstructor * Time.time |
+ Trust_Playable of reconstructor * Time.time option |
+ Failed_to_Play of reconstructor
+
+type minimize_command = string list -> string
+
+type one_line_params =
+ play * string * (string * stature) list * minimize_command * int * int
+
+val smtN = "smt"
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Jul 08 14:24:36 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jul 09 18:44:59 2013 +0200
@@ -10,7 +10,7 @@
sig
type fact = Sledgehammer_Fact.fact
type fact_override = Sledgehammer_Fact.fact_override
- type minimize_command = Sledgehammer_Reconstruct.minimize_command
+ type minimize_command = Sledgehammer_Reconstructor.minimize_command
type mode = Sledgehammer_Provers.mode
type params = Sledgehammer_Provers.params