src/Pure/unify.ML
changeset 15797 a63605582573
parent 15574 b1d1b5bfc464
child 16425 2427be27cc60
     1.1 --- a/src/Pure/unify.ML	Thu Apr 21 19:02:54 2005 +0200
     1.2 +++ b/src/Pure/unify.ML	Thu Apr 21 19:12:03 2005 +0200
     1.3 @@ -1,13 +1,10 @@
     1.4 -(*  Title: 	unify
     1.5 +(*  Title:      Pure/unify.ML
     1.6      ID:         $Id$
     1.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   Cambridge University 1992
     1.9  
    1.10  Higher-Order Unification
    1.11  
    1.12 -Potential problem: type of Vars is often ignored, so two Vars with same
    1.13 -indexname but different types can cause errors!
    1.14 -
    1.15  Types as well as terms are unified.  The outermost functions assume the
    1.16  terms to be unified already have the same type.  In resolution, this is
    1.17  assured because both have type "prop".
    1.18 @@ -49,14 +46,14 @@
    1.19  
    1.20  fun body_type(Envir.Envir{iTs,...}) = 
    1.21  let fun bT(Type("fun",[_,T])) = bT T
    1.22 -      | bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
    1.23 +      | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
    1.24  		NONE => T | SOME(T') => bT T')
    1.25        | bT T = T
    1.26  in bT end;
    1.27  
    1.28  fun binder_types(Envir.Envir{iTs,...}) = 
    1.29  let fun bTs(Type("fun",[T,U])) = T :: bTs U
    1.30 -      | bTs(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
    1.31 +      | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
    1.32  		NONE => [] | SOME(T') => bTs T')
    1.33        | bTs _ = []
    1.34  in bTs end;
    1.35 @@ -70,8 +67,8 @@
    1.36  fun eta_norm(env as Envir.Envir{iTs,...}) =
    1.37    let fun etif (Type("fun",[T,U]), t) =
    1.38  	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    1.39 -	| etif (TVar(ixn,_),t) = 
    1.40 -	    (case Vartab.lookup (iTs,ixn) of
    1.41 +	| etif (TVar ixnS, t) = 
    1.42 +	    (case Type.lookup (iTs, ixnS) of
    1.43  		  NONE => t | SOME(T) => etif(T,t))
    1.44  	| etif (_,t) = t;
    1.45        fun eta_nm (rbinder, Abs(a,T,body)) =
    1.46 @@ -84,7 +81,11 @@
    1.47    Does the uvar occur in the term t?  
    1.48    two forms of search, for whether there is a rigid path to the current term.
    1.49    "seen" is list of variables passed thru, is a memo variable for sharing.
    1.50 -  This version searches for nonrigid occurrence, returns true if found. *)
    1.51 +  This version searches for nonrigid occurrence, returns true if found.
    1.52 +  Since terms may contain variables with same name and different types,
    1.53 +  the occurs check must ignore the types of variables. This avoids
    1.54 +  that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
    1.55 +  substitution when ?'a is instantiated with T later. *)
    1.56  fun occurs_terms (seen: (indexname list) ref,
    1.57   		  env: Envir.env, v: indexname, ts: term list): bool =
    1.58    let fun occurs [] = false
    1.59 @@ -92,12 +93,12 @@
    1.60        and occur (Const _)  = false
    1.61  	| occur (Bound _)  = false
    1.62  	| occur (Free _)  = false
    1.63 -	| occur (Var (w,_))  = 
    1.64 +	| occur (Var (w, T))  = 
    1.65  	    if mem_ix (w, !seen) then false
    1.66  	    else if eq_ix(v,w) then true
    1.67  	      (*no need to lookup: v has no assignment*)
    1.68  	    else (seen := w:: !seen;  
    1.69 -	          case  Envir.lookup(env,w)  of
    1.70 +	          case Envir.lookup (env, (w, T)) of
    1.71  		      NONE    => false
    1.72  		    | SOME t => occur t)
    1.73  	| occur (Abs(_,_,body)) = occur body
    1.74 @@ -109,7 +110,7 @@
    1.75  (* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
    1.76  fun head_of_in (env,t) : term = case t of
    1.77      f$_ => head_of_in(env,f)
    1.78 -  | Var (v,_) => (case  Envir.lookup(env,v)  of  
    1.79 +  | Var vT => (case Envir.lookup (env, vT) of  
    1.80  			SOME u => head_of_in(env,u)  |  NONE   => t)
    1.81    | _ => t;
    1.82  
    1.83 @@ -155,11 +156,11 @@
    1.84        and occur (Const _)  = NoOcc
    1.85  	| occur (Bound _)  = NoOcc
    1.86  	| occur (Free _)  = NoOcc
    1.87 -	| occur (Var (w,_))  = 
    1.88 +	| occur (Var (w, T))  = 
    1.89  	    if mem_ix (w, !seen) then NoOcc
    1.90  	    else if eq_ix(v,w) then Rigid
    1.91  	    else (seen := w:: !seen;  
    1.92 -	          case  Envir.lookup(env,w)  of
    1.93 +	          case Envir.lookup (env, (w, T)) of
    1.94  		      NONE    => NoOcc
    1.95  		    | SOME t => occur t)
    1.96  	| occur (Abs(_,_,body)) = occur body
    1.97 @@ -210,11 +211,11 @@
    1.98    If v occurs rigidly then nonunifiable.
    1.99    If v occurs nonrigidly then must use full algorithm. *)
   1.100  fun assignment (env, rbinder, t, u) =
   1.101 -    let val (v,T) = get_eta_var(rbinder,0,t)
   1.102 -    in  case rigid_occurs_term (ref[], env, v, u) of
   1.103 +    let val vT as (v,T) = get_eta_var (rbinder, 0, t)
   1.104 +    in  case rigid_occurs_term (ref [], env, v, u) of
   1.105  	      NoOcc => let val env = unify_types(body_type env T,
   1.106  						 fastype env (rbinder,u),env)
   1.107 -		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
   1.108 +		in Envir.update ((vT, rlist_abs (rbinder, u)), env) end
   1.109  	    | Nonrigid =>  raise ASSIGN
   1.110  	    | Rigid =>  raise CANTUNIFY
   1.111      end;
   1.112 @@ -282,7 +283,7 @@
   1.113  
   1.114  (* changed(env,t) checks whether the head of t is a variable assigned in env*)
   1.115  fun changed (env, f$_) = changed (env,f)
   1.116 -  | changed (env, Var (v,_)) =
   1.117 +  | changed (env, Var v) =
   1.118        (case Envir.lookup(env,v) of NONE=>false  |  _ => true)
   1.119    | changed _ = false;
   1.120  
   1.121 @@ -395,12 +396,12 @@
   1.122  (*Call matchcopy to produce assignments to the variable in the dpair*)
   1.123  fun MATCH (env, (rbinder,t,u), dpairs)
   1.124  	: (Envir.env * dpair list)Seq.seq = 
   1.125 -  let val (Var(v,T), targs) = strip_comb t;
   1.126 +  let val (Var (vT as (v, T)), targs) = strip_comb t;
   1.127        val Ts = binder_types env T;
   1.128        fun new_dset (u', (env',dpairs')) =
   1.129  	  (*if v was updated to s, must unify s with u' *)
   1.130 -	  case Envir.lookup(env',v) of
   1.131 -	      NONE => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
   1.132 +	  case Envir.lookup (env', vT) of
   1.133 +	      NONE => (Envir.update ((vT, types_abs(Ts, u')), env'),  dpairs')
   1.134  	    | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   1.135    in Seq.map new_dset
   1.136           (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   1.137 @@ -413,12 +414,12 @@
   1.138  (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
   1.139    Attempts to update t with u, raising ASSIGN if impossible*)
   1.140  fun ff_assign(env, rbinder, t, u) : Envir.env = 
   1.141 -let val (v,T) = get_eta_var(rbinder,0,t)
   1.142 -in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
   1.143 +let val vT as (v,T) = get_eta_var(rbinder,0,t)
   1.144 +in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
   1.145     else let val env = unify_types(body_type env T,
   1.146  				  fastype env (rbinder,u),
   1.147  				  env)
   1.148 -	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
   1.149 +	in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end
   1.150  end;
   1.151  
   1.152  
   1.153 @@ -494,7 +495,7 @@
   1.154      if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   1.155      else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
   1.156  	     val body = list_comb(v', map (Bound o #j) args)
   1.157 -	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
   1.158 +	     val env2 = Envir.vupdate ((((v, T), types_abs(Ts, body)),   env'))
   1.159  	     (*the vupdate affects ts' if they contain v*)
   1.160  	 in  
   1.161  	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
   1.162 @@ -615,12 +616,12 @@
   1.163      requires more work yet gives a less general unifier (fewer variables).
   1.164    Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   1.165  fun smash_flexflex1 ((t,u), env) : Envir.env =
   1.166 -  let val (v,T) = var_head_of (env,t)
   1.167 -      and (w,U) = var_head_of (env,u);
   1.168 +  let val vT as (v,T) = var_head_of (env,t)
   1.169 +      and wU as (w,U) = var_head_of (env,u);
   1.170        val (env', var) = Envir.genvar (#1v) (env, body_type env T)
   1.171 -      val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
   1.172 -  in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
   1.173 -      else Envir.vupdate((v, type_abs(env',T,var)), env'')
   1.174 +      val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env')
   1.175 +  in  if vT = wU then env''  (*the other update would be identical*)
   1.176 +      else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
   1.177    end;
   1.178  
   1.179