# HG changeset patch # User wenzelm # Date 1303238822 -7200 # Node ID 13ecdb3057d8965a1fa06ecf51bd811cfa240a75 # Parent fbd136946b35c0067d2a7f59402302ca99a694a1 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; diff -r fbd136946b35 -r 13ecdb3057d8 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Apr 19 16:13:04 2011 +0200 +++ b/src/Pure/IsaMakefile Tue Apr 19 20:47:02 2011 +0200 @@ -253,6 +253,7 @@ thm.ML \ type.ML \ type_infer.ML \ + type_infer_context.ML \ unify.ML \ variable.ML @./mk diff -r fbd136946b35 -r 13ecdb3057d8 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 19 16:13:04 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 19 20:47:02 2011 +0200 @@ -76,7 +76,6 @@ val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort val check_tvar: Proof.context -> indexname * sort -> indexname * sort val check_tfree: Proof.context -> string * sort -> string * sort - val standard_infer_types: Proof.context -> term list -> term list val intern_skolem: Proof.context -> string -> string option val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term @@ -678,25 +677,18 @@ end; -(* type checking/inference *) +(* check/uncheck *) fun def_type ctxt = let val Mode {pattern, ...} = get_mode ctxt in Variable.def_type ctxt pattern end; -fun standard_infer_types ctxt = - Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt); - local fun standard_typ_check ctxt = map (cert_typ_mode (Type.get_mode ctxt) ctxt) #> map (prepare_patternT ctxt); -fun standard_term_check ctxt = - standard_infer_types ctxt #> - map (expand_abbrevs ctxt); - fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); @@ -704,7 +696,6 @@ val _ = Context.>> (Syntax.add_typ_check 0 "standard" standard_typ_check #> - Syntax.add_term_check 0 "standard" standard_term_check #> Syntax.add_term_check 100 "fixate" prepare_patterns #> Syntax.add_term_uncheck 0 "standard" standard_term_uncheck); diff -r fbd136946b35 -r 13ecdb3057d8 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Apr 19 16:13:04 2011 +0200 +++ b/src/Pure/ROOT.ML Tue Apr 19 20:47:02 2011 +0200 @@ -173,6 +173,7 @@ use "type_infer.ML"; use "Syntax/local_syntax.ML"; use "Isar/proof_context.ML"; +use "type_infer_context.ML"; use "Syntax/syntax_phases.ML"; use "Isar/local_defs.ML"; diff -r fbd136946b35 -r 13ecdb3057d8 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Tue Apr 19 16:13:04 2011 +0200 +++ b/src/Pure/type_infer.ML Tue Apr 19 20:47:02 2011 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/type_infer.ML Author: Stefan Berghofer and Markus Wenzel, TU Muenchen -Representation of type-inference problems. Simple type inference. +Basic representation of type-inference problems. *) signature TYPE_INFER = @@ -18,10 +18,6 @@ val deref: typ Vartab.table -> typ -> typ val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list val fixate: Proof.context -> term list -> term list - val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) -> - term list -> int * term list - val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) -> - term list -> term list end; structure Type_Infer: TYPE_INFER = @@ -70,96 +66,6 @@ -(** prepare types/terms: create inference parameters **) - -(* prepare_typ *) - -fun prepare_typ typ params_idx = - let - val (params', idx) = fold_atyps - (fn TVar (xi, S) => - (fn ps_idx as (ps, idx) => - if is_param xi andalso not (Vartab.defined ps xi) - then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx) - | _ => I) typ params_idx; - - fun prepare (T as Type (a, Ts)) idx = - if T = dummyT then (mk_param idx [], idx + 1) - else - let val (Ts', idx') = fold_map prepare Ts idx - in (Type (a, Ts'), idx') end - | prepare (T as TVar (xi, _)) idx = - (case Vartab.lookup params' xi of - NONE => T - | SOME p => p, idx) - | prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1) - | prepare (T as TFree _) idx = (T, idx); - - val (typ', idx') = prepare typ idx; - in (typ', (params', idx')) end; - - -(* prepare_term *) - -fun prepare_term ctxt const_type tm (vparams, params, idx) = - let - fun add_vparm xi (ps_idx as (ps, idx)) = - if not (Vartab.defined ps xi) then - (Vartab.update (xi, mk_param idx []) ps, idx + 1) - else ps_idx; - - val (vparams', idx') = fold_aterms - (fn Var (_, Type ("_polymorphic_", _)) => I - | Var (xi, _) => add_vparm xi - | Free (x, _) => add_vparm (x, ~1) - | _ => I) - tm (vparams, idx); - fun var_param xi = the (Vartab.lookup vparams' xi); - - fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx)); - - fun constraint T t ps = - if T = dummyT then (t, ps) - else - let val (T', ps') = prepare_typ T ps - in (Type.constraint T' t, ps') end; - - fun prepare (Const ("_type_constraint_", T) $ t) ps_idx = - let - fun err () = - error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T); - val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()); - val (A', ps_idx') = prepare_typ A ps_idx; - val (t', ps_idx'') = prepare t ps_idx'; - in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end - | prepare (Const (c, T)) (ps, idx) = - (case const_type c of - SOME U => - let val (U', idx') = polyT_of U idx - in constraint T (Const (c, U')) (ps, idx') end - | NONE => error ("Undeclared constant: " ^ quote c)) - | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = - let val (T', idx') = polyT_of T idx - in (Var (xi, T'), (ps, idx')) end - | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx - | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx - | prepare (Bound i) ps_idx = (Bound i, ps_idx) - | prepare (Abs (x, T, t)) ps_idx = - let - val (T', ps_idx') = prepare_typ T ps_idx; - val (t', ps_idx'') = prepare t ps_idx'; - in (Abs (x, T', t'), ps_idx'') end - | prepare (t $ u) ps_idx = - let - val (t', ps_idx') = prepare t ps_idx; - val (u', ps_idx'') = prepare u ps_idx'; - in (t' $ u', ps_idx'') end; - - val (tm', (params', idx'')) = prepare tm (params, idx'); - in (tm', (vparams', params', idx'')) end; - - - (** results **) (* dereferenced views *) @@ -219,149 +125,4 @@ val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used); in (map o map_types) (Term_Subst.instantiateT inst) ts end; - - -(** order-sorted unification of types **) - -exception NO_UNIFIER of string * typ Vartab.table; - -fun unify ctxt = - let - val thy = Proof_Context.theory_of ctxt; - val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); - - - (* adjust sorts of parameters *) - - fun not_of_sort x S' S = - "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^ - Syntax.string_of_sort ctxt S; - - fun meet (_, []) tye_idx = tye_idx - | meet (Type (a, Ts), S) (tye_idx as (tye, _)) = - meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx - | meet (TFree (x, S'), S) (tye_idx as (tye, _)) = - if Sign.subsort thy (S', S) then tye_idx - else raise NO_UNIFIER (not_of_sort x S' S, tye) - | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = - if Sign.subsort thy (S', S) then tye_idx - else if is_param xi then - (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) - else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) - and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = - meets (Ts, Ss) (meet (deref tye T, S) tye_idx) - | meets _ tye_idx = tye_idx; - - - (* occurs check and assignment *) - - fun occurs_check tye xi (TVar (xi', _)) = - if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye) - else - (case Vartab.lookup tye xi' of - NONE => () - | SOME T => occurs_check tye xi T) - | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts - | occurs_check _ _ _ = (); - - fun assign xi (T as TVar (xi', _)) S env = - if xi = xi' then env - else env |> meet (T, S) |>> Vartab.update_new (xi, T) - | assign xi T S (env as (tye, _)) = - (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T)); - - - (* unification *) - - fun show_tycon (a, Ts) = - quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); - - fun unif (T1, T2) (env as (tye, _)) = - (case pairself (`is_paramT o deref tye) (T1, T2) of - ((true, TVar (xi, S)), (_, T)) => assign xi T S env - | ((_, T), (true, TVar (xi, S))) => assign xi T S env - | ((_, Type (a, Ts)), (_, Type (b, Us))) => - if a <> b then - raise NO_UNIFIER - ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) - else fold unif (Ts ~~ Us) env - | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye)); - - in unif end; - - - -(** simple type inference **) - -(* infer *) - -fun infer ctxt = - let - (* errors *) - - fun prep_output tye bs ts Ts = - let - val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts); - val (Ts', Ts'') = chop (length Ts) Ts_bTs'; - fun prep t = - let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) - in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; - in (map prep ts', Ts') end; - - fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); - - fun unif_failed msg = - "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; - - fun err_appl msg tye bs t T u U = - let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U] - in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end; - - - (* main *) - - fun inf _ (Const (_, T)) tye_idx = (T, tye_idx) - | inf _ (Free (_, T)) tye_idx = (T, tye_idx) - | inf _ (Var (_, T)) tye_idx = (T, tye_idx) - | inf bs (Bound i) tye_idx = - (snd (nth bs i handle Subscript => err_loose i), tye_idx) - | inf bs (Abs (x, T, t)) tye_idx = - let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx - in (T --> U, tye_idx') end - | inf bs (t $ u) tye_idx = - let - val (T, tye_idx') = inf bs t tye_idx; - val (U, (tye, idx)) = inf bs u tye_idx'; - val V = mk_param idx []; - val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1) - handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; - in (V, tye_idx'') end; - - in inf [] end; - - -(* main interfaces *) - -fun prepare ctxt const_type var_type raw_ts = - let - val get_type = the_default dummyT o var_type; - val constrain_vars = Term.map_aterms - (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1))) - | Var (xi, T) => Type.constraint T (Var (xi, get_type xi)) - | t => t); - - val ts = burrow_types (Syntax.check_typs ctxt) raw_ts; - val idx = param_maxidx_of ts + 1; - val (ts', (_, _, idx')) = - fold_map (prepare_term ctxt const_type o constrain_vars) ts - (Vartab.empty, Vartab.empty, idx); - in (idx', ts') end; - -fun infer_types ctxt const_type var_type raw_ts = - let - val (idx, ts) = prepare ctxt const_type var_type raw_ts; - val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx); - val (_, ts') = finish ctxt tye ([], ts); - in ts' end; - end; diff -r fbd136946b35 -r 13ecdb3057d8 src/Pure/type_infer_context.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/type_infer_context.ML Tue Apr 19 20:47:02 2011 +0200 @@ -0,0 +1,267 @@ +(* Title: Pure/type_infer_context.ML + Author: Stefan Berghofer and Markus Wenzel, TU Muenchen + +Type-inference preparation and standard type inference. +*) + +signature TYPE_INFER_CONTEXT = +sig + val const_sorts: bool Config.T + val prepare: Proof.context -> term list -> int * term list + val infer_types: Proof.context -> term list -> term list +end; + +structure Type_Infer_Context: TYPE_INFER_CONTEXT = +struct + +(** prepare types/terms: create inference parameters **) + +(* constraints *) + +val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true))); + +fun const_type ctxt = + try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o + Consts.the_constraint (Proof_Context.consts_of ctxt)); + +fun var_type ctxt = the_default dummyT o Proof_Context.def_type ctxt; + + +(* prepare_typ *) + +fun prepare_typ typ params_idx = + let + val (params', idx) = fold_atyps + (fn TVar (xi, S) => + (fn ps_idx as (ps, idx) => + if Type_Infer.is_param xi andalso not (Vartab.defined ps xi) + then (Vartab.update (xi, Type_Infer.mk_param idx S) ps, idx + 1) else ps_idx) + | _ => I) typ params_idx; + + fun prepare (T as Type (a, Ts)) idx = + if T = dummyT then (Type_Infer.mk_param idx [], idx + 1) + else + let val (Ts', idx') = fold_map prepare Ts idx + in (Type (a, Ts'), idx') end + | prepare (T as TVar (xi, _)) idx = + (case Vartab.lookup params' xi of + NONE => T + | SOME p => p, idx) + | prepare (TFree ("'_dummy_", S)) idx = (Type_Infer.mk_param idx S, idx + 1) + | prepare (T as TFree _) idx = (T, idx); + + val (typ', idx') = prepare typ idx; + in (typ', (params', idx')) end; + + +(* prepare_term *) + +fun prepare_term ctxt tm (vparams, params, idx) = + let + fun add_vparm xi (ps_idx as (ps, idx)) = + if not (Vartab.defined ps xi) then + (Vartab.update (xi, Type_Infer.mk_param idx []) ps, idx + 1) + else ps_idx; + + val (vparams', idx') = fold_aterms + (fn Var (_, Type ("_polymorphic_", _)) => I + | Var (xi, _) => add_vparm xi + | Free (x, _) => add_vparm (x, ~1) + | _ => I) + tm (vparams, idx); + fun var_param xi = the (Vartab.lookup vparams' xi); + + fun polyT_of T idx = + apsnd snd (prepare_typ (Type_Infer.paramify_vars T) (Vartab.empty, idx)); + + fun constraint T t ps = + if T = dummyT then (t, ps) + else + let val (T', ps') = prepare_typ T ps + in (Type.constraint T' t, ps') end; + + fun prepare (Const ("_type_constraint_", T) $ t) ps_idx = + let + fun err () = + error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T); + val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()); + val (A', ps_idx') = prepare_typ A ps_idx; + val (t', ps_idx'') = prepare t ps_idx'; + in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end + | prepare (Const (c, T)) (ps, idx) = + (case const_type ctxt c of + SOME U => + let val (U', idx') = polyT_of U idx + in constraint T (Const (c, U')) (ps, idx') end + | NONE => error ("Undeclared constant: " ^ quote c)) + | prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = + let val (T', idx') = polyT_of T idx + in (Var (xi, T'), (ps, idx')) end + | prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx + | prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx + | prepare (Bound i) ps_idx = (Bound i, ps_idx) + | prepare (Abs (x, T, t)) ps_idx = + let + val (T', ps_idx') = prepare_typ T ps_idx; + val (t', ps_idx'') = prepare t ps_idx'; + in (Abs (x, T', t'), ps_idx'') end + | prepare (t $ u) ps_idx = + let + val (t', ps_idx') = prepare t ps_idx; + val (u', ps_idx'') = prepare u ps_idx'; + in (t' $ u', ps_idx'') end; + + val (tm', (params', idx'')) = prepare tm (params, idx'); + in (tm', (vparams', params', idx'')) end; + + + +(** order-sorted unification of types **) + +exception NO_UNIFIER of string * typ Vartab.table; + +fun unify ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); + + + (* adjust sorts of parameters *) + + fun not_of_sort x S' S = + "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^ + Syntax.string_of_sort ctxt S; + + fun meet (_, []) tye_idx = tye_idx + | meet (Type (a, Ts), S) (tye_idx as (tye, _)) = + meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx + | meet (TFree (x, S'), S) (tye_idx as (tye, _)) = + if Sign.subsort thy (S', S) then tye_idx + else raise NO_UNIFIER (not_of_sort x S' S, tye) + | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = + if Sign.subsort thy (S', S) then tye_idx + else if Type_Infer.is_param xi then + (Vartab.update_new + (xi, Type_Infer.mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) + else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) + and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = + meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx) + | meets _ tye_idx = tye_idx; + + + (* occurs check and assignment *) + + fun occurs_check tye xi (TVar (xi', _)) = + if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye) + else + (case Vartab.lookup tye xi' of + NONE => () + | SOME T => occurs_check tye xi T) + | occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts + | occurs_check _ _ _ = (); + + fun assign xi (T as TVar (xi', _)) S env = + if xi = xi' then env + else env |> meet (T, S) |>> Vartab.update_new (xi, T) + | assign xi T S (env as (tye, _)) = + (occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T)); + + + (* unification *) + + fun show_tycon (a, Ts) = + quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); + + fun unif (T1, T2) (env as (tye, _)) = + (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of + ((true, TVar (xi, S)), (_, T)) => assign xi T S env + | ((_, T), (true, TVar (xi, S))) => assign xi T S env + | ((_, Type (a, Ts)), (_, Type (b, Us))) => + if a <> b then + raise NO_UNIFIER + ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) + else fold unif (Ts ~~ Us) env + | ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye)); + + in unif end; + + + +(** simple type inference **) + +(* infer *) + +fun infer ctxt = + let + (* errors *) + + fun prep_output tye bs ts Ts = + let + val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts); + val (Ts', Ts'') = chop (length Ts) Ts_bTs'; + fun prep t = + let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) + in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; + in (map prep ts', Ts') end; + + fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); + + fun unif_failed msg = + "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; + + fun err_appl msg tye bs t T u U = + let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U] + in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end; + + + (* main *) + + fun inf _ (Const (_, T)) tye_idx = (T, tye_idx) + | inf _ (Free (_, T)) tye_idx = (T, tye_idx) + | inf _ (Var (_, T)) tye_idx = (T, tye_idx) + | inf bs (Bound i) tye_idx = + (snd (nth bs i handle Subscript => err_loose i), tye_idx) + | inf bs (Abs (x, T, t)) tye_idx = + let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx + in (T --> U, tye_idx') end + | inf bs (t $ u) tye_idx = + let + val (T, tye_idx') = inf bs t tye_idx; + val (U, (tye, idx)) = inf bs u tye_idx'; + val V = Type_Infer.mk_param idx []; + val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1) + handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; + in (V, tye_idx'') end; + + in inf [] end; + + +(* main interfaces *) + +fun prepare ctxt raw_ts = + let + val constrain_vars = Term.map_aterms + (fn Free (x, T) => Type.constraint T (Free (x, var_type ctxt (x, ~1))) + | Var (xi, T) => Type.constraint T (Var (xi, var_type ctxt xi)) + | t => t); + + val ts = burrow_types (Syntax.check_typs ctxt) raw_ts; + val idx = Type_Infer.param_maxidx_of ts + 1; + val (ts', (_, _, idx')) = + fold_map (prepare_term ctxt o constrain_vars) ts + (Vartab.empty, Vartab.empty, idx); + in (idx', ts') end; + +fun infer_types ctxt raw_ts = + let + val (idx, ts) = prepare ctxt raw_ts; + val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx); + val (_, ts') = Type_Infer.finish ctxt tye ([], ts); + in ts' end; + +val _ = + Context.>> + (Syntax.add_term_check 0 "standard" + (fn ctxt => infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt))); + +end; diff -r fbd136946b35 -r 13ecdb3057d8 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Apr 19 16:13:04 2011 +0200 +++ b/src/Tools/nbe.ML Tue Apr 19 20:47:02 2011 +0200 @@ -545,9 +545,9 @@ val ctxt = Syntax.init_pretty_global thy; val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); val ty' = typ_of_itype program vs0 ty; - fun type_infer t = singleton - (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE)) - (Type.constraint ty' t); + fun type_infer t = + Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt) + (Type.constraint ty' t); fun check_tvars t = if null (Term.add_tvars t []) then t else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t); diff -r fbd136946b35 -r 13ecdb3057d8 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Tue Apr 19 16:13:04 2011 +0200 +++ b/src/Tools/subtyping.ML Tue Apr 19 20:47:02 2011 +0200 @@ -516,8 +516,8 @@ | SOME S => SOME (map nameT - (filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))), - S)); + (filter_out Type_Infer.is_paramT + (map (Type_Infer.deref tye) (get_bound G T))), S)); val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound); val assignment = if null bound orelse null not_params then NONE @@ -647,7 +647,8 @@ end | insert bs (t $ u) = let - val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t); + val (t', Type ("fun", [U, T])) = + apsnd (Type_Infer.deref tye) (insert bs t); val (u', U') = insert bs u; in if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U') @@ -664,10 +665,7 @@ fun coercion_infer_types ctxt raw_ts = let - val const_type = try (Consts.the_constraint (Proof_Context.consts_of ctxt)); - val var_type = Proof_Context.def_type ctxt; - - val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts; + val (idx, ts) = Type_Infer_Context.prepare ctxt raw_ts; fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx) | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)