--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:04:23 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:34 2011 +0200
@@ -19,14 +19,15 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
- datatype tff_flavor = Implicit | Explicit
- datatype thf_flavor = Without_Choice | With_Choice
+ datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
+ datatype tff_explicitness = TFF_Implicit | TFF_Explicit
+ datatype thf_flavor = THF_Without_Choice | THF_With_Choice
datatype format =
CNF |
CNF_UEQ |
FOF |
- TFF of tff_flavor |
- THF of thf_flavor
+ TFF of tff_polymorphism * tff_explicitness |
+ THF0 of thf_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -119,15 +120,16 @@
datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
-datatype tff_flavor = Implicit | Explicit
-datatype thf_flavor = Without_Choice | With_Choice
+datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
+datatype tff_explicitness = TFF_Implicit | TFF_Explicit
+datatype thf_flavor = THF_Without_Choice | THF_With_Choice
datatype format =
CNF |
CNF_UEQ |
FOF |
- TFF of tff_flavor |
- THF of thf_flavor
+ TFF of tff_polymorphism * tff_explicitness |
+ THF0 of thf_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -211,10 +213,10 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
-fun is_format_thf (THF _) = true
+fun is_format_thf (THF0 _) = true
| is_format_thf _ = false
fun is_format_typed (TFF _) = true
- | is_format_typed (THF _) = true
+ | is_format_typed (THF0 _) = true
| is_format_typed _ = false
fun string_for_kind Axiom = "axiom"
@@ -228,7 +230,7 @@
raise Fail "unexpected higher-order type in first-order format"
| strip_tff_type (AType s) = ([], s)
-fun string_for_type (THF _) ty =
+fun string_for_type (THF0 _) ty =
let
fun aux _ (AType s) = s
| aux rhs (AFun (ty1, ty2)) =
@@ -270,7 +272,7 @@
|> is_format_thf format ? enclose "(" ")"
else
(case (s = tptp_ho_forall orelse s = tptp_ho_exists,
- s = tptp_choice andalso format = THF With_Choice, ts) of
+ s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
(true, _, [AAbs ((s', ty), tm)]) =>
(* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
possible, to work around LEO-II 1.2.8 parser limitation. *)
@@ -291,7 +293,7 @@
else
s ^ "(" ^ commas ss ^ ")"
end)
- | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
+ | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
"(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
string_for_term format tm ^ ")"
| string_for_term _ _ = raise Fail "unexpected term in first-order format"
@@ -324,7 +326,7 @@
| string_for_format CNF_UEQ = tptp_cnf
| string_for_format FOF = tptp_fof
| string_for_format (TFF _) = tptp_tff
- | string_for_format (THF _) = tptp_thf
+ | string_for_format (THF0 _) = tptp_thf
fun string_for_problem_line format (Decl (ident, sym, ty)) =
string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^