split Type_Infer into early and late part, after Proof_Context;
authorwenzelm
Tue Apr 19 20:47:02 2011 +0200 (2011-04-19)
changeset 4240513ecdb3057d8
parent 42404 fbd136946b35
child 42406 05f2468d6b36
split Type_Infer into early and late part, after Proof_Context;
added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;
src/Pure/IsaMakefile
src/Pure/Isar/proof_context.ML
src/Pure/ROOT.ML
src/Pure/type_infer.ML
src/Pure/type_infer_context.ML
src/Tools/nbe.ML
src/Tools/subtyping.ML
     1.1 --- a/src/Pure/IsaMakefile	Tue Apr 19 16:13:04 2011 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Tue Apr 19 20:47:02 2011 +0200
     1.3 @@ -253,6 +253,7 @@
     1.4    thm.ML						\
     1.5    type.ML						\
     1.6    type_infer.ML						\
     1.7 +  type_infer_context.ML					\
     1.8    unify.ML						\
     1.9    variable.ML
    1.10  	@./mk
     2.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 19 16:13:04 2011 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 19 20:47:02 2011 +0200
     2.3 @@ -76,7 +76,6 @@
     2.4    val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
     2.5    val check_tvar: Proof.context -> indexname * sort -> indexname * sort
     2.6    val check_tfree: Proof.context -> string * sort -> string * sort
     2.7 -  val standard_infer_types: Proof.context -> term list -> term list
     2.8    val intern_skolem: Proof.context -> string -> string option
     2.9    val read_term_pattern: Proof.context -> string -> term
    2.10    val read_term_schematic: Proof.context -> string -> term
    2.11 @@ -678,25 +677,18 @@
    2.12  end;
    2.13  
    2.14  
    2.15 -(* type checking/inference *)
    2.16 +(* check/uncheck *)
    2.17  
    2.18  fun def_type ctxt =
    2.19    let val Mode {pattern, ...} = get_mode ctxt
    2.20    in Variable.def_type ctxt pattern end;
    2.21  
    2.22 -fun standard_infer_types ctxt =
    2.23 -  Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt);
    2.24 -
    2.25  local
    2.26  
    2.27  fun standard_typ_check ctxt =
    2.28    map (cert_typ_mode (Type.get_mode ctxt) ctxt) #>
    2.29    map (prepare_patternT ctxt);
    2.30  
    2.31 -fun standard_term_check ctxt =
    2.32 -  standard_infer_types ctxt #>
    2.33 -  map (expand_abbrevs ctxt);
    2.34 -
    2.35  fun standard_term_uncheck ctxt =
    2.36    map (contract_abbrevs ctxt);
    2.37  
    2.38 @@ -704,7 +696,6 @@
    2.39  
    2.40  val _ = Context.>>
    2.41   (Syntax.add_typ_check 0 "standard" standard_typ_check #>
    2.42 -  Syntax.add_term_check 0 "standard" standard_term_check #>
    2.43    Syntax.add_term_check 100 "fixate" prepare_patterns #>
    2.44    Syntax.add_term_uncheck 0 "standard" standard_term_uncheck);
    2.45  
     3.1 --- a/src/Pure/ROOT.ML	Tue Apr 19 16:13:04 2011 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Tue Apr 19 20:47:02 2011 +0200
     3.3 @@ -173,6 +173,7 @@
     3.4  use "type_infer.ML";
     3.5  use "Syntax/local_syntax.ML";
     3.6  use "Isar/proof_context.ML";
     3.7 +use "type_infer_context.ML";
     3.8  use "Syntax/syntax_phases.ML";
     3.9  use "Isar/local_defs.ML";
    3.10  
     4.1 --- a/src/Pure/type_infer.ML	Tue Apr 19 16:13:04 2011 +0200
     4.2 +++ b/src/Pure/type_infer.ML	Tue Apr 19 20:47:02 2011 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      Pure/type_infer.ML
     4.5      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     4.6  
     4.7 -Representation of type-inference problems.  Simple type inference.
     4.8 +Basic representation of type-inference problems.
     4.9  *)
    4.10  
    4.11  signature TYPE_INFER =
    4.12 @@ -18,10 +18,6 @@
    4.13    val deref: typ Vartab.table -> typ -> typ
    4.14    val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    4.15    val fixate: Proof.context -> term list -> term list
    4.16 -  val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) ->
    4.17 -    term list -> int * term list
    4.18 -  val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
    4.19 -    term list -> term list
    4.20  end;
    4.21  
    4.22  structure Type_Infer: TYPE_INFER =
    4.23 @@ -70,96 +66,6 @@
    4.24  
    4.25  
    4.26  
    4.27 -(** prepare types/terms: create inference parameters **)
    4.28 -
    4.29 -(* prepare_typ *)
    4.30 -
    4.31 -fun prepare_typ typ params_idx =
    4.32 -  let
    4.33 -    val (params', idx) = fold_atyps
    4.34 -      (fn TVar (xi, S) =>
    4.35 -          (fn ps_idx as (ps, idx) =>
    4.36 -            if is_param xi andalso not (Vartab.defined ps xi)
    4.37 -            then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx)
    4.38 -        | _ => I) typ params_idx;
    4.39 -
    4.40 -    fun prepare (T as Type (a, Ts)) idx =
    4.41 -          if T = dummyT then (mk_param idx [], idx + 1)
    4.42 -          else
    4.43 -            let val (Ts', idx') = fold_map prepare Ts idx
    4.44 -            in (Type (a, Ts'), idx') end
    4.45 -      | prepare (T as TVar (xi, _)) idx =
    4.46 -          (case Vartab.lookup params' xi of
    4.47 -            NONE => T
    4.48 -          | SOME p => p, idx)
    4.49 -      | prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1)
    4.50 -      | prepare (T as TFree _) idx = (T, idx);
    4.51 -
    4.52 -    val (typ', idx') = prepare typ idx;
    4.53 -  in (typ', (params', idx')) end;
    4.54 -
    4.55 -
    4.56 -(* prepare_term *)
    4.57 -
    4.58 -fun prepare_term ctxt const_type tm (vparams, params, idx) =
    4.59 -  let
    4.60 -    fun add_vparm xi (ps_idx as (ps, idx)) =
    4.61 -      if not (Vartab.defined ps xi) then
    4.62 -        (Vartab.update (xi, mk_param idx []) ps, idx + 1)
    4.63 -      else ps_idx;
    4.64 -
    4.65 -    val (vparams', idx') = fold_aterms
    4.66 -      (fn Var (_, Type ("_polymorphic_", _)) => I
    4.67 -        | Var (xi, _) => add_vparm xi
    4.68 -        | Free (x, _) => add_vparm (x, ~1)
    4.69 -        | _ => I)
    4.70 -      tm (vparams, idx);
    4.71 -    fun var_param xi = the (Vartab.lookup vparams' xi);
    4.72 -
    4.73 -    fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx));
    4.74 -
    4.75 -    fun constraint T t ps =
    4.76 -      if T = dummyT then (t, ps)
    4.77 -      else
    4.78 -        let val (T', ps') = prepare_typ T ps
    4.79 -        in (Type.constraint T' t, ps') end;
    4.80 -
    4.81 -    fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
    4.82 -          let
    4.83 -            fun err () =
    4.84 -              error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
    4.85 -            val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
    4.86 -            val (A', ps_idx') = prepare_typ A ps_idx;
    4.87 -            val (t', ps_idx'') = prepare t ps_idx';
    4.88 -          in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
    4.89 -      | prepare (Const (c, T)) (ps, idx) =
    4.90 -          (case const_type c of
    4.91 -            SOME U =>
    4.92 -              let val (U', idx') = polyT_of U idx
    4.93 -              in constraint T (Const (c, U')) (ps, idx') end
    4.94 -          | NONE => error ("Undeclared constant: " ^ quote c))
    4.95 -      | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
    4.96 -          let val (T', idx') = polyT_of T idx
    4.97 -          in (Var (xi, T'), (ps, idx')) end
    4.98 -      | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx
    4.99 -      | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx
   4.100 -      | prepare (Bound i) ps_idx = (Bound i, ps_idx)
   4.101 -      | prepare (Abs (x, T, t)) ps_idx =
   4.102 -          let
   4.103 -            val (T', ps_idx') = prepare_typ T ps_idx;
   4.104 -            val (t', ps_idx'') = prepare t ps_idx';
   4.105 -          in (Abs (x, T', t'), ps_idx'') end
   4.106 -      | prepare (t $ u) ps_idx =
   4.107 -          let
   4.108 -            val (t', ps_idx') = prepare t ps_idx;
   4.109 -            val (u', ps_idx'') = prepare u ps_idx';
   4.110 -          in (t' $ u', ps_idx'') end;
   4.111 -
   4.112 -    val (tm', (params', idx'')) = prepare tm (params, idx');
   4.113 -  in (tm', (vparams', params', idx'')) end;
   4.114 -
   4.115 -
   4.116 -
   4.117  (** results **)
   4.118  
   4.119  (* dereferenced views *)
   4.120 @@ -219,149 +125,4 @@
   4.121      val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
   4.122    in (map o map_types) (Term_Subst.instantiateT inst) ts end;
   4.123  
   4.124 -
   4.125 -
   4.126 -(** order-sorted unification of types **)
   4.127 -
   4.128 -exception NO_UNIFIER of string * typ Vartab.table;
   4.129 -
   4.130 -fun unify ctxt =
   4.131 -  let
   4.132 -    val thy = Proof_Context.theory_of ctxt;
   4.133 -    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
   4.134 -
   4.135 -
   4.136 -    (* adjust sorts of parameters *)
   4.137 -
   4.138 -    fun not_of_sort x S' S =
   4.139 -      "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
   4.140 -        Syntax.string_of_sort ctxt S;
   4.141 -
   4.142 -    fun meet (_, []) tye_idx = tye_idx
   4.143 -      | meet (Type (a, Ts), S) (tye_idx as (tye, _)) =
   4.144 -          meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
   4.145 -      | meet (TFree (x, S'), S) (tye_idx as (tye, _)) =
   4.146 -          if Sign.subsort thy (S', S) then tye_idx
   4.147 -          else raise NO_UNIFIER (not_of_sort x S' S, tye)
   4.148 -      | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
   4.149 -          if Sign.subsort thy (S', S) then tye_idx
   4.150 -          else if is_param xi then
   4.151 -            (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
   4.152 -          else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
   4.153 -    and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
   4.154 -          meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
   4.155 -      | meets _ tye_idx = tye_idx;
   4.156 -
   4.157 -
   4.158 -    (* occurs check and assignment *)
   4.159 -
   4.160 -    fun occurs_check tye xi (TVar (xi', _)) =
   4.161 -          if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
   4.162 -          else
   4.163 -            (case Vartab.lookup tye xi' of
   4.164 -              NONE => ()
   4.165 -            | SOME T => occurs_check tye xi T)
   4.166 -      | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts
   4.167 -      | occurs_check _ _ _ = ();
   4.168 -
   4.169 -    fun assign xi (T as TVar (xi', _)) S env =
   4.170 -          if xi = xi' then env
   4.171 -          else env |> meet (T, S) |>> Vartab.update_new (xi, T)
   4.172 -      | assign xi T S (env as (tye, _)) =
   4.173 -          (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T));
   4.174 -
   4.175 -
   4.176 -    (* unification *)
   4.177 -
   4.178 -    fun show_tycon (a, Ts) =
   4.179 -      quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
   4.180 -
   4.181 -    fun unif (T1, T2) (env as (tye, _)) =
   4.182 -      (case pairself (`is_paramT o deref tye) (T1, T2) of
   4.183 -        ((true, TVar (xi, S)), (_, T)) => assign xi T S env
   4.184 -      | ((_, T), (true, TVar (xi, S))) => assign xi T S env
   4.185 -      | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
   4.186 -          if a <> b then
   4.187 -            raise NO_UNIFIER
   4.188 -              ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
   4.189 -          else fold unif (Ts ~~ Us) env
   4.190 -      | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye));
   4.191 -
   4.192 -  in unif end;
   4.193 -
   4.194 -
   4.195 -
   4.196 -(** simple type inference **)
   4.197 -
   4.198 -(* infer *)
   4.199 -
   4.200 -fun infer ctxt =
   4.201 -  let
   4.202 -    (* errors *)
   4.203 -
   4.204 -    fun prep_output tye bs ts Ts =
   4.205 -      let
   4.206 -        val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts);
   4.207 -        val (Ts', Ts'') = chop (length Ts) Ts_bTs';
   4.208 -        fun prep t =
   4.209 -          let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
   4.210 -          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
   4.211 -      in (map prep ts', Ts') end;
   4.212 -
   4.213 -    fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
   4.214 -
   4.215 -    fun unif_failed msg =
   4.216 -      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
   4.217 -
   4.218 -    fun err_appl msg tye bs t T u U =
   4.219 -      let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
   4.220 -      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
   4.221 -
   4.222 -
   4.223 -    (* main *)
   4.224 -
   4.225 -    fun inf _ (Const (_, T)) tye_idx = (T, tye_idx)
   4.226 -      | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
   4.227 -      | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
   4.228 -      | inf bs (Bound i) tye_idx =
   4.229 -          (snd (nth bs i handle Subscript => err_loose i), tye_idx)
   4.230 -      | inf bs (Abs (x, T, t)) tye_idx =
   4.231 -          let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
   4.232 -          in (T --> U, tye_idx') end
   4.233 -      | inf bs (t $ u) tye_idx =
   4.234 -          let
   4.235 -            val (T, tye_idx') = inf bs t tye_idx;
   4.236 -            val (U, (tye, idx)) = inf bs u tye_idx';
   4.237 -            val V = mk_param idx [];
   4.238 -            val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
   4.239 -              handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
   4.240 -          in (V, tye_idx'') end;
   4.241 -
   4.242 -  in inf [] end;
   4.243 -
   4.244 -
   4.245 -(* main interfaces *)
   4.246 -
   4.247 -fun prepare ctxt const_type var_type raw_ts =
   4.248 -  let
   4.249 -    val get_type = the_default dummyT o var_type;
   4.250 -    val constrain_vars = Term.map_aterms
   4.251 -      (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
   4.252 -        | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
   4.253 -        | t => t);
   4.254 -
   4.255 -    val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
   4.256 -    val idx = param_maxidx_of ts + 1;
   4.257 -    val (ts', (_, _, idx')) =
   4.258 -      fold_map (prepare_term ctxt const_type o constrain_vars) ts
   4.259 -        (Vartab.empty, Vartab.empty, idx);
   4.260 -  in (idx', ts') end;
   4.261 -
   4.262 -fun infer_types ctxt const_type var_type raw_ts =
   4.263 -  let
   4.264 -    val (idx, ts) = prepare ctxt const_type var_type raw_ts;
   4.265 -    val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
   4.266 -    val (_, ts') = finish ctxt tye ([], ts);
   4.267 -  in ts' end;
   4.268 -
   4.269  end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/type_infer_context.ML	Tue Apr 19 20:47:02 2011 +0200
     5.3 @@ -0,0 +1,267 @@
     5.4 +(*  Title:      Pure/type_infer_context.ML
     5.5 +    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     5.6 +
     5.7 +Type-inference preparation and standard type inference.
     5.8 +*)
     5.9 +
    5.10 +signature TYPE_INFER_CONTEXT =
    5.11 +sig
    5.12 +  val const_sorts: bool Config.T
    5.13 +  val prepare: Proof.context -> term list -> int * term list
    5.14 +  val infer_types: Proof.context -> term list -> term list
    5.15 +end;
    5.16 +
    5.17 +structure Type_Infer_Context: TYPE_INFER_CONTEXT =
    5.18 +struct
    5.19 +
    5.20 +(** prepare types/terms: create inference parameters **)
    5.21 +
    5.22 +(* constraints *)
    5.23 +
    5.24 +val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true)));
    5.25 +
    5.26 +fun const_type ctxt =
    5.27 +  try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o
    5.28 +    Consts.the_constraint (Proof_Context.consts_of ctxt));
    5.29 +
    5.30 +fun var_type ctxt = the_default dummyT o Proof_Context.def_type ctxt;
    5.31 +
    5.32 +
    5.33 +(* prepare_typ *)
    5.34 +
    5.35 +fun prepare_typ typ params_idx =
    5.36 +  let
    5.37 +    val (params', idx) = fold_atyps
    5.38 +      (fn TVar (xi, S) =>
    5.39 +          (fn ps_idx as (ps, idx) =>
    5.40 +            if Type_Infer.is_param xi andalso not (Vartab.defined ps xi)
    5.41 +            then (Vartab.update (xi, Type_Infer.mk_param idx S) ps, idx + 1) else ps_idx)
    5.42 +        | _ => I) typ params_idx;
    5.43 +
    5.44 +    fun prepare (T as Type (a, Ts)) idx =
    5.45 +          if T = dummyT then (Type_Infer.mk_param idx [], idx + 1)
    5.46 +          else
    5.47 +            let val (Ts', idx') = fold_map prepare Ts idx
    5.48 +            in (Type (a, Ts'), idx') end
    5.49 +      | prepare (T as TVar (xi, _)) idx =
    5.50 +          (case Vartab.lookup params' xi of
    5.51 +            NONE => T
    5.52 +          | SOME p => p, idx)
    5.53 +      | prepare (TFree ("'_dummy_", S)) idx = (Type_Infer.mk_param idx S, idx + 1)
    5.54 +      | prepare (T as TFree _) idx = (T, idx);
    5.55 +
    5.56 +    val (typ', idx') = prepare typ idx;
    5.57 +  in (typ', (params', idx')) end;
    5.58 +
    5.59 +
    5.60 +(* prepare_term *)
    5.61 +
    5.62 +fun prepare_term ctxt tm (vparams, params, idx) =
    5.63 +  let
    5.64 +    fun add_vparm xi (ps_idx as (ps, idx)) =
    5.65 +      if not (Vartab.defined ps xi) then
    5.66 +        (Vartab.update (xi, Type_Infer.mk_param idx []) ps, idx + 1)
    5.67 +      else ps_idx;
    5.68 +
    5.69 +    val (vparams', idx') = fold_aterms
    5.70 +      (fn Var (_, Type ("_polymorphic_", _)) => I
    5.71 +        | Var (xi, _) => add_vparm xi
    5.72 +        | Free (x, _) => add_vparm (x, ~1)
    5.73 +        | _ => I)
    5.74 +      tm (vparams, idx);
    5.75 +    fun var_param xi = the (Vartab.lookup vparams' xi);
    5.76 +
    5.77 +    fun polyT_of T idx =
    5.78 +      apsnd snd (prepare_typ (Type_Infer.paramify_vars T) (Vartab.empty, idx));
    5.79 +
    5.80 +    fun constraint T t ps =
    5.81 +      if T = dummyT then (t, ps)
    5.82 +      else
    5.83 +        let val (T', ps') = prepare_typ T ps
    5.84 +        in (Type.constraint T' t, ps') end;
    5.85 +
    5.86 +    fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
    5.87 +          let
    5.88 +            fun err () =
    5.89 +              error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
    5.90 +            val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
    5.91 +            val (A', ps_idx') = prepare_typ A ps_idx;
    5.92 +            val (t', ps_idx'') = prepare t ps_idx';
    5.93 +          in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
    5.94 +      | prepare (Const (c, T)) (ps, idx) =
    5.95 +          (case const_type ctxt c of
    5.96 +            SOME U =>
    5.97 +              let val (U', idx') = polyT_of U idx
    5.98 +              in constraint T (Const (c, U')) (ps, idx') end
    5.99 +          | NONE => error ("Undeclared constant: " ^ quote c))
   5.100 +      | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
   5.101 +          let val (T', idx') = polyT_of T idx
   5.102 +          in (Var (xi, T'), (ps, idx')) end
   5.103 +      | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx
   5.104 +      | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx
   5.105 +      | prepare (Bound i) ps_idx = (Bound i, ps_idx)
   5.106 +      | prepare (Abs (x, T, t)) ps_idx =
   5.107 +          let
   5.108 +            val (T', ps_idx') = prepare_typ T ps_idx;
   5.109 +            val (t', ps_idx'') = prepare t ps_idx';
   5.110 +          in (Abs (x, T', t'), ps_idx'') end
   5.111 +      | prepare (t $ u) ps_idx =
   5.112 +          let
   5.113 +            val (t', ps_idx') = prepare t ps_idx;
   5.114 +            val (u', ps_idx'') = prepare u ps_idx';
   5.115 +          in (t' $ u', ps_idx'') end;
   5.116 +
   5.117 +    val (tm', (params', idx'')) = prepare tm (params, idx');
   5.118 +  in (tm', (vparams', params', idx'')) end;
   5.119 +
   5.120 +
   5.121 +
   5.122 +(** order-sorted unification of types **)
   5.123 +
   5.124 +exception NO_UNIFIER of string * typ Vartab.table;
   5.125 +
   5.126 +fun unify ctxt =
   5.127 +  let
   5.128 +    val thy = Proof_Context.theory_of ctxt;
   5.129 +    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
   5.130 +
   5.131 +
   5.132 +    (* adjust sorts of parameters *)
   5.133 +
   5.134 +    fun not_of_sort x S' S =
   5.135 +      "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
   5.136 +        Syntax.string_of_sort ctxt S;
   5.137 +
   5.138 +    fun meet (_, []) tye_idx = tye_idx
   5.139 +      | meet (Type (a, Ts), S) (tye_idx as (tye, _)) =
   5.140 +          meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
   5.141 +      | meet (TFree (x, S'), S) (tye_idx as (tye, _)) =
   5.142 +          if Sign.subsort thy (S', S) then tye_idx
   5.143 +          else raise NO_UNIFIER (not_of_sort x S' S, tye)
   5.144 +      | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
   5.145 +          if Sign.subsort thy (S', S) then tye_idx
   5.146 +          else if Type_Infer.is_param xi then
   5.147 +            (Vartab.update_new
   5.148 +              (xi, Type_Infer.mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
   5.149 +          else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
   5.150 +    and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
   5.151 +          meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx)
   5.152 +      | meets _ tye_idx = tye_idx;
   5.153 +
   5.154 +
   5.155 +    (* occurs check and assignment *)
   5.156 +
   5.157 +    fun occurs_check tye xi (TVar (xi', _)) =
   5.158 +          if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
   5.159 +          else
   5.160 +            (case Vartab.lookup tye xi' of
   5.161 +              NONE => ()
   5.162 +            | SOME T => occurs_check tye xi T)
   5.163 +      | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts
   5.164 +      | occurs_check _ _ _ = ();
   5.165 +
   5.166 +    fun assign xi (T as TVar (xi', _)) S env =
   5.167 +          if xi = xi' then env
   5.168 +          else env |> meet (T, S) |>> Vartab.update_new (xi, T)
   5.169 +      | assign xi T S (env as (tye, _)) =
   5.170 +          (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T));
   5.171 +
   5.172 +
   5.173 +    (* unification *)
   5.174 +
   5.175 +    fun show_tycon (a, Ts) =
   5.176 +      quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
   5.177 +
   5.178 +    fun unif (T1, T2) (env as (tye, _)) =
   5.179 +      (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of
   5.180 +        ((true, TVar (xi, S)), (_, T)) => assign xi T S env
   5.181 +      | ((_, T), (true, TVar (xi, S))) => assign xi T S env
   5.182 +      | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
   5.183 +          if a <> b then
   5.184 +            raise NO_UNIFIER
   5.185 +              ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
   5.186 +          else fold unif (Ts ~~ Us) env
   5.187 +      | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye));
   5.188 +
   5.189 +  in unif end;
   5.190 +
   5.191 +
   5.192 +
   5.193 +(** simple type inference **)
   5.194 +
   5.195 +(* infer *)
   5.196 +
   5.197 +fun infer ctxt =
   5.198 +  let
   5.199 +    (* errors *)
   5.200 +
   5.201 +    fun prep_output tye bs ts Ts =
   5.202 +      let
   5.203 +        val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
   5.204 +        val (Ts', Ts'') = chop (length Ts) Ts_bTs';
   5.205 +        fun prep t =
   5.206 +          let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
   5.207 +          in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end;
   5.208 +      in (map prep ts', Ts') end;
   5.209 +
   5.210 +    fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
   5.211 +
   5.212 +    fun unif_failed msg =
   5.213 +      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
   5.214 +
   5.215 +    fun err_appl msg tye bs t T u U =
   5.216 +      let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
   5.217 +      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
   5.218 +
   5.219 +
   5.220 +    (* main *)
   5.221 +
   5.222 +    fun inf _ (Const (_, T)) tye_idx = (T, tye_idx)
   5.223 +      | inf _ (Free (_, T)) tye_idx = (T, tye_idx)
   5.224 +      | inf _ (Var (_, T)) tye_idx = (T, tye_idx)
   5.225 +      | inf bs (Bound i) tye_idx =
   5.226 +          (snd (nth bs i handle Subscript => err_loose i), tye_idx)
   5.227 +      | inf bs (Abs (x, T, t)) tye_idx =
   5.228 +          let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx
   5.229 +          in (T --> U, tye_idx') end
   5.230 +      | inf bs (t $ u) tye_idx =
   5.231 +          let
   5.232 +            val (T, tye_idx') = inf bs t tye_idx;
   5.233 +            val (U, (tye, idx)) = inf bs u tye_idx';
   5.234 +            val V = Type_Infer.mk_param idx [];
   5.235 +            val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
   5.236 +              handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
   5.237 +          in (V, tye_idx'') end;
   5.238 +
   5.239 +  in inf [] end;
   5.240 +
   5.241 +
   5.242 +(* main interfaces *)
   5.243 +
   5.244 +fun prepare ctxt raw_ts =
   5.245 +  let
   5.246 +    val constrain_vars = Term.map_aterms
   5.247 +      (fn Free (x, T) => Type.constraint T (Free (x, var_type ctxt (x, ~1)))
   5.248 +        | Var (xi, T) => Type.constraint T (Var (xi, var_type ctxt xi))
   5.249 +        | t => t);
   5.250 +
   5.251 +    val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
   5.252 +    val idx = Type_Infer.param_maxidx_of ts + 1;
   5.253 +    val (ts', (_, _, idx')) =
   5.254 +      fold_map (prepare_term ctxt o constrain_vars) ts
   5.255 +        (Vartab.empty, Vartab.empty, idx);
   5.256 +  in (idx', ts') end;
   5.257 +
   5.258 +fun infer_types ctxt raw_ts =
   5.259 +  let
   5.260 +    val (idx, ts) = prepare ctxt raw_ts;
   5.261 +    val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
   5.262 +    val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
   5.263 +  in ts' end;
   5.264 +
   5.265 +val _ =
   5.266 +  Context.>>
   5.267 +    (Syntax.add_term_check 0 "standard"
   5.268 +      (fn ctxt => infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)));
   5.269 +
   5.270 +end;
     6.1 --- a/src/Tools/nbe.ML	Tue Apr 19 16:13:04 2011 +0200
     6.2 +++ b/src/Tools/nbe.ML	Tue Apr 19 20:47:02 2011 +0200
     6.3 @@ -545,9 +545,9 @@
     6.4      val ctxt = Syntax.init_pretty_global thy;
     6.5      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
     6.6      val ty' = typ_of_itype program vs0 ty;
     6.7 -    fun type_infer t = singleton
     6.8 -      (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
     6.9 -      (Type.constraint ty' t);
    6.10 +    fun type_infer t =
    6.11 +      Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
    6.12 +        (Type.constraint ty' t);
    6.13      fun check_tvars t =
    6.14        if null (Term.add_tvars t []) then t
    6.15        else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
     7.1 --- a/src/Tools/subtyping.ML	Tue Apr 19 16:13:04 2011 +0200
     7.2 +++ b/src/Tools/subtyping.ML	Tue Apr 19 20:47:02 2011 +0200
     7.3 @@ -516,8 +516,8 @@
     7.4              | SOME S =>
     7.5                  SOME
     7.6                    (map nameT
     7.7 -                    (filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))),
     7.8 -                      S));
     7.9 +                    (filter_out Type_Infer.is_paramT
    7.10 +                      (map (Type_Infer.deref tye) (get_bound G T))), S));
    7.11            val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound);
    7.12            val assignment =
    7.13              if null bound orelse null not_params then NONE
    7.14 @@ -647,7 +647,8 @@
    7.15            end
    7.16        | insert bs (t $ u) =
    7.17            let
    7.18 -            val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t);
    7.19 +            val (t', Type ("fun", [U, T])) =
    7.20 +              apsnd (Type_Infer.deref tye) (insert bs t);
    7.21              val (u', U') = insert bs u;
    7.22            in
    7.23              if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U')
    7.24 @@ -664,10 +665,7 @@
    7.25  
    7.26  fun coercion_infer_types ctxt raw_ts =
    7.27    let
    7.28 -    val const_type = try (Consts.the_constraint (Proof_Context.consts_of ctxt));
    7.29 -    val var_type = Proof_Context.def_type ctxt;
    7.30 -
    7.31 -    val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts;
    7.32 +    val (idx, ts) = Type_Infer_Context.prepare ctxt raw_ts;
    7.33  
    7.34      fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
    7.35        | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)