load type_infer.ML later -- proper context for Type_Infer.infer_types;
authorwenzelm
Sun Sep 12 20:47:47 2010 +0200 (2010-09-12)
changeset 3929044e4d8dfd6bf
parent 39289 92b50c8bb67b
child 39291 4b632bb847a8
load type_infer.ML later -- proper context for Type_Infer.infer_types;
renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
src/Pure/Isar/proof_context.ML
src/Pure/ROOT.ML
src/Pure/sign.ML
src/Pure/type.ML
src/Pure/type_infer.ML
src/Pure/variable.ML
src/Tools/nbe.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Sep 12 19:55:45 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Sep 12 20:47:47 2010 +0200
     1.3 @@ -699,9 +699,7 @@
     1.4    in Variable.def_type ctxt pattern end;
     1.5  
     1.6  fun standard_infer_types ctxt ts =
     1.7 -  Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
     1.8 -    (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
     1.9 -    (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
    1.10 +  Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt) ts
    1.11    handle TYPE (msg, _, _) => error msg;
    1.12  
    1.13  local
     2.1 --- a/src/Pure/ROOT.ML	Sun Sep 12 19:55:45 2010 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Sun Sep 12 20:47:47 2010 +0200
     2.3 @@ -116,8 +116,6 @@
     2.4  use "Syntax/printer.ML";
     2.5  use "Syntax/syntax.ML";
     2.6  
     2.7 -use "type_infer.ML";
     2.8 -
     2.9  
    2.10  (* core of tactical proof system *)
    2.11  
    2.12 @@ -159,6 +157,7 @@
    2.13  use "Isar/rule_cases.ML";
    2.14  use "Isar/auto_bind.ML";
    2.15  use "Isar/local_syntax.ML";
    2.16 +use "type_infer.ML";
    2.17  use "Isar/proof_context.ML";
    2.18  use "Isar/local_defs.ML";
    2.19  
     3.1 --- a/src/Pure/sign.ML	Sun Sep 12 19:55:45 2010 +0200
     3.2 +++ b/src/Pure/sign.ML	Sun Sep 12 20:47:47 2010 +0200
     3.3 @@ -29,6 +29,7 @@
     3.4    val defaultS: theory -> sort
     3.5    val subsort: theory -> sort * sort -> bool
     3.6    val of_sort: theory -> typ * sort -> bool
     3.7 +  val inter_sort: theory -> sort * sort -> sort
     3.8    val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
     3.9    val is_logtype: theory -> string -> bool
    3.10    val typ_instance: theory -> typ * typ -> bool
    3.11 @@ -201,6 +202,7 @@
    3.12  val defaultS = Type.defaultS o tsig_of;
    3.13  val subsort = Type.subsort o tsig_of;
    3.14  val of_sort = Type.of_sort o tsig_of;
    3.15 +val inter_sort = Type.inter_sort o tsig_of;
    3.16  val witness_sorts = Type.witness_sorts o tsig_of;
    3.17  val is_logtype = member (op =) o Type.logical_types o tsig_of;
    3.18  
     4.1 --- a/src/Pure/type.ML	Sun Sep 12 19:55:45 2010 +0200
     4.2 +++ b/src/Pure/type.ML	Sun Sep 12 20:47:47 2010 +0200
     4.3 @@ -8,6 +8,7 @@
     4.4  signature TYPE =
     4.5  sig
     4.6    (*constraints*)
     4.7 +  val mark_polymorphic: typ -> typ
     4.8    val constraint: typ -> term -> term
     4.9    val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
    4.10    (*type signatures and certified types*)
    4.11 @@ -101,6 +102,9 @@
    4.12  
    4.13  (** constraints **)
    4.14  
    4.15 +(*indicate polymorphic Vars*)
    4.16 +fun mark_polymorphic T = Type ("_polymorphic_", [T]);
    4.17 +
    4.18  fun constraint T t =
    4.19    if T = dummyT then t
    4.20    else Const ("_type_constraint_", T --> T) $ t;
     5.1 --- a/src/Pure/type_infer.ML	Sun Sep 12 19:55:45 2010 +0200
     5.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 20:47:47 2010 +0200
     5.3 @@ -7,14 +7,12 @@
     5.4  signature TYPE_INFER =
     5.5  sig
     5.6    val anyT: sort -> typ
     5.7 -  val polymorphicT: typ -> typ
     5.8    val is_param: indexname -> bool
     5.9    val param: int -> string * sort -> typ
    5.10    val paramify_vars: typ -> typ
    5.11    val paramify_dummies: typ -> int -> typ * int
    5.12    val fixate_params: Name.context -> term list -> term list
    5.13 -  val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
    5.14 -    (string -> typ option) -> (indexname -> typ option) -> Name.context -> int ->
    5.15 +  val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
    5.16      term list -> term list
    5.17  end;
    5.18  
    5.19 @@ -26,9 +24,6 @@
    5.20  
    5.21  fun anyT S = TFree ("'_dummy_", S);
    5.22  
    5.23 -(*indicate polymorphic Vars*)
    5.24 -fun polymorphicT T = Type ("_polymorphic_", [T]);
    5.25 -
    5.26  
    5.27  (* type inference parameters -- may get instantiated *)
    5.28  
    5.29 @@ -235,12 +230,14 @@
    5.30  
    5.31  (* typs_terms_of *)
    5.32  
    5.33 -fun typs_terms_of tye used maxidx (Ts, ts) =
    5.34 +fun typs_terms_of ctxt tye (Ts, ts) =
    5.35    let
    5.36 -    val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used);
    5.37 +    val used = fold (add_names tye) ts (fold (add_namesT tye) Ts (Variable.names_of ctxt));
    5.38      val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts []));
    5.39 -    val names = Name.invents used' ("?" ^ Name.aT) (length parms);
    5.40 +    val names = Name.invents used ("?" ^ Name.aT) (length parms);
    5.41      val tab = Inttab.make (parms ~~ names);
    5.42 +
    5.43 +    val maxidx = Variable.maxidx_of ctxt;
    5.44      fun f i = (the (Inttab.lookup tab i), maxidx + 1);
    5.45    in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end;
    5.46  
    5.47 @@ -250,27 +247,31 @@
    5.48  
    5.49  exception NO_UNIFIER of string * pretyp Inttab.table;
    5.50  
    5.51 -fun unify pp tsig =
    5.52 +fun unify ctxt pp =
    5.53    let
    5.54 +    val thy = ProofContext.theory_of ctxt;
    5.55 +    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
    5.56 +
    5.57 +
    5.58      (* adjust sorts of parameters *)
    5.59  
    5.60      fun not_of_sort x S' S =
    5.61 -      "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^
    5.62 -        Pretty.string_of_sort pp S;
    5.63 +      "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
    5.64 +        Syntax.string_of_sort ctxt S;
    5.65  
    5.66      fun meet (_, []) tye_idx = tye_idx
    5.67        | meet (Param (i, S'), S) (tye_idx as (tye, idx)) =
    5.68 -          if Type.subsort tsig (S', S) then tye_idx
    5.69 +          if Sign.subsort thy (S', S) then tye_idx
    5.70            else (Inttab.update_new (i,
    5.71 -            Param (idx, Type.inter_sort tsig (S', S))) tye, idx + 1)
    5.72 +            Param (idx, Sign.inter_sort thy (S', S))) tye, idx + 1)
    5.73        | meet (PType (a, Ts), S) (tye_idx as (tye, _)) =
    5.74 -          meets (Ts, Type.arity_sorts pp tsig a S
    5.75 +          meets (Ts, arity_sorts a S
    5.76              handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
    5.77        | meet (PTFree (x, S'), S) (tye_idx as (tye, _)) =
    5.78 -          if Type.subsort tsig (S', S) then tye_idx
    5.79 +          if Sign.subsort thy (S', S) then tye_idx
    5.80            else raise NO_UNIFIER (not_of_sort x S' S, tye)
    5.81        | meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) =
    5.82 -          if Type.subsort tsig (S', S) then tye_idx
    5.83 +          if Sign.subsort thy (S', S) then tye_idx
    5.84            else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
    5.85      and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
    5.86            meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
    5.87 @@ -298,7 +299,7 @@
    5.88      (* unification *)
    5.89  
    5.90      fun show_tycon (a, Ts) =
    5.91 -      quote (Pretty.string_of_typ pp (Type (a, replicate (length Ts) dummyT)));
    5.92 +      quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
    5.93  
    5.94      fun unif (T1, T2) (tye_idx as (tye, idx)) =
    5.95        (case (deref tye T1, deref tye T2) of
    5.96 @@ -319,13 +320,16 @@
    5.97  
    5.98  (* infer *)
    5.99  
   5.100 -fun infer pp tsig =
   5.101 +fun infer ctxt =
   5.102    let
   5.103 +    val pp = Syntax.pp ctxt;
   5.104 +
   5.105 +
   5.106      (* errors *)
   5.107  
   5.108      fun prep_output tye bs ts Ts =
   5.109        let
   5.110 -        val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts);
   5.111 +        val (Ts_bTs', ts') = typs_terms_of ctxt tye (Ts @ map snd bs, ts);
   5.112          val (Ts', Ts'') = chop (length Ts) Ts_bTs';
   5.113          fun prep t =
   5.114            let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
   5.115 @@ -355,8 +359,6 @@
   5.116  
   5.117      (* main *)
   5.118  
   5.119 -    val unif = unify pp tsig;
   5.120 -
   5.121      fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx)
   5.122        | inf _ (PFree (_, T)) tye_idx = (T, tye_idx)
   5.123        | inf _ (PVar (_, T)) tye_idx = (T, tye_idx)
   5.124 @@ -371,13 +373,13 @@
   5.125              val (U, (tye, idx)) = inf bs u tye_idx';
   5.126              val V = Param (idx, []);
   5.127              val U_to_V = PType ("fun", [U, V]);
   5.128 -            val tye_idx'' = unif (U_to_V, T) (tye, idx + 1)
   5.129 +            val tye_idx'' = unify ctxt pp (U_to_V, T) (tye, idx + 1)
   5.130                handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
   5.131            in (V, tye_idx'') end
   5.132        | inf bs (Constraint (t, U)) tye_idx =
   5.133            let val (T, tye_idx') = inf bs t tye_idx in
   5.134              (T,
   5.135 -             unif (T, U) tye_idx'
   5.136 +             unify ctxt pp (T, U) tye_idx'
   5.137                 handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
   5.138            end;
   5.139  
   5.140 @@ -386,7 +388,7 @@
   5.141  
   5.142  (* infer_types *)
   5.143  
   5.144 -fun infer_types pp tsig check_typs const_type var_type used maxidx raw_ts =
   5.145 +fun infer_types ctxt const_type var_type raw_ts =
   5.146    let
   5.147      (*constrain vars*)
   5.148      val get_type = the_default dummyT o var_type;
   5.149 @@ -396,13 +398,13 @@
   5.150          | t => t);
   5.151  
   5.152      (*convert to preterms*)
   5.153 -    val ts = burrow_types check_typs raw_ts;
   5.154 +    val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
   5.155      val (ts', (_, _, idx)) =
   5.156        fold_map (preterm_of const_type o constrain_vars) ts
   5.157        (Vartab.empty, Vartab.empty, 0);
   5.158  
   5.159      (*do type inference*)
   5.160 -    val (tye, _) = fold (snd oo infer pp tsig) ts' (Inttab.empty, idx);
   5.161 -  in #2 (typs_terms_of tye used maxidx ([], ts')) end;
   5.162 +    val (tye, _) = fold (snd oo infer ctxt) ts' (Inttab.empty, idx);
   5.163 +  in #2 (typs_terms_of ctxt tye ([], ts')) end;
   5.164  
   5.165  end;
     6.1 --- a/src/Pure/variable.ML	Sun Sep 12 19:55:45 2010 +0200
     6.2 +++ b/src/Pure/variable.ML	Sun Sep 12 20:47:47 2010 +0200
     6.3 @@ -168,7 +168,7 @@
     6.4      (case Vartab.lookup types xi of
     6.5        NONE =>
     6.6          if pattern then NONE
     6.7 -        else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1)
     6.8 +        else Vartab.lookup binds xi |> Option.map (Type.mark_polymorphic o #1)
     6.9      | some => some)
    6.10    end;
    6.11  
     7.1 --- a/src/Tools/nbe.ML	Sun Sep 12 19:55:45 2010 +0200
     7.2 +++ b/src/Tools/nbe.ML	Sun Sep 12 20:47:47 2010 +0200
     7.3 @@ -547,13 +547,13 @@
     7.4  
     7.5  fun normalize thy program ((vs0, (vs, ty)), t) deps =
     7.6    let
     7.7 +    val ctxt = Syntax.init_pretty_global thy;
     7.8      val ty' = typ_of_itype program vs0 ty;
     7.9      fun type_infer t =
    7.10 -      singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    7.11 -        (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
    7.12 -      (Type.constraint ty' t);
    7.13 -    val string_of_term =
    7.14 -      Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
    7.15 +      singleton
    7.16 +        (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
    7.17 +        (Type.constraint ty' t);
    7.18 +    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    7.19      fun check_tvars t =
    7.20        if null (Term.add_tvars t []) then t
    7.21        else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);