--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 10:01:00 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 10:01:03 2011 +0200
@@ -25,17 +25,31 @@
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list
- (* official TPTP syntax *)
+ val tptp_cnf : string
+ val tptp_fof : string
+ val tptp_tff : string
+ val tptp_thf : string
val tptp_special_prefix : string
val tptp_has_type : string
val tptp_type_of_types : string
val tptp_bool_type : string
val tptp_individual_type : string
val tptp_fun_type : string
+ val tptp_prod_type : string
+ val tptp_forall : string
+ val tptp_exists : string
+ val tptp_not : string
+ val tptp_and : string
+ val tptp_or : string
+ val tptp_implies : string
+ val tptp_if : string
+ val tptp_iff : string
+ val tptp_not_iff : string
+ val tptp_app : string
+ val tptp_not_infix : string
+ val tptp_equal : string
val tptp_false : string
val tptp_true : string
- val tptp_not : string
- val tptp_app : string
val is_atp_variable : string -> bool
val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val mk_aconn :
@@ -78,16 +92,31 @@
type 'a problem = (string * 'a problem_line list) list
(* official TPTP syntax *)
+val tptp_cnf = "cnf"
+val tptp_fof = "fof"
+val tptp_tff = "tff"
+val tptp_thf = "thf"
val tptp_special_prefix = "$"
val tptp_has_type = ":"
val tptp_type_of_types = "$tType"
val tptp_bool_type = "$o"
val tptp_individual_type = "$i"
val tptp_fun_type = ">"
+val tptp_prod_type = "*"
+val tptp_forall = "!"
+val tptp_exists = "?"
+val tptp_not = "~"
+val tptp_and = "&"
+val tptp_or = "|"
+val tptp_implies = "=>"
+val tptp_if = "<="
+val tptp_iff = "<=>"
+val tptp_not_iff = "<~>"
+val tptp_app = "@"
+val tptp_not_infix = "!"
+val tptp_equal = "="
val tptp_false = "$false"
val tptp_true = "$true"
-val tptp_not = "~"
-val tptp_app = "@"
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
@@ -130,36 +159,39 @@
(case strip_tff_type ty of
([], s) => s
| ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
- | (ss, s) => "(" ^ space_implode " * " ss ^ ") " ^ tptp_fun_type ^ " " ^ s)
+ | (ss, s) =>
+ "(" ^ space_implode tptp_prod_type ss ^ ") " ^ tptp_fun_type ^ " " ^ s)
| string_for_type _ _ = raise Fail "unexpected type in untyped format"
fun string_for_term _ (ATerm (s, [])) = s
| string_for_term format (ATerm ("equal", ts)) =
- space_implode " = " (map (string_for_term format) ts)
+ space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
|> format = THF ? enclose "(" ")"
| string_for_term format (ATerm ("[]", ts)) =
(* used for lists in the optional "source" field of a derivation *)
"[" ^ commas (map (string_for_term format) ts) ^ "]"
| string_for_term format (ATerm (s, ts)) =
let val ss = map (string_for_term format) ts in
- if format = THF then "(" ^ space_implode " @ " (s :: ss) ^ ")"
- else s ^ "(" ^ commas ss ^ ")"
+ if format = THF then
+ "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
+ else
+ s ^ "(" ^ commas ss ^ ")"
end
-fun string_for_quantifier AForall = "!"
- | string_for_quantifier AExists = "?"
+fun string_for_quantifier AForall = tptp_forall
+ | string_for_quantifier AExists = tptp_exists
fun string_for_connective ANot = tptp_not
- | string_for_connective AAnd = "&"
- | string_for_connective AOr = "|"
- | string_for_connective AImplies = "=>"
- | string_for_connective AIf = "<="
- | string_for_connective AIff = "<=>"
- | string_for_connective ANotIff = "<~>"
+ | string_for_connective AAnd = tptp_and
+ | string_for_connective AOr = tptp_or
+ | string_for_connective AImplies = tptp_implies
+ | string_for_connective AIf = tptp_if
+ | string_for_connective AIff = tptp_iff
+ | string_for_connective ANotIff = tptp_not_iff
fun string_for_bound_var format (s, ty) =
s ^ (if format = TFF orelse format = THF then
- " : " ^
+ " " ^ tptp_has_type ^ " " ^
string_for_type format (ty |> the_default (AType tptp_individual_type))
else
"")
@@ -169,7 +201,8 @@
"[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
string_for_formula format phi ^ ")"
| string_for_formula format (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
- space_implode " != " (map (string_for_term format) ts)
+ space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
+ (map (string_for_term format) ts)
|> format = THF ? enclose "(" ")"
| string_for_formula format (AConn (c, [phi])) =
"(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")"
@@ -181,10 +214,10 @@
val default_source =
ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
-fun string_for_format CNF_UEQ = "cnf"
- | string_for_format FOF = "fof"
- | string_for_format TFF = "tff"
- | string_for_format THF = "thf"
+fun string_for_format CNF_UEQ = tptp_cnf
+ | string_for_format FOF = tptp_fof
+ | string_for_format TFF = tptp_tff
+ | string_for_format THF = tptp_thf
fun string_for_problem_line format (Decl (ident, sym, ty)) =
string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 10:01:00 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 10:01:03 2011 +0200
@@ -53,11 +53,12 @@
val extract_tstplike_proof_and_outcome :
bool -> bool -> int -> (string * string) list -> (failure * string) list
-> string -> string * failure option
- val is_same_step : step_name * step_name -> bool
+ val is_same_atp_step : step_name -> step_name -> bool
val scan_general_id : string list -> string * string list
val parse_formula :
string list -> (string, 'a, string fo_term) formula * string list
val atp_proof_from_tstplike_proof : string problem -> string -> string proof
+ val clean_up_atp_proof_dependencies : string proof -> string proof
val map_term_names_in_atp_proof :
(string -> string) -> string proof -> string proof
val nasty_atp_proof : string Symtab.table -> string proof -> string proof
@@ -142,10 +143,8 @@
fun involving [] = ""
| involving ss = "involving " ^ commas_quote ss ^ " "
-fun string_for_failure Unprovable =
- "The problem is unprovable."
- | string_for_failure IncompleteUnprovable =
- "The prover gave up."
+fun string_for_failure Unprovable = "The problem is unprovable."
+ | string_for_failure IncompleteUnprovable = "The prover gave up."
| string_for_failure ProofMissing =
"The prover claims the conjecture is a theorem but did not provide a proof."
| string_for_failure ProofIncomplete =
@@ -239,14 +238,17 @@
type step_name = string * string option
-fun is_same_step p = p |> pairself fst |> op =
+fun is_same_atp_step (s1, _) (s2, _) = s1 = s2
+
+val vampire_fact_prefix = "f"
fun step_name_ord p =
let val q = pairself fst p in
(* The "unprefix" part is to cope with remote Vampire's output. The proper
solution would be to perform a topological sort, e.g. using the nice
"Graph" functor. *)
- case pairself (Int.fromString o perhaps (try (unprefix "f"))) q of
+ case pairself (Int.fromString
+ o perhaps (try (unprefix vampire_fact_prefix))) q of
(NONE, NONE) => string_ord q
| (NONE, SOME _) => LESS
| (SOME _, NONE) => GREATER
@@ -282,23 +284,32 @@
>> flat) x
fun list_app (f, args) =
- fold (fn arg => fn f => ATerm (tptp_app_op, [f, arg])) args f
+ fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f
-fun parse_arg x =
- (scan_general_id
- (* We ignore TFF and THF types for now. *)
- --| Scan.repeat (($$ ":" || $$ ">") |-- parse_arg)
- -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
- >> ATerm) x
+(* We ignore TFF and THF types for now. *)
+fun parse_type_stuff x =
+ Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
+and parse_arg x =
+ ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff
+ || scan_general_id --| parse_type_stuff
+ -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
+ >> ATerm) x
and parse_app x =
- (parse_arg -- Scan.repeat ($$ tptp_app_op |-- parse_arg) >> list_app) x
+ (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
and parse_term x =
- (parse_app -- Scan.optional)
+ (parse_app -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal
+ -- parse_app)
+ >> (fn (u1, NONE) => u1
+ | (u1, SOME (NONE, u2)) => ATerm ("equal", [u1, u2])
+ | (u1, SOME (SOME _, u2)) =>
+ ATerm (tptp_not, [ATerm ("equal", [u1, u2])]))) x
and parse_terms x =
(parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
+(* TODO: Avoid duplication with "parse_term" above. *)
fun parse_atom x =
- (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
+ (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal
+ -- parse_term)
>> (fn (u1, NONE) => AAtom u1
| (u1, SOME (NONE, u2)) => AAtom (ATerm ("equal", [u1, u2]))
| (u1, SOME (SOME _, u2)) =>
@@ -309,29 +320,42 @@
(* TPTP formulas are fully parenthesized, so we don't need to worry about
operator precedence. *)
fun parse_literal x =
- ((Scan.repeat ($$ "~") >> length)
+ ((Scan.repeat ($$ tptp_not) >> length)
-- ($$ "(" |-- parse_formula --| $$ ")"
|| parse_quantified_formula
|| parse_atom)
>> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x
and parse_formula x =
(parse_literal
- -- Scan.option ((Scan.this_string "=>" >> K AImplies
- || Scan.this_string "<=>" >> K AIff
- || Scan.this_string "<~>" >> K ANotIff
- || Scan.this_string "<=" >> K AIf
- || $$ "|" >> K AOr
- || $$ "&" >> K AAnd)
+ -- Scan.option ((Scan.this_string tptp_implies >> K AImplies
+ || Scan.this_string tptp_iff >> K AIff
+ || Scan.this_string tptp_not_iff >> K ANotIff
+ || Scan.this_string tptp_if >> K AIf
+ || $$ tptp_or >> K AOr
+ || $$ tptp_and >> K AAnd)
-- parse_formula)
>> (fn (phi1, NONE) => phi1
| (phi1, SOME (c, phi2)) => mk_aconn c phi1 phi2)) x
and parse_quantified_formula x =
- (($$ "!" >> K AForall || $$ "?" >> K AExists)
+ (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists)
--| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
>> (fn ((q, ts), phi) =>
(* We ignore TFF and THF types for now. *)
AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x
+fun skip_formula ss =
+ let
+ fun skip _ [] = []
+ | skip 0 (ss as "," :: _) = ss
+ | skip 0 (ss as ")" :: _) = ss
+ | skip 0 (ss as "]" :: _) = ss
+ | skip n ("(" :: ss) = skip (n + 1) ss
+ | skip n ("[" :: ss) = skip (n + 1) ss
+ | skip n ("]" :: ss) = skip (n - 1) ss
+ | skip n (")" :: ss) = skip (n - 1) ss
+ | skip n (_ :: ss) = skip n ss
+ in (AAtom (ATerm ("", [])), skip 0 ss) end
+
val parse_tstp_extra_arguments =
Scan.optional ($$ "," |-- parse_annotation
--| Scan.option ($$ "," |-- parse_annotations)) []
@@ -384,10 +408,11 @@
<formula> <extra_arguments>\).
The <num> could be an identifier, but we assume integers. *)
fun parse_tstp_line problem =
- ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff"
- || Scan.this_string "thf") -- $$ "(")
+ ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
+ || Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(")
|-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
- -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
+ -- (parse_formula || skip_formula) -- parse_tstp_extra_arguments --| $$ ")"
+ --| $$ "."
>> (fn (((num, role), phi), deps) =>
let
val (name, deps) =
@@ -413,7 +438,7 @@
| AAtom (ATerm ("equal", _)) =>
(* Vampire's equality proxy axiom *)
Inference (name, phi, map (rpair NONE) deps)
- | _ => raise Fail "malformed definition")
+ | _ => raise UNRECOGNIZED_ATP_PROOF ())
| _ => Inference (name, phi, map (rpair NONE) deps)
end)
@@ -462,20 +487,22 @@
(Scan.repeat1 (parse_line problem))))
|> fst
-fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
-fun clean_up_dependencies _ [] = []
- | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) =
- step :: clean_up_dependencies (name :: seen) steps
- | clean_up_dependencies seen (Inference (name, u, deps) :: steps) =
- Inference (name, u, map_filter (clean_up_dependency seen) deps) ::
- clean_up_dependencies (name :: seen) steps
-
fun atp_proof_from_tstplike_proof _ "" = []
| atp_proof_from_tstplike_proof problem s =
s ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
|> sort (step_name_ord o pairself step_name)
- |> clean_up_dependencies []
+
+fun clean_up_dependencies _ [] = []
+ | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) =
+ step :: clean_up_dependencies (name :: seen) steps
+ | clean_up_dependencies seen (Inference (name, u, deps) :: steps) =
+ Inference (name, u,
+ map_filter (fn dep => find_first (is_same_atp_step dep) seen)
+ deps) ::
+ clean_up_dependencies (name :: seen) steps
+
+val clean_up_atp_proof_dependencies = clean_up_dependencies []
fun map_term_names_in_term f (ATerm (s, ts)) =
ATerm (f s, map (map_term_names_in_term f) ts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 24 10:01:00 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 24 10:01:03 2011 +0200
@@ -16,8 +16,7 @@
string * minimize_command * type_system * string proof * int
* (string * locality) list vector * int list * thm * int
type isar_params =
- Proof.context * bool * int * string Symtab.table * int list list
- * int Symtab.table
+ bool * int * string Symtab.table * int list list * int Symtab.table
type text_result = string * (string * locality) list
val repair_conjecture_shape_and_fact_names :
@@ -25,11 +24,11 @@
-> (string * locality) list vector -> int list
-> int list list * int * (string * locality) list vector * int list
val used_facts_in_atp_proof :
- type_system -> int -> (string * locality) list vector -> string proof
- -> (string * locality) list
+ Proof.context -> type_system -> int -> (string * locality) list vector
+ -> string proof -> (string * locality) list
val used_facts_in_unsound_atp_proof :
- type_system -> int list list -> int -> (string * locality) list vector
- -> string proof -> string list option
+ Proof.context -> type_system -> int list list -> int
+ -> (string * locality) list vector -> string proof -> string list option
val apply_on_subgoal : string -> int -> int -> string
val command_call : string -> string list -> string
val try_command_line : string -> string -> string
@@ -37,9 +36,11 @@
val split_used_facts :
(string * locality) list
-> (string * locality) list * (string * locality) list
- val metis_proof_text : metis_params -> text_result
- val isar_proof_text : isar_params -> metis_params -> text_result
- val proof_text : bool -> isar_params -> metis_params -> text_result
+ val metis_proof_text : Proof.context -> metis_params -> text_result
+ val isar_proof_text :
+ Proof.context -> isar_params -> metis_params -> text_result
+ val proof_text :
+ Proof.context -> bool -> isar_params -> metis_params -> text_result
end;
structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT =
@@ -57,8 +58,7 @@
string * minimize_command * type_system * string proof * int
* (string * locality) list vector * int list * thm * int
type isar_params =
- Proof.context * bool * int * string Symtab.table * int list list
- * int Symtab.table
+ bool * int * string Symtab.table * int list list * int Symtab.table
type text_result = string * (string * locality) list
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
@@ -182,23 +182,39 @@
SOME i => member (op =) typed_helpers i
| NONE => false)
-fun add_fact type_sys facts_offset fact_names (Inference (name, _, [])) =
- union (op =) (resolve_fact type_sys facts_offset fact_names name)
- | add_fact _ _ _ _ = I
+val leo2_ext = "extcnf_equal_neg"
+val isa_ext = Thm.get_name_hint @{thm ext}
+val isa_short_ext = Long_Name.base_name isa_ext
+
+fun ext_name ctxt =
+ if Thm.eq_thm_prop (@{thm ext},
+ singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
+ isa_short_ext
+ else
+ isa_ext
-fun used_facts_in_atp_proof type_sys facts_offset fact_names atp_proof =
+fun add_fact _ type_sys facts_offset fact_names (Inference (name, _, [])) =
+ union (op =) (resolve_fact type_sys facts_offset fact_names name)
+ | add_fact ctxt _ _ _ (Inference (_, _, deps)) =
+ if AList.defined (op =) deps leo2_ext then
+ insert (op =) (ext_name ctxt, General (* or Chained... *))
+ else
+ I
+ | add_fact _ _ _ _ _ = I
+
+fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof =
if null atp_proof then Vector.foldl (op @) [] fact_names
- else fold (add_fact type_sys facts_offset fact_names) atp_proof []
+ else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof []
fun is_conjecture_referred_to_in_proof conjecture_shape =
exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
| _ => false)
-fun used_facts_in_unsound_atp_proof type_sys conjecture_shape facts_offset
+fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
fact_names atp_proof =
let
- val used_facts = used_facts_in_atp_proof type_sys facts_offset fact_names
- atp_proof
+ val used_facts =
+ used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
in
if forall (is_locality_global o snd) used_facts andalso
not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then
@@ -244,11 +260,11 @@
exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
| _ => false)
-fun metis_proof_text (banner, minimize_command, type_sys, atp_proof,
- facts_offset, fact_names, typed_helpers, goal, i) =
+fun metis_proof_text ctxt (banner, minimize_command, type_sys, atp_proof,
+ facts_offset, fact_names, typed_helpers, goal, i) =
let
val (chained, extra) =
- atp_proof |> used_facts_in_atp_proof type_sys facts_offset fact_names
+ atp_proof |> used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
|> split_used_facts
val full_types = uses_typed_helpers typed_helpers atp_proof
val n = Logic.count_prems (prop_of goal)
@@ -561,7 +577,7 @@
val is_only_type_information = curry (op aconv) HOLogic.true_const
fun replace_one_dependency (old, new) dep =
- if is_same_step (dep, old) then new else [dep]
+ if is_same_atp_step dep old then new else [dep]
fun replace_dependencies_in_line _ (line as Definition _) = line
| replace_dependencies_in_line p (Inference (name, t, deps)) =
Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
@@ -692,6 +708,7 @@
let
val lines =
atp_proof
+ |> clean_up_atp_proof_dependencies
|> nasty_atp_proof pool
|> map_term_names_in_atp_proof repair_name
|> decode_lines ctxt sym_tab tfrees
@@ -995,17 +1012,17 @@
(if n <> 1 then "next" else "qed")
in do_proof end
-fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape,
- sym_tab)
- (metis_params as (_, _, type_sys, atp_proof, facts_offset,
- fact_names, typed_helpers, goal, i)) =
+fun isar_proof_text ctxt
+ (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
+ (metis_params as (_, _, type_sys, atp_proof, facts_offset, fact_names,
+ typed_helpers, goal, i)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
val full_types = uses_typed_helpers typed_helpers atp_proof
val n = Logic.count_prems (prop_of goal)
- val (one_line_proof, lemma_names) = metis_proof_text metis_params
+ val (one_line_proof, lemma_names) = metis_proof_text ctxt metis_params
fun isar_proof_for () =
case isar_proof_from_atp_proof pool ctxt type_sys tfrees
isar_shrink_factor atp_proof conjecture_shape facts_offset
@@ -1026,8 +1043,7 @@
|> the_default "\nWarning: The Isar proof construction failed."
in (one_line_proof ^ isar_proof, lemma_names) end
-fun proof_text isar_proof isar_params metis_params =
- (if isar_proof then isar_proof_text isar_params else metis_proof_text)
- metis_params
+fun proof_text ctxt isar_proof isar_params =
+ if isar_proof then isar_proof_text ctxt isar_params else metis_proof_text ctxt
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 10:01:00 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 10:01:03 2011 +0200
@@ -622,7 +622,7 @@
val outcome =
case outcome of
NONE =>
- used_facts_in_unsound_atp_proof type_sys
+ used_facts_in_unsound_atp_proof ctxt type_sys
conjecture_shape facts_offset fact_names atp_proof
|> Option.map (fn facts =>
UnsoundProof (is_type_sys_virtually_sound type_sys,
@@ -656,8 +656,8 @@
(result as ((_, _, facts_offset, fact_names, _, _),
(_, _, type_sys, atp_proof,
SOME (UnsoundProof (false, _))))) =
- (case used_facts_in_atp_proof type_sys facts_offset fact_names
- atp_proof of
+ (case used_facts_in_atp_proof ctxt type_sys facts_offset
+ fact_names atp_proof of
[] => result
| new_baddies =>
if slicing andalso iter < atp_blacklist_max_iters - 1 then
@@ -712,18 +712,18 @@
else
"")
val isar_params =
- (ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
+ (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
val metis_params =
(proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset,
fact_names, typed_helpers, goal, subgoal)
val (outcome, (message, used_facts)) =
case outcome of
NONE =>
- (NONE, proof_text isar_proof isar_params metis_params
+ (NONE, proof_text ctxt isar_proof isar_params metis_params
|>> append_to_message)
| SOME failure =>
if failure = ProofMissing orelse failure = ProofIncomplete then
- (NONE, metis_proof_text metis_params |>> append_to_message)
+ (NONE, metis_proof_text ctxt metis_params |>> append_to_message)
else
(outcome, (string_for_failure failure, []))
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 24 10:01:00 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 24 10:01:03 2011 +0200
@@ -44,7 +44,7 @@
val auto_minimize_min_facts =
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
- (fn generic => (* ### Config.get_generic generic binary_min_facts *) 10000 (*###*))
+ (fn generic => Config.get_generic generic binary_min_facts)
fun get_minimizing_prover ctxt auto name
(params as {debug, verbose, explicit_apply, ...}) minimize_command