# HG changeset patch # User fleury # Date 1402928295 -7200 # Node ID 488046fdda590ee780439c2c92aa0f78ee2cff35 # Parent d3d91422f4080d2ccdc9c56da13a886b6840834f add support for Isar reconstruction for thf1 ATP provers like Leo-II. diff -r d3d91422f408 -r 488046fdda59 src/HOL/ATP.thy --- 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 diff -r d3d91422f408 -r 488046fdda59 src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r d3d91422f408 -r 488046fdda59 src/HOL/Tools/ATP/atp_proof.ML --- 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)\(, , \). The 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) diff -r d3d91422f408 -r 488046fdda59 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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 diff -r d3d91422f408 -r 488046fdda59 src/HOL/Tools/ATP/atp_systems.ML --- 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] diff -r d3d91422f408 -r 488046fdda59 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 = diff -r d3d91422f408 -r 488046fdda59 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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