# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID f1d903f789b108f883ae639a26ff0f4135e37c98 # Parent 23ddc4e3d19c6d5e174ea3bf6f970121021f3878 killed needless datatype "combtyp" in Metis diff -r 23ddc4e3d19c -r f1d903f789b1 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Sun May 01 18:37:24 2011 +0200 @@ -20,13 +20,9 @@ ArityClause of {name: string, conclLit: arLit, premLits: arLit list} datatype class_rel_clause = ClassRelClause of {name: string, subclass: name, superclass: name} - datatype combtyp = - CombTVar of name | - CombTFree of name | - CombType of name * combtyp list datatype combterm = - CombConst of name * combtyp * combtyp list (* Const and Free *) | - CombVar of name * combtyp | + CombConst of name * typ * typ list (* Const and Free *) | + CombVar of name * typ | CombApp of combterm * combterm datatype fol_literal = FOLLiteral of bool * combterm @@ -66,10 +62,8 @@ theory -> class list -> class list -> class_rel_clause list val make_arity_clauses : theory -> string list -> class list -> class list * arity_clause list - val dest_combfun : combtyp -> combtyp * combtyp - val combtyp_of : combterm -> combtyp + val combtyp_of : combterm -> typ val strip_combterm_comb : combterm -> combterm * combterm list - val combtyp_from_typ : typ -> combtyp val combterm_from_term : theory -> (string * typ) list -> term -> combterm * typ list val reveal_old_skolem_terms : (string * term) list -> term -> term @@ -365,14 +359,9 @@ let val (classes', cpairs) = iter_type_class_pairs thy tycons classes in (classes', multi_arity_clause cpairs) end; -datatype combtyp = - CombTVar of name | - CombTFree of name | - CombType of name * combtyp list - datatype combterm = - CombConst of name * combtyp * combtyp list (* Const and Free *) | - CombVar of name * combtyp | + CombConst of name * typ * typ list (* Const and Free *) | + CombVar of name * typ | CombApp of combterm * combterm datatype fol_literal = FOLLiteral of bool * combterm @@ -381,13 +370,9 @@ (* convert a clause with type Term.term to a clause with type clause *) (*********************************************************************) -(*Result of a function type; no need to check that the argument type matches.*) -fun dest_combfun (CombType (_, [ty1, ty2])) = (ty1, ty2) - | dest_combfun _ = raise Fail "non-function type" - -fun combtyp_of (CombConst (_, tp, _)) = tp - | combtyp_of (CombVar (_, tp)) = tp - | combtyp_of (CombApp (t1, _)) = snd (dest_combfun (combtyp_of t1)) +fun combtyp_of (CombConst (_, T, _)) = T + | combtyp_of (CombVar (_, T)) = T + | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1)) (*gets the head of a combinator application, along with the list of arguments*) fun strip_combterm_comb u = @@ -395,25 +380,7 @@ | stripc x = x in stripc(u,[]) end -fun combtyp_and_sorts_from_type (Type (a, Ts)) = - let val (tys, ts) = combtyps_and_sorts_from_types Ts in - (CombType (`make_fixed_type_const a, tys), ts) - end - | combtyp_and_sorts_from_type (tp as TFree (a, _)) = - (CombTFree (`make_fixed_type_var a), [tp]) - | combtyp_and_sorts_from_type (tp as TVar (x as (s, _), _)) = - (CombTVar (make_schematic_type_var x, s), [tp]) -and combtyps_and_sorts_from_types Ts = - let val (tys, ts) = ListPair.unzip (map combtyp_and_sorts_from_type Ts) in - (tys, union_all ts) - end - -(* same as above, but no gathering of sort information *) -fun combtyp_from_typ (Type (a, Ts)) = - CombType (`make_fixed_type_const a, map combtyp_from_typ Ts) - | combtyp_from_typ (TFree (a, _)) = CombTFree (`make_fixed_type_var a) - | combtyp_from_typ (TVar (x as (s, _), _)) = - CombTVar (make_schematic_type_var x, s) +fun atyps_of T = fold_atyps (insert (op =)) T [] fun new_skolem_const_name s num_T_args = [new_skolem_const_prefix, s, string_of_int num_T_args] @@ -423,42 +390,40 @@ infomation. *) fun combterm_from_term thy bs (P $ Q) = let - val (P', tsP) = combterm_from_term thy bs P - val (Q', tsQ) = combterm_from_term thy bs Q - in (CombApp (P', Q'), union (op =) tsP tsQ) end + val (P', P_atomics_Ts) = combterm_from_term thy bs P + val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q + in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end | combterm_from_term thy _ (Const (c, T)) = let - val (tp, ts) = combtyp_and_sorts_from_type T val tvar_list = (if String.isPrefix old_skolem_const_prefix c then [] |> Term.add_tvarsT T |> map TVar else (c, T) |> Sign.const_typargs thy) - |> map combtyp_from_typ - val c' = CombConst (`make_fixed_const c, tp, tvar_list) - in (c',ts) end + val c' = CombConst (`make_fixed_const c, T, tvar_list) + in (c', atyps_of T) end | combterm_from_term _ _ (Free (v, T)) = - let val (tp, ts) = combtyp_and_sorts_from_type T - val v' = CombConst (`make_fixed_var v, tp, []) - in (v',ts) end + let + val at = atyps_of T + val v' = CombConst (`make_fixed_var v, T, []) + in (v', atyps_of T) end | combterm_from_term _ _ (Var (v as (s, _), T)) = let - val (tp, ts) = combtyp_and_sorts_from_type T val v' = if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then let - val tys = T |> strip_type |> swap |> op :: - val s' = new_skolem_const_name s (length tys) - in CombConst (`make_fixed_const s', tp, map combtyp_from_typ tys) end + val Ts = T |> strip_type |> swap |> op :: + val s' = new_skolem_const_name s (length Ts) + in CombConst (`make_fixed_const s', T, Ts) end else - CombVar ((make_schematic_var v, s), tp) - in (v', ts) end + CombVar ((make_schematic_var v, s), T) + in (v', atyps_of T) end | combterm_from_term _ bs (Bound j) = let val (s, T) = nth bs j - val (tp, ts) = combtyp_and_sorts_from_type T - val v' = CombConst (`make_bound_var s, tp, []) - in (v', ts) end + val ts = atyps_of T + val v' = CombConst (`make_bound_var s, T, []) + in (v', atyps_of T) end | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) @@ -580,32 +545,34 @@ fun metis_lit b c args = (b, (c, args)); -fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s - | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, []) - | metis_term_from_combtyp (CombType ((s, _), tps)) = - Metis_Term.Fn (s, map metis_term_from_combtyp tps); +fun metis_term_from_typ (Type (s, Ts)) = + Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts) + | metis_term_from_typ (TFree (s, _)) = + Metis_Term.Fn (make_fixed_type_var s, []) + | metis_term_from_typ (TVar (x, _)) = + Metis_Term.Var (make_schematic_type_var x) (*These two functions insert type literals before the real literals. That is the opposite order from TPTP linkup, but maybe OK.*) fun hol_term_to_fol_FO tm = case strip_combterm_comb tm of - (CombConst ((c, _), _, tys), tms) => - let val tyargs = map metis_term_from_combtyp tys - val args = map hol_term_to_fol_FO tms + (CombConst ((c, _), _, Ts), tms) => + let val tyargs = map metis_term_from_typ Ts + val args = map hol_term_to_fol_FO tms in Metis_Term.Fn (c, tyargs @ args) end | (CombVar ((v, _), _), []) => Metis_Term.Var v | _ => raise Fail "non-first-order combterm" -fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = - Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) +fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) = + Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts) | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s | hol_term_to_fol_HO (CombApp (tm1, tm2)) = Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); (*The fully-typed translation, to avoid type errors*) -fun tag_with_type tm ty = - Metis_Term.Fn (type_tag_name, [tm, metis_term_from_combtyp ty]) +fun tag_with_type tm T = + Metis_Term.Fn (type_tag_name, [tm, metis_term_from_typ T]) fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = tag_with_type (Metis_Term.Var s) ty @@ -616,9 +583,10 @@ (combtyp_of tm) fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = - let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm - val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys - val lits = map hol_term_to_fol_FO tms + let + val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm + val tylits = if p = "equal" then [] else map metis_term_from_typ Ts + val lits = map hol_term_to_fol_FO tms in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = (case strip_combterm_comb tm of diff -r 23ddc4e3d19c -r f1d903f789b1 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200 @@ -346,7 +346,7 @@ [typ_u, term_u] => aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u | _ => raise FO_TERM us - else if String.isPrefix type_prefix a then + else if String.isPrefix tff_type_prefix a then @{const True} (* ignore TFF type information *) else case strip_prefix_and_unascii const_prefix a of SOME "equal" => diff -r 23ddc4e3d19c -r f1d903f789b1 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 @@ -24,7 +24,7 @@ val boolify_base : string val explicit_app_base : string val type_pred_base : string - val type_prefix : string + val tff_type_prefix : string val is_type_system_sound : type_system -> bool val type_system_types_dangerous_types : type_system -> bool val num_atp_type_args : theory -> type_system -> string -> int @@ -59,9 +59,9 @@ val boolify_base = "hBOOL" val explicit_app_base = "hAPP" val type_pred_base = "is" -val type_prefix = "ty_" +val tff_type_prefix = "ty_" -fun make_type ty = type_prefix ^ ascii_of ty +fun make_tff_type s = tff_type_prefix ^ ascii_of s (* official TPTP TFF syntax *) val tff_type_of_types = "$tType" @@ -73,13 +73,13 @@ type translated_formula = {name: string, kind: formula_kind, - combformula: (name, combtyp, combterm) formula, - ctypes_sorts: typ list} + combformula: (name, typ, combterm) formula, + atomic_types: typ list} fun update_combformula f - ({name, kind, combformula, ctypes_sorts} : translated_formula) = + ({name, kind, combformula, atomic_types} : translated_formula) = {name = name, kind = kind, combformula = f combformula, - ctypes_sorts = ctypes_sorts} : translated_formula + atomic_types = atomic_types} : translated_formula fun fact_lift f ({combformula, ...} : translated_formula) = f combformula @@ -165,29 +165,32 @@ #> fold term_vars tms val close_formula_universally = close_universally term_vars -(* We are crossing our fingers that it doesn't clash with anything else. *) +fun fo_term_from_typ (Type (s, Ts)) = + ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts) + | fo_term_from_typ (TFree (s, _)) = + ATerm (`make_fixed_type_var s, []) + | fo_term_from_typ (TVar ((x as (s, _)), _)) = + ATerm ((make_schematic_type_var x, s), []) + +(* This shouldn't clash with anything else. *) val mangled_type_sep = "\000" -fun mangled_combtyp_component f (CombTFree name) = f name - | mangled_combtyp_component f (CombTVar name) = - f name (* FIXME: shouldn't happen *) - (* raise Fail "impossible schematic type variable" *) - | mangled_combtyp_component f (CombType (name, tys)) = - f name ^ "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" +fun generic_mangled_type_name f (ATerm (name, [])) = f name + | generic_mangled_type_name f (ATerm (name, tys)) = + f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")" +val mangled_type_name = + fo_term_from_typ + #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty), + generic_mangled_type_name snd ty)) -fun mangled_combtyp ty = - (make_type (mangled_combtyp_component fst ty), - mangled_combtyp_component snd ty) - -fun mangled_type_suffix f g tys = +fun generic_mangled_type_suffix f g tys = fold_rev (curry (op ^) o g o prefix mangled_type_sep - o mangled_combtyp_component f) tys "" - -fun mangled_const_name_fst ty_args s = - s ^ mangled_type_suffix fst ascii_of ty_args -fun mangled_const_name_snd ty_args s' = s' ^ mangled_type_suffix snd I ty_args -fun mangled_const_name ty_args (s, s') = - (mangled_const_name_fst ty_args s, mangled_const_name_snd ty_args s') + o generic_mangled_type_name f) tys "" +fun mangled_const_name T_args (s, s') = + let val ty_args = map fo_term_from_typ T_args in + (s ^ generic_mangled_type_suffix fst ascii_of ty_args, + s' ^ generic_mangled_type_suffix snd I ty_args) + end val parse_mangled_ident = Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode @@ -212,7 +215,7 @@ (hd ss, map unmangled_type (tl ss)) end -fun combformula_for_prop thy eq_as_iff = +fun combformula_from_prop thy eq_as_iff = let fun do_term bs t ts = combterm_from_term thy bs (Envir.eta_contract t) @@ -220,7 +223,7 @@ fun do_quant bs q s T t' = let val s = Name.variant (map fst bs) s in do_formula ((s, T) :: bs) t' - #>> mk_aquant q [(`make_bound_var s, SOME (combtyp_from_typ T))] + #>> mk_aquant q [(`make_bound_var s, SOME T)] end and do_conn bs c t1 t2 = do_formula bs t1 ##>> do_formula bs t2 @@ -334,11 +337,11 @@ |> perhaps (try (HOLogic.dest_Trueprop)) |> introduce_combinators_in_term ctxt kind |> kind <> Axiom ? freeze_term - val (combformula, ctypes_sorts) = - combformula_for_prop thy eq_as_iff t [] + val (combformula, atomic_types) = + combformula_from_prop thy eq_as_iff t [] in {name = name, combformula = combformula, kind = kind, - ctypes_sorts = ctypes_sorts} + atomic_types = atomic_types} end fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), t) = @@ -374,17 +377,7 @@ |> close_formula_universally, NONE, NONE) end -(* FIXME #### : abolish combtyp altogether *) -fun typ_from_combtyp (CombType ((s, _), tys)) = - Type (s |> strip_prefix_and_unascii type_const_prefix |> the - |> invert_const, - map typ_from_combtyp tys) - | typ_from_combtyp (CombTFree (s, _)) = - TFree (s |> strip_prefix_and_unascii tfree_prefix |> the, HOLogic.typeS) - | typ_from_combtyp (CombTVar (s, _)) = - TVar ((s |> strip_prefix_and_unascii tvar_prefix |> the, 0), HOLogic.typeS) - -fun helper_facts_for_typed_const ctxt type_sys s (_, _, ty) = +fun helper_facts_for_typed_const ctxt type_sys s (_, _, T) = case strip_prefix_and_unascii const_prefix s of SOME s'' => let @@ -395,8 +388,7 @@ ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), false), th |> prop_of - |> specialize_type thy (invert_const unmangled_s, - typ_from_combtyp ty)) + |> specialize_type thy (invert_const unmangled_s, T)) fun make_facts eq_as_iff = map_filter (make_fact ctxt false eq_as_iff false) in @@ -488,17 +480,12 @@ fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) - | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) - | fo_term_for_combtyp (CombType (name, tys)) = - ATerm (name, map fo_term_for_combtyp tys) - -fun fo_literal_for_type_literal (TyLitVar (class, name)) = +fun fo_literal_from_type_literal (TyLitVar (class, name)) = (true, ATerm (class, [ATerm (name, [])])) - | fo_literal_for_type_literal (TyLitFree (class, name)) = + | fo_literal_from_type_literal (TyLitFree (class, name)) = (true, ATerm (class, [ATerm (name, [])])) -fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot +fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are considered dangerous because their "exhaust" properties can easily lead to @@ -524,29 +511,17 @@ | [] => true end -fun is_combtyp_dangerous ctxt (CombType ((s, _), tys)) = - (case strip_prefix_and_unascii type_const_prefix s of - SOME s' => forall (is_combtyp_dangerous ctxt) tys andalso - is_type_constr_dangerous ctxt (invert_const s') - | NONE => false) - | is_combtyp_dangerous _ _ = false - -fun should_tag_with_type ctxt (Tags full_types) ty = - full_types orelse is_combtyp_dangerous ctxt ty +fun should_tag_with_type ctxt (Tags full_types) T = + full_types orelse is_type_dangerous ctxt T | should_tag_with_type _ _ _ = false -fun pred_combtyp ty = - case combtyp_from_typ @{typ "unit => bool"} of - CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty]) - | _ => raise Fail "expected two-argument type constructor" - -fun type_pred_combatom type_sys ty tm = - CombApp (CombConst (`make_fixed_const type_pred_base, pred_combtyp ty, [ty]), - tm) +fun type_pred_combatom type_sys T tm = + CombApp (CombConst (`make_fixed_const type_pred_base, + T --> HOLogic.boolT, [T]), tm) |> repair_combterm_consts type_sys |> AAtom -fun formula_for_combformula ctxt type_sys = +fun formula_from_combformula ctxt type_sys = let fun do_term top_level u = let @@ -556,23 +531,23 @@ CombConst (name, _, ty_args) => (name, ty_args) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_for_combtyp ty_args @ + val t = ATerm (x, map fo_term_from_typ ty_args @ map (do_term false) args) val ty = combtyp_of u in t |> (if not top_level andalso should_tag_with_type ctxt type_sys ty then - tag_with_type (fo_term_for_combtyp ty) + tag_with_type (fo_term_from_typ ty) else I) end val do_bound_type = - if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE + if type_sys = Many_Typed then SOME o mangled_type_name else K NONE val do_out_of_bound_type = if member (op =) [Mangled true, Args true] type_sys then (fn (s, ty) => type_pred_combatom type_sys ty (CombVar (s, ty)) - |> formula_for_combformula ctxt type_sys |> SOME) + |> formula_from_combformula ctxt type_sys |> SOME) else K NONE fun do_formula (AQuant (q, xs, phi)) = @@ -588,11 +563,11 @@ in do_formula end fun formula_for_fact ctxt type_sys - ({combformula, ctypes_sorts, ...} : translated_formula) = - mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) - (atp_type_literals_for_types type_sys Axiom ctypes_sorts)) - (formula_for_combformula ctxt type_sys - (close_combformula_universally combformula)) + ({combformula, atomic_types, ...} : translated_formula) = + mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) + (atp_type_literals_for_types type_sys Axiom atomic_types)) + (formula_from_combformula ctxt type_sys + (close_combformula_universally combformula)) |> close_formula_universally fun logic_for_type_sys Many_Typed = Tff @@ -616,34 +591,34 @@ |> close_formula_universally, NONE, NONE) end -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = +fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | fo_literal_for_arity_literal (TVarLit (c, sort)) = + | fo_literal_from_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits, ...}) = Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom, - mk_ahorn (map (formula_for_fo_literal o apfst not - o fo_literal_for_arity_literal) premLits) - (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit)) + mk_ahorn (map (formula_from_fo_literal o apfst not + o fo_literal_from_arity_literal) premLits) + (formula_from_fo_literal + (fo_literal_from_arity_literal conclLit)) |> close_formula_universally, NONE, NONE) fun formula_line_for_conjecture ctxt type_sys ({name, kind, combformula, ...} : translated_formula) = Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind, - formula_for_combformula ctxt type_sys - (close_combformula_universally combformula) + formula_from_combformula ctxt type_sys + (close_combformula_universally combformula) |> close_formula_universally, NONE, NONE) -fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) = - ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture - |> map fo_literal_for_type_literal +fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) = + atomic_types |> atp_type_literals_for_types type_sys Conjecture + |> map fo_literal_from_type_literal fun formula_line_for_free_type j lit = Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis, - formula_for_fo_literal lit, NONE, NONE) + formula_from_fo_literal lit, NONE, NONE) fun formula_lines_for_free_types type_sys facts = let val litss = map (free_type_literals type_sys) facts @@ -720,8 +695,7 @@ | NONE => false val boolify_combconst = - CombConst (`make_fixed_const boolify_base, - combtyp_from_typ @{typ "bool => bool"}, []) + CombConst (`make_fixed_const boolify_base, @{typ "bool => bool"}, []) fun boolify tm = CombApp (boolify_combconst, tm) fun repair_pred_syms_in_combterm sym_tab tm = @@ -732,15 +706,13 @@ fun list_app head args = fold (curry (CombApp o swap)) args head -val fun_name = `make_fixed_type_const @{type_name fun} - fun explicit_app arg head = let - val head_ty = combtyp_of head - val (arg_ty, res_ty) = dest_combfun head_ty + val head_T = combtyp_of head + val (arg_T, res_T) = dest_funT head_T val explicit_app = - CombConst (`make_fixed_const explicit_app_base, - CombType (fun_name, [head_ty, head_ty]), [arg_ty, res_ty]) + CombConst (`make_fixed_const explicit_app_base, head_T --> head_T, + [arg_T, res_T]) in list_app explicit_app [head, arg] end fun list_explicit_app head args = fold explicit_app args head @@ -786,43 +758,39 @@ Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys ? fold (consider_fact_consts type_sys sym_tab) facts -fun strip_and_map_combtyp 0 f ty = ([], f ty) - | strip_and_map_combtyp n f (ty as CombType ((s, _), tys)) = - (case (strip_prefix_and_unascii type_const_prefix s, tys) of - (SOME @{type_name fun}, [dom_ty, ran_ty]) => - strip_and_map_combtyp (n - 1) f ran_ty |>> cons (f dom_ty) - | _ => ([], f ty)) - | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function" +fun strip_and_map_type 0 f T = ([], f T) + | strip_and_map_type n f (Type (@{type_name fun}, [dom_T, ran_T])) = + strip_and_map_type (n - 1) f ran_T |>> cons (f dom_T) + | strip_and_map_type _ _ _ = raise Fail "unexpected non-function" -fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, ty) = +fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, T) = let val arity = min_arity_of sym_tab s in if type_sys = Many_Typed then let - val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty + val (arg_Ts, res_T) = strip_and_map_type arity mangled_type_name T val (s, s') = (s, s') |> mangled_const_name ty_args in - Decl (sym_decl_prefix ^ ascii_of s, (s, s'), - arg_tys, + Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_Ts, (* ### FIXME: put that in typed_const_tab *) - if is_pred_sym sym_tab s then `I tff_bool_type else res_ty) + if is_pred_sym sym_tab s then `I tff_bool_type else res_T) end else let - val (arg_tys, res_ty) = strip_and_map_combtyp arity I ty + val (arg_Ts, res_T) = strip_and_map_type arity I T val bounds = - map (`I o make_bound_var o string_of_int) (1 upto length arg_tys) - ~~ map SOME arg_tys + map (`I o make_bound_var o string_of_int) (1 upto length arg_Ts) + ~~ map SOME arg_Ts val bound_tms = - map (fn (name, ty) => CombConst (name, the ty, [])) bounds + map (fn (name, T) => CombConst (name, the T, [])) bounds val freshener = case type_sys of Args _ => string_of_int j ^ "_" | _ => "" in Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom, - CombConst ((s, s'), ty, ty_args) + CombConst ((s, s'), T, ty_args) |> fold (curry (CombApp o swap)) bound_tms - |> type_pred_combatom type_sys res_ty + |> type_pred_combatom type_sys res_T |> mk_aquant AForall bounds - |> formula_for_combformula ctxt type_sys, + |> formula_from_combformula ctxt type_sys, NONE, NONE) end end @@ -840,8 +808,8 @@ fold add_tff_types_in_formula phis | add_tff_types_in_formula (AAtom _) = I -fun add_tff_types_in_problem_line (Decl (_, _, arg_tys, res_ty)) = - union (op =) (res_ty :: arg_tys) +fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) = + union (op =) (res_T :: arg_Ts) | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) = add_tff_types_in_formula phi