# HG changeset patch # User wenzelm # Date 1284317267 -7200 # Node ID 44e4d8dfd6bfcfb68d01384e295645bfdc90401a # Parent 92b50c8bb67b6c0a6450c8640ebf323cd6b3f6f9 load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic; diff -r 92b50c8bb67b -r 44e4d8dfd6bf src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Sep 12 19:55:45 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun Sep 12 20:47:47 2010 +0200 @@ -699,9 +699,7 @@ in Variable.def_type ctxt pattern end; fun standard_infer_types ctxt ts = - Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt) - (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt) - (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts + Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt) ts handle TYPE (msg, _, _) => error msg; local diff -r 92b50c8bb67b -r 44e4d8dfd6bf src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sun Sep 12 19:55:45 2010 +0200 +++ b/src/Pure/ROOT.ML Sun Sep 12 20:47:47 2010 +0200 @@ -116,8 +116,6 @@ use "Syntax/printer.ML"; use "Syntax/syntax.ML"; -use "type_infer.ML"; - (* core of tactical proof system *) @@ -159,6 +157,7 @@ use "Isar/rule_cases.ML"; use "Isar/auto_bind.ML"; use "Isar/local_syntax.ML"; +use "type_infer.ML"; use "Isar/proof_context.ML"; use "Isar/local_defs.ML"; diff -r 92b50c8bb67b -r 44e4d8dfd6bf src/Pure/sign.ML --- a/src/Pure/sign.ML Sun Sep 12 19:55:45 2010 +0200 +++ b/src/Pure/sign.ML Sun Sep 12 20:47:47 2010 +0200 @@ -29,6 +29,7 @@ val defaultS: theory -> sort val subsort: theory -> sort * sort -> bool val of_sort: theory -> typ * sort -> bool + val inter_sort: theory -> sort * sort -> sort val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list val is_logtype: theory -> string -> bool val typ_instance: theory -> typ * typ -> bool @@ -201,6 +202,7 @@ val defaultS = Type.defaultS o tsig_of; val subsort = Type.subsort o tsig_of; val of_sort = Type.of_sort o tsig_of; +val inter_sort = Type.inter_sort o tsig_of; val witness_sorts = Type.witness_sorts o tsig_of; val is_logtype = member (op =) o Type.logical_types o tsig_of; diff -r 92b50c8bb67b -r 44e4d8dfd6bf src/Pure/type.ML --- a/src/Pure/type.ML Sun Sep 12 19:55:45 2010 +0200 +++ b/src/Pure/type.ML Sun Sep 12 20:47:47 2010 +0200 @@ -8,6 +8,7 @@ signature TYPE = sig (*constraints*) + val mark_polymorphic: typ -> typ val constraint: typ -> term -> term val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string (*type signatures and certified types*) @@ -101,6 +102,9 @@ (** constraints **) +(*indicate polymorphic Vars*) +fun mark_polymorphic T = Type ("_polymorphic_", [T]); + fun constraint T t = if T = dummyT then t else Const ("_type_constraint_", T --> T) $ t; diff -r 92b50c8bb67b -r 44e4d8dfd6bf src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Sun Sep 12 19:55:45 2010 +0200 +++ b/src/Pure/type_infer.ML Sun Sep 12 20:47:47 2010 +0200 @@ -7,14 +7,12 @@ signature TYPE_INFER = sig val anyT: sort -> typ - val polymorphicT: typ -> typ val is_param: indexname -> bool val param: int -> string * sort -> typ val paramify_vars: typ -> typ val paramify_dummies: typ -> int -> typ * int val fixate_params: Name.context -> term list -> term list - val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) -> - (string -> typ option) -> (indexname -> typ option) -> Name.context -> int -> + val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) -> term list -> term list end; @@ -26,9 +24,6 @@ fun anyT S = TFree ("'_dummy_", S); -(*indicate polymorphic Vars*) -fun polymorphicT T = Type ("_polymorphic_", [T]); - (* type inference parameters -- may get instantiated *) @@ -235,12 +230,14 @@ (* typs_terms_of *) -fun typs_terms_of tye used maxidx (Ts, ts) = +fun typs_terms_of ctxt tye (Ts, ts) = let - val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used); + val used = fold (add_names tye) ts (fold (add_namesT tye) Ts (Variable.names_of ctxt)); val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts [])); - val names = Name.invents used' ("?" ^ Name.aT) (length parms); + val names = Name.invents used ("?" ^ Name.aT) (length parms); val tab = Inttab.make (parms ~~ names); + + val maxidx = Variable.maxidx_of ctxt; fun f i = (the (Inttab.lookup tab i), maxidx + 1); in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end; @@ -250,27 +247,31 @@ exception NO_UNIFIER of string * pretyp Inttab.table; -fun unify pp tsig = +fun unify ctxt pp = let + val thy = ProofContext.theory_of ctxt; + val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy); + + (* adjust sorts of parameters *) fun not_of_sort x S' S = - "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ - Pretty.string_of_sort pp 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 (Param (i, S'), S) (tye_idx as (tye, idx)) = - if Type.subsort tsig (S', S) then tye_idx + if Sign.subsort thy (S', S) then tye_idx else (Inttab.update_new (i, - Param (idx, Type.inter_sort tsig (S', S))) tye, idx + 1) + Param (idx, Sign.inter_sort thy (S', S))) tye, idx + 1) | meet (PType (a, Ts), S) (tye_idx as (tye, _)) = - meets (Ts, Type.arity_sorts pp tsig a S + meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx | meet (PTFree (x, S'), S) (tye_idx as (tye, _)) = - if Type.subsort tsig (S', S) then tye_idx + if Sign.subsort thy (S', S) then tye_idx else raise NO_UNIFIER (not_of_sort x S' S, tye) | meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) = - if Type.subsort tsig (S', S) then tye_idx + if Sign.subsort thy (S', S) then tye_idx 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) @@ -298,7 +299,7 @@ (* unification *) fun show_tycon (a, Ts) = - quote (Pretty.string_of_typ pp (Type (a, replicate (length Ts) dummyT))); + quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); fun unif (T1, T2) (tye_idx as (tye, idx)) = (case (deref tye T1, deref tye T2) of @@ -319,13 +320,16 @@ (* infer *) -fun infer pp tsig = +fun infer ctxt = let + val pp = Syntax.pp ctxt; + + (* errors *) fun prep_output tye bs ts Ts = let - val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts); + val (Ts_bTs', ts') = typs_terms_of 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''))) @@ -355,8 +359,6 @@ (* main *) - val unif = unify pp tsig; - fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx) | inf _ (PFree (_, T)) tye_idx = (T, tye_idx) | inf _ (PVar (_, T)) tye_idx = (T, tye_idx) @@ -371,13 +373,13 @@ val (U, (tye, idx)) = inf bs u tye_idx'; val V = Param (idx, []); val U_to_V = PType ("fun", [U, V]); - val tye_idx'' = unif (U_to_V, T) (tye, idx + 1) + val tye_idx'' = unify ctxt pp (U_to_V, T) (tye, idx + 1) handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; in (V, tye_idx'') end | inf bs (Constraint (t, U)) tye_idx = let val (T, tye_idx') = inf bs t tye_idx in (T, - unif (T, U) tye_idx' + unify ctxt pp (T, U) tye_idx' handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U) end; @@ -386,7 +388,7 @@ (* infer_types *) -fun infer_types pp tsig check_typs const_type var_type used maxidx raw_ts = +fun infer_types ctxt const_type var_type raw_ts = let (*constrain vars*) val get_type = the_default dummyT o var_type; @@ -396,13 +398,13 @@ | t => t); (*convert to preterms*) - val ts = burrow_types check_typs raw_ts; + val ts = burrow_types (Syntax.check_typs ctxt) raw_ts; val (ts', (_, _, idx)) = fold_map (preterm_of const_type o constrain_vars) ts (Vartab.empty, Vartab.empty, 0); (*do type inference*) - val (tye, _) = fold (snd oo infer pp tsig) ts' (Inttab.empty, idx); - in #2 (typs_terms_of tye used maxidx ([], ts')) end; + val (tye, _) = fold (snd oo infer ctxt) ts' (Inttab.empty, idx); + in #2 (typs_terms_of ctxt tye ([], ts')) end; end; diff -r 92b50c8bb67b -r 44e4d8dfd6bf src/Pure/variable.ML --- a/src/Pure/variable.ML Sun Sep 12 19:55:45 2010 +0200 +++ b/src/Pure/variable.ML Sun Sep 12 20:47:47 2010 +0200 @@ -168,7 +168,7 @@ (case Vartab.lookup types xi of NONE => if pattern then NONE - else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1) + else Vartab.lookup binds xi |> Option.map (Type.mark_polymorphic o #1) | some => some) end; diff -r 92b50c8bb67b -r 44e4d8dfd6bf src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sun Sep 12 19:55:45 2010 +0200 +++ b/src/Tools/nbe.ML Sun Sep 12 20:47:47 2010 +0200 @@ -547,13 +547,13 @@ fun normalize thy program ((vs0, (vs, ty)), t) deps = let + val ctxt = Syntax.init_pretty_global thy; val ty' = typ_of_itype program vs0 ty; fun type_infer t = - singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I - (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0) - (Type.constraint ty' t); - val string_of_term = - Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy)); + singleton + (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE)) + (Type.constraint ty' t); + val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); 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);