# HG changeset patch # User blanchet # Date 1379016657 -7200 # Node ID bd5fa6425993361dfe0b44b4ea020c6438e4b138 # Parent fcd36f587512f8759f28ea016ca5db54f97f6454 prefixed types and some functions with "atp_" for disambiguation diff -r fcd36f587512 -r bd5fa6425993 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Thu Sep 12 22:10:57 2013 +0200 @@ -71,7 +71,7 @@ tracing ("Ran ATP: " ^ (case outcome of NONE => "Success" - | SOME failure => string_of_failure failure)) + | SOME failure => string_of_atp_failure failure)) in outcome end fun is_problem_line_reprovable ctxt format prelude axioms deps diff -r fcd36f587512 -r bd5fa6425993 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Sep 12 22:10:57 2013 +0200 @@ -7,21 +7,23 @@ signature ATP_PROBLEM = sig - datatype ('a, 'b) ho_term = - ATerm of ('a * 'b list) * ('a, 'b) ho_term list | - AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list - datatype quantifier = AForall | AExists - datatype connective = ANot | AAnd | AOr | AImplies | AIff - datatype ('a, 'b, 'c, 'd) formula = - ATyQuant of quantifier * ('b * 'd list) list * ('a, 'b, 'c, 'd) formula | - AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c, 'd) formula | - AConn of connective * ('a, 'b, 'c, 'd) formula list | + datatype ('a, 'b) atp_term = + ATerm of ('a * 'b list) * ('a, 'b) atp_term list | + AAbs of (('a * 'b) * ('a, 'b) atp_term) * ('a, 'b) atp_term list + datatype atp_quantifier = AForall | AExists + datatype atp_connective = ANot | AAnd | AOr | AImplies | AIff + datatype ('a, 'b, 'c, 'd) atp_formula = + ATyQuant of atp_quantifier * ('b * 'd list) list + * ('a, 'b, 'c, 'd) atp_formula | + AQuant of atp_quantifier * ('a * 'b option) list + * ('a, 'b, 'c, 'd) atp_formula | + AConn of atp_connective * ('a, 'b, 'c, 'd) atp_formula list | AAtom of 'c - datatype 'a ho_type = - AType of 'a * 'a ho_type list | - AFun of 'a ho_type * 'a ho_type | - APi of 'a list * 'a ho_type + datatype 'a atp_type = + AType of 'a * 'a atp_type list | + AFun of 'a atp_type * 'a atp_type | + APi of 'a list * 'a atp_type type term_order = {is_lpo : bool, @@ -41,22 +43,22 @@ THF of polymorphism * thf_choice * thf_defs | DFG of polymorphism - datatype formula_role = + datatype atp_formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture | Plain | Unknown - datatype 'a problem_line = + datatype 'a atp_problem_line = Class_Decl of string * 'a * 'a list | Type_Decl of string * 'a * int | - Sym_Decl of string * 'a * 'a ho_type | - Datatype_Decl of string * ('a * 'a list) list * 'a ho_type - * ('a, 'a ho_type) ho_term list * bool | - Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a | - Formula of (string * string) * formula_role - * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula - * (string, string ho_type) ho_term option - * (string, string ho_type) ho_term list - type 'a problem = (string * 'a problem_line list) list + Sym_Decl of string * 'a * 'a atp_type | + Datatype_Decl of string * ('a * 'a list) list * 'a atp_type + * ('a, 'a atp_type) atp_term list * bool | + Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | + Formula of (string * string) * atp_formula_role + * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula + * (string, string atp_type) atp_term option + * (string, string atp_type) atp_term list + type 'a atp_problem = (string * 'a atp_problem_line list) list val tptp_cnf : string val tptp_fof : string @@ -89,9 +91,9 @@ val tptp_true : string val tptp_empty_list : string val isabelle_info_prefix : string - val isabelle_info : string -> int -> (string, 'a) ho_term list - val extract_isabelle_status : (string, 'a) ho_term list -> string option - val extract_isabelle_rank : (string, 'a) ho_term list -> int + val isabelle_info : string -> int -> (string, 'a) atp_term list + val extract_isabelle_status : (string, 'a) atp_term list -> string option + val extract_isabelle_rank : (string, 'a) atp_term list -> int val inductionN : string val introN : string val inductiveN : string @@ -107,37 +109,37 @@ val is_built_in_tptp_symbol : string -> bool val is_tptp_variable : string -> bool val is_tptp_user_symbol : string -> bool - val bool_atype : (string * string) ho_type - val individual_atype : (string * string) ho_type - val mk_anot : ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'c, 'd) formula + val bool_atype : (string * string) atp_type + val individual_atype : (string * string) atp_type + val mk_anot : ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula val mk_aconn : - connective -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'c, 'd) formula - -> ('a, 'b, 'c, 'd) formula + atp_connective -> ('a, 'b, 'c, 'd) atp_formula + -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula val aconn_fold : - bool option -> (bool option -> 'a -> 'b -> 'b) -> connective * 'a list + bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list -> 'b -> 'b val aconn_map : - bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) formula) - -> connective * 'a list -> ('b, 'c, 'd, 'e) formula + bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula) + -> atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula val formula_fold : - bool option -> (bool option -> 'c -> 'e -> 'e) -> ('a, 'b, 'c, 'd) formula - -> 'e -> 'e + bool option -> (bool option -> 'c -> 'e -> 'e) + -> ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e val formula_map : - ('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula - val strip_atype : 'a ho_type -> 'a list * ('a ho_type list * 'a ho_type) + ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula + val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type) val is_format_higher_order : atp_format -> bool - val tptp_string_of_line : atp_format -> string problem_line -> string + val tptp_string_of_line : atp_format -> string atp_problem_line -> string val lines_of_atp_problem : - atp_format -> term_order -> (unit -> (string * int) list) -> string problem - -> string list + atp_format -> term_order -> (unit -> (string * int) list) + -> string atp_problem -> string list val ensure_cnf_problem : - (string * string) problem -> (string * string) problem + (string * string) atp_problem -> (string * string) atp_problem val filter_cnf_ueq_problem : - (string * string) problem -> (string * string) problem - val declared_in_atp_problem : 'a problem -> ('a list * 'a list) * 'a list + (string * string) atp_problem -> (string * string) atp_problem + val declared_in_atp_problem : 'a atp_problem -> ('a list * 'a list) * 'a list val nice_atp_problem : - bool -> atp_format -> ('a * (string * string) problem_line list) list - -> ('a * string problem_line list) list + bool -> atp_format -> ('a * (string * string) atp_problem_line list) list + -> ('a * string atp_problem_line list) list * (string Symtab.table * string Symtab.table) option end; @@ -151,21 +153,23 @@ (** ATP problem **) -datatype ('a, 'b) ho_term = - ATerm of ('a * 'b list) * ('a, 'b) ho_term list | - AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list -datatype quantifier = AForall | AExists -datatype connective = ANot | AAnd | AOr | AImplies | AIff -datatype ('a, 'b, 'c, 'd) formula = - ATyQuant of quantifier * ('b * 'd list) list * ('a, 'b, 'c, 'd) formula | - AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c, 'd) formula | - AConn of connective * ('a, 'b, 'c, 'd) formula list | +datatype ('a, 'b) atp_term = + ATerm of ('a * 'b list) * ('a, 'b) atp_term list | + AAbs of (('a * 'b) * ('a, 'b) atp_term) * ('a, 'b) atp_term list +datatype atp_quantifier = AForall | AExists +datatype atp_connective = ANot | AAnd | AOr | AImplies | AIff +datatype ('a, 'b, 'c, 'd) atp_formula = + ATyQuant of atp_quantifier * ('b * 'd list) list + * ('a, 'b, 'c, 'd) atp_formula | + AQuant of atp_quantifier * ('a * 'b option) list + * ('a, 'b, 'c, 'd) atp_formula | + AConn of atp_connective * ('a, 'b, 'c, 'd) atp_formula list | AAtom of 'c -datatype 'a ho_type = - AType of 'a * 'a ho_type list | - AFun of 'a ho_type * 'a ho_type | - APi of 'a list * 'a ho_type +datatype 'a atp_type = + AType of 'a * 'a atp_type list | + AFun of 'a atp_type * 'a atp_type | + APi of 'a list * 'a atp_type type term_order = {is_lpo : bool, @@ -185,22 +189,22 @@ THF of polymorphism * thf_choice * thf_defs | DFG of polymorphism -datatype formula_role = +datatype atp_formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture | Plain | Unknown -datatype 'a problem_line = +datatype 'a atp_problem_line = Class_Decl of string * 'a * 'a list | Type_Decl of string * 'a * int | - Sym_Decl of string * 'a * 'a ho_type | - Datatype_Decl of string * ('a * 'a list) list * 'a ho_type - * ('a, 'a ho_type) ho_term list * bool | - Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a | - Formula of (string * string) * formula_role - * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula - * (string, string ho_type) ho_term option - * (string, string ho_type) ho_term list -type 'a problem = (string * 'a problem_line list) list + Sym_Decl of string * 'a * 'a atp_type | + Datatype_Decl of string * ('a * 'a list) list * 'a atp_type + * ('a, 'a atp_type) atp_term list * bool | + Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | + Formula of (string * string) * atp_formula_role + * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula + * (string, string atp_type) atp_term option + * (string, string atp_type) atp_term list +type 'a atp_problem = (string * 'a atp_problem_line list) list (* official TPTP syntax *) val tptp_cnf = "cnf" diff -r fcd36f587512 -r bd5fa6425993 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Sep 12 22:10:57 2013 +0200 @@ -8,12 +8,12 @@ signature ATP_PROBLEM_GENERATE = sig - type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term - type connective = ATP_Problem.connective - type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula + type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term + type atp_connective = ATP_Problem.atp_connective + type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula type atp_format = ATP_Problem.atp_format - type formula_role = ATP_Problem.formula_role - type 'a problem = 'a ATP_Problem.problem + type atp_formula_role = ATP_Problem.atp_formula_role + type 'a atp_problem = 'a ATP_Problem.atp_problem datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter @@ -100,8 +100,9 @@ val adjust_type_enc : atp_format -> type_enc -> type_enc val is_lambda_free : term -> bool val mk_aconns : - connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula - val unmangled_const : string -> string * (string, 'b) ho_term list + atp_connective -> ('a, 'b, 'c, 'd) atp_formula list + -> ('a, 'b, 'c, 'd) atp_formula + val unmangled_const : string -> string * (string, 'b) atp_term list val unmangled_const_name : string -> string list val helper_table : ((string * bool) * (status * thm) list) list val trans_lams_of_string : @@ -109,13 +110,13 @@ val string_of_status : status -> string val factsN : string val prepare_atp_problem : - Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string - -> bool -> bool -> bool -> term list -> term + Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode + -> string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list - -> string problem * string Symtab.table * (string * stature) list vector + -> string atp_problem * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table - val atp_problem_selection_weights : string problem -> (string * real) list - val atp_problem_term_order_info : string problem -> (string * int) list + val atp_problem_selection_weights : string atp_problem -> (string * real) list + val atp_problem_term_order_info : string atp_problem -> (string * int) list end; structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE = @@ -826,8 +827,8 @@ type ifact = {name : string, stature : stature, - role : formula_role, - iformula : (string * string, typ, iterm, string * string) formula, + role : atp_formula_role, + iformula : (string * string, typ, iterm, string * string) atp_formula, atomic_types : typ list} fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) = @@ -916,9 +917,9 @@ | term (TVar z) = AType (tvar_name z, []) in term end -fun ho_term_of_ho_type (AType (name, tys)) = - ATerm ((name, []), map ho_term_of_ho_type tys) - | ho_term_of_ho_type _ = raise Fail "unexpected type" +fun atp_term_of_ho_type (AType (name, tys)) = + ATerm ((name, []), map atp_term_of_ho_type tys) + | atp_term_of_ho_type _ = raise Fail "unexpected type" fun ho_type_of_type_arg type_enc T = if T = dummyT then NONE else SOME (raw_ho_type_of_typ type_enc T) @@ -983,7 +984,7 @@ if is_type_enc_native type_enc then (map (native_ho_type_of_typ type_enc false 0) T_args, []) else - ([], map_filter (Option.map ho_term_of_ho_type + ([], map_filter (Option.map atp_term_of_ho_type o ho_type_of_type_arg type_enc) T_args) fun class_atom type_enc (cl, T) = @@ -2071,10 +2072,10 @@ fun tag_with_type ctxt mono type_enc pos T tm = IConst (type_tag, T --> T, [T]) |> mangle_type_args_in_iterm type_enc - |> ho_term_of_iterm ctxt mono type_enc pos + |> atp_term_of_iterm ctxt mono type_enc pos |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm]) | _ => raise Fail "unexpected lambda-abstraction") -and ho_term_of_iterm ctxt mono type_enc pos = +and atp_term_of_iterm ctxt mono type_enc pos = let fun term site u = let @@ -2112,7 +2113,7 @@ let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc - val do_term = ho_term_of_iterm ctxt mono type_enc + val do_term = atp_term_of_iterm ctxt mono type_enc fun do_out_of_bound_type pos phi universal (name, T) = if should_guard_type ctxt mono type_enc (fn () => should_guard_var thy level pos phi universal name) T then @@ -2599,7 +2600,7 @@ val base_ary = min_ary_of sym_tab0 base_s fun do_const name = IConst (name, T, T_args) val filter_ty_args = filter_type_args_in_iterm thy ctrss type_enc - val ho_term_of = ho_term_of_iterm ctxt mono type_enc (SOME true) + val atp_term_of = atp_term_of_iterm ctxt mono type_enc (SOME true) val name1 as (s1, _) = base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1) val name2 as (s2, _) = base_name |> aliased_uncurried ary @@ -2619,7 +2620,7 @@ val eq = eq_formula type_enc (atomic_types_of T) (map (apsnd do_bound_type) bounds) false - (ho_term_of tm1) (ho_term_of tm2) + (atp_term_of tm1) (atp_term_of tm2) in ([tm1, tm2], [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, diff -r fcd36f587512 -r bd5fa6425993 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 12 22:10:57 2013 +0200 @@ -8,14 +8,14 @@ signature ATP_PROOF = sig - type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term - type formula_role = ATP_Problem.formula_role - type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula - type 'a problem = 'a ATP_Problem.problem + type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term + type atp_formula_role = ATP_Problem.atp_formula_role + type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula + type 'a atp_problem = 'a ATP_Problem.atp_problem exception UNRECOGNIZED_ATP_PROOF of unit - datatype failure = + datatype atp_failure = Unprovable | GaveUp | ProofMissing | @@ -34,32 +34,35 @@ InternalError | UnknownError of string - type step_name = string * string list - type 'a step = step_name * formula_role * 'a * string * step_name list + type atp_step_name = string * string list + type 'a atp_step = + atp_step_name * atp_formula_role * 'a * string * atp_step_name list - type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list + type 'a atp_proof = ('a, 'a, ('a, 'a) atp_term, 'a) atp_formula atp_step list val short_output : bool -> string -> string - val string_of_failure : failure -> string + val string_of_atp_failure : atp_failure -> string val extract_important_message : string -> string - val extract_known_failure : - (failure * string) list -> string -> failure option + val extract_known_atp_failure : + (atp_failure * string) list -> string -> atp_failure option val extract_tstplike_proof_and_outcome : - bool -> (string * string) list -> (failure * string) list -> string - -> string * failure option - val is_same_atp_step : step_name -> step_name -> bool + bool -> (string * string) list -> (atp_failure * string) list -> string + -> string * atp_failure option + val is_same_atp_step : atp_step_name -> atp_step_name -> bool val scan_general_id : string list -> string * string list val agsyhol_coreN : string val satallax_coreN : string val z3_tptp_coreN : string val parse_formula : string list - -> (string, 'a, (string, 'a) ho_term, string) formula * string list - val atp_proof_of_tstplike_proof : string problem -> string -> string proof - val clean_up_atp_proof_dependencies : string proof -> string proof + -> (string, 'a, (string, 'a) atp_term, string) atp_formula * string list + val atp_proof_of_tstplike_proof : + string atp_problem -> string -> string atp_proof + val clean_up_atp_proof_dependencies : string atp_proof -> string atp_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 + (string -> string) -> string atp_proof -> string atp_proof + val nasty_atp_proof : + string Symtab.table -> string atp_proof -> string atp_proof end; structure ATP_Proof : ATP_PROOF = @@ -70,7 +73,7 @@ exception UNRECOGNIZED_ATP_PROOF of unit -datatype failure = +datatype atp_failure = Unprovable | GaveUp | ProofMissing | @@ -103,37 +106,37 @@ | involving ss = " involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) -fun string_of_failure Unprovable = "The generated problem is unprovable." - | string_of_failure GaveUp = "The prover gave up." - | string_of_failure ProofMissing = +fun string_of_atp_failure Unprovable = "The generated problem is unprovable." + | string_of_atp_failure GaveUp = "The prover gave up." + | string_of_atp_failure ProofMissing = "The prover claims the conjecture is a theorem but did not provide a proof." - | string_of_failure ProofIncomplete = + | string_of_atp_failure ProofIncomplete = "The prover claims the conjecture is a theorem but provided an incomplete \ \(or unparsable) proof." - | string_of_failure (UnsoundProof (false, ss)) = + | string_of_atp_failure (UnsoundProof (false, ss)) = "The prover derived \"False\" using" ^ involving ss ^ ". Specify a sound type encoding or omit the \"type_enc\" option." - | string_of_failure (UnsoundProof (true, ss)) = + | string_of_atp_failure (UnsoundProof (true, ss)) = "The prover derived \"False\" using" ^ involving ss ^ ". This could be due to inconsistent axioms (including \"sorry\"s) or to \ \a bug in Sledgehammer. If the problem persists, please contact the \ \Isabelle developers." - | string_of_failure CantConnect = "Cannot connect to remote server." - | string_of_failure TimedOut = "Timed out." - | string_of_failure Inappropriate = + | string_of_atp_failure CantConnect = "Cannot connect to remote server." + | string_of_atp_failure TimedOut = "Timed out." + | string_of_atp_failure Inappropriate = "The generated problem lies outside the prover's scope." - | string_of_failure OutOfResources = "The prover ran out of resources." - | string_of_failure NoPerl = "Perl" ^ missing_message_tail - | string_of_failure NoLibwwwPerl = + | string_of_atp_failure OutOfResources = "The prover ran out of resources." + | string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail + | string_of_atp_failure NoLibwwwPerl = "The Perl module \"libwww-perl\"" ^ missing_message_tail - | string_of_failure MalformedInput = + | string_of_atp_failure MalformedInput = "The generated problem is malformed. Please report this to the Isabelle \ \developers." - | string_of_failure MalformedOutput = "The prover output is malformed." - | string_of_failure Interrupted = "The prover was interrupted." - | string_of_failure Crashed = "The prover crashed." - | string_of_failure InternalError = "An internal prover error occurred." - | string_of_failure (UnknownError s) = + | string_of_atp_failure MalformedOutput = "The prover output is malformed." + | string_of_atp_failure Interrupted = "The prover was interrupted." + | string_of_atp_failure Crashed = "The prover crashed." + | string_of_atp_failure InternalError = "An internal prover error occurred." + | string_of_atp_failure (UnknownError s) = "A prover error occurred" ^ (if s = "" then ". (Pass the \"verbose\" option for details.)" else ":\n" ^ s) @@ -163,7 +166,7 @@ extract_delimited (begin_delim, end_delim) output | _ => "" -fun extract_known_failure known_failures output = +fun extract_known_atp_failure known_failures output = known_failures |> find_first (fn (_, pattern) => String.isSubstring pattern output) |> Option.map fst @@ -171,14 +174,14 @@ fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures output = case (extract_tstplike_proof proof_delims output, - extract_known_failure known_failures output) of + extract_known_atp_failure known_failures output) of (_, SOME ProofIncomplete) => ("", NONE) | ("", SOME ProofMissing) => ("", NONE) | ("", NONE) => ("", SOME (UnknownError (short_output verbose output))) | res as ("", _) => res | (tstplike_proof, _) => (tstplike_proof, NONE) -type step_name = string * string list +type atp_step_name = string * string list fun is_same_atp_step (s1, _) (s2, _) = s1 = s2 @@ -193,9 +196,10 @@ | _ => raise Fail "not Vampire" end -type 'a step = step_name * formula_role * 'a * string * step_name list +type 'a atp_step = + atp_step_name * atp_formula_role * 'a * string * atp_step_name list -type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list +type 'a atp_proof = ('a, 'a, ('a, 'a) atp_term, 'a) atp_formula atp_step list (**** PARSING OF TSTP FORMAT ****) @@ -205,8 +209,6 @@ || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (fn (ss1, ss2) => implode ss1 ^ implode ss2) -val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode - val skip_term = let fun skip _ accum [] = (accum, []) diff -r fcd36f587512 -r bd5fa6425993 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Sep 12 22:10:57 2013 +0200 @@ -8,8 +8,8 @@ signature ATP_PROOF_RECONSTRUCT = sig - type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term - type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula + type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term + type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula val metisN : string val full_typesN : string @@ -28,10 +28,10 @@ val unalias_type_enc : string -> string list val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option -> - (string, string) ho_term -> term + (string, string) atp_term -> term val prop_of_atp : Proof.context -> bool -> int Symtab.table -> - (string, string, (string, string) ho_term, string) formula -> term + (string, string, (string, string) atp_term, string) atp_formula -> term end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = @@ -90,9 +90,9 @@ TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end -exception HO_TERM of (string, string) ho_term list -exception FORMULA of - (string, string, (string, string) ho_term, string) formula list +exception ATP_TERM of (string, string) atp_term list +exception ATP_FORMULA of + (string, string, (string, string) atp_term, string) atp_formula list exception SAME of unit (* Type variables are given the basic sort "HOL.type". Some will later be @@ -103,7 +103,7 @@ SOME b => Type (invert_const b, Ts) | NONE => if not (null us) then - raise HO_TERM [u] (* only "tconst"s have type arguments *) + raise ATP_TERM [u] (* only "tconst"s have type arguments *) else case unprefix_and_unascii tfree_prefix a of SOME b => make_tfree ctxt b | NONE => @@ -120,7 +120,7 @@ fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) = case (unprefix_and_unascii class_prefix a, map (typ_of_atp ctxt) us) of (SOME b, [T]) => (b, T) - | _ => raise HO_TERM [u] + | _ => raise ATP_TERM [u] (* Accumulate type constraints in a formula: negative type literals. *) fun add_var (key, z) = Vartab.map_default (key, []) (cons z) @@ -178,7 +178,8 @@ case u of ATerm ((s, _), us) => if s = "" - then error "Isar proof reconstruction failed because the ATP proof contained unparsable material." + 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 @@ -199,7 +200,7 @@ case mangled_us @ us of [typ_u, term_u] => do_term extra_ts (SOME (typ_of_atp ctxt typ_u)) term_u - | _ => raise HO_TERM us + | _ => raise ATP_TERM us else if s' = predicator_name then do_term [] (SOME @{typ bool}) (hd us) else if s' = app_op_name then @@ -335,7 +336,7 @@ | AIff => s_iff | ANot => raise Fail "impossible connective") | AAtom tm => term_of_atom ctxt textual sym_tab pos tm - | _ => raise FORMULA [phi] + | _ => raise ATP_FORMULA [phi] in repair_tvar_sorts (do_formula true phi Vartab.empty) end end; diff -r fcd36f587512 -r bd5fa6425993 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Sep 12 22:10:57 2013 +0200 @@ -9,8 +9,8 @@ sig type term_order = ATP_Problem.term_order type atp_format = ATP_Problem.atp_format - type formula_role = ATP_Problem.formula_role - type failure = ATP_Proof.failure + type atp_formula_role = ATP_Problem.atp_formula_role + type atp_failure = ATP_Proof.atp_failure type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = @@ -20,8 +20,8 @@ -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, - known_failures : (failure * string) list, - prem_role : formula_role, + known_failures : (atp_failure * string) list, + prem_role : atp_formula_role, best_slices : Proof.context -> (real * (slice_spec * string)) list, best_max_mono_iters : int, best_max_new_mono_instances : int} @@ -69,7 +69,7 @@ val remote_prefix : string val remote_atp : string -> string -> string list -> (string * string) list - -> (failure * string) list -> formula_role + -> (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) @@ -102,8 +102,8 @@ -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, - known_failures : (failure * string) list, - prem_role : formula_role, + known_failures : (atp_failure * string) list, + prem_role : atp_formula_role, best_slices : Proof.context -> (real * (slice_spec * string)) list, best_max_mono_iters : int, best_max_new_mono_instances : int} @@ -675,8 +675,8 @@ "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of (output, 0) => split_lines output | (output, _) => - (warning (case extract_known_failure known_perl_failures output of - SOME failure => string_of_failure failure + (warning (case extract_known_atp_failure known_perl_failures output of + SOME failure => string_of_atp_failure failure | NONE => trim_line output ^ "."); [])) () handle TimeLimit.TimeOut => [] diff -r fcd36f587512 -r bd5fa6425993 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Sep 12 22:10:57 2013 +0200 @@ -97,7 +97,7 @@ print silent (fn () => case outcome of - SOME failure => string_of_failure failure + SOME failure => string_of_atp_failure failure | NONE => "Found proof" ^ (if length used_facts = length facts then "" diff -r fcd36f587512 -r bd5fa6425993 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Sep 12 22:10:57 2013 +0200 @@ -8,7 +8,7 @@ signature SLEDGEHAMMER_PROVERS = sig - type failure = ATP_Proof.failure + type atp_failure = ATP_Proof.atp_failure type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc type fact = Sledgehammer_Fact.fact @@ -75,7 +75,7 @@ factss : (string * fact list) list} type prover_result = - {outcome : failure option, + {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, run_time : Time.time, @@ -390,7 +390,7 @@ factss : (string * fact list) list} type prover_result = - {outcome : failure option, + {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, run_time : Time.time, @@ -878,8 +878,10 @@ val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in - if debug then (warning (string_of_failure failure); NONE) - else SOME failure + if debug then + (warning (string_of_atp_failure failure); NONE) + else + SOME failure end | NONE => NONE) | _ => outcome @@ -982,7 +984,7 @@ end | SOME failure => ([], Lazy.value (Failed_to_Play plain_metis), - fn _ => string_of_failure failure, "") + fn _ => string_of_atp_failure failure, "") in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, @@ -1124,7 +1126,7 @@ if debug then quote name ^ " invoked with " ^ num_of_facts fact_filter num_facts ^ ": " ^ - string_of_failure (failure_of_smt_failure (the outcome)) ^ + string_of_atp_failure (failure_of_smt_failure (the outcome)) ^ " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^ "..." |> Output.urgent_message @@ -1180,7 +1182,7 @@ "") | SOME failure => (Lazy.value (Failed_to_Play plain_metis), - fn _ => string_of_failure failure, "") + fn _ => string_of_atp_failure failure, "") in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, @@ -1228,7 +1230,7 @@ in {outcome = SOME failure, used_facts = [], used_from = [], run_time = Time.zeroTime, preplay = Lazy.value play, - message = fn _ => string_of_failure failure, message_tail = ""} + message = fn _ => string_of_atp_failure failure, message_tail = ""} end end diff -r fcd36f587512 -r bd5fa6425993 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Sep 12 22:10:57 2013 +0200 @@ -7,22 +7,22 @@ signature SLEDGEHAMMER_RECONSTRUCT = sig - type 'a proof = 'a ATP_Proof.proof + type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature type one_line_params = Sledgehammer_Print.one_line_params type isar_params = bool * bool * Time.time option * bool * real * int * real * bool * bool * string Symtab.table * (string * stature) list vector - * (string * term) list * int Symtab.table * string proof * thm + * (string * term) list * int Symtab.table * string atp_proof * thm - val lam_trans_of_atp_proof : string proof -> string -> string - val is_typed_helper_used_in_atp_proof : string proof -> bool + val lam_trans_of_atp_proof : string atp_proof -> string -> string + val is_typed_helper_used_in_atp_proof : string atp_proof -> bool val used_facts_in_atp_proof : - Proof.context -> (string * stature) list vector -> string proof -> + Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list val used_facts_in_unsound_atp_proof : - Proof.context -> (string * stature) list vector -> 'a proof -> + Proof.context -> (string * stature) list vector -> 'a atp_proof -> string list option val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string @@ -50,7 +50,7 @@ open Sledgehammer_Minimize_Isar structure String_Redirect = ATP_Proof_Redirect( - type key = step_name + type key = atp_step_name val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') val string_of = fst) @@ -410,7 +410,7 @@ type isar_params = bool * bool * Time.time option * bool * real * int * real * bool * bool * string Symtab.table * (string * stature) list vector - * (string * term) list * int Symtab.table * string proof * thm + * (string * term) list * int Symtab.table * string atp_proof * thm fun isar_proof_text ctxt isar_proofs (debug, verbose, preplay_timeout, preplay_trace, isar_compress,