--- a/src/HOL/Tools/ATP/atp_problem.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri May 27 10:30:07 2011 +0200
@@ -29,13 +29,12 @@
val tptp_fof : string
val tptp_tff : string
val tptp_thf : string
- val tptp_special_prefix : string
val tptp_has_type : string
val tptp_type_of_types : string
val tptp_bool_type : string
val tptp_individual_type : string
val tptp_fun_type : string
- val tptp_prod_type : string
+ val tptp_product_type : string
val tptp_forall : string
val tptp_exists : string
val tptp_not : string
@@ -50,18 +49,32 @@
val tptp_equal : string
val tptp_false : string
val tptp_true : string
- val is_atp_variable : string -> bool
+ val is_built_in_tptp_symbol : string -> bool
+ val is_tptp_variable : string -> bool
+ val is_tptp_user_symbol : string -> bool
val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val mk_aconn :
connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
-> ('a, 'b, 'c) 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
+ 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
+ val is_format_typed : format -> bool
val timestamp : unit -> string
val hashw : word * word -> word
val hashw_string : string * word -> word
val tptp_strings_for_atp_problem : format -> string problem -> string list
val filter_cnf_ueq_problem :
(string * string) problem -> (string * string) problem
+ val declare_undeclared_syms_in_atp_problem :
+ string -> string -> (string * string) problem -> (string * string) problem
val nice_atp_problem :
bool -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -96,13 +109,12 @@
val tptp_fof = "fof"
val tptp_tff = "tff"
val tptp_thf = "thf"
-val tptp_special_prefix = "$"
val tptp_has_type = ":"
val tptp_type_of_types = "$tType"
val tptp_bool_type = "$o"
val tptp_individual_type = "$i"
val tptp_fun_type = ">"
-val tptp_prod_type = "*"
+val tptp_product_type = "*"
val tptp_forall = "!"
val tptp_exists = "?"
val tptp_not = "~"
@@ -118,16 +130,42 @@
val tptp_false = "$false"
val tptp_true = "$true"
-fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
+fun is_built_in_tptp_symbol "equal" = true (* deprecated *)
+ | is_built_in_tptp_symbol s = not (Char.isAlpha (String.sub (s, 0)))
+fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
+val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
fun mk_anot (AConn (ANot, [phi])) = phi
| mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
+ | aconn_fold pos f (AImplies, [phi1, phi2]) =
+ f (Option.map not pos) phi1 #> f pos phi2
+ | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
+ | aconn_fold pos f (AOr, phis) = fold (f pos) phis
+ | aconn_fold _ f (_, phis) = fold (f NONE) phis
+
+fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
+ | aconn_map pos f (AImplies, [phi1, phi2]) =
+ AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
+ | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
+ | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
+ | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
+
+fun formula_fold pos f =
+ let
+ fun aux pos (AQuant (_, _, phi)) = aux pos phi
+ | aux pos (AConn conn) = aconn_fold pos aux conn
+ | aux pos (AAtom tm) = f pos tm
+ in aux pos end
+
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
| 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]
+
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
(* This hash function is recommended in "Compilers: Principles, Techniques, and
@@ -160,7 +198,7 @@
([], s) => s
| ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
| (ss, s) =>
- "(" ^ space_implode (" " ^ tptp_prod_type ^ " ") ss ^ ") " ^
+ "(" ^ space_implode (" " ^ tptp_product_type ^ " ") ss ^ ") " ^
tptp_fun_type ^ " " ^ s)
| string_for_type _ _ = raise Fail "unexpected type in untyped format"
@@ -256,7 +294,7 @@
| is_problem_line_cnf_ueq _ = false
fun open_conjecture_term (ATerm ((s, s'), tms)) =
- ATerm (if is_atp_variable s then (s |> Name.desymbolize false, s')
+ ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
else (s, s'), tms |> map open_conjecture_term)
fun open_formula conj (AQuant (AForall, _, phi)) = open_formula conj phi
| open_formula true (AAtom t) = AAtom (open_conjecture_term t)
@@ -280,6 +318,58 @@
in if length conjs = 1 then problem else [] end)
+(** Symbol declarations **)
+
+(* TFF allows implicit declarations of types, function symbols, and predicate
+ symbols (with "$i" as the type of individuals), but some provers (e.g.,
+ SNARK) require explicit declarations. The situation is similar for THF. *)
+
+val atype_of_types = AType (`I tptp_type_of_types)
+val bool_atype = AType (`I tptp_bool_type)
+val individual_atype = AType (`I tptp_individual_type)
+
+fun default_type pred_sym =
+ let
+ fun typ 0 = if pred_sym then bool_atype else individual_atype
+ | typ ary = AFun (individual_atype, typ (ary - 1))
+ in typ end
+
+fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
+ | add_declared_syms_in_problem_line _ = I
+fun declared_syms_in_problem problem =
+ fold (fold add_declared_syms_in_problem_line o snd) problem []
+
+fun undeclared_syms_in_problem declared problem =
+ let
+ fun do_sym name ty =
+ if member (op =) declared name then I else AList.default (op =) (name, ty)
+ fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2]
+ | do_type (AType name) = do_sym name (K atype_of_types)
+ fun do_term pred_sym (ATerm (name as (s, _), tms)) =
+ is_tptp_user_symbol s
+ ? do_sym name (fn _ => default_type pred_sym (length tms))
+ #> fold (do_term false) tms
+ fun do_formula (AQuant (_, xs, phi)) =
+ fold do_type (map_filter snd xs) #> do_formula phi
+ | do_formula (AConn (_, phis)) = fold do_formula phis
+ | do_formula (AAtom tm) = do_term true tm
+ fun do_problem_line (Decl (_, _, ty)) = do_type ty
+ | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
+ in
+ fold (fold do_problem_line o snd) problem []
+ |> filter_out (is_built_in_tptp_symbol o fst o fst)
+ end
+
+fun declare_undeclared_syms_in_atp_problem prefix heading problem =
+ let
+ fun decl_line (x as (s, _), ty) = Decl (prefix ^ s, x, ty ())
+ val declared = problem |> declared_syms_in_problem
+ val decls =
+ problem |> undeclared_syms_in_problem declared
+ |> sort_wrt (fst o fst)
+ |> map decl_line
+ in (heading, decls) :: problem end
+
(** Nice names **)
fun empty_name_pool readable_names =
@@ -325,7 +415,7 @@
fun nice_name (full_name, _) NONE = (full_name, NONE)
| nice_name (full_name, desired_name) (SOME the_pool) =
- if String.isPrefix tptp_special_prefix full_name then
+ if is_built_in_tptp_symbol full_name then
(full_name, SOME the_pool)
else case Symtab.lookup (fst the_pool) full_name of
SOME nice_name => (nice_name, SOME the_pool)
@@ -362,8 +452,7 @@
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
fun nice_problem_line (Decl (ident, sym, ty)) =
- nice_name sym ##>> nice_type ty
- #>> (fn (sym, ty) => Decl (ident, sym, ty))
+ nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Decl (ident, sym, ty))
| nice_problem_line (Formula (ident, kind, phi, source, info)) =
nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
fun nice_problem problem =
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri May 27 10:30:07 2011 +0200
@@ -378,7 +378,7 @@
let
fun do_term_pair _ NONE = NONE
| do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) =
- case pairself is_atp_variable (s1, s2) of
+ case pairself is_tptp_variable (s1, s2) of
(true, true) =>
(case AList.lookup (op =) subst s1 of
SOME s2' => if s2' = s2 then SOME subst else NONE
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 27 10:30:07 2011 +0200
@@ -364,7 +364,7 @@
| add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ _ = I
-fun repair_atp_variable_name f s =
+fun repair_tptp_variable_name f s =
let
fun subscript_name s n = s ^ nat_subscript n
val s = String.map f s
@@ -445,11 +445,11 @@
case strip_prefix_and_unascii schematic_var_prefix a of
SOME b => Var ((b, 0), T)
| NONE =>
- if is_atp_variable a then
- Var ((repair_atp_variable_name Char.toLower a, 0), T)
+ if is_tptp_variable a then
+ Var ((repair_tptp_variable_name Char.toLower a, 0), T)
else
(* Skolem constants? *)
- Var ((repair_atp_variable_name Char.toUpper a, 0), T)
+ Var ((repair_tptp_variable_name Char.toUpper a, 0), T)
in list_comb (t, ts) end
in aux (SOME HOLogic.boolT) [] end
@@ -514,7 +514,7 @@
#>> quantify_over_var (case q of
AForall => forall_of
| AExists => exists_of)
- (repair_atp_variable_name Char.toLower s)
+ (repair_tptp_variable_name Char.toLower s)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 27 10:30:07 2011 +0200
@@ -81,8 +81,9 @@
val readable_names =
Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
-val type_decl_prefix = "type_"
-val sym_decl_prefix = "sym_"
+val type_decl_prefix = "ty_"
+val sym_decl_prefix = "sy_"
+val sym_formula_prefix = "sym_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
@@ -184,27 +185,6 @@
fun is_setting_higher_order THF (Simple_Types _) = true
| is_setting_higher_order _ _ = false
-fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
- | aconn_fold pos f (AImplies, [phi1, phi2]) =
- f (Option.map not pos) phi1 #> f pos phi2
- | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
- | aconn_fold pos f (AOr, phis) = fold (f pos) phis
- | aconn_fold _ f (_, phis) = fold (f NONE) phis
-
-fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
- | aconn_map pos f (AImplies, [phi1, phi2]) =
- AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
- | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
- | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
- | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
-
-fun formula_fold pos f =
- let
- fun aux pos (AQuant (_, _, phi)) = aux pos phi
- | aux pos (AConn conn) = aconn_fold pos aux conn
- | aux pos (AAtom tm) = f pos tm
- in aux pos end
-
type translated_formula =
{name: string,
locality: locality,
@@ -282,8 +262,7 @@
fun close_combformula_universally phi = close_universally combterm_vars phi
fun term_vars (ATerm (name as (s, _), tms)) =
- is_atp_variable s ? insert (op =) (name, NONE)
- #> fold term_vars tms
+ is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
fun close_formula_universally phi = close_universally term_vars phi
val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
@@ -311,14 +290,15 @@
f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
^ ")"
+val bool_atype = AType (`I tptp_bool_type)
+
fun ho_type_from_fo_term higher_order pred_sym ary =
let
fun to_atype ty =
AType ((make_simple_type (generic_mangled_type_name fst ty),
generic_mangled_type_name snd ty))
fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
- fun to_fo 0 ty =
- if pred_sym then AType (`I tptp_bool_type) else to_atype ty
+ fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
| to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
fun to_ho (ty as ATerm ((s, _), tys)) =
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
@@ -1013,8 +993,7 @@
end
fun should_declare_sym type_sys pred_sym s =
- not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
- not (String.isPrefix tptp_special_prefix s) andalso
+ is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
(case type_sys of
Simple_Types _ => true
| Tags (_, _, Light) => true
@@ -1086,7 +1065,7 @@
Simple_Types level => (format = THF, [], level)
| _ => (false, replicate (length T_args) homo_infinite_type, No_Types)
in
- Decl (type_decl_prefix ^ s, (s, s'),
+ Decl (sym_decl_prefix ^ s, (s, s'),
(T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
|> mangled_type higher_order pred_sym (length T_arg_Ts + ary))
end
@@ -1108,7 +1087,7 @@
arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
else NONE)
in
- Formula (sym_decl_prefix ^ s ^
+ Formula (sym_formula_prefix ^ s ^
(if n > 1 then "_" ^ string_of_int j else ""), kind,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bounds
@@ -1126,7 +1105,7 @@
n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
val ident_base =
- sym_decl_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
+ sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
val (kind, maybe_negate) =
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
else (Axiom, I)
@@ -1173,74 +1152,50 @@
fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
(s, decls) =
- (if member (op =) [TFF, THF] format then
- decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
- else
- []) @
- (case type_sys of
- Simple_Types _ => []
- | Preds _ =>
- let
- val decls =
- case decls of
- decl :: (decls' as _ :: _) =>
- let val T = result_type_of_decl decl in
- if forall (curry (type_instance ctxt o swap) T
- o result_type_of_decl) decls' then
- [decl]
- else
- decls
- end
- | _ => decls
- val n = length decls
- val decls =
- decls
- |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
- o result_type_of_decl)
- in
- (0 upto length decls - 1, decls)
- |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
- nonmono_Ts type_sys n s)
- end
- | Tags (_, _, heaviness) =>
- (case heaviness of
- Heavy => []
- | Light =>
- let val n = length decls in
- (0 upto n - 1 ~~ decls)
- |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
- nonmono_Ts type_sys n s)
- end))
+ case type_sys of
+ Simple_Types _ =>
+ decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
+ | Preds _ =>
+ let
+ val decls =
+ case decls of
+ decl :: (decls' as _ :: _) =>
+ let val T = result_type_of_decl decl in
+ if forall (curry (type_instance ctxt o swap) T
+ o result_type_of_decl) decls' then
+ [decl]
+ else
+ decls
+ end
+ | _ => decls
+ val n = length decls
+ val decls =
+ decls
+ |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
+ o result_type_of_decl)
+ in
+ (0 upto length decls - 1, decls)
+ |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
+ nonmono_Ts type_sys n s)
+ end
+ | Tags (_, _, heaviness) =>
+ (case heaviness of
+ Heavy => []
+ | Light =>
+ let val n = length decls in
+ (0 upto n - 1 ~~ decls)
+ |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
+ nonmono_Ts type_sys n s)
+ end)
fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
type_sys sym_decl_tab =
- Symtab.fold_rev
- (append o problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
- type_sys)
- sym_decl_tab []
-
-fun add_simple_types_in_type (AFun (ty1, ty2)) =
- fold add_simple_types_in_type [ty1, ty2]
- | add_simple_types_in_type (AType name) = insert (op =) name
-
-fun add_simple_types_in_formula (AQuant (_, xs, phi)) =
- fold add_simple_types_in_type (map_filter snd xs)
- #> add_simple_types_in_formula phi
- | add_simple_types_in_formula (AConn (_, phis)) =
- fold add_simple_types_in_formula phis
- | add_simple_types_in_formula (AAtom _) = I
-
-fun add_simple_types_in_problem_line (Decl (_, _, ty)) =
- add_simple_types_in_type ty
- | add_simple_types_in_problem_line (Formula (_, _, phi, _, _)) =
- add_simple_types_in_formula phi
-
-fun simple_types_in_problem problem =
- fold (fold add_simple_types_in_problem_line o snd) problem []
- |> filter_out (String.isPrefix tptp_special_prefix o fst)
-
-fun decl_line_for_simple_type (s, s') =
- Decl (type_decl_prefix ^ s, (s, s'), AType (`I tptp_type_of_types))
+ sym_decl_tab
+ |> Symtab.dest
+ |> sort_wrt fst
+ |> rpair []
+ |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
+ nonmono_Ts type_sys)
fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
level = Nonmonotonic_Types orelse level = Finite_Types
@@ -1251,8 +1206,8 @@
if heading = needle then j
else offset_of_heading_in_problem needle problem (j + length lines)
-val type_declsN = "Types"
-val sym_declsN = "Symbol types"
+val implicit_declsN = "Should-be-implicit typings"
+val explicit_declsN = "Explicit typings"
val factsN = "Relevant facts"
val class_relsN = "Class relationships"
val aritiesN = "Arities"
@@ -1293,7 +1248,7 @@
(* Reordering these might confuse the proof reconstruction code or the SPASS
Flotter hack. *)
val problem =
- [(sym_declsN, sym_decl_lines),
+ [(explicit_declsN, sym_decl_lines),
(factsN,
map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
(0 upto length facts - 1 ~~ facts)),
@@ -1307,13 +1262,12 @@
formula_lines_for_free_types format type_sys (facts @ conjs))]
val problem =
problem
- |> (case type_sys of
- Simple_Types _ =>
- cons (type_declsN, problem |> simple_types_in_problem
- |> map decl_line_for_simple_type)
- | _ => I)
- val problem =
- problem |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
+ |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
+ |> (if is_format_typed format then
+ declare_undeclared_syms_in_atp_problem type_decl_prefix
+ implicit_declsN
+ else
+ I)
val (problem, pool) =
problem |> nice_atp_problem (Config.get ctxt readable_names)
val helpers_offset = offset_of_heading_in_problem helpersN problem 0
@@ -1348,8 +1302,7 @@
val type_info_default_weight = 0.8
fun add_term_weights weight (ATerm (s, tms)) =
- (not (is_atp_variable s) andalso s <> "equal" andalso
- not (String.isPrefix tptp_special_prefix s)) ? Symtab.default (s, weight)
+ is_tptp_user_symbol s ? Symtab.default (s, weight)
#> fold (add_term_weights weight) tms
fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
formula_fold NONE (K (add_term_weights weight)) phi
@@ -1380,7 +1333,7 @@
|> add_conjectures_weights (get free_typesN @ get conjsN)
|> add_facts_weights (get factsN)
|> fold (fold (add_problem_line_weights type_info_default_weight) o get)
- [sym_declsN, class_relsN, aritiesN]
+ [explicit_declsN, class_relsN, aritiesN]
|> Symtab.dest
|> sort (prod_ord Real.compare string_ord o pairself swap)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200
@@ -446,20 +446,14 @@
else
adjust_dumb_type_sys formats (Preds (Mangled_Monomorphic, level, Heavy))
| adjust_dumb_type_sys formats type_sys =
- if member (op =) formats FOF then
- (FOF, type_sys)
- else if member (op =) formats CNF_UEQ then
- (CNF_UEQ, case type_sys of
- Preds stuff =>
- (if is_type_sys_fairly_sound type_sys then Preds else Tags)
- stuff
- | _ => type_sys)
- else
- (* We could return "type_sys" unchanged for TFF but this would require the
- TFF and THF provers to accept problems in which some constants are
- implicitly declared. Today only ToFoF-E seems to meet this
- criterion. *)
- (hd formats, Simple_Types All_Types)
+ (case hd formats of
+ CNF_UEQ =>
+ (CNF_UEQ, case type_sys of
+ Preds stuff =>
+ (if is_type_sys_fairly_sound type_sys then Preds else Tags)
+ stuff
+ | _ => type_sys)
+ | format => (format, type_sys))
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
adjust_dumb_type_sys formats type_sys