internal params: Vartab instead of AList;
authorwenzelm
Wed Sep 27 21:13:11 2006 +0200 (2006-09-27)
changeset 20735a041bf3c8f2f
parent 20734 8aa9590bd452
child 20736 934358468a1b
internal params: Vartab instead of AList;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Wed Sep 27 21:13:09 2006 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Wed Sep 27 21:13:11 2006 +0200
     1.3 @@ -118,12 +118,12 @@
     1.4      val params' = fold_atyps
     1.5        (fn TVar (xi as (x, _), S) =>
     1.6            (fn ps =>
     1.7 -            if is_param xi andalso not (AList.defined (op =) ps xi)
     1.8 -            then (xi, mk_param S) :: ps else ps)
     1.9 +            if is_param xi andalso not (Vartab.defined ps xi)
    1.10 +            then Vartab.update (xi, mk_param S) ps else ps)
    1.11          | _ => I) typ params;
    1.12  
    1.13      fun pre_of (TVar (v as (xi, _))) =
    1.14 -          (case AList.lookup (op =) params' xi of
    1.15 +          (case Vartab.lookup params' xi of
    1.16              NONE => PTVar v
    1.17            | SOME p => p)
    1.18        | pre_of (TFree ("'_dummy_", S)) = mk_param S
    1.19 @@ -139,8 +139,8 @@
    1.20  fun preterm_of const_type is_param tm (vparams, params) =
    1.21    let
    1.22      fun add_vparm xi ps =
    1.23 -      if not (AList.defined Term.eq_ix ps xi) then
    1.24 -        (xi, mk_param []) :: ps
    1.25 +      if not (Vartab.defined ps xi) then
    1.26 +        Vartab.update (xi, mk_param []) ps
    1.27        else ps;
    1.28  
    1.29      val vparams' = fold_aterms
    1.30 @@ -149,10 +149,11 @@
    1.31          | Free (x, _) => add_vparm (x, ~1)
    1.32          | _ => I)
    1.33        tm vparams;
    1.34 -    fun var_param xi = (the o AList.lookup (op =) vparams') xi;
    1.35 +    fun var_param xi = the (Vartab.lookup vparams' xi);
    1.36  
    1.37  
    1.38      val preT_of = pretyp_of is_param;
    1.39 +    fun polyT_of T = fst (pretyp_of (K true) T Vartab.empty);
    1.40  
    1.41      fun constrain T t ps =
    1.42        if T = dummyT then (t, ps)
    1.43 @@ -162,10 +163,9 @@
    1.44  
    1.45      fun pre_of (Const (c, T)) ps =
    1.46            (case const_type c of
    1.47 -            SOME U => constrain T (PConst (c, fst (pretyp_of (K true) U []))) ps
    1.48 +            SOME U => constrain T (PConst (c, polyT_of U)) ps
    1.49            | NONE => raise TYPE ("No such constant: " ^ quote c, [], []))
    1.50 -      | pre_of (Var (xi, Type ("_polymorphic_", [T]))) ps =
    1.51 -          (PVar (xi, fst (pretyp_of (K true) T [])), ps)
    1.52 +      | pre_of (Var (xi, Type ("_polymorphic_", [T]))) ps = (PVar (xi, polyT_of T), ps)
    1.53        | pre_of (Var (xi, T)) ps = constrain T (PVar (xi, var_param xi)) ps
    1.54        | pre_of (Free (x, T)) ps = constrain T (PFree (x, var_param (x, ~1))) ps
    1.55        | pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps =
    1.56 @@ -397,8 +397,8 @@
    1.57  fun basic_infer_types pp tsig const_type used freeze is_param ts Ts =
    1.58    let
    1.59      (*convert to preterms/typs*)
    1.60 -    val (Ts', Tps) = fold_map (pretyp_of (K true)) Ts [];
    1.61 -    val (ts', (vps, ps)) = fold_map (preterm_of const_type is_param) ts ([], Tps);
    1.62 +    val (Ts', Tps) = fold_map (pretyp_of (K true)) Ts Vartab.empty;
    1.63 +    val (ts', (vps, ps)) = fold_map (preterm_of const_type is_param) ts (Vartab.empty, Tps);
    1.64  
    1.65      (*run type inference*)
    1.66      val tTs' = ListPair.map Constraint (ts', Ts');
    1.67 @@ -407,7 +407,7 @@
    1.68      (*collect result unifier*)
    1.69      fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE)
    1.70        | ch_var xi_T = SOME xi_T;
    1.71 -    val env = map_filter ch_var Tps;
    1.72 +    val env = map_filter ch_var (Vartab.dest Tps);
    1.73  
    1.74      (*convert back to terms/typs*)
    1.75      val mk_var =