--- 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