src/Pure/type_infer.ML
changeset 22771 ce1fe6ca7dbb
parent 22698 7e6412e8d64b
child 24275 bbc3dab6d4fe
     1.1 --- a/src/Pure/type_infer.ML	Mon Apr 23 20:44:09 2007 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Apr 23 20:44:10 2007 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    val polymorphicT: typ -> typ
     1.5    val constrain: term -> typ -> term
     1.6    val param: int -> string * sort -> typ
     1.7 +  val paramify_vars: typ -> typ
     1.8    val paramify_dummies: typ -> int -> typ * int
     1.9    val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
    1.10    val infer_types: Pretty.pp -> Type.tsig ->
    1.11 @@ -41,6 +42,8 @@
    1.12  fun is_param_default (x, _) = size x > 0 andalso ord x = ord "?";
    1.13  fun param i (x, S) = TVar (("?" ^ x, i), S);
    1.14  
    1.15 +val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | T => T);
    1.16 +
    1.17  val paramify_dummies =
    1.18    let
    1.19      fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
    1.20 @@ -402,17 +405,16 @@
    1.21      val tTs' = ListPair.map Constraint (ts', Ts');
    1.22      val _ = List.app (fn t => (infer pp tsig t; ())) tTs';
    1.23  
    1.24 -    (*collect result unifier*)
    1.25 -    fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE)
    1.26 -      | ch_var xi_T = SOME xi_T;
    1.27 -    val env = map_filter ch_var (Vartab.dest Tps);
    1.28 -
    1.29      (*convert back to terms/typs*)
    1.30      val mk_var =
    1.31        if freeze then PTFree
    1.32        else (fn (x, S) => PTVar ((x, 0), S));
    1.33      val (final_Ts, final_ts) = typs_terms_of used mk_var "" (Ts', ts');
    1.34 -    val final_env = map (apsnd simple_typ_of) env;
    1.35 -  in (final_ts ~~ final_Ts, final_env) end;
    1.36 +
    1.37 +    (*collect result unifier*)
    1.38 +    val redundant = fn (xi, TVar (yi, _)) => xi = yi | _ => false;
    1.39 +    val env = filter_out redundant (map (apsnd simple_typ_of) (Vartab.dest Tps));
    1.40 +
    1.41 +  in (final_ts ~~ final_Ts, env) end;
    1.42  
    1.43  end;