--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
@@ -12,10 +12,10 @@
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) formula =
- ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula |
- AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
- AConn of connective * ('a, 'b, 'c) formula list |
+ 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 |
AAtom of 'c
datatype 'a ho_type =
@@ -46,7 +46,7 @@
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
Formula of string * formula_role
- * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+ * ('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
@@ -101,20 +101,21 @@
val atype_of_types : (string * string) ho_type
val bool_atype : (string * string) ho_type
val individual_atype : (string * string) ho_type
- val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
+ val mk_anot : ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'c, 'd) formula
val mk_aconn :
- connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
- -> ('a, 'b, 'c) formula
+ connective -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'c, 'd) formula
+ -> ('a, 'b, 'c, 'd) formula
val aconn_fold :
bool option -> (bool option -> 'a -> 'b -> 'b) -> connective * 'a list
-> 'b -> 'b
val aconn_map :
- bool option -> (bool option -> 'a -> ('b, 'c, 'd) formula)
- -> connective * 'a list -> ('b, 'c, 'd) formula
+ bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) formula)
+ -> connective * 'a list -> ('b, 'c, 'd, 'e) formula
val formula_fold :
- bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
- -> 'd -> 'd
- val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
+ bool option -> (bool option -> 'c -> 'e -> 'e) -> ('a, 'b, 'c, 'd) formula
+ -> 'e -> 'e
+ val formula_map :
+ ('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula
val is_function_type : string ho_type -> bool
val is_predicate_type : string ho_type -> bool
val is_format_higher_order : atp_format -> bool
@@ -145,10 +146,10 @@
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) formula =
- ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula |
- AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
- AConn of connective * ('a, 'b, 'c) formula list |
+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 |
AAtom of 'c
datatype 'a ho_type =
@@ -179,7 +180,7 @@
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
Formula of string * formula_role
- * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+ * ('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
@@ -429,7 +430,8 @@
raise Fail "unexpected term in first-order format"
and tptp_string_for_formula format (ATyQuant (q, xs, phi)) =
tptp_string_for_quantifier q ^
- "[" ^ commas (map (suffix_type_of_types o string_for_type format) xs) ^
+ "[" ^
+ commas (map (suffix_type_of_types o string_for_type format o fst) xs) ^
"]: " ^ tptp_string_for_formula format phi
|> enclose "(" ")"
| tptp_string_for_formula format (AQuant (q, xs, phi)) =
@@ -520,7 +522,7 @@
| str_for_conn _ AImplies = "implies"
| str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
fun str_for_formula top_level (ATyQuant (q, xs, phi)) =
- str_for_quant q ^ "_sorts([" ^ commas (map str_for_typ xs) ^
+ str_for_quant q ^ "_sorts([" ^ commas (map (str_for_typ o fst) xs) ^
"], " ^ str_for_formula top_level phi ^ ")"
| str_for_formula top_level (AQuant (q, xs, phi)) =
str_for_quant q ^ "([" ^
@@ -847,8 +849,9 @@
nice_name name ##>> nice_type ty ##>> nice_term tm
##>> pool_map nice_term args #>> AAbs
fun nice_formula (ATyQuant (q, xs, phi)) =
- pool_map nice_type xs ##>> nice_formula phi
- #>> (fn (xs, phi) => ATyQuant (q, xs, phi))
+ pool_map nice_type (map fst xs)
+ ##>> pool_map (pool_map nice_name) (map snd xs) ##>> nice_formula phi
+ #>> (fn ((tys, sorts), phi) => ATyQuant (q, tys ~~ sorts, phi))
| nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
##>> pool_map (fn NONE => pair NONE
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
@@ -10,7 +10,7 @@
sig
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type connective = ATP_Problem.connective
- type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
+ type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
type atp_format = ATP_Problem.atp_format
type formula_role = ATP_Problem.formula_role
type 'a problem = 'a ATP_Problem.problem
@@ -91,7 +91,7 @@
val type_enc_from_string : strictness -> string -> type_enc
val adjust_type_enc : atp_format -> type_enc -> type_enc
val mk_aconns :
- connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
+ connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula
val unmangled_const : string -> string * (string, 'b) ho_term list
val unmangled_const_name : string -> string list
val helper_table : ((string * bool) * (status * thm) list) list
@@ -114,8 +114,6 @@
open ATP_Util
open ATP_Problem
-type name = string * string
-
datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
datatype scope = Global | Local | Assum | Chained
@@ -512,10 +510,10 @@
(* intermediate terms *)
datatype iterm =
- IConst of name * typ * typ list |
- IVar of name * typ |
+ IConst of (string * string) * typ * typ list |
+ IVar of (string * string) * typ |
IApp of iterm * iterm |
- IAbs of (name * typ) * iterm
+ IAbs of ((string * string) * typ) * iterm
fun ityp_of (IConst (_, T, _)) = T
| ityp_of (IVar (_, T)) = T
@@ -829,7 +827,7 @@
{name : string,
stature : stature,
role : formula_role,
- iformula : (name, typ, iterm) formula,
+ iformula : (string * string, typ, iterm, string * string) formula,
atomic_types : typ list}
fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) =
@@ -1741,7 +1739,8 @@
(sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
#> (if is_type_enc_native type_enc then
mk_atyquant AForall
- (map (fn TVar (x, _) => AType (tvar_name x, [])) Ts)
+ (map (fn TVar (x, S) =>
+ (AType (tvar_name x, []), map (`make_type_class) S)) Ts)
else
mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
@@ -2076,7 +2075,7 @@
else
NONE
fun do_formula pos (ATyQuant (q, xs, phi)) =
- ATyQuant (q, map (ho_type_from_typ type_enc false 0) xs,
+ ATyQuant (q, map (apfst (ho_type_from_typ type_enc false 0)) xs,
do_formula pos phi)
| do_formula pos (AQuant (q, xs, phi)) =
let
@@ -2573,6 +2572,7 @@
val ind =
case type_enc of
Native _ =>
+ (* ### FIXME: get rid of that, and move to "atp_problem.ML" *)
if String.isPrefix type_const_prefix s orelse
String.isPrefix tfree_prefix s then
atype_of_types
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:40 2012 +0200
@@ -9,7 +9,7 @@
signature ATP_PROOF =
sig
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
- type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
+ type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
type 'a problem = 'a ATP_Problem.problem
exception UNRECOGNIZED_ATP_PROOF of unit
@@ -40,7 +40,7 @@
Definition_Step of step_name * 'a * 'a |
Inference_Step of step_name * 'a * string * step_name list
- type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
+ type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
val short_output : bool -> string -> string
val string_for_failure : failure -> string
@@ -55,7 +55,7 @@
val satallax_unsat_coreN : string
val parse_formula :
string list
- -> (string, 'a, (string, 'a) ho_term) formula * string list
+ -> (string, 'a, (string, 'a) ho_term, string) formula * string list
val atp_proof_from_tstplike_proof : string problem -> string -> string proof
val clean_up_atp_proof_dependencies : string proof -> string proof
val map_term_names_in_atp_proof :
@@ -222,7 +222,7 @@
Definition_Step of step_name * 'a * 'a |
Inference_Step of step_name * 'a * string * step_name list
-type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
+type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
fun step_name (Definition_Step (name, _, _)) = name
| step_name (Inference_Step (name, _, _, _)) = name
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 26 11:14:40 2012 +0200
@@ -9,7 +9,7 @@
signature ATP_PROOF_RECONSTRUCT =
sig
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
- type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
+ type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
type 'a proof = 'a ATP_Proof.proof
type stature = ATP_Problem_Generate.stature
@@ -60,7 +60,7 @@
-> (string, string) ho_term -> term
val prop_from_atp :
Proof.context -> bool -> int Symtab.table
- -> (string, string, (string, string) ho_term) formula -> term
+ -> (string, string, (string, string) ho_term, string) formula -> term
val isar_proof_text :
Proof.context -> bool -> isar_params -> one_line_params -> string
val proof_text :
@@ -326,7 +326,8 @@
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
exception HO_TERM of (string, string) ho_term list
-exception FORMULA of (string, string, (string, string) ho_term) formula list
+exception FORMULA of
+ (string, string, (string, string) ho_term, string) formula list
exception SAME of unit
(* Type variables are given the basic sort "HOL.type". Some will later be