author blanchet Wed, 17 Aug 2011 10:03:58 +0200 changeset 44235 85e9dad3c187 parent 44234 17ae4af434aa child 44236 b73b7832b384 child 44244 567fb5f5c639
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
 src/HOL/Tools/ATP/atp_problem.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 16 15:02:20 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Aug 17 10:03:58 2011 +0200
@@ -19,7 +19,14 @@

datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type

-  datatype format = CNF | CNF_UEQ | FOF | TFF | THF
+  datatype thf_flavor = Without_Choice | With_Choice
+  datatype format =
+    CNF |
+    CNF_UEQ |
+    FOF |
+    TFF |
+    THF of thf_flavor
+
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
@@ -73,6 +80,7 @@
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
+  val is_format_thf : format -> bool
val is_format_typed : format -> bool
val tptp_lines_for_atp_problem : format -> string problem -> string list
val ensure_cnf_problem :
@@ -107,7 +115,14 @@

datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type

-datatype format = CNF | CNF_UEQ | FOF | TFF | THF
+datatype thf_flavor = Without_Choice | With_Choice
+datatype format =
+  CNF |
+  CNF_UEQ |
+  FOF |
+  TFF |
+  THF of thf_flavor
+
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
@@ -189,7 +204,11 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)

-val is_format_typed = member (op =) [TFF, THF]
+fun is_format_thf (THF _) = true
+  | is_format_thf _ = false
+fun is_format_typed TFF = true
+  | is_format_typed (THF _) = true
+  | is_format_typed _ = false

fun string_for_kind Axiom = "axiom"
| string_for_kind Definition = "definition"
@@ -202,7 +221,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 (THF _) ty =
let
fun aux _ (AType s) = s
| aux rhs (AFun (ty1, ty2)) =
@@ -228,7 +247,7 @@
| string_for_connective AIff = tptp_iff

fun string_for_bound_var format (s, ty) =
-  s ^ (if format = TFF orelse format = THF then
+  s ^ (if is_format_typed format then
" " ^ tptp_has_type ^ " " ^
string_for_type format (ty |> the_default (AType tptp_individual_type))
else
@@ -241,7 +260,7 @@
"[" ^ commas (map (string_for_term format) ts) ^ "]"
else if is_tptp_equal s then
space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
-      |> format = THF ? enclose "(" ")"
+      |> is_format_thf format ? enclose "(" ")"
else
(case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of
(true, [AAbs ((s', ty), tm)]) =>
@@ -252,14 +271,14 @@
[(s', SOME ty)], AAtom tm))
| _ =>
let val ss = map (string_for_term format) ts in
-           if format = THF then
+           if is_format_thf format then
"(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
else
s ^ "(" ^ commas ss ^ ")"
end)
-  | string_for_term THF (AAbs ((s, ty), tm)) =
-    "(^[" ^ s ^ " : " ^ string_for_type THF ty ^ "] : " ^
-    string_for_term THF tm ^ ")"
+  | string_for_term (format as THF _) (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"
and string_for_formula format (AQuant (q, xs, phi)) =
string_for_quantifier q ^
@@ -270,10 +289,10 @@
(AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
(map (string_for_term format) ts)
-    |> format = THF ? enclose "(" ")"
+    |> is_format_thf format ? enclose "(" ")"
| string_for_formula format (AConn (c, [phi])) =
string_for_connective c ^ " " ^
-    (string_for_formula format phi |> format = THF ? enclose "(" ")")
+    (string_for_formula format phi |> is_format_thf format ? enclose "(" ")")
|> enclose "(" ")"
| string_for_formula format (AConn (c, phis)) =
space_implode (" " ^ string_for_connective c ^ " ")
@@ -290,7 +309,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 (THF _) = tptp_thf

fun string_for_problem_line format (Decl (ident, sym, ty)) =
string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^```
```--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 16 15:02:20 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 17 10:03:58 2011 +0200
@@ -242,7 +242,7 @@
known_failures = [],
conj_sym_kind = Axiom,
prem_kind = Hypothesis,
-   formats = [THF, FOF],
+   formats = [THF Without_Choice, FOF],
best_slices = fn ctxt =>
(* FUDGE *)
[(0.667, (false, (150, "simple_higher", sosN))),
@@ -265,7 +265,7 @@
known_failures = [(ProofMissing, "SZS status Theorem")],
conj_sym_kind = Axiom,
prem_kind = Hypothesis,
-   formats = [THF],
+   formats = [THF With_Choice],
best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}

val satallax = (satallaxN, satallax_config)```
```--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 16 15:02:20 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 17 10:03:58 2011 +0200
@@ -604,12 +604,14 @@
val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc

fun choose_format formats (Simple_Types (order, level)) =
-    if member (op =) formats THF then
-      (THF, Simple_Types (order, level))
-    else if member (op =) formats TFF then
-      (TFF, Simple_Types (First_Order, level))
-    else
-      choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight))
+    (case find_first is_format_thf formats of
+       SOME format => (format, Simple_Types (order, level))
+     | NONE =>
+       if member (op =) formats TFF then
+         (TFF, Simple_Types (First_Order, level))
+       else
+         choose_format formats
+                       (Guards (Mangled_Monomorphic, level, Heavyweight)))
| choose_format formats type_enc =
(case hd formats of
CNF_UEQ =>
@@ -760,7 +762,7 @@
(true, @{type_name bool}) => `I tptp_bool_type
| (true, @{type_name fun}) => `I tptp_fun_type
| _ => if s = homo_infinite_type_name andalso
-                       (format = TFF orelse format = THF) then
+                       is_format_typed format then
`I tptp_individual_type
else
`make_fixed_type_const s,```