# HG changeset patch # User blanchet # Date 1306485007 -7200 # Node ID 1c80902d04567fb617a17906898ba2d7f2b0b44b # Parent 038bb26d74b0ff13d27b10978fa3b2fef2002a98 fully support all type system encodings in typed formats (TFF, THF) diff -r 038bb26d74b0 -r 1c80902d0456 src/HOL/Tools/ATP/atp_problem.ML --- 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 = diff -r 038bb26d74b0 -r 1c80902d0456 src/HOL/Tools/ATP/atp_proof.ML --- 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 diff -r 038bb26d74b0 -r 1c80902d0456 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- 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 diff -r 038bb26d74b0 -r 1c80902d0456 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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 diff -r 038bb26d74b0 -r 1c80902d0456 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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