killed needless datatype "combtyp" in Metis
authorblanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 42562f1d903f789b1
parent 42561 23ddc4e3d19c
child 42563 e70ffe3846d0
killed needless datatype "combtyp" in Metis
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -20,13 +20,9 @@
     1.4      ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
     1.5    datatype class_rel_clause =
     1.6      ClassRelClause of {name: string, subclass: name, superclass: name}
     1.7 -  datatype combtyp =
     1.8 -    CombTVar of name |
     1.9 -    CombTFree of name |
    1.10 -    CombType of name * combtyp list
    1.11    datatype combterm =
    1.12 -    CombConst of name * combtyp * combtyp list (* Const and Free *) |
    1.13 -    CombVar of name * combtyp |
    1.14 +    CombConst of name * typ * typ list (* Const and Free *) |
    1.15 +    CombVar of name * typ |
    1.16      CombApp of combterm * combterm
    1.17    datatype fol_literal = FOLLiteral of bool * combterm
    1.18  
    1.19 @@ -66,10 +62,8 @@
    1.20      theory -> class list -> class list -> class_rel_clause list
    1.21    val make_arity_clauses :
    1.22      theory -> string list -> class list -> class list * arity_clause list
    1.23 -  val dest_combfun : combtyp -> combtyp * combtyp
    1.24 -  val combtyp_of : combterm -> combtyp
    1.25 +  val combtyp_of : combterm -> typ
    1.26    val strip_combterm_comb : combterm -> combterm * combterm list
    1.27 -  val combtyp_from_typ : typ -> combtyp
    1.28    val combterm_from_term :
    1.29      theory -> (string * typ) list -> term -> combterm * typ list
    1.30    val reveal_old_skolem_terms : (string * term) list -> term -> term
    1.31 @@ -365,14 +359,9 @@
    1.32    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
    1.33    in  (classes', multi_arity_clause cpairs)  end;
    1.34  
    1.35 -datatype combtyp =
    1.36 -  CombTVar of name |
    1.37 -  CombTFree of name |
    1.38 -  CombType of name * combtyp list
    1.39 -
    1.40  datatype combterm =
    1.41 -  CombConst of name * combtyp * combtyp list (* Const and Free *) |
    1.42 -  CombVar of name * combtyp |
    1.43 +  CombConst of name * typ * typ list (* Const and Free *) |
    1.44 +  CombVar of name * typ |
    1.45    CombApp of combterm * combterm
    1.46  
    1.47  datatype fol_literal = FOLLiteral of bool * combterm
    1.48 @@ -381,13 +370,9 @@
    1.49  (* convert a clause with type Term.term to a clause with type clause *)
    1.50  (*********************************************************************)
    1.51  
    1.52 -(*Result of a function type; no need to check that the argument type matches.*)
    1.53 -fun dest_combfun (CombType (_, [ty1, ty2])) = (ty1, ty2)
    1.54 -  | dest_combfun _ = raise Fail "non-function type"
    1.55 -
    1.56 -fun combtyp_of (CombConst (_, tp, _)) = tp
    1.57 -  | combtyp_of (CombVar (_, tp)) = tp
    1.58 -  | combtyp_of (CombApp (t1, _)) = snd (dest_combfun (combtyp_of t1))
    1.59 +fun combtyp_of (CombConst (_, T, _)) = T
    1.60 +  | combtyp_of (CombVar (_, T)) = T
    1.61 +  | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
    1.62  
    1.63  (*gets the head of a combinator application, along with the list of arguments*)
    1.64  fun strip_combterm_comb u =
    1.65 @@ -395,25 +380,7 @@
    1.66          |   stripc  x =  x
    1.67      in stripc(u,[]) end
    1.68  
    1.69 -fun combtyp_and_sorts_from_type (Type (a, Ts)) =
    1.70 -    let val (tys, ts) = combtyps_and_sorts_from_types Ts in
    1.71 -      (CombType (`make_fixed_type_const a, tys), ts)
    1.72 -    end
    1.73 -  | combtyp_and_sorts_from_type (tp as TFree (a, _)) =
    1.74 -    (CombTFree (`make_fixed_type_var a), [tp])
    1.75 -  | combtyp_and_sorts_from_type (tp as TVar (x as (s, _), _)) =
    1.76 -    (CombTVar (make_schematic_type_var x, s), [tp])
    1.77 -and combtyps_and_sorts_from_types Ts =
    1.78 -  let val (tys, ts) = ListPair.unzip (map combtyp_and_sorts_from_type Ts) in
    1.79 -    (tys, union_all ts)
    1.80 -  end
    1.81 -
    1.82 -(* same as above, but no gathering of sort information *)
    1.83 -fun combtyp_from_typ (Type (a, Ts)) =
    1.84 -    CombType (`make_fixed_type_const a, map combtyp_from_typ Ts)
    1.85 -  | combtyp_from_typ (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
    1.86 -  | combtyp_from_typ (TVar (x as (s, _), _)) =
    1.87 -    CombTVar (make_schematic_type_var x, s)
    1.88 +fun atyps_of T = fold_atyps (insert (op =)) T []
    1.89  
    1.90  fun new_skolem_const_name s num_T_args =
    1.91    [new_skolem_const_prefix, s, string_of_int num_T_args]
    1.92 @@ -423,42 +390,40 @@
    1.93     infomation. *)
    1.94  fun combterm_from_term thy bs (P $ Q) =
    1.95        let
    1.96 -        val (P', tsP) = combterm_from_term thy bs P
    1.97 -        val (Q', tsQ) = combterm_from_term thy bs Q
    1.98 -      in (CombApp (P', Q'), union (op =) tsP tsQ) end
    1.99 +        val (P', P_atomics_Ts) = combterm_from_term thy bs P
   1.100 +        val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
   1.101 +      in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
   1.102    | combterm_from_term thy _ (Const (c, T)) =
   1.103        let
   1.104 -        val (tp, ts) = combtyp_and_sorts_from_type T
   1.105          val tvar_list =
   1.106            (if String.isPrefix old_skolem_const_prefix c then
   1.107               [] |> Term.add_tvarsT T |> map TVar
   1.108             else
   1.109               (c, T) |> Sign.const_typargs thy)
   1.110 -          |> map combtyp_from_typ
   1.111 -        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
   1.112 -      in  (c',ts)  end
   1.113 +        val c' = CombConst (`make_fixed_const c, T, tvar_list)
   1.114 +      in (c', atyps_of T) end
   1.115    | combterm_from_term _ _ (Free (v, T)) =
   1.116 -      let val (tp, ts) = combtyp_and_sorts_from_type T
   1.117 -          val v' = CombConst (`make_fixed_var v, tp, [])
   1.118 -      in  (v',ts)  end
   1.119 +      let
   1.120 +        val at = atyps_of T
   1.121 +        val v' = CombConst (`make_fixed_var v, T, [])
   1.122 +      in (v', atyps_of T) end
   1.123    | combterm_from_term _ _ (Var (v as (s, _), T)) =
   1.124      let
   1.125 -      val (tp, ts) = combtyp_and_sorts_from_type T
   1.126        val v' =
   1.127          if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
   1.128            let
   1.129 -            val tys = T |> strip_type |> swap |> op ::
   1.130 -            val s' = new_skolem_const_name s (length tys)
   1.131 -          in CombConst (`make_fixed_const s', tp, map combtyp_from_typ tys) end
   1.132 +            val Ts = T |> strip_type |> swap |> op ::
   1.133 +            val s' = new_skolem_const_name s (length Ts)
   1.134 +          in CombConst (`make_fixed_const s', T, Ts) end
   1.135          else
   1.136 -          CombVar ((make_schematic_var v, s), tp)
   1.137 -    in (v', ts) end
   1.138 +          CombVar ((make_schematic_var v, s), T)
   1.139 +    in (v', atyps_of T) end
   1.140    | combterm_from_term _ bs (Bound j) =
   1.141        let
   1.142          val (s, T) = nth bs j
   1.143 -        val (tp, ts) = combtyp_and_sorts_from_type T
   1.144 -        val v' = CombConst (`make_bound_var s, tp, [])
   1.145 -      in (v', ts) end
   1.146 +        val ts = atyps_of T
   1.147 +        val v' = CombConst (`make_bound_var s, T, [])
   1.148 +      in (v', atyps_of T) end
   1.149    | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
   1.150  
   1.151  fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
   1.152 @@ -580,32 +545,34 @@
   1.153  
   1.154  fun metis_lit b c args = (b, (c, args));
   1.155  
   1.156 -fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
   1.157 -  | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
   1.158 -  | metis_term_from_combtyp (CombType ((s, _), tps)) =
   1.159 -    Metis_Term.Fn (s, map metis_term_from_combtyp tps);
   1.160 +fun metis_term_from_typ (Type (s, Ts)) =
   1.161 +    Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts)
   1.162 +  | metis_term_from_typ (TFree (s, _)) =
   1.163 +    Metis_Term.Fn (make_fixed_type_var s, [])
   1.164 +  | metis_term_from_typ (TVar (x, _)) =
   1.165 +    Metis_Term.Var (make_schematic_type_var x)
   1.166  
   1.167  (*These two functions insert type literals before the real literals. That is the
   1.168    opposite order from TPTP linkup, but maybe OK.*)
   1.169  
   1.170  fun hol_term_to_fol_FO tm =
   1.171    case strip_combterm_comb tm of
   1.172 -      (CombConst ((c, _), _, tys), tms) =>
   1.173 -        let val tyargs = map metis_term_from_combtyp tys
   1.174 -            val args   = map hol_term_to_fol_FO tms
   1.175 +      (CombConst ((c, _), _, Ts), tms) =>
   1.176 +        let val tyargs = map metis_term_from_typ Ts
   1.177 +            val args = map hol_term_to_fol_FO tms
   1.178          in Metis_Term.Fn (c, tyargs @ args) end
   1.179      | (CombVar ((v, _), _), []) => Metis_Term.Var v
   1.180      | _ => raise Fail "non-first-order combterm"
   1.181  
   1.182 -fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
   1.183 -      Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
   1.184 +fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) =
   1.185 +      Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts)
   1.186    | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
   1.187    | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
   1.188         Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
   1.189  
   1.190  (*The fully-typed translation, to avoid type errors*)
   1.191 -fun tag_with_type tm ty =
   1.192 -  Metis_Term.Fn (type_tag_name, [tm, metis_term_from_combtyp ty])
   1.193 +fun tag_with_type tm T =
   1.194 +  Metis_Term.Fn (type_tag_name, [tm, metis_term_from_typ T])
   1.195  
   1.196  fun hol_term_to_fol_FT (CombVar ((s, _), ty)) =
   1.197      tag_with_type (Metis_Term.Var s) ty
   1.198 @@ -616,9 +583,10 @@
   1.199                    (combtyp_of tm)
   1.200  
   1.201  fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
   1.202 -      let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
   1.203 -          val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
   1.204 -          val lits = map hol_term_to_fol_FO tms
   1.205 +      let
   1.206 +        val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm
   1.207 +        val tylits = if p = "equal" then [] else map metis_term_from_typ Ts
   1.208 +        val lits = map hol_term_to_fol_FO tms
   1.209        in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
   1.210    | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
   1.211       (case strip_combterm_comb tm of
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     2.3 @@ -346,7 +346,7 @@
     2.4              [typ_u, term_u] =>
     2.5              aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
     2.6            | _ => raise FO_TERM us
     2.7 -        else if String.isPrefix type_prefix a then
     2.8 +        else if String.isPrefix tff_type_prefix a then
     2.9            @{const True} (* ignore TFF type information *)
    2.10          else case strip_prefix_and_unascii const_prefix a of
    2.11            SOME "equal" =>
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     3.3 @@ -24,7 +24,7 @@
     3.4    val boolify_base : string
     3.5    val explicit_app_base : string
     3.6    val type_pred_base : string
     3.7 -  val type_prefix : string
     3.8 +  val tff_type_prefix : string
     3.9    val is_type_system_sound : type_system -> bool
    3.10    val type_system_types_dangerous_types : type_system -> bool
    3.11    val num_atp_type_args : theory -> type_system -> string -> int
    3.12 @@ -59,9 +59,9 @@
    3.13  val boolify_base = "hBOOL"
    3.14  val explicit_app_base = "hAPP"
    3.15  val type_pred_base = "is"
    3.16 -val type_prefix = "ty_"
    3.17 +val tff_type_prefix = "ty_"
    3.18  
    3.19 -fun make_type ty = type_prefix ^ ascii_of ty
    3.20 +fun make_tff_type s = tff_type_prefix ^ ascii_of s
    3.21  
    3.22  (* official TPTP TFF syntax *)
    3.23  val tff_type_of_types = "$tType"
    3.24 @@ -73,13 +73,13 @@
    3.25  type translated_formula =
    3.26    {name: string,
    3.27     kind: formula_kind,
    3.28 -   combformula: (name, combtyp, combterm) formula,
    3.29 -   ctypes_sorts: typ list}
    3.30 +   combformula: (name, typ, combterm) formula,
    3.31 +   atomic_types: typ list}
    3.32  
    3.33  fun update_combformula f
    3.34 -        ({name, kind, combformula, ctypes_sorts} : translated_formula) =
    3.35 +        ({name, kind, combformula, atomic_types} : translated_formula) =
    3.36    {name = name, kind = kind, combformula = f combformula,
    3.37 -   ctypes_sorts = ctypes_sorts} : translated_formula
    3.38 +   atomic_types = atomic_types} : translated_formula
    3.39  
    3.40  fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
    3.41  
    3.42 @@ -165,29 +165,32 @@
    3.43    #> fold term_vars tms
    3.44  val close_formula_universally = close_universally term_vars
    3.45  
    3.46 -(* We are crossing our fingers that it doesn't clash with anything else. *)
    3.47 +fun fo_term_from_typ (Type (s, Ts)) =
    3.48 +    ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts)
    3.49 +  | fo_term_from_typ (TFree (s, _)) =
    3.50 +    ATerm (`make_fixed_type_var s, [])
    3.51 +  | fo_term_from_typ (TVar ((x as (s, _)), _)) =
    3.52 +    ATerm ((make_schematic_type_var x, s), [])
    3.53 +
    3.54 +(* This shouldn't clash with anything else. *)
    3.55  val mangled_type_sep = "\000"
    3.56  
    3.57 -fun mangled_combtyp_component f (CombTFree name) = f name
    3.58 -  | mangled_combtyp_component f (CombTVar name) =
    3.59 -    f name (* FIXME: shouldn't happen *)
    3.60 -    (* raise Fail "impossible schematic type variable" *)
    3.61 -  | mangled_combtyp_component f (CombType (name, tys)) =
    3.62 -    f name ^ "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")"
    3.63 +fun generic_mangled_type_name f (ATerm (name, [])) = f name
    3.64 +  | generic_mangled_type_name f (ATerm (name, tys)) =
    3.65 +    f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
    3.66 +val mangled_type_name =
    3.67 +  fo_term_from_typ
    3.68 +  #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
    3.69 +                generic_mangled_type_name snd ty))
    3.70  
    3.71 -fun mangled_combtyp ty =
    3.72 -  (make_type (mangled_combtyp_component fst ty),
    3.73 -   mangled_combtyp_component snd ty)
    3.74 -
    3.75 -fun mangled_type_suffix f g tys =
    3.76 +fun generic_mangled_type_suffix f g tys =
    3.77    fold_rev (curry (op ^) o g o prefix mangled_type_sep
    3.78 -            o mangled_combtyp_component f) tys ""
    3.79 -
    3.80 -fun mangled_const_name_fst ty_args s =
    3.81 -  s ^ mangled_type_suffix fst ascii_of ty_args
    3.82 -fun mangled_const_name_snd ty_args s' = s' ^ mangled_type_suffix snd I ty_args
    3.83 -fun mangled_const_name ty_args (s, s') =
    3.84 -  (mangled_const_name_fst ty_args s, mangled_const_name_snd ty_args s')
    3.85 +            o generic_mangled_type_name f) tys ""
    3.86 +fun mangled_const_name T_args (s, s') =
    3.87 +  let val ty_args = map fo_term_from_typ T_args in
    3.88 +    (s ^ generic_mangled_type_suffix fst ascii_of ty_args,
    3.89 +     s' ^ generic_mangled_type_suffix snd I ty_args)
    3.90 +  end
    3.91  
    3.92  val parse_mangled_ident =
    3.93    Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
    3.94 @@ -212,7 +215,7 @@
    3.95      (hd ss, map unmangled_type (tl ss))
    3.96    end
    3.97  
    3.98 -fun combformula_for_prop thy eq_as_iff =
    3.99 +fun combformula_from_prop thy eq_as_iff =
   3.100    let
   3.101      fun do_term bs t ts =
   3.102        combterm_from_term thy bs (Envir.eta_contract t)
   3.103 @@ -220,7 +223,7 @@
   3.104      fun do_quant bs q s T t' =
   3.105        let val s = Name.variant (map fst bs) s in
   3.106          do_formula ((s, T) :: bs) t'
   3.107 -        #>> mk_aquant q [(`make_bound_var s, SOME (combtyp_from_typ T))]
   3.108 +        #>> mk_aquant q [(`make_bound_var s, SOME T)]
   3.109        end
   3.110      and do_conn bs c t1 t2 =
   3.111        do_formula bs t1 ##>> do_formula bs t2
   3.112 @@ -334,11 +337,11 @@
   3.113                |> perhaps (try (HOLogic.dest_Trueprop))
   3.114                |> introduce_combinators_in_term ctxt kind
   3.115                |> kind <> Axiom ? freeze_term
   3.116 -    val (combformula, ctypes_sorts) =
   3.117 -      combformula_for_prop thy eq_as_iff t []
   3.118 +    val (combformula, atomic_types) =
   3.119 +      combformula_from_prop thy eq_as_iff t []
   3.120    in
   3.121      {name = name, combformula = combformula, kind = kind,
   3.122 -     ctypes_sorts = ctypes_sorts}
   3.123 +     atomic_types = atomic_types}
   3.124    end
   3.125  
   3.126  fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), t) =
   3.127 @@ -374,17 +377,7 @@
   3.128               |> close_formula_universally, NONE, NONE)
   3.129    end
   3.130  
   3.131 -(* FIXME #### : abolish combtyp altogether *)
   3.132 -fun typ_from_combtyp (CombType ((s, _), tys)) =
   3.133 -    Type (s |> strip_prefix_and_unascii type_const_prefix |> the
   3.134 -            |> invert_const,
   3.135 -          map typ_from_combtyp tys)
   3.136 -  | typ_from_combtyp (CombTFree (s, _)) =
   3.137 -    TFree (s |> strip_prefix_and_unascii tfree_prefix |> the, HOLogic.typeS)
   3.138 -  | typ_from_combtyp (CombTVar (s, _)) =
   3.139 -    TVar ((s |> strip_prefix_and_unascii tvar_prefix |> the, 0), HOLogic.typeS)
   3.140 -
   3.141 -fun helper_facts_for_typed_const ctxt type_sys s (_, _, ty) =
   3.142 +fun helper_facts_for_typed_const ctxt type_sys s (_, _, T) =
   3.143    case strip_prefix_and_unascii const_prefix s of
   3.144      SOME s'' =>
   3.145      let
   3.146 @@ -395,8 +388,7 @@
   3.147          ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
   3.148            false),
   3.149           th |> prop_of
   3.150 -            |> specialize_type thy (invert_const unmangled_s,
   3.151 -                                    typ_from_combtyp ty))
   3.152 +            |> specialize_type thy (invert_const unmangled_s, T))
   3.153        fun make_facts eq_as_iff =
   3.154          map_filter (make_fact ctxt false eq_as_iff false)
   3.155      in
   3.156 @@ -488,17 +480,12 @@
   3.157  
   3.158  fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t])
   3.159  
   3.160 -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   3.161 -  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   3.162 -  | fo_term_for_combtyp (CombType (name, tys)) =
   3.163 -    ATerm (name, map fo_term_for_combtyp tys)
   3.164 -
   3.165 -fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   3.166 +fun fo_literal_from_type_literal (TyLitVar (class, name)) =
   3.167      (true, ATerm (class, [ATerm (name, [])]))
   3.168 -  | fo_literal_for_type_literal (TyLitFree (class, name)) =
   3.169 +  | fo_literal_from_type_literal (TyLitFree (class, name)) =
   3.170      (true, ATerm (class, [ATerm (name, [])]))
   3.171  
   3.172 -fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   3.173 +fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   3.174  
   3.175  (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
   3.176     considered dangerous because their "exhaust" properties can easily lead to
   3.177 @@ -524,29 +511,17 @@
   3.178        | [] => true
   3.179    end
   3.180  
   3.181 -fun is_combtyp_dangerous ctxt (CombType ((s, _), tys)) =
   3.182 -    (case strip_prefix_and_unascii type_const_prefix s of
   3.183 -       SOME s' => forall (is_combtyp_dangerous ctxt) tys andalso
   3.184 -                  is_type_constr_dangerous ctxt (invert_const s')
   3.185 -     | NONE => false)
   3.186 -  | is_combtyp_dangerous _ _ = false
   3.187 -
   3.188 -fun should_tag_with_type ctxt (Tags full_types) ty =
   3.189 -    full_types orelse is_combtyp_dangerous ctxt ty
   3.190 +fun should_tag_with_type ctxt (Tags full_types) T =
   3.191 +    full_types orelse is_type_dangerous ctxt T
   3.192    | should_tag_with_type _ _ _ = false
   3.193  
   3.194 -fun pred_combtyp ty =
   3.195 -  case combtyp_from_typ @{typ "unit => bool"} of
   3.196 -    CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty])
   3.197 -  | _ => raise Fail "expected two-argument type constructor"
   3.198 -
   3.199 -fun type_pred_combatom type_sys ty tm =
   3.200 -  CombApp (CombConst (`make_fixed_const type_pred_base, pred_combtyp ty, [ty]),
   3.201 -           tm)
   3.202 +fun type_pred_combatom type_sys T tm =
   3.203 +  CombApp (CombConst (`make_fixed_const type_pred_base,
   3.204 +                      T --> HOLogic.boolT, [T]), tm)
   3.205    |> repair_combterm_consts type_sys
   3.206    |> AAtom
   3.207  
   3.208 -fun formula_for_combformula ctxt type_sys =
   3.209 +fun formula_from_combformula ctxt type_sys =
   3.210    let
   3.211      fun do_term top_level u =
   3.212        let
   3.213 @@ -556,23 +531,23 @@
   3.214              CombConst (name, _, ty_args) => (name, ty_args)
   3.215            | CombVar (name, _) => (name, [])
   3.216            | CombApp _ => raise Fail "impossible \"CombApp\""
   3.217 -        val t = ATerm (x, map fo_term_for_combtyp ty_args @
   3.218 +        val t = ATerm (x, map fo_term_from_typ ty_args @
   3.219                            map (do_term false) args)
   3.220          val ty = combtyp_of u
   3.221        in
   3.222          t |> (if not top_level andalso
   3.223                   should_tag_with_type ctxt type_sys ty then
   3.224 -                tag_with_type (fo_term_for_combtyp ty)
   3.225 +                tag_with_type (fo_term_from_typ ty)
   3.226                else
   3.227                  I)
   3.228        end
   3.229      val do_bound_type =
   3.230 -      if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE
   3.231 +      if type_sys = Many_Typed then SOME o mangled_type_name else K NONE
   3.232      val do_out_of_bound_type =
   3.233        if member (op =) [Mangled true, Args true] type_sys then
   3.234          (fn (s, ty) =>
   3.235              type_pred_combatom type_sys ty (CombVar (s, ty))
   3.236 -            |> formula_for_combformula ctxt type_sys |> SOME)
   3.237 +            |> formula_from_combformula ctxt type_sys |> SOME)
   3.238        else
   3.239          K NONE
   3.240      fun do_formula (AQuant (q, xs, phi)) =
   3.241 @@ -588,11 +563,11 @@
   3.242    in do_formula end
   3.243  
   3.244  fun formula_for_fact ctxt type_sys
   3.245 -                     ({combformula, ctypes_sorts, ...} : translated_formula) =
   3.246 -  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   3.247 -                (atp_type_literals_for_types type_sys Axiom ctypes_sorts))
   3.248 -           (formula_for_combformula ctxt type_sys
   3.249 -                                    (close_combformula_universally combformula))
   3.250 +                     ({combformula, atomic_types, ...} : translated_formula) =
   3.251 +  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
   3.252 +                (atp_type_literals_for_types type_sys Axiom atomic_types))
   3.253 +           (formula_from_combformula ctxt type_sys
   3.254 +                (close_combformula_universally combformula))
   3.255    |> close_formula_universally
   3.256  
   3.257  fun logic_for_type_sys Many_Typed = Tff
   3.258 @@ -616,34 +591,34 @@
   3.259               |> close_formula_universally, NONE, NONE)
   3.260    end
   3.261  
   3.262 -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   3.263 +fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
   3.264      (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   3.265 -  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   3.266 +  | fo_literal_from_arity_literal (TVarLit (c, sort)) =
   3.267      (false, ATerm (c, [ATerm (sort, [])]))
   3.268  
   3.269  fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   3.270                                                  ...}) =
   3.271    Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
   3.272 -           mk_ahorn (map (formula_for_fo_literal o apfst not
   3.273 -                          o fo_literal_for_arity_literal) premLits)
   3.274 -                    (formula_for_fo_literal
   3.275 -                         (fo_literal_for_arity_literal conclLit))
   3.276 +           mk_ahorn (map (formula_from_fo_literal o apfst not
   3.277 +                          o fo_literal_from_arity_literal) premLits)
   3.278 +                    (formula_from_fo_literal
   3.279 +                         (fo_literal_from_arity_literal conclLit))
   3.280             |> close_formula_universally, NONE, NONE)
   3.281  
   3.282  fun formula_line_for_conjecture ctxt type_sys
   3.283          ({name, kind, combformula, ...} : translated_formula) =
   3.284    Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
   3.285 -           formula_for_combformula ctxt type_sys
   3.286 -                                   (close_combformula_universally combformula)
   3.287 +           formula_from_combformula ctxt type_sys
   3.288 +                                    (close_combformula_universally combformula)
   3.289             |> close_formula_universally, NONE, NONE)
   3.290  
   3.291 -fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
   3.292 -  ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture
   3.293 -               |> map fo_literal_for_type_literal
   3.294 +fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
   3.295 +  atomic_types |> atp_type_literals_for_types type_sys Conjecture
   3.296 +               |> map fo_literal_from_type_literal
   3.297  
   3.298  fun formula_line_for_free_type j lit =
   3.299    Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
   3.300 -           formula_for_fo_literal lit, NONE, NONE)
   3.301 +           formula_from_fo_literal lit, NONE, NONE)
   3.302  fun formula_lines_for_free_types type_sys facts =
   3.303    let
   3.304      val litss = map (free_type_literals type_sys) facts
   3.305 @@ -720,8 +695,7 @@
   3.306    | NONE => false
   3.307  
   3.308  val boolify_combconst =
   3.309 -  CombConst (`make_fixed_const boolify_base,
   3.310 -             combtyp_from_typ @{typ "bool => bool"}, [])
   3.311 +  CombConst (`make_fixed_const boolify_base, @{typ "bool => bool"}, [])
   3.312  fun boolify tm = CombApp (boolify_combconst, tm)
   3.313  
   3.314  fun repair_pred_syms_in_combterm sym_tab tm =
   3.315 @@ -732,15 +706,13 @@
   3.316  
   3.317  fun list_app head args = fold (curry (CombApp o swap)) args head
   3.318  
   3.319 -val fun_name = `make_fixed_type_const @{type_name fun}
   3.320 -
   3.321  fun explicit_app arg head =
   3.322    let
   3.323 -    val head_ty = combtyp_of head
   3.324 -    val (arg_ty, res_ty) = dest_combfun head_ty
   3.325 +    val head_T = combtyp_of head
   3.326 +    val (arg_T, res_T) = dest_funT head_T
   3.327      val explicit_app =
   3.328 -      CombConst (`make_fixed_const explicit_app_base,
   3.329 -                 CombType (fun_name, [head_ty, head_ty]), [arg_ty, res_ty])
   3.330 +      CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
   3.331 +                 [arg_T, res_T])
   3.332    in list_app explicit_app [head, arg] end
   3.333  fun list_explicit_app head args = fold explicit_app args head
   3.334  
   3.335 @@ -786,43 +758,39 @@
   3.336    Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys
   3.337                    ? fold (consider_fact_consts type_sys sym_tab) facts
   3.338  
   3.339 -fun strip_and_map_combtyp 0 f ty = ([], f ty)
   3.340 -  | strip_and_map_combtyp n f (ty as CombType ((s, _), tys)) =
   3.341 -    (case (strip_prefix_and_unascii type_const_prefix s, tys) of
   3.342 -       (SOME @{type_name fun}, [dom_ty, ran_ty]) =>
   3.343 -       strip_and_map_combtyp (n - 1) f ran_ty |>> cons (f dom_ty)
   3.344 -     | _ => ([], f ty))
   3.345 -  | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
   3.346 +fun strip_and_map_type 0 f T = ([], f T)
   3.347 +  | strip_and_map_type n f (Type (@{type_name fun}, [dom_T, ran_T])) =
   3.348 +    strip_and_map_type (n - 1) f ran_T |>> cons (f dom_T)
   3.349 +  | strip_and_map_type _ _ _ = raise Fail "unexpected non-function"
   3.350  
   3.351 -fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, ty) =
   3.352 +fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, T) =
   3.353    let val arity = min_arity_of sym_tab s in
   3.354      if type_sys = Many_Typed then
   3.355        let
   3.356 -        val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty
   3.357 +        val (arg_Ts, res_T) = strip_and_map_type arity mangled_type_name T
   3.358          val (s, s') = (s, s') |> mangled_const_name ty_args
   3.359        in
   3.360 -        Decl (sym_decl_prefix ^ ascii_of s, (s, s'),
   3.361 -              arg_tys,
   3.362 +        Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_Ts,
   3.363                (* ### FIXME: put that in typed_const_tab *)
   3.364 -              if is_pred_sym sym_tab s then `I tff_bool_type else res_ty)
   3.365 +              if is_pred_sym sym_tab s then `I tff_bool_type else res_T)
   3.366        end
   3.367      else
   3.368        let
   3.369 -        val (arg_tys, res_ty) = strip_and_map_combtyp arity I ty
   3.370 +        val (arg_Ts, res_T) = strip_and_map_type arity I T
   3.371          val bounds =
   3.372 -          map (`I o make_bound_var o string_of_int) (1 upto length arg_tys)
   3.373 -          ~~ map SOME arg_tys
   3.374 +          map (`I o make_bound_var o string_of_int) (1 upto length arg_Ts)
   3.375 +          ~~ map SOME arg_Ts
   3.376          val bound_tms =
   3.377 -          map (fn (name, ty) => CombConst (name, the ty, [])) bounds
   3.378 +          map (fn (name, T) => CombConst (name, the T, [])) bounds
   3.379          val freshener =
   3.380            case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
   3.381        in
   3.382          Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
   3.383 -                 CombConst ((s, s'), ty, ty_args)
   3.384 +                 CombConst ((s, s'), T, ty_args)
   3.385                   |> fold (curry (CombApp o swap)) bound_tms
   3.386 -                 |> type_pred_combatom type_sys res_ty
   3.387 +                 |> type_pred_combatom type_sys res_T
   3.388                   |> mk_aquant AForall bounds
   3.389 -                 |> formula_for_combformula ctxt type_sys,
   3.390 +                 |> formula_from_combformula ctxt type_sys,
   3.391                   NONE, NONE)
   3.392        end
   3.393    end
   3.394 @@ -840,8 +808,8 @@
   3.395      fold add_tff_types_in_formula phis
   3.396    | add_tff_types_in_formula (AAtom _) = I
   3.397  
   3.398 -fun add_tff_types_in_problem_line (Decl (_, _, arg_tys, res_ty)) =
   3.399 -    union (op =) (res_ty :: arg_tys)
   3.400 +fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
   3.401 +    union (op =) (res_T :: arg_Ts)
   3.402    | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) =
   3.403      add_tff_types_in_formula phi
   3.404