--- 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
--- 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"
--- 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,
--- 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, [])
--- 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;
--- 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 => []
--- 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 ""
--- 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
--- 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,