Removed add_env because Vartab.map was too slow for large environments.
authorberghofe
Mon Oct 21 17:15:40 2002 +0200 (2002-10-21 ago)
changeset 13666a2730043029b
parent 13665 66e151df01c8
child 13667 0009325e9af0
Removed add_env because Vartab.map was too slow for large environments.
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Mon Oct 21 17:14:19 2002 +0200
     1.2 +++ b/src/Pure/type.ML	Mon Oct 21 17:15:40 2002 +0200
     1.3 @@ -755,13 +755,6 @@
     1.4    | devar (T, tye) = T;
     1.5  
     1.6  
     1.7 -(* add_env *)
     1.8 -
     1.9 -(*avoids chains 'a |-> 'b |-> 'c ...*)
    1.10 -fun add_env (vT as (v, T), tab) = Vartab.update_new (vT, Vartab.map
    1.11 -  (fn (U as (TVar (w, S))) => if eq_ix (v, w) then T else U | U => U) tab);
    1.12 -
    1.13 -
    1.14  (* unify *)
    1.15  
    1.16  fun unify (tsig as TySg {classrel, arities, ...}) (tyenv, maxidx) TU =
    1.17 @@ -775,7 +768,8 @@
    1.18      fun meet ((_, []), tye) = tye
    1.19        | meet ((TVar (xi, S'), S), tye) =
    1.20            if Sorts.sort_le classrel (S', S) then tye
    1.21 -          else add_env ((xi, gen_tyvar (Sorts.inter_sort classrel (S', S))), tye)
    1.22 +          else Vartab.update_new ((xi,
    1.23 +            gen_tyvar (Sorts.inter_sort classrel (S', S))), tye)
    1.24        | meet ((TFree (_, S'), S), tye) =
    1.25            if Sorts.sort_le classrel (S', S) then tye
    1.26            else raise TUNIFY
    1.27 @@ -789,18 +783,20 @@
    1.28        (case (devar (ty1, tye), devar (ty2, tye)) of
    1.29          (T as TVar (v, S1), U as TVar (w, S2)) =>
    1.30            if eq_ix (v, w) then tye
    1.31 -          else if Sorts.sort_le classrel (S1, S2) then add_env ((w, T), tye)
    1.32 -          else if Sorts.sort_le classrel (S2, S1) then add_env ((v, U), tye)
    1.33 +          else if Sorts.sort_le classrel (S1, S2) then
    1.34 +            Vartab.update_new ((w, T), tye)
    1.35 +          else if Sorts.sort_le classrel (S2, S1) then
    1.36 +            Vartab.update_new ((v, U), tye)
    1.37            else
    1.38              let val S = gen_tyvar (Sorts.inter_sort classrel (S1, S2)) in
    1.39 -              add_env ((v, S), add_env ((w, S), tye))
    1.40 +              Vartab.update_new ((v, S), Vartab.update_new ((w, S), tye))
    1.41              end
    1.42        | (TVar (v, S), T) =>
    1.43            if occurs v tye T then raise TUNIFY
    1.44 -          else meet ((T, S), add_env ((v, T), tye))
    1.45 +          else meet ((T, S), Vartab.update_new ((v, T), tye))
    1.46        | (T, TVar (v, S)) =>
    1.47            if occurs v tye T then raise TUNIFY
    1.48 -          else meet ((T, S), add_env ((v, T), tye))
    1.49 +          else meet ((T, S), Vartab.update_new ((v, T), tye))
    1.50        | (Type (a, Ts), Type (b, Us)) =>
    1.51            if a <> b then raise TUNIFY
    1.52            else foldr unif (Ts ~~ Us, tye)