--- a/NEWS Thu Mar 31 11:17:52 2011 +0200
+++ b/NEWS Thu Mar 31 17:15:13 2011 +0200
@@ -49,6 +49,7 @@
* Sledgehammer:
- sledgehammer available_provers ~> sledgehammer supported_provers
INCOMPATIBILITY.
+ - Added "monomorphize" and "monomorphize_limit" options.
* "try":
- Added "simp:", "intro:", and "elim:" options.
--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Mar 31 11:17:52 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Mar 31 17:15:13 2011 +0200
@@ -555,6 +555,19 @@
filter. If the option is set to \textit{smart}, it is set to a value that was
empirically found to be appropriate for the prover. A typical value would be
300.
+
+\opfalse{monomorphize}{dont\_monomorphize}
+Specifies whether the relevant facts should be monomorphized---i.e., whether
+their type variables should be instantiated with relevant ground types.
+Monomorphization is always performed for SMT solvers, irrespective of this
+option. Monomorphization can simplify reasoning but also leads to larger fact
+bases, which can slow down the ATPs.
+
+\opdefault{monomorphize\_limit}{int}{\upshape 4}
+Specifies the maximum number of iterations for the monomorphization fixpoint
+construction. The higher this limit is, the more monomorphic instances are
+potentially generated.
+
\end{enum}
\subsection{Output Format}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 17:15:13 2011 +0200
@@ -558,7 +558,7 @@
Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
- val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre
+ val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre
handle TimeLimit.TimeOut => false
fun apply_reconstructor m1 m2 =
if metis_ft
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 31 17:15:13 2011 +0200
@@ -154,7 +154,7 @@
let
val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
in
- case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
+ case Try.invoke_try (SOME (seconds 5.0)) ([], [], [], []) state of
true => (Solved, [])
| false => (Unsolved, [])
end
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Thu Mar 31 17:15:13 2011 +0200
@@ -28,8 +28,9 @@
signature SMT_MONOMORPH =
sig
- val monomorph: (int * thm) list -> Proof.context ->
- (int * thm) list * Proof.context
+ val typ_has_tvars: typ -> bool
+ val monomorph: bool -> ('a * thm) list -> Proof.context ->
+ ('a * thm) list * Proof.context
end
structure SMT_Monomorph: SMT_MONOMORPH =
@@ -159,37 +160,44 @@
in most_specific [] end
-fun instantiate (i, thm) substs (ithms, ctxt) =
+fun instantiate full (i, thm) substs (ithms, ctxt) =
let
+ val thy = ProofContext.theory_of ctxt
+
val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
val (Tenv, ctxt') =
ctxt
|> Variable.invent_types Ss
|>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
- val thy = ProofContext.theory_of ctxt'
+ exception PARTIAL_INST of unit
+
+ fun update_subst vT subst =
+ if full then Vartab.update vT subst
+ else raise PARTIAL_INST ()
fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
| replace _ T = T
fun complete (vT as (v, _)) subst =
subst
- |> not (Vartab.defined subst v) ? Vartab.update vT
+ |> not (Vartab.defined subst v) ? update_subst vT
|> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
fun inst subst =
let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
- in (i, Thm.instantiate (cTs, []) thm) end
+ in SOME (i, Thm.instantiate (cTs, []) thm) end
+ handle PARTIAL_INST () => NONE
- in (map inst substs @ ithms, ctxt') end
+ in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end
(* overall procedure *)
-fun mono_all ctxt polys monos =
+fun mono_all full ctxt polys monos =
let
val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys
@@ -208,13 +216,13 @@
|> search_substitutions ctxt limit instances Symtab.empty grounds
|> map (filter_most_specific (ProofContext.theory_of ctxt))
|> rpair (monos, ctxt)
- |-> fold2 instantiate polys
+ |-> fold2 (instantiate full) polys
end
-fun monomorph irules ctxt =
+fun monomorph full irules ctxt =
irules
|> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
|>> incr_indexes (* avoid clashes of schematic type variables *)
- |-> (fn [] => rpair ctxt | polys => mono_all ctxt polys)
+ |-> (fn [] => rpair ctxt | polys => mono_all full ctxt polys)
end
--- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 31 17:15:13 2011 +0200
@@ -631,7 +631,7 @@
|> gen_normalize ctxt
|> unfold1 ctxt
|> rpair ctxt
- |-> SMT_Monomorph.monomorph
+ |-> SMT_Monomorph.monomorph true
|-> unfold2
|-> apply_extra_norms
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Mar 31 17:15:13 2011 +0200
@@ -88,6 +88,8 @@
#> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
#> fst
+val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
+
fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
if String.isSubstring set_ClauseFormulaRelationN output then
let
@@ -100,7 +102,8 @@
|> map (fn s => find_index (curry (op =) s) seq + 1)
fun names_for_number j =
j |> AList.lookup (op =) name_map |> these
- |> map_filter (try (unprefix fact_prefix)) |> map unascii_of
+ |> map_filter (try (unascii_of o unprefix_fact_number
+ o unprefix fact_prefix))
|> map (fn name =>
(name, name |> find_first_in_list_vector fact_names |> the)
handle Option.Option =>
@@ -145,16 +148,19 @@
"\nTo minimize the number of lemmas, try this: " ^
Markup.markup Markup.sendback command ^ "."
-val vampire_fact_prefix = "f" (* grrr... *)
+val vampire_step_prefix = "f" (* grrr... *)
fun resolve_fact fact_names ((_, SOME s)) =
- (case strip_prefix_and_unascii fact_prefix s of
- SOME s' => (case find_first_in_list_vector fact_names s' of
- SOME x => [(s', x)]
- | NONE => [])
+ (case try (unprefix fact_prefix) s of
+ SOME s' =>
+ let val s' = s' |> unprefix_fact_number |> unascii_of in
+ case find_first_in_list_vector fact_names s' of
+ SOME x => [(s', x)]
+ | NONE => []
+ end
| NONE => [])
| resolve_fact fact_names (num, NONE) =
- case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of
+ case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
SOME j =>
if j > 0 andalso j <= Vector.length fact_names then
Vector.sub (fact_names, j - 1)
@@ -233,7 +239,7 @@
val raw_prefix = "X"
val assum_prefix = "A"
-val fact_prefix = "F"
+val have_prefix = "F"
fun resolve_conjecture conjecture_shape (num, s_opt) =
let
@@ -847,7 +853,7 @@
(l, subst, next_fact)
else
let
- val l' = (prefix_for_depth depth fact_prefix, next_fact)
+ val l' = (prefix_for_depth depth have_prefix, next_fact)
in (l', (l, l') :: subst, next_fact + 1) end
val relabel_facts =
apfst (maps (the_list o AList.lookup (op =) subst))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Mar 31 17:15:13 2011 +0200
@@ -442,9 +442,13 @@
(atp_type_literals_for_types type_sys ctypes_sorts))
(formula_for_combformula ctxt type_sys combformula)
-fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) =
- Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula,
- NONE)
+(* Each fact is given a unique fact number to avoid name clashes (e.g., because
+ of monomorphization). The TPTP explicitly forbids name clashes, and some of
+ the remote provers might care. *)
+fun problem_line_for_fact ctxt prefix type_sys
+ (j, formula as {name, kind, ...}) =
+ Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
+ formula_for_fact ctxt type_sys formula, NONE)
fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
superclass, ...}) =
@@ -626,7 +630,8 @@
(* Reordering these might or might not confuse the proof reconstruction
code or the SPASS Flotter hack. *)
val problem =
- [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) facts),
+ [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
+ (0 upto length facts - 1 ~~ facts)),
(class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map problem_line_for_arity_clause arity_clauses),
(helpersN, []),
@@ -638,7 +643,8 @@
val helper_lines =
get_helper_facts ctxt explicit_forall type_sys
(maps (map (#3 o dest_Fof) o snd) problem)
- |>> map (problem_line_for_fact ctxt helper_prefix type_sys
+ |>> map (pair 0
+ #> problem_line_for_fact ctxt helper_prefix type_sys
#> repair_problem_line thy explicit_forall type_sys const_tab)
|> op @
val (problem, pool) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 31 17:15:13 2011 +0200
@@ -79,10 +79,12 @@
("verbose", "false"),
("overlord", "false"),
("blocking", "false"),
+ ("relevance_thresholds", "0.45 0.85"),
+ ("max_relevant", "smart"),
+ ("monomorphize", "false"),
+ ("monomorphize_limit", "4"),
("type_sys", "smart"),
("explicit_apply", "false"),
- ("relevance_thresholds", "0.45 0.85"),
- ("max_relevant", "smart"),
("isar_proof", "false"),
("isar_shrink_factor", "1")]
@@ -95,6 +97,7 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("non_blocking", "blocking"),
+ ("dont_monomorphize", "monomorphize"),
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
("no_isar_proof", "isar_proof")]
@@ -233,6 +236,10 @@
val blocking = auto orelse debug orelse lookup_bool "blocking"
val provers = lookup_string "provers" |> space_explode " "
|> auto ? single o hd
+ val relevance_thresholds = lookup_real_pair "relevance_thresholds"
+ val max_relevant = lookup_int_option "max_relevant"
+ val monomorphize = lookup_bool "monomorphize"
+ val monomorphize_limit = lookup_int "monomorphize_limit"
val type_sys =
case (lookup_string "type_sys", lookup_bool "full_types") of
("tags", full_types) => Tags full_types
@@ -245,18 +252,18 @@
else
error ("Unknown type system: " ^ quote type_sys ^ ".")
val explicit_apply = lookup_bool "explicit_apply"
- val relevance_thresholds = lookup_real_pair "relevance_thresholds"
- val max_relevant = lookup_int_option "max_relevant"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
- provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
- relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout, expect = expect}
+ provers = provers, relevance_thresholds = relevance_thresholds,
+ max_relevant = max_relevant, monomorphize = monomorphize,
+ monomorphize_limit = monomorphize_limit, type_sys = type_sys,
+ explicit_apply = explicit_apply, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, timeout = timeout,
+ expect = expect}
end
fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Mar 31 17:15:13 2011 +0200
@@ -42,8 +42,8 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
-fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof,
- isar_shrink_factor, ...} : params)
+fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit,
+ type_sys, isar_proof, isar_shrink_factor, ...} : params)
explicit_apply_opt silent (prover : prover) timeout i n state facts =
let
val thy = Proof.theory_of state
@@ -65,6 +65,7 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
+ monomorphize = false, monomorphize_limit = monomorphize_limit,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
timeout = timeout, expect = ""}
val facts =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 31 17:15:13 2011 +0200
@@ -21,10 +21,12 @@
overlord: bool,
blocking: bool,
provers: string list,
+ relevance_thresholds: real * real,
+ max_relevant: int option,
+ monomorphize: bool,
+ monomorphize_limit: int,
type_sys: type_system,
explicit_apply: bool,
- relevance_thresholds: real * real,
- max_relevant: int option,
isar_proof: bool,
isar_shrink_factor: int,
timeout: Time.time,
@@ -66,7 +68,6 @@
val smt_iter_fact_frac : real Unsynchronized.ref
val smt_iter_time_frac : real Unsynchronized.ref
val smt_iter_min_msecs : int Unsynchronized.ref
- val smt_monomorphize_limit : int Unsynchronized.ref
val das_Tool : string
val select_smt_solver : string -> Proof.context -> Proof.context
@@ -229,10 +230,12 @@
overlord: bool,
blocking: bool,
provers: string list,
+ relevance_thresholds: real * real,
+ max_relevant: int option,
+ monomorphize: bool,
+ monomorphize_limit: int,
type_sys: type_system,
explicit_apply: bool,
- relevance_thresholds: real * real,
- max_relevant: int option,
isar_proof: bool,
isar_shrink_factor: int,
timeout: Time.time,
@@ -333,13 +336,40 @@
({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
: atp_config)
- ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof,
- isar_shrink_factor, timeout, ...} : params)
+ ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys,
+ explicit_apply, isar_proof, isar_shrink_factor, timeout, ...}
+ : params)
minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
let
+ val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
- val facts = facts |> map (atp_translated_fact ctxt)
+ fun monomorphize_facts facts =
+ let
+ val facts = facts |> map untranslated_fact
+ (* pseudo-theorem involving the same constants as the subgoal *)
+ val subgoal_th =
+ Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
+ val indexed_facts =
+ (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
+ val (mono_facts, ctxt') =
+ ctxt |> Config.put SMT_Config.verbose debug
+ |> Config.put SMT_Config.monomorph_limit monomorphize_limit
+ |> SMT_Monomorph.monomorph true indexed_facts
+ in
+ mono_facts
+ |> sort (int_ord o pairself fst)
+ |> filter_out (curry (op =) ~1 o fst)
+ (* The next step shouldn't be necessary but currently the monomorphizer
+ generates unexpected instances with fresh TFrees, which typically
+ become TVars once exported. *)
+ |> filter_out (Term.exists_type SMT_Monomorph.typ_has_tvars
+ o singleton (Variable.export_terms ctxt' ctxt)
+ o prop_of o snd)
+ |> map (Untranslated_Fact o apfst (fst o nth facts))
+ end
+ val facts = facts |> monomorphize ? monomorphize_facts
+ |> map (atp_translated_fact ctxt)
val (dest_dir, problem_prefix) =
if overlord then overlord_file_location_for_prover name
else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
@@ -513,9 +543,9 @@
val smt_iter_fact_frac = Unsynchronized.ref 0.5
val smt_iter_time_frac = Unsynchronized.ref 0.5
val smt_iter_min_msecs = Unsynchronized.ref 5000
-val smt_monomorphize_limit = Unsynchronized.ref 4
-fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params)
+fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,
+ timeout, ...} : params)
state i smt_filter =
let
val ctxt = Proof.context_of state
@@ -529,7 +559,7 @@
else
I)
#> Config.put SMT_Config.infer_triggers (!smt_triggers)
- #> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit)
+ #> Config.put SMT_Config.monomorph_limit monomorphize_limit
val state = state |> Proof.map_context repair_context
fun iter timeout iter_num outcome0 time_so_far facts =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Mar 31 17:15:13 2011 +0200
@@ -164,9 +164,9 @@
(* FUDGE *)
val auto_max_relevant_divisor = 2
-fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
- relevance_thresholds, max_relevant, timeout,
- ...})
+fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
+ type_sys, relevance_thresholds, max_relevant,
+ timeout, ...})
auto i (relevance_override as {only, ...}) minimize_command
state =
if null provers then
@@ -246,7 +246,10 @@
else
launch_provers state
(get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
- (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
+ (if monomorphize then
+ K (Untranslated_Fact o fst)
+ else
+ ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
(K (K NONE)) atps
fun launch_smts accum =
if null smts then
--- a/src/HOL/Tools/try.ML Thu Mar 31 11:17:52 2011 +0200
+++ b/src/HOL/Tools/try.ML Thu Mar 31 17:15:13 2011 +0200
@@ -8,8 +8,8 @@
sig
val auto : bool Unsynchronized.ref
val invoke_try :
- Time.time option -> string list * string list * string list -> Proof.state
- -> bool
+ Time.time option -> string list * string list * string list * string list
+ -> Proof.state -> bool
val setup : theory -> theory
end;
@@ -61,13 +61,13 @@
| add_attr_text (_, []) s = s
| add_attr_text (SOME x, fs) s =
s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
-fun attrs_text (sx, ix, ex) (ss, is, es) =
- "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es)]
+fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
+ "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
- triple st =
+ quad st =
if not auto orelse run_if_auto then
- let val attrs = attrs_text attrs triple in
+ let val attrs = attrs_text attrs quad in
do_generic timeout_opt
(name ^ (if all_goals andalso
nprems_of (#goal (Proof.goal st)) > 1 then
@@ -81,13 +81,13 @@
else
NONE
-val full_attrs = (SOME "simp", SOME "intro", SOME "elim")
-val clas_attrs = (NONE, SOME "intro", SOME "elim")
-val simp_attrs = (SOME "add", NONE, NONE)
-val metis_attrs = (SOME "", SOME "", SOME "")
-val no_attrs = (NONE, NONE, NONE)
+val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
+val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
+val simp_attrs = (SOME "add", NONE, NONE, NONE)
+val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
+val no_attrs = (NONE, NONE, NONE, NONE)
-(* name * ((all_goals, run_if_auto), (simp, intro, elim) *)
+(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
val named_methods =
[("simp", ((false, true), simp_attrs)),
("auto", ((true, true), full_attrs)),
@@ -102,11 +102,11 @@
fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
-fun do_try auto timeout_opt triple st =
+fun do_try auto timeout_opt quad st =
let
val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
in
- case do_methods |> Par_List.map (fn f => f auto timeout_opt triple st)
+ case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
|> map_filter I |> sort (int_ord o pairself snd) of
[] => (if auto then () else writeln "No proof found."; (false, st))
| xs as (s, _) :: _ =>
@@ -137,11 +137,12 @@
val tryN = "try"
-fun try_trans triple =
- Toplevel.keep (K () o do_try false (SOME default_timeout) triple
+fun try_trans quad =
+ Toplevel.keep (K () o do_try false (SOME default_timeout) quad
o Toplevel.proof_of)
-fun merge_attrs (s1, i1, e1) (s2, i2, e2) = (s1 @ s2, i1 @ i2, e1 @ e2)
+fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
+ (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
fun string_of_xthm (xref, args) =
Facts.string_of_ref xref ^
@@ -153,23 +154,25 @@
(Parse_Spec.xthm >> string_of_xthm))
val parse_attr =
Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
- >> (fn ss => (ss, [], []))
+ >> (fn ss => (ss, [], [], []))
|| Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
- >> (fn is => ([], is, []))
+ >> (fn is => ([], is, [], []))
|| Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
- >> (fn es => ([], [], es))
+ >> (fn es => ([], [], es, []))
+ || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
+ >> (fn ds => ([], [], [], ds))
fun parse_attrs x =
(Args.parens parse_attrs
|| Scan.repeat parse_attr
- >> (fn triple => fold merge_attrs triple ([], [], []))) x
+ >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
-val parse_try_command = Scan.optional parse_attrs ([], [], []) #>> try_trans
+val parse_try_command = Scan.optional parse_attrs ([], [], [], []) #>> try_trans
val _ =
Outer_Syntax.improper_command tryN
"try a combination of proof methods" Keyword.diag parse_try_command
-val auto_try = do_try true NONE ([], [], [])
+val auto_try = do_try true NONE ([], [], [], [])
val setup = Auto_Tools.register_tool (auto, auto_try)