src/Pure/type_infer.ML
changeset 39296 e275d581a218
parent 39295 6e8b0672c6a2
child 40286 b928e3960446
     1.1 --- a/src/Pure/type_infer.ML	Mon Sep 13 12:42:08 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Sep 13 13:20:18 2010 +0200
     1.3 @@ -1,18 +1,22 @@
     1.4  (*  Title:      Pure/type_infer.ML
     1.5      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Simple type inference.
     1.8 +Representation of type-inference problems.  Simple type inference.
     1.9  *)
    1.10  
    1.11  signature TYPE_INFER =
    1.12  sig
    1.13 -  val anyT: sort -> typ
    1.14    val is_param: indexname -> bool
    1.15    val is_paramT: typ -> bool
    1.16    val param: int -> string * sort -> typ
    1.17 +  val anyT: sort -> typ
    1.18    val paramify_vars: typ -> typ
    1.19    val paramify_dummies: typ -> int -> typ * int
    1.20 -  val fixate_params: Proof.context -> term list -> term list
    1.21 +  val deref: typ Vartab.table -> typ -> typ
    1.22 +  val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    1.23 +  val fixate: Proof.context -> term list -> term list
    1.24 +  val prepare: Proof.context -> (string -> typ option) -> (string * int -> typ option) ->
    1.25 +    term list -> int * term list
    1.26    val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
    1.27      term list -> term list
    1.28  end;
    1.29 @@ -20,12 +24,8 @@
    1.30  structure Type_Infer: TYPE_INFER =
    1.31  struct
    1.32  
    1.33 -
    1.34  (** type parameters and constraints **)
    1.35  
    1.36 -fun anyT S = TFree ("'_dummy_", S);
    1.37 -
    1.38 -
    1.39  (* type inference parameters -- may get instantiated *)
    1.40  
    1.41  fun is_param (x, _: int) = String.isPrefix "?" x;
    1.42 @@ -37,6 +37,11 @@
    1.43  
    1.44  fun mk_param i S = TVar (("?'a", i), S);
    1.45  
    1.46 +
    1.47 +(* pre-stage parameters *)
    1.48 +
    1.49 +fun anyT S = TFree ("'_dummy_", S);
    1.50 +
    1.51  val paramify_vars =
    1.52    Same.commit
    1.53      (Term_Subst.map_atypsT_same
    1.54 @@ -54,19 +59,6 @@
    1.55        | paramify T maxidx = (T, maxidx);
    1.56    in paramify end;
    1.57  
    1.58 -fun fixate_params ctxt ts =
    1.59 -  let
    1.60 -    fun subst_param (xi, S) (inst, used) =
    1.61 -      if is_param xi then
    1.62 -        let
    1.63 -          val [a] = Name.invents used Name.aT 1;
    1.64 -          val used' = Name.declare a used;
    1.65 -        in (((xi, S), TFree (a, S)) :: inst, used') end
    1.66 -      else (inst, used);
    1.67 -    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
    1.68 -    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
    1.69 -  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
    1.70 -
    1.71  
    1.72  
    1.73  (** prepare types/terms: create inference parameters **)
    1.74 @@ -156,7 +148,7 @@
    1.75  
    1.76  
    1.77  
    1.78 -(** finish types/terms: standardize remaining parameters **)
    1.79 +(** results **)
    1.80  
    1.81  (* dereferenced views *)
    1.82  
    1.83 @@ -179,7 +171,7 @@
    1.84    | TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x);
    1.85  
    1.86  
    1.87 -(* finish *)
    1.88 +(* finish -- standardize remaining parameters *)
    1.89  
    1.90  fun finish ctxt tye (Ts, ts) =
    1.91    let
    1.92 @@ -200,6 +192,22 @@
    1.93    in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;
    1.94  
    1.95  
    1.96 +(* fixate -- introduce fresh type variables *)
    1.97 +
    1.98 +fun fixate ctxt ts =
    1.99 +  let
   1.100 +    fun subst_param (xi, S) (inst, used) =
   1.101 +      if is_param xi then
   1.102 +        let
   1.103 +          val [a] = Name.invents used Name.aT 1;
   1.104 +          val used' = Name.declare a used;
   1.105 +        in (((xi, S), TFree (a, S)) :: inst, used') end
   1.106 +      else (inst, used);
   1.107 +    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
   1.108 +    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
   1.109 +  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
   1.110 +
   1.111 +
   1.112  
   1.113  (** order-sorted unification of types **)
   1.114  
   1.115 @@ -271,7 +279,7 @@
   1.116  
   1.117  
   1.118  
   1.119 -(** type inference **)
   1.120 +(** simple type inference **)
   1.121  
   1.122  (* infer *)
   1.123  
   1.124 @@ -323,25 +331,27 @@
   1.125    in inf [] end;
   1.126  
   1.127  
   1.128 -(* infer_types *)
   1.129 +(* main interfaces *)
   1.130  
   1.131 -fun infer_types ctxt const_type var_type raw_ts =
   1.132 +fun prepare ctxt const_type var_type raw_ts =
   1.133    let
   1.134 -    (*constrain vars*)
   1.135      val get_type = the_default dummyT o var_type;
   1.136      val constrain_vars = Term.map_aterms
   1.137        (fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1)))
   1.138          | Var (xi, T) => Type.constraint T (Var (xi, get_type xi))
   1.139          | t => t);
   1.140  
   1.141 -    (*convert to preterms*)
   1.142      val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
   1.143      val (ts', (_, _, idx)) =
   1.144        fold_map (prepare_term const_type o constrain_vars) ts
   1.145        (Vartab.empty, Vartab.empty, 0);
   1.146 +  in (idx, ts') end;
   1.147  
   1.148 -    (*do type inference*)
   1.149 -    val (tye, _) = fold (snd oo infer ctxt) ts' (Vartab.empty, idx);
   1.150 -  in #2 (finish ctxt tye ([], ts')) end;
   1.151 +fun infer_types ctxt const_type var_type raw_ts =
   1.152 +  let
   1.153 +    val (idx, ts) = prepare ctxt const_type var_type raw_ts;
   1.154 +    val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx);
   1.155 +    val (_, ts') = finish ctxt tye ([], ts);
   1.156 +  in ts' end;
   1.157  
   1.158  end;