more precise treatment of existing type inference parameters;
authorwenzelm
Tue Apr 19 10:37:38 2011 +0200 (2011-04-19)
changeset 4240026c8c9cabb24
parent 42399 95b17b4901b5
child 42401 9bfaf6819291
more precise treatment of existing type inference parameters;
tuned;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Mon Apr 18 23:41:15 2011 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Apr 19 10:37:38 2011 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  sig
     1.5    val is_param: indexname -> bool
     1.6    val is_paramT: typ -> bool
     1.7 +  val param_maxidx: term -> int -> int
     1.8 +  val param_maxidx_of: term list -> int
     1.9    val param: int -> string * sort -> typ
    1.10    val mk_param: int -> sort -> typ
    1.11    val anyT: sort -> typ
    1.12 @@ -34,6 +36,12 @@
    1.13  fun is_paramT (TVar (xi, _)) = is_param xi
    1.14    | is_paramT _ = false;
    1.15  
    1.16 +val param_maxidx =
    1.17 +  (Term.fold_types o Term.fold_atyps)
    1.18 +    (fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I);
    1.19 +
    1.20 +fun param_maxidx_of ts = fold param_maxidx ts ~1;
    1.21 +
    1.22  fun param i (x, S) = TVar (("?" ^ x, i), S);
    1.23  
    1.24  fun mk_param i S = TVar (("?'a", i), S);
    1.25 @@ -69,7 +77,7 @@
    1.26  fun prepare_typ typ params_idx =
    1.27    let
    1.28      val (params', idx) = fold_atyps
    1.29 -      (fn TVar (xi as (x, _), S) =>
    1.30 +      (fn TVar (xi, S) =>
    1.31            (fn ps_idx as (ps, idx) =>
    1.32              if is_param xi andalso not (Vartab.defined ps xi)
    1.33              then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx)
    1.34 @@ -160,7 +168,7 @@
    1.35        (case Vartab.lookup tye xi of
    1.36          NONE => T
    1.37        | SOME U => deref tye U)
    1.38 -  | deref tye T = T;
    1.39 +  | deref _ T = T;
    1.40  
    1.41  fun add_parms tye T =
    1.42    (case deref tye T of
    1.43 @@ -247,7 +255,7 @@
    1.44  
    1.45      (* occurs check and assignment *)
    1.46  
    1.47 -    fun occurs_check tye xi (TVar (xi', S)) =
    1.48 +    fun occurs_check tye xi (TVar (xi', _)) =
    1.49            if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
    1.50            else
    1.51              (case Vartab.lookup tye xi' of
    1.52 @@ -343,10 +351,11 @@
    1.53          | t => t);
    1.54  
    1.55      val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
    1.56 -    val (ts', (_, _, idx)) =
    1.57 +    val idx = param_maxidx_of ts + 1;
    1.58 +    val (ts', (_, _, idx')) =
    1.59        fold_map (prepare_term ctxt const_type o constrain_vars) ts
    1.60 -        (Vartab.empty, Vartab.empty, 0);
    1.61 -  in (idx, ts') end;
    1.62 +        (Vartab.empty, Vartab.empty, idx);
    1.63 +  in (idx', ts') end;
    1.64  
    1.65  fun infer_types ctxt const_type var_type raw_ts =
    1.66    let