add support for Isar reconstruction for thf1 ATP provers like Leo-II.
--- a/src/HOL/ATP.thy Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/ATP.thy Mon Jun 16 16:18:15 2014 +0200
@@ -16,7 +16,6 @@
ML_file "Tools/ATP/atp_proof.ML"
ML_file "Tools/ATP/atp_proof_redirect.ML"
-
subsection {* Higher-order reasoning helpers *}
definition fFalse :: bool where
--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 16 16:18:15 2014 +0200
@@ -44,7 +44,7 @@
datatype atp_formula_role =
Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture |
- Plain | Unknown
+ Plain | Type_Role | Unknown
datatype 'a atp_problem_line =
Class_Decl of string * 'a * 'a list |
@@ -75,9 +75,12 @@
val tptp_exists : string
val tptp_ho_exists : string
val tptp_choice : string
+ val tptp_ho_choice : string
val tptp_not : string
val tptp_and : string
+ val tptp_not_and : string
val tptp_or : string
+ val tptp_not_or : string
val tptp_implies : string
val tptp_if : string
val tptp_iff : string
@@ -85,10 +88,13 @@
val tptp_app : string
val tptp_not_infix : string
val tptp_equal : string
+ val tptp_not_equal : string
val tptp_old_equal : string
val tptp_false : string
val tptp_true : string
+ val tptp_lambda : string
val tptp_empty_list : string
+ val tptp_binary_op_list : string list
val isabelle_info_prefix : string
val isabelle_info : string -> int -> (string, 'a) atp_term list
val extract_isabelle_status : (string, 'a) atp_term list -> string option
@@ -114,6 +120,9 @@
val mk_aconn :
atp_connective -> ('a, 'b, 'c, 'd) atp_formula
-> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula
+ val mk_app : (string, 'a) atp_term -> (string, 'a) atp_term -> (string, 'a) atp_term
+ val mk_apps : (string, 'a) atp_term -> (string, 'a) atp_term list -> (string, 'a) atp_term
+ val mk_simple_aterm: 'a -> ('a, 'b) atp_term
val aconn_fold :
bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list
-> 'b -> 'b
@@ -189,7 +198,7 @@
datatype atp_formula_role =
Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture |
- Plain | Unknown
+ Plain | Type_Role | Unknown
datatype 'a atp_problem_line =
Class_Decl of string * 'a * 'a list |
@@ -221,9 +230,12 @@
val tptp_exists = "?"
val tptp_ho_exists = "??"
val tptp_choice = "@+"
+val tptp_ho_choice = "@@+"
val tptp_not = "~"
val tptp_and = "&"
+val tptp_not_and = "~&"
val tptp_or = "|"
+val tptp_not_or = "~|"
val tptp_implies = "=>"
val tptp_if = "<="
val tptp_iff = "<=>"
@@ -231,11 +243,14 @@
val tptp_app = "@"
val tptp_not_infix = "!"
val tptp_equal = "="
+val tptp_not_equal = "!="
val tptp_old_equal = "equal"
val tptp_false = "$false"
val tptp_true = "$true"
+val tptp_lambda = "^"
val tptp_empty_list = "[]"
-
+val tptp_binary_op_list = [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if,
+ tptp_iff, tptp_not_iff, tptp_equal, tptp_app]
val isabelle_info_prefix = "isabelle_"
val inductionN = "induction"
@@ -291,6 +306,11 @@
| mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun mk_app t u = ATerm ((tptp_app, []), [t, u])
+fun mk_apps f xs = fold (fn x => fn f => mk_app f x) xs f
+
+fun mk_simple_aterm p = ATerm ((p, []), [])
+
fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
| aconn_fold pos f (AImplies, [phi1, phi2]) =
f (Option.map not pos) phi1 #> f pos phi2
@@ -345,6 +365,7 @@
| tptp_string_of_role Conjecture = "conjecture"
| tptp_string_of_role Negated_Conjecture = "negated_conjecture"
| tptp_string_of_role Plain = "plain"
+ | tptp_string_of_role Type_Role = "type"
| tptp_string_of_role Unknown = "unknown"
fun tptp_string_of_app _ func [] = func
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 16 16:18:15 2014 +0200
@@ -289,6 +289,8 @@
val dummy_phi = AAtom (ATerm (("", []), []))
val dummy_inference = Inference_Source ("", [])
+val dummy_aterm = ATerm (("", []), [])
+val dummy_atype = AType(("", []), [])
(* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
fun parse_dependency x =
@@ -433,8 +435,88 @@
| role_of_tptp_string "conjecture" = Conjecture
| role_of_tptp_string "negated_conjecture" = Negated_Conjecture
| role_of_tptp_string "plain" = Plain
+ | role_of_tptp_string "type" = Type_Role
| role_of_tptp_string _ = Unknown
+fun parse_binary_op x =
+ foldl1 (op||) (map Scan.this_string tptp_binary_op_list) x
+
+fun parse_thf0_type x =
+ ($$ "(" |-- parse_thf0_type --| $$ ")"
+ || parse_type --| $$ tptp_fun_type -- parse_thf0_type >> AFun
+ || parse_type) x
+
+fun mk_ho_of_fo_quant q =
+ if q = tptp_forall then tptp_ho_forall
+ else if q = tptp_exists then tptp_ho_exists
+ else raise Fail ("unrecognized quantification: " ^ q)
+
+fun remove_thf_app (ATerm ((x, ty), arg)) =
+ if x = tptp_app then
+ (case arg of
+ ATerm ((x, ty), arg) :: t => remove_thf_app (ATerm ((x, ty), map remove_thf_app arg @ t))
+ | [AAbs ((var, tvar), phi), t] =>
+ remove_thf_app (AAbs ((var, tvar), map remove_thf_app phi @ [t])))
+ else ATerm ((x, ty), map remove_thf_app arg)
+ | remove_thf_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_thf_app arg), t)
+
+fun parse_thf0_typed_var x =
+ (Scan.repeat (scan_general_id -- Scan.option ($$ ":" |-- parse_thf0_type)
+ --| Scan.option (Scan.this_string ","))
+ || $$ "(" |-- parse_thf0_typed_var --| $$ ")") x
+
+fun parse_literal_hol x =
+ ((Scan.repeat ($$ tptp_not) >> length)
+ -- ($$ "(" |-- parse_formula_hol_raw --| $$ ")"
+ || scan_general_id >> mk_simple_aterm
+ || scan_general_id --| $$ ":" --| scan_general_id >> mk_simple_aterm
+ || (Scan.this_string tptp_ho_forall || Scan.this_string tptp_ho_exists) >> mk_simple_aterm)
+ >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_app (mk_simple_aterm tptp_not))) x
+
+and parse_formula_hol_raw x =
+ (((parse_literal_hol
+ -- parse_binary_op
+ -- parse_formula_hol_raw)
+ >> (fn ((phi1, c) , phi2) =>
+ if c = tptp_app then mk_app phi1 phi2
+ else mk_apps (mk_simple_aterm c) [phi1, phi2]))
+ || (Scan.this_string tptp_forall || Scan.this_string tptp_exists || Scan.this_string tptp_lambda)
+ -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_formula_hol_raw
+ >> (fn ((q, t), phi) =>
+ if q <> tptp_lambda then
+ fold_rev
+ (fn (var, ty) => fn r =>
+ mk_app (q |> mk_ho_of_fo_quant |> mk_simple_aterm)
+ (AAbs (((var, the_default dummy_atype ty), r), [])))
+ t phi
+ else
+ fold_rev (fn (var, ty) => fn r => AAbs (((var, the_default dummy_atype ty), r), []))
+ t phi)
+ || Scan.this_string tptp_not |-- parse_formula_hol_raw >> (mk_app (mk_simple_aterm tptp_not))
+ || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
+ || parse_literal_hol
+ || scan_general_id >> mk_simple_aterm) x
+
+fun parse_formula_hol x = (parse_formula_hol_raw #>> remove_thf_app #>> AAtom) x
+
+fun parse_tstp_line_hol problem =
+ ((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_ascii_id --| $$ ","
+ -- parse_formula_hol -- parse_tstp_extra_arguments--| $$ ")" --| $$ "."
+ >> (fn (((num, role), phi), deps) =>
+ let
+ val ((name, phi), rule, deps) =
+ (case deps of
+ File_Source (_, SOME s) =>
+ (((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]), phi), "", [])
+ | File_Source _ =>
+ (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
+ | Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
+ in
+ [(name, role_of_tptp_string role, phi, rule, map (rpair []) deps)]
+ end)
+
(* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
The <num> could be an identifier, but we assume integers. *)
fun parse_tstp_line problem =
@@ -469,7 +551,7 @@
[(case role_of_tptp_string role of
Definition =>
(case phi of
- AAtom (ATerm (("equal", _), _)) =>
+ AAtom (ATerm (("equal", _), _)) =>
(* Vampire's equality proxy axiom *)
(name, Definition, phi, rule, map (rpair []) deps)
| _ => mk_step ())
@@ -554,10 +636,11 @@
>> map (core_inference z3_tptp_core_rule)) x
fun parse_line name problem =
- if name = z3_tptpN then parse_z3_tptp_core_line
- else if name = spass_pirateN then parse_spass_pirate_line
- else if name = spassN then parse_spass_line
+ if name = leo2N then parse_tstp_line_hol problem
else if name = satallaxN then parse_satallax_core_line
+ else if name = spassN then parse_spass_line
+ else if name = spass_pirateN then parse_spass_pirate_line
+ else if name = z3_tptpN then parse_z3_tptp_core_line
else parse_tstp_line problem
fun parse_proof name problem =
@@ -573,7 +656,7 @@
_ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
| _ => NONE)
-fun atp_proof_of_tstplike_proof prover _ "" = []
+fun atp_proof_of_tstplike_proof prover _ "" = []
| atp_proof_of_tstplike_proof prover problem tstp =
(case core_of_agsyhol_proof tstp of
SOME facts => facts |> map (core_inference agsyhol_core_rule)
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 16:18:15 2014 +0200
@@ -32,9 +32,10 @@
val exists_of : term -> term -> term
val type_enc_aliases : (string * string list) list
val unalias_type_enc : string -> string list
- val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
- (string, string atp_type) atp_term -> term
- val prop_of_atp : Proof.context -> bool -> int Symtab.table ->
+ val term_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc ->
+ bool -> int Symtab.table -> typ option -> (string, string atp_type) atp_term -> term
+ val prop_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc ->
+ bool -> int Symtab.table ->
(string, string, (string, string atp_type) atp_term, string) atp_formula -> term
val used_facts_in_atp_proof :
@@ -45,7 +46,8 @@
val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
('a, 'b) atp_step
- val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list ->
+ val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format ->
+ ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
int Symtab.table -> string atp_proof -> (term, string) atp_step list
val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
val factify_atp_proof : (string * 'a) list vector -> term list -> term ->
@@ -140,7 +142,7 @@
| _ => raise ATP_TERM [u])
(* Accumulate type constraints in a formula: negative type literals. *)
-fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
+fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)
| add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ _ = I
@@ -184,9 +186,144 @@
val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
val vampire_skolem_prefix = "sK"
+
+(* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
+ are typed. *)
+fun term_of_atp_ho ctxt textual sym_tab =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ fun norm_var_types var T' t =
+ let
+ fun norm_term (ATerm ((x, ty), l)) =
+ ATerm((x, if x = var then [T'] else ty), List.map norm_term l)
+ | norm_term (AAbs(((x, ty), term), l)) = AAbs(((x, ty), term), List.map norm_term l)
+ in
+ norm_term t
+ end
+ fun mk_op_of_tptp_operator s =
+ if s = tptp_or then HOLogic.mk_disj
+ else if s = tptp_and then HOLogic.mk_conj
+ else if s = tptp_implies then HOLogic.mk_imp
+ else if s = tptp_iff orelse s = tptp_equal then HOLogic.mk_eq
+ else if s = tptp_not_iff orelse s = tptp_not_equal then HOLogic.mk_eq #> HOLogic.mk_not
+ else if s = tptp_if then HOLogic.mk_imp #> HOLogic.mk_not
+ else if s = tptp_not_and then HOLogic.mk_conj #> HOLogic.mk_not
+ else if s = tptp_not_or then HOLogic.mk_disj #> HOLogic.mk_not
+ else raise Fail ("unknown operator: " ^ s)
+ fun mk_quant_of_tptp_quant s =
+ if s = tptp_ho_exists then HOLogic.mk_exists
+ else if s = tptp_ho_forall then HOLogic.mk_all
+ else raise Fail ("unknown quantifier: " ^ s)
+ val var_index = if textual then 0 else 1
+
+ fun do_term opt_T u =
+ (case u of
+ AAbs(((var, ty), term), []) =>
+ let val typ = typ_of_atp_type ctxt ty in
+ absfree (repair_var_name textual var, typ) (do_term NONE (norm_var_types var ty term))
+ end
+ | ATerm ((s, tys), us) =>
+ if s = ""
+ then error "Isar proof reconstruction failed because the ATP proof \
+ \contains unparsable material."
+ else if String.isPrefix native_type_prefix s then
+ @{const True} (* ignore TPTP type information *)
+ else if s = tptp_equal then
+ let val ts = map (do_term NONE) us in
+ if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
+ @{const True}
+ else
+ list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
+ end
+ else if s = tptp_app then
+ let val ts = map (do_term NONE) us in
+ hd ts $ List.last ts
+ end
+ else if s = tptp_not then
+ let val ts = map (do_term NONE) us in
+ List.last ts |> HOLogic.mk_not
+ end
+ else if s = tptp_ho_forall orelse s = tptp_ho_exists then
+ (case us of
+ [AAbs (((var, ty), term), [])] =>
+ let val typ = typ_of_atp_type ctxt ty in
+ (repair_var_name textual var, typ , do_term NONE (norm_var_types var ty term))
+ |> mk_quant_of_tptp_quant s
+ end
+ | [] => if s = tptp_ho_exists then HOLogic.exists_const dummyT
+ else HOLogic.all_const dummyT)
+ else if List.exists (curry (op=) s) tptp_binary_op_list then
+ let val ts = map (do_term NONE) us in
+ (mk_op_of_tptp_operator s) (hd ts, List.last ts)
+ end
+ else
+ if us <> [] then
+ let
+ val applicant_list = List.map (do_term NONE) us
+ val opt_typ = SOME (fold_rev
+ (fn t1 => fn t2 => slack_fastype_of t1 --> t2)
+ applicant_list (the_default dummyT opt_T))
+ val func_name = do_term opt_typ (ATerm ((s, tys), []))
+ in
+ foldl1 (op$) (func_name :: applicant_list) end
+ else (*FIXME: clean (remove stuff related to vampire and other provers)*)
+ (case unprefix_and_unascii const_prefix s of
+ SOME s' =>
+ let
+ val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const
+ val new_skolem = String.isPrefix new_skolem_const_prefix s''
+ val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s)
+ val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
+ val term_ts = map (do_term NONE) term_us
+ val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us
+ val T =
+ (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then
+ if new_skolem then
+ SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
+ else if textual then
+ try (Sign.const_instance thy) (s', Ts)
+ else
+ NONE
+ else
+ NONE)
+ |> (fn SOME T => T
+ | NONE =>
+ map slack_fastype_of term_ts --->
+ the_default (Type_Infer.anyT @{sort type}) opt_T)
+ val t =
+ if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
+ else Const (unproxify_const s', T)
+ in list_comb (t, term_ts) end
+ | NONE => (* a free or schematic variable *)
+ let
+ (* This assumes that distinct names are mapped to distinct names by
+ "Variable.variant_frees". This does not hold in general but should hold for
+ ATP-generated Skolem function names, since these end with a digit and
+ "variant_frees" appends letters. *)
+ fun fresh_up s =
+ [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
+ val ts = map (do_term NONE) us
+ val T =
+ (case opt_T of
+ SOME T => map slack_fastype_of ts ---> T
+ | NONE =>
+ map slack_fastype_of ts --->
+ (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT
+ @{sort type}))
+ val t =
+ (case unprefix_and_unascii fixed_var_prefix s of
+ SOME s => Free (s, T)
+ | NONE =>
+ if textual andalso not (is_tptp_variable s) then
+ Free (s |> textual ? (repair_var_name_raw #> fresh_up), T)
+ else
+ Var ((repair_var_name textual s, var_index), T))
+ in list_comb (t, ts) end))
+ in do_term end
+
(* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
should allow them to be inferred. *)
-fun term_of_atp ctxt textual sym_tab =
+fun term_of_atp_fo ctxt textual sym_tab =
let
val thy = Proof_Context.theory_of ctxt
(* For Metis, we use 1 rather than 0 because variable references in clauses may otherwise
@@ -249,7 +386,9 @@
val t =
if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
else Const (unproxify_const s', T)
- in list_comb (t, term_ts @ extra_ts) end
+ in
+ list_comb (t, term_ts @ extra_ts)
+ end
end
| NONE => (* a free or schematic variable *)
let
@@ -283,12 +422,21 @@
in list_comb (t, ts) end))
in do_term [] end
-fun term_of_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
+fun term_of_atp ctxt (ATP_Problem.THF _) type_enc =
+ if ATP_Problem_Generate.is_type_enc_higher_order type_enc
+ then term_of_atp_ho ctxt
+ else error "Unsupported Isar reconstruction."
+ | term_of_atp ctxt _ type_enc =
+ if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc)
+ then term_of_atp_fo ctxt
+ else error "Unsupported Isar reconstruction."
+
+fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) =
if String.isPrefix class_prefix s then
add_type_constraint pos (type_constraint_of_term ctxt u)
#> pair @{const True}
else
- pair (term_of_atp ctxt textual sym_tab (SOME @{typ bool}) u)
+ pair (term_of_atp ctxt format type_enc textual sym_tab (SOME @{typ bool}) u)
(* Update schematic type variables with detected sort constraints. It's not
totally clear whether this code is necessary. *)
@@ -317,7 +465,7 @@
(* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the
formula. *)
-fun prop_of_atp ctxt textual sym_tab phi =
+fun prop_of_atp ctxt format type_enc textual sym_tab phi =
let
fun do_formula pos phi =
(case phi of
@@ -337,7 +485,7 @@
| AImplies => s_imp
| AIff => s_iff
| ANot => raise Fail "impossible connective")
- | AAtom tm => term_of_atom ctxt textual sym_tab pos tm
+ | AAtom tm => term_of_atom ctxt format type_enc textual sym_tab pos tm
| _ => raise ATP_FORMULA [phi])
in
repair_tvar_sorts (do_formula true phi Vartab.empty)
@@ -475,18 +623,19 @@
t
| t => t)
-fun termify_line ctxt lifted sym_tab (name, role, u, rule, deps) =
- let
- val thy = Proof_Context.theory_of ctxt
- val t = u
- |> prop_of_atp ctxt true sym_tab
- |> uncombine_term thy
- |> unlift_term lifted
- |> infer_formula_types ctxt
- |> HOLogic.mk_Trueprop
- in
- (name, role, t, rule, deps)
- end
+fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) = NONE
+ | termify_line ctxt format type_enc lifted sym_tab (name, role, u, rule, deps) =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val t = u
+ |> prop_of_atp ctxt format type_enc true sym_tab
+ |> uncombine_term thy
+ |> unlift_term lifted
+ |> infer_formula_types ctxt
+ |> HOLogic.mk_Trueprop
+ in
+ SOME (name, role, t, rule, deps)
+ end
val waldmeister_conjecture_num = "1.0.0.0"
@@ -502,12 +651,12 @@
repair_body proof
end
-fun termify_atp_proof ctxt pool lifted sym_tab =
+fun termify_atp_proof ctxt prover format type_enc pool lifted sym_tab =
clean_up_atp_proof_dependencies
#> nasty_atp_proof pool
#> map_term_names_in_atp_proof repair_name
- #> map (termify_line ctxt lifted sym_tab)
- #> repair_waldmeister_endgame
+ #> map_filter (termify_line ctxt format type_enc lifted sym_tab)
+ #> prover = waldmeisterN ? repair_waldmeister_endgame
fun take_distinct_vars seen ((t as Var _) :: ts) =
if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 16:18:15 2014 +0200
@@ -569,7 +569,6 @@
val vampire = (vampireN, fn () => vampire_config)
-
(* Z3 with TPTP syntax (half experimental, half legacy) *)
val z3_tff0 = TFF Monomorphic
@@ -796,7 +795,7 @@
val atps =
[agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
- z3_tptp,zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
+ z3_tptp, zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
remote_spass_pirate, remote_waldmeister]
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 16 16:18:15 2014 +0200
@@ -48,7 +48,7 @@
ATerm ((Metis_Name.toString s, []), [])
fun hol_term_of_metis ctxt type_enc sym_tab =
- atp_term_of_metis type_enc #> term_of_atp ctxt false sym_tab NONE
+ atp_term_of_metis type_enc #> term_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab NONE
fun atp_literal_of_metis type_enc (pos, atom) =
atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
@@ -65,7 +65,7 @@
Metis_Thm.clause
#> Metis_LiteralSet.toList
#> atp_clause_of_metis type_enc
- #> prop_of_atp ctxt false sym_tab
+ #> prop_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab
#> singleton (polish_hol_terms ctxt concealed)
fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 16 16:18:15 2014 +0200
@@ -302,36 +302,39 @@
| NONE => NONE)
| _ => outcome)
in
- ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
+ ((SOME key, value), (output, run_time, facts, atp_proof, outcome),
+ SOME (format, type_enc))
end
val timer = Timer.startRealTimer ()
- fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _))) =
+ fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) =
let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in
if Time.<= (time_left, Time.zeroTime) then
result
else
run_slice time_left cache slice
- |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
- (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
+ |> (fn (cache, (output, run_time, used_from, atp_proof, outcome),
+ format_type_enc) =>
+ (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome),
+ format_type_enc))
end
| maybe_run_slice _ result = result
in
((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
- ("", Time.zeroTime, [], [], SOME InternalError))
+ ("", Time.zeroTime, [], [], SOME InternalError), NONE)
|> fold maybe_run_slice actual_slices
end
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else ()
- fun export (_, (output, _, _, _, _)) =
+ fun export (_, (output, _, _, _, _), _) =
if dest_dir = "" then ()
else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
val ((_, (_, pool, fact_names, lifted, sym_tab)),
- (output, run_time, used_from, atp_proof, outcome)) =
+ (output, run_time, used_from, atp_proof, outcome), SOME (format, type_enc)) =
with_cleanup clean_up run () |> tap export
val important_message =
@@ -367,7 +370,7 @@
if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE
val atp_proof =
atp_proof
- |> termify_atp_proof ctxt pool lifted sym_tab
+ |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
|> introduce_spass_skolem
|> factify_atp_proof fact_names hyp_ts concl_t
in