src/Pure/unify.ML
changeset 32032 a6a6e8031c14
parent 29269 5c25a2012975
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/unify.ML	Fri Jul 17 21:33:00 2009 +0200
     1.2 +++ b/src/Pure/unify.ML	Fri Jul 17 21:33:00 2009 +0200
     1.3 @@ -52,36 +52,48 @@
     1.4  
     1.5  type dpair = binderlist * term * term;
     1.6  
     1.7 -fun body_type(Envir.Envir{iTs,...}) =
     1.8 -let fun bT(Type("fun",[_,T])) = bT T
     1.9 -      | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
    1.10 -    NONE => T | SOME(T') => bT T')
    1.11 -      | bT T = T
    1.12 -in bT end;
    1.13 +fun body_type env =
    1.14 +  let
    1.15 +    val tyenv = Envir.type_env env;
    1.16 +    fun bT (Type ("fun", [_, T])) = bT T
    1.17 +      | bT (T as TVar v) =
    1.18 +          (case Type.lookup tyenv v of
    1.19 +            NONE => T
    1.20 +          | SOME T' => bT T')
    1.21 +      | bT T = T;
    1.22 +  in bT end;
    1.23  
    1.24 -fun binder_types(Envir.Envir{iTs,...}) =
    1.25 -let fun bTs(Type("fun",[T,U])) = T :: bTs U
    1.26 -      | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
    1.27 -    NONE => [] | SOME(T') => bTs T')
    1.28 -      | bTs _ = []
    1.29 -in bTs end;
    1.30 +fun binder_types env =
    1.31 +  let
    1.32 +    val tyenv = Envir.type_env env;
    1.33 +    fun bTs (Type ("fun", [T, U])) = T :: bTs U
    1.34 +      | bTs (T as TVar v) =
    1.35 +          (case Type.lookup tyenv v of
    1.36 +            NONE => []
    1.37 +          | SOME T' => bTs T')
    1.38 +      | bTs _ = [];
    1.39 +  in bTs end;
    1.40  
    1.41  fun strip_type env T = (binder_types env T, body_type env T);
    1.42  
    1.43  fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
    1.44  
    1.45  
    1.46 -(*Eta normal form*)
    1.47 -fun eta_norm(env as Envir.Envir{iTs,...}) =
    1.48 -  let fun etif (Type("fun",[T,U]), t) =
    1.49 -      Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    1.50 -  | etif (TVar ixnS, t) =
    1.51 -      (case Type.lookup iTs ixnS of
    1.52 -      NONE => t | SOME(T) => etif(T,t))
    1.53 -  | etif (_,t) = t;
    1.54 -      fun eta_nm (rbinder, Abs(a,T,body)) =
    1.55 -      Abs(a, T, eta_nm ((a,T)::rbinder, body))
    1.56 -  | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
    1.57 +(* eta normal form *)
    1.58 +
    1.59 +fun eta_norm env =
    1.60 +  let
    1.61 +    val tyenv = Envir.type_env env;
    1.62 +    fun etif (Type ("fun", [T, U]), t) =
    1.63 +          Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0))
    1.64 +      | etif (TVar v, t) =
    1.65 +          (case Type.lookup tyenv v of
    1.66 +            NONE => t
    1.67 +          | SOME T => etif (T, t))
    1.68 +      | etif (_, t) = t;
    1.69 +    fun eta_nm (rbinder, Abs (a, T, body)) =
    1.70 +          Abs (a, T, eta_nm ((a, T) :: rbinder, body))
    1.71 +      | eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t);
    1.72    in eta_nm end;
    1.73  
    1.74  
    1.75 @@ -186,11 +198,14 @@
    1.76  exception ASSIGN; (*Raised if not an assignment*)
    1.77  
    1.78  
    1.79 -fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.80 -  if T=U then env
    1.81 -  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
    1.82 -       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.83 -       handle Type.TUNIFY => raise CANTUNIFY;
    1.84 +fun unify_types thy (T, U, env) =
    1.85 +  if T = U then env
    1.86 +  else
    1.87 +    let
    1.88 +      val Envir.Envir {maxidx, tenv, tyenv} = env;
    1.89 +      val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
    1.90 +    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
    1.91 +    handle Type.TUNIFY => raise CANTUNIFY;
    1.92  
    1.93  fun test_unify_types thy (args as (T,U,_)) =
    1.94  let val str_of = Syntax.string_of_typ_global thy;
    1.95 @@ -636,9 +651,9 @@
    1.96  
    1.97  
    1.98  (*Pattern matching*)
    1.99 -fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
   1.100 +fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
   1.101    let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
   1.102 -  in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
   1.103 +  in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
   1.104    handle Pattern.MATCH => Seq.empty;
   1.105  
   1.106  (*General matching -- keeps variables disjoint*)
   1.107 @@ -661,10 +676,12 @@
   1.108            Term.map_aterms (fn t as Var ((x, i), T) =>
   1.109              if i > maxidx then Var ((x, i - offset), T) else t | t => t);
   1.110  
   1.111 -        fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) =
   1.112 -          ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S)))));
   1.113 -        fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) =
   1.114 +        fun norm_tvar env ((x, i), S) =
   1.115 +          ((x, i - offset),
   1.116 +            (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
   1.117 +        fun norm_var env ((x, i), T) =
   1.118            let
   1.119 +            val tyenv = Envir.type_env env;
   1.120              val T' = Envir.norm_type tyenv T;
   1.121              val t' = Envir.norm_term env (Var ((x, i), T'));
   1.122            in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
   1.123 @@ -672,8 +689,8 @@
   1.124          fun result env =
   1.125            if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
   1.126              SOME (Envir.Envir {maxidx = maxidx,
   1.127 -              iTs = Vartab.make (map (norm_tvar env) pat_tvars),
   1.128 -              asol = Vartab.make (map (norm_var env) pat_vars)})
   1.129 +              tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
   1.130 +              tenv = Vartab.make (map (norm_var env) pat_vars)})
   1.131            else NONE;
   1.132  
   1.133          val empty = Envir.empty maxidx';