src/Pure/unify.ML
changeset 1458 fd510875fb71
parent 1435 aefcd255ed4a
child 1460 5a6f2aabd538
     1.1 --- a/src/Pure/unify.ML	Mon Jan 29 13:50:10 1996 +0100
     1.2 +++ b/src/Pure/unify.ML	Mon Jan 29 13:56:41 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	unify
     1.5 +(*  Title:      unify
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   Cambridge University 1992
    1.10  
    1.11  Higher-Order Unification
    1.12 @@ -28,16 +28,16 @@
    1.13    val combound : (term*int*int) -> term
    1.14    val rlist_abs: (string*typ)list * term -> term   
    1.15    val smash_unifiers : Sign.sg * Envir.env * (term*term)list
    1.16 -	-> (Envir.env Sequence.seq)
    1.17 +        -> (Envir.env Sequence.seq)
    1.18    val unifiers: Sign.sg * Envir.env * ((term*term)list)
    1.19 -	-> (Envir.env * (term * term)list) Sequence.seq
    1.20 +        -> (Envir.env * (term * term)list) Sequence.seq
    1.21  end;
    1.22  
    1.23  functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE
    1.24                    and Pattern:PATTERN
    1.25                    sharing type Sign.sg = Pattern.sg
    1.26                    and     type Envir.env = Pattern.env)
    1.27 -	: UNIFY = 
    1.28 +        : UNIFY = 
    1.29  struct
    1.30  
    1.31  structure Sign = Sign;
    1.32 @@ -47,11 +47,11 @@
    1.33  
    1.34  (*Unification options*)
    1.35  
    1.36 -val trace_bound = ref 10	(*tracing starts above this depth, 0 for full*)
    1.37 -and search_bound = ref 20	(*unification quits above this depth*)
    1.38 -and trace_simp = ref false	(*print dpairs before calling SIMPL*)
    1.39 -and trace_types = ref false	(*announce potential incompleteness
    1.40 -				  of type unification*)
    1.41 +val trace_bound = ref 10        (*tracing starts above this depth, 0 for full*)
    1.42 +and search_bound = ref 20       (*unification quits above this depth*)
    1.43 +and trace_simp = ref false      (*print dpairs before calling SIMPL*)
    1.44 +and trace_types = ref false     (*announce potential incompleteness
    1.45 +                                  of type unification*)
    1.46  
    1.47  val sgr = ref(Sign.proto_pure);
    1.48  
    1.49 @@ -62,14 +62,14 @@
    1.50  fun body_type(Envir.Envir{iTs,...}) = 
    1.51  let fun bT(Type("fun",[_,T])) = bT T
    1.52        | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
    1.53 -		None => T | Some(T') => bT T')
    1.54 +                None => T | Some(T') => bT T')
    1.55        | bT T = T
    1.56  in bT end;
    1.57  
    1.58  fun binder_types(Envir.Envir{iTs,...}) = 
    1.59  let fun bTs(Type("fun",[T,U])) = T :: bTs U
    1.60        | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
    1.61 -		None => [] | Some(T') => bTs T')
    1.62 +                None => [] | Some(T') => bTs T')
    1.63        | bTs _ = []
    1.64  in bTs end;
    1.65  
    1.66 @@ -82,7 +82,7 @@
    1.67    inefficiency, avoid partial application:  if an atom is applied to
    1.68    any arguments at all, apply it to its full number of arguments.
    1.69    For
    1.70 -    rbinder = [(x1,T),...,(xm,Tm)]		(user's var names preserved!)
    1.71 +    rbinder = [(x1,T),...,(xm,Tm)]              (user's var names preserved!)
    1.72      args  =   [arg1,...,argn]
    1.73    the value of 
    1.74        (xm,...,x1)(head(arg1,...,argn))  remains invariant.
    1.75 @@ -92,18 +92,18 @@
    1.76  in
    1.77    fun head_norm (env,t) : term =
    1.78      let fun hnorm (Var (v,T)) = 
    1.79 -	      (case Envir.lookup (env,v) of
    1.80 -		  Some u => head_norm (env, u)
    1.81 -		| None   => raise SAME)
    1.82 -	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
    1.83 -	  | hnorm (Abs(_,_,body) $ t) =
    1.84 -	      head_norm (env, subst_bounds([t], body))
    1.85 -	  | hnorm (f $ t) =
    1.86 -	      (case hnorm f of
    1.87 -		 Abs(_,_,body) =>
    1.88 -		   head_norm (env, subst_bounds([t], body))
    1.89 -	       | nf => nf $ t)
    1.90 -	  | hnorm _ =  raise SAME
    1.91 +              (case Envir.lookup (env,v) of
    1.92 +                  Some u => head_norm (env, u)
    1.93 +                | None   => raise SAME)
    1.94 +          | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
    1.95 +          | hnorm (Abs(_,_,body) $ t) =
    1.96 +              head_norm (env, subst_bounds([t], body))
    1.97 +          | hnorm (f $ t) =
    1.98 +              (case hnorm f of
    1.99 +                 Abs(_,_,body) =>
   1.100 +                   head_norm (env, subst_bounds([t], body))
   1.101 +               | nf => nf $ t)
   1.102 +          | hnorm _ =  raise SAME
   1.103      in  hnorm t  handle SAME=> t  end
   1.104  end;
   1.105  
   1.106 @@ -113,18 +113,18 @@
   1.107  fun fastype (Envir.Envir{iTs,...}) =
   1.108  let val funerr = "fastype: expected function type";
   1.109      fun fast(rbinder, f$u) =
   1.110 -	(case (fast (rbinder, f)) of
   1.111 -	   Type("fun",[_,T]) => T
   1.112 -	 | TVar(ixn,_) =>
   1.113 -		(case assoc(iTs,ixn) of
   1.114 -		   Some(Type("fun",[_,T])) => T
   1.115 -		 | _ => raise TERM(funerr, [f$u]))
   1.116 -	 | _ => raise TERM(funerr, [f$u]))
   1.117 +        (case (fast (rbinder, f)) of
   1.118 +           Type("fun",[_,T]) => T
   1.119 +         | TVar(ixn,_) =>
   1.120 +                (case assoc(iTs,ixn) of
   1.121 +                   Some(Type("fun",[_,T])) => T
   1.122 +                 | _ => raise TERM(funerr, [f$u]))
   1.123 +         | _ => raise TERM(funerr, [f$u]))
   1.124        | fast (rbinder, Const (_,T)) = T
   1.125        | fast (rbinder, Free (_,T)) = T
   1.126        | fast (rbinder, Bound i) =
   1.127 -	(#2 (nth_elem (i,rbinder))
   1.128 -  	 handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
   1.129 +        (#2 (nth_elem (i,rbinder))
   1.130 +         handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
   1.131        | fast (rbinder, Var (_,T)) = T 
   1.132        | fast (rbinder, Abs (_,T,u)) =  T --> fast (("",T) :: rbinder, u)
   1.133  in fast end;
   1.134 @@ -133,14 +133,14 @@
   1.135  (*Eta normal form*)
   1.136  fun eta_norm(env as Envir.Envir{iTs,...}) =
   1.137    let fun etif (Type("fun",[T,U]), t) =
   1.138 -	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
   1.139 -	| etif (TVar(ixn,_),t) = 
   1.140 -	    (case assoc(iTs,ixn) of
   1.141 -		  None => t | Some(T) => etif(T,t))
   1.142 -	| etif (_,t) = t;
   1.143 +            Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
   1.144 +        | etif (TVar(ixn,_),t) = 
   1.145 +            (case assoc(iTs,ixn) of
   1.146 +                  None => t | Some(T) => etif(T,t))
   1.147 +        | etif (_,t) = t;
   1.148        fun eta_nm (rbinder, Abs(a,T,body)) =
   1.149 -	    Abs(a, T, eta_nm ((a,T)::rbinder, body))
   1.150 -	| eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
   1.151 +            Abs(a, T, eta_nm ((a,T)::rbinder, body))
   1.152 +        | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
   1.153    in eta_nm end;
   1.154  
   1.155  
   1.156 @@ -150,22 +150,22 @@
   1.157    "seen" is list of variables passed thru, is a memo variable for sharing.
   1.158    This version searches for nonrigid occurrence, returns true if found. *)
   1.159  fun occurs_terms (seen: (indexname list) ref,
   1.160 - 		  env: Envir.env, v: indexname, ts: term list): bool =
   1.161 +                  env: Envir.env, v: indexname, ts: term list): bool =
   1.162    let fun occurs [] = false
   1.163 -	| occurs (t::ts) =  occur t  orelse  occurs ts
   1.164 +        | occurs (t::ts) =  occur t  orelse  occurs ts
   1.165        and occur (Const _)  = false
   1.166 -	| occur (Bound _)  = false
   1.167 -	| occur (Free _)  = false
   1.168 -	| occur (Var (w,_))  = 
   1.169 -	    if w mem !seen then false
   1.170 -	    else if v=w then true
   1.171 -	      (*no need to lookup: v has no assignment*)
   1.172 -	    else (seen := w:: !seen;  
   1.173 -	          case  Envir.lookup(env,w)  of
   1.174 -		      None    => false
   1.175 -		    | Some t => occur t)
   1.176 -	| occur (Abs(_,_,body)) = occur body
   1.177 -	| occur (f$t) = occur t  orelse   occur f
   1.178 +        | occur (Bound _)  = false
   1.179 +        | occur (Free _)  = false
   1.180 +        | occur (Var (w,_))  = 
   1.181 +            if w mem !seen then false
   1.182 +            else if v=w then true
   1.183 +              (*no need to lookup: v has no assignment*)
   1.184 +            else (seen := w:: !seen;  
   1.185 +                  case  Envir.lookup(env,w)  of
   1.186 +                      None    => false
   1.187 +                    | Some t => occur t)
   1.188 +        | occur (Abs(_,_,body)) = occur body
   1.189 +        | occur (f$t) = occur t  orelse   occur f
   1.190    in  occurs ts  end;
   1.191  
   1.192  
   1.193 @@ -174,7 +174,7 @@
   1.194  fun head_of_in (env,t) : term = case t of
   1.195      f$_ => head_of_in(env,f)
   1.196    | Var (v,_) => (case  Envir.lookup(env,v)  of  
   1.197 -			Some u => head_of_in(env,u)  |  None   => t)
   1.198 +                        Some u => head_of_in(env,u)  |  None   => t)
   1.199    | _ => t;
   1.200  
   1.201  
   1.202 @@ -205,9 +205,9 @@
   1.203  *)
   1.204  fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 
   1.205    let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 
   1.206 -		       else NoOcc
   1.207 +                       else NoOcc
   1.208        fun occurs [] = NoOcc
   1.209 -	| occurs (t::ts) =
   1.210 +        | occurs (t::ts) =
   1.211              (case occur t of
   1.212                 Rigid => Rigid
   1.213               | oc =>  (case occurs ts of NoOcc => oc  |  oc2 => oc2))
   1.214 @@ -217,28 +217,28 @@
   1.215               | oc =>  (case occomb f of NoOcc => oc  |  oc2 => oc2))
   1.216          | occomb t = occur t
   1.217        and occur (Const _)  = NoOcc
   1.218 -	| occur (Bound _)  = NoOcc
   1.219 -	| occur (Free _)  = NoOcc
   1.220 -	| occur (Var (w,_))  = 
   1.221 -	    if w mem !seen then NoOcc
   1.222 -	    else if v=w then Rigid
   1.223 -	    else (seen := w:: !seen;  
   1.224 -	          case  Envir.lookup(env,w)  of
   1.225 -		      None    => NoOcc
   1.226 -		    | Some t => occur t)
   1.227 -	| occur (Abs(_,_,body)) = occur body
   1.228 -	| occur (t as f$_) =  (*switch to nonrigid search?*)
   1.229 -	   (case head_of_in (env,f) of
   1.230 -	      Var (w,_) => (*w is not assigned*)
   1.231 -		if v=w then Rigid  
   1.232 -		else  nonrigid t
   1.233 -	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
   1.234 -	    | _ => occomb t)
   1.235 +        | occur (Bound _)  = NoOcc
   1.236 +        | occur (Free _)  = NoOcc
   1.237 +        | occur (Var (w,_))  = 
   1.238 +            if w mem !seen then NoOcc
   1.239 +            else if v=w then Rigid
   1.240 +            else (seen := w:: !seen;  
   1.241 +                  case  Envir.lookup(env,w)  of
   1.242 +                      None    => NoOcc
   1.243 +                    | Some t => occur t)
   1.244 +        | occur (Abs(_,_,body)) = occur body
   1.245 +        | occur (t as f$_) =  (*switch to nonrigid search?*)
   1.246 +           (case head_of_in (env,f) of
   1.247 +              Var (w,_) => (*w is not assigned*)
   1.248 +                if v=w then Rigid  
   1.249 +                else  nonrigid t
   1.250 +            | Abs(_,_,body) => nonrigid t (*not in normal form*)
   1.251 +            | _ => occomb t)
   1.252    in  occur t  end;
   1.253  
   1.254  
   1.255 -exception CANTUNIFY;	(*Signals non-unifiability.  Does not signal errors!*)
   1.256 -exception ASSIGN;	(*Raised if not an assignment*)
   1.257 +exception CANTUNIFY;    (*Signals non-unifiability.  Does not signal errors!*)
   1.258 +exception ASSIGN;       (*Raised if not an assignment*)
   1.259  
   1.260  
   1.261  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   1.262 @@ -261,8 +261,8 @@
   1.263    Result is var a for use in SIMPL. *)
   1.264  fun get_eta_var ([], _, Var vT)  =  vT
   1.265    | get_eta_var (_::rbinder, n, f $ Bound i) =
   1.266 -	if  n=i  then  get_eta_var (rbinder, n+1, f) 
   1.267 -		 else  raise ASSIGN
   1.268 +        if  n=i  then  get_eta_var (rbinder, n+1, f) 
   1.269 +                 else  raise ASSIGN
   1.270    | get_eta_var _ = raise ASSIGN;
   1.271  
   1.272  
   1.273 @@ -277,11 +277,11 @@
   1.274  fun assignment (env, rbinder, t, u) =
   1.275      let val (v,T) = get_eta_var(rbinder,0,t)
   1.276      in  case rigid_occurs_term (ref[], env, v, u) of
   1.277 -	      NoOcc => let val env = unify_types(body_type env T,
   1.278 -						 fastype env (rbinder,u),env)
   1.279 -		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
   1.280 -	    | Nonrigid =>  raise ASSIGN
   1.281 -	    | Rigid =>  raise CANTUNIFY
   1.282 +              NoOcc => let val env = unify_types(body_type env T,
   1.283 +                                                 fastype env (rbinder,u),env)
   1.284 +                in Envir.update ((v, rlist_abs(rbinder,u)), env) end
   1.285 +            | Nonrigid =>  raise ASSIGN
   1.286 +            | Rigid =>  raise CANTUNIFY
   1.287      end;
   1.288  
   1.289  
   1.290 @@ -291,9 +291,9 @@
   1.291      if not, raises TERM, probably indicating type mismatch.
   1.292    Uses variable a (unless the null string) to preserve user's naming.*) 
   1.293  fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
   1.294 -	let val env' = unify_types(T,U,env)
   1.295 -	    val c = if a="" then b else a
   1.296 -	in new_dpair((c,T) :: rbinder, body1, body2, env') end
   1.297 +        let val env' = unify_types(T,U,env)
   1.298 +            val c = if a="" then b else a
   1.299 +        in new_dpair((c,T) :: rbinder, body1, body2, env') end
   1.300      | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
   1.301      | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
   1.302      | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
   1.303 @@ -301,8 +301,8 @@
   1.304  
   1.305  fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
   1.306       new_dpair (rbinder,
   1.307 -		eta_norm env (rbinder, head_norm(env,t)),
   1.308 -	  	eta_norm env (rbinder, head_norm(env,u)), env);
   1.309 +                eta_norm env (rbinder, head_norm(env,t)),
   1.310 +                eta_norm env (rbinder, head_norm(env,u)), env);
   1.311  
   1.312  
   1.313  
   1.314 @@ -313,34 +313,34 @@
   1.315      do so caused numerous problems with no compensating advantage.
   1.316  *)
   1.317  fun SIMPL0 (dp0, (env,flexflex,flexrigid))
   1.318 -	: Envir.env * dpair list * dpair list =
   1.319 +        : Envir.env * dpair list * dpair list =
   1.320      let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
   1.321 -	    fun SIMRANDS(f$t, g$u, env) =
   1.322 -			SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
   1.323 -	      | SIMRANDS (t as _$_, _, _) =
   1.324 -		raise TERM ("SIMPL: operands mismatch", [t,u])
   1.325 -	      | SIMRANDS (t, u as _$_, _) =
   1.326 -		raise TERM ("SIMPL: operands mismatch", [t,u])
   1.327 -	      | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
   1.328 +            fun SIMRANDS(f$t, g$u, env) =
   1.329 +                        SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
   1.330 +              | SIMRANDS (t as _$_, _, _) =
   1.331 +                raise TERM ("SIMPL: operands mismatch", [t,u])
   1.332 +              | SIMRANDS (t, u as _$_, _) =
   1.333 +                raise TERM ("SIMPL: operands mismatch", [t,u])
   1.334 +              | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
   1.335      in case (head_of t, head_of u) of
   1.336         (Var(_,T), Var(_,U)) =>
   1.337 -	    let val T' = body_type env T and U' = body_type env U;
   1.338 -		val env = unify_types(T',U',env)
   1.339 -	    in (env, dp::flexflex, flexrigid) end
   1.340 +            let val T' = body_type env T and U' = body_type env U;
   1.341 +                val env = unify_types(T',U',env)
   1.342 +            in (env, dp::flexflex, flexrigid) end
   1.343       | (Var _, _) =>
   1.344 -	    ((assignment (env,rbinder,t,u), flexflex, flexrigid)
   1.345 -	     handle ASSIGN => (env, flexflex, dp::flexrigid))
   1.346 +            ((assignment (env,rbinder,t,u), flexflex, flexrigid)
   1.347 +             handle ASSIGN => (env, flexflex, dp::flexrigid))
   1.348       | (_, Var _) =>
   1.349 -	    ((assignment (env,rbinder,u,t), flexflex, flexrigid)
   1.350 -	     handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
   1.351 +            ((assignment (env,rbinder,u,t), flexflex, flexrigid)
   1.352 +             handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
   1.353       | (Const(a,T), Const(b,U)) =>
   1.354 -	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   1.355 -	    else raise CANTUNIFY
   1.356 +            if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   1.357 +            else raise CANTUNIFY
   1.358       | (Bound i,    Bound j)    =>
   1.359 -	    if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
   1.360 +            if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
   1.361       | (Free(a,T),  Free(b,U))  =>
   1.362 -	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   1.363 -	    else raise CANTUNIFY
   1.364 +            if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   1.365 +            else raise CANTUNIFY
   1.366       | _ => raise CANTUNIFY
   1.367      end;
   1.368  
   1.369 @@ -356,8 +356,8 @@
   1.370    Clever would be to re-do just the affected dpairs*)
   1.371  fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
   1.372      let val all as (env',flexflex,flexrigid) =
   1.373 -	    foldr SIMPL0 (dpairs, (env,[],[]));
   1.374 -	val dps = flexrigid@flexflex
   1.375 +            foldr SIMPL0 (dpairs, (env,[],[]));
   1.376 +        val dps = flexrigid@flexflex
   1.377      in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
   1.378         then SIMPL(env',dps) else all
   1.379      end;
   1.380 @@ -376,7 +376,7 @@
   1.381  fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
   1.382    | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
   1.383         let fun funtype T = binder--->T;
   1.384 -	   val (env', vars) = Envir.genvars name (env, map funtype Ts)
   1.385 +           val (env', vars) = Envir.genvars name (env, map funtype Ts)
   1.386         in  (env',  map (fn var=> combound(var, 0, length binder)) vars)  end;
   1.387  
   1.388  
   1.389 @@ -398,60 +398,60 @@
   1.390    The order for trying projections is crucial in ?b'(?a)   
   1.391    NB "vname" is only used in the call to make_args!!   *)
   1.392  fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
   1.393 -	: (term * (Envir.env * dpair list))Sequence.seq =
   1.394 +        : (term * (Envir.env * dpair list))Sequence.seq =
   1.395  let (*Produce copies of uarg and cons them in front of uargs*)
   1.396      fun copycons uarg (uargs, (env, dpairs)) =
   1.397 -	Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
   1.398 -	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
   1.399 -		 (env, dpairs)));
   1.400 -	(*Produce sequence of all possible ways of copying the arg list*)
   1.401 +        Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
   1.402 +            (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
   1.403 +                 (env, dpairs)));
   1.404 +        (*Produce sequence of all possible ways of copying the arg list*)
   1.405      fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
   1.406        | copyargs (uarg::uargs) =
   1.407 -	    Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
   1.408 +            Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
   1.409      val (uhead,uargs) = strip_comb u;
   1.410      val base = body_type env (fastype env (rbinder,uhead));
   1.411      fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
   1.412      (*attempt projection on argument with given typ*)
   1.413      val Ts = map (curry (fastype env) rbinder) targs;
   1.414      fun projenv (head, (Us,bary), targ, tail) = 
   1.415 -	let val env = if !trace_types then test_unify_types(base,bary,env)
   1.416 -		      else unify_types(base,bary,env)
   1.417 -	in Sequence.seqof (fn () =>  
   1.418 -	    let val (env',args) = make_args vname (Ts,env,Us);
   1.419 -		(*higher-order projection: plug in targs for bound vars*)
   1.420 -		fun plugin arg = list_comb(head_of arg, targs);
   1.421 -		val dp = (rbinder, list_comb(targ, map plugin args), u);
   1.422 -		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
   1.423 -		    (*may raise exception CANTUNIFY*)
   1.424 -	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
   1.425 -			tail)
   1.426 -	    end  handle CANTUNIFY => Sequence.pull tail)
   1.427 -	end handle CANTUNIFY => tail;
   1.428 +        let val env = if !trace_types then test_unify_types(base,bary,env)
   1.429 +                      else unify_types(base,bary,env)
   1.430 +        in Sequence.seqof (fn () =>  
   1.431 +            let val (env',args) = make_args vname (Ts,env,Us);
   1.432 +                (*higher-order projection: plug in targs for bound vars*)
   1.433 +                fun plugin arg = list_comb(head_of arg, targs);
   1.434 +                val dp = (rbinder, list_comb(targ, map plugin args), u);
   1.435 +                val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
   1.436 +                    (*may raise exception CANTUNIFY*)
   1.437 +            in  Some ((list_comb(head,args), (env2, frigid@fflex)),
   1.438 +                        tail)
   1.439 +            end  handle CANTUNIFY => Sequence.pull tail)
   1.440 +        end handle CANTUNIFY => tail;
   1.441      (*make a list of projections*)
   1.442      fun make_projs (T::Ts, targ::targs) =
   1.443 -	      (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
   1.444 +              (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
   1.445        | make_projs ([],[]) = []
   1.446        | make_projs _ = raise TERM ("make_projs", u::targs);
   1.447      (*try projections and imitation*)
   1.448      fun matchfun ((bvar,T,targ)::projs) =
   1.449 -	       (projenv(bvar, strip_type env T, targ, matchfun projs))
   1.450 +               (projenv(bvar, strip_type env T, targ, matchfun projs))
   1.451        | matchfun [] = (*imitation last of all*)
   1.452 -	      (case uhead of
   1.453 -		 Const _ => Sequence.maps joinargs (copyargs uargs)
   1.454 -	       | Free _  => Sequence.maps joinargs (copyargs uargs)
   1.455 -	       | _ => Sequence.null)  (*if Var, would be a loop!*)
   1.456 +              (case uhead of
   1.457 +                 Const _ => Sequence.maps joinargs (copyargs uargs)
   1.458 +               | Free _  => Sequence.maps joinargs (copyargs uargs)
   1.459 +               | _ => Sequence.null)  (*if Var, would be a loop!*)
   1.460  in case uhead of
   1.461 -	Abs(a, T, body) =>
   1.462 -	    Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
   1.463 -		(mc ((a,T)::rbinder,
   1.464 -			(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
   1.465 +        Abs(a, T, body) =>
   1.466 +            Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
   1.467 +                (mc ((a,T)::rbinder,
   1.468 +                        (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
   1.469        | Var (w,uary) => 
   1.470 -	    (*a flex-flex dpair: make variable for t*)
   1.471 -	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
   1.472 -		val tabs = combound(newhd, 0, length Ts)
   1.473 -		val tsub = list_comb(newhd,targs)
   1.474 -	    in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
   1.475 -	    end
   1.476 +            (*a flex-flex dpair: make variable for t*)
   1.477 +            let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
   1.478 +                val tabs = combound(newhd, 0, length Ts)
   1.479 +                val tsub = list_comb(newhd,targs)
   1.480 +            in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
   1.481 +            end
   1.482        | _ =>  matchfun(rev(make_projs(Ts, targs)))
   1.483  end
   1.484  in mc end;
   1.485 @@ -459,14 +459,14 @@
   1.486  
   1.487  (*Call matchcopy to produce assignments to the variable in the dpair*)
   1.488  fun MATCH (env, (rbinder,t,u), dpairs)
   1.489 -	: (Envir.env * dpair list)Sequence.seq = 
   1.490 +        : (Envir.env * dpair list)Sequence.seq = 
   1.491    let val (Var(v,T), targs) = strip_comb t;
   1.492        val Ts = binder_types env T;
   1.493        fun new_dset (u', (env',dpairs')) =
   1.494 -	  (*if v was updated to s, must unify s with u' *)
   1.495 -	  case Envir.lookup(env',v) of
   1.496 -	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
   1.497 -	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   1.498 +          (*if v was updated to s, must unify s with u' *)
   1.499 +          case Envir.lookup(env',v) of
   1.500 +              None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
   1.501 +            | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   1.502    in Sequence.maps new_dset
   1.503           (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   1.504    end;
   1.505 @@ -481,9 +481,9 @@
   1.506  let val (v,T) = get_eta_var(rbinder,0,t)
   1.507  in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
   1.508     else let val env = unify_types(body_type env T,
   1.509 -				  fastype env (rbinder,u),
   1.510 -				  env)
   1.511 -	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
   1.512 +                                  fastype env (rbinder,u),
   1.513 +                                  env)
   1.514 +        in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
   1.515  end;
   1.516  
   1.517  
   1.518 @@ -508,30 +508,30 @@
   1.519    let val (head,args) = strip_comb t 
   1.520    in  
   1.521        case head of
   1.522 -	  Bound i => (i-lev) mem banned  orelse
   1.523 -	      	     exists (rigid_bound (lev, banned)) args
   1.524 -	| Var _ => false	(*no rigid occurrences here!*)
   1.525 -	| Abs (_,_,u) => 
   1.526 -	       rigid_bound(lev+1, banned) u  orelse
   1.527 -	       exists (rigid_bound (lev, banned)) args
   1.528 -	| _ => exists (rigid_bound (lev, banned)) args
   1.529 +          Bound i => (i-lev) mem banned  orelse
   1.530 +                     exists (rigid_bound (lev, banned)) args
   1.531 +        | Var _ => false        (*no rigid occurrences here!*)
   1.532 +        | Abs (_,_,u) => 
   1.533 +               rigid_bound(lev+1, banned) u  orelse
   1.534 +               exists (rigid_bound (lev, banned)) args
   1.535 +        | _ => exists (rigid_bound (lev, banned)) args
   1.536    end;
   1.537  
   1.538  (*Squash down indices at level >=lev to delete the banned from a term.*)
   1.539  fun change_bnos banned =
   1.540    let fun change lev (Bound i) = 
   1.541 -	    if i<lev then Bound i
   1.542 -	    else  if (i-lev) mem banned  
   1.543 -		  then raise CHANGE_FAIL (**flexible occurrence: give up**)
   1.544 -	    else  Bound (i - length (filter (fn j => j < i-lev) banned))
   1.545 -	| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
   1.546 -	| change lev (t$u) = change lev t $ change lev u
   1.547 -	| change lev t = t
   1.548 +            if i<lev then Bound i
   1.549 +            else  if (i-lev) mem banned  
   1.550 +                  then raise CHANGE_FAIL (**flexible occurrence: give up**)
   1.551 +            else  Bound (i - length (filter (fn j => j < i-lev) banned))
   1.552 +        | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
   1.553 +        | change lev (t$u) = change lev t $ change lev u
   1.554 +        | change lev t = t
   1.555    in  change 0  end;
   1.556  
   1.557  (*Change indices, delete the argument if it contains a banned Bound*)
   1.558  fun change_arg banned ({j,t,T}, args) : flarg list =
   1.559 -    if rigid_bound (0, banned) t  then  args	(*delete argument!*)
   1.560 +    if rigid_bound (0, banned) t  then  args    (*delete argument!*)
   1.561      else  {j=j, t= change_bnos banned t, T=T} :: args;
   1.562  
   1.563  
   1.564 @@ -550,19 +550,19 @@
   1.565    Update its head; squash indices in arguments. *)
   1.566  fun clean_term banned (env,t) =
   1.567      let val (Var(v,T), ts) = strip_comb t
   1.568 -	val (Ts,U) = strip_type env T
   1.569 -	and js = length ts - 1  downto 0
   1.570 -	val args = sort arg_less
   1.571 -		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
   1.572 -	val ts' = map (#t) args
   1.573 +        val (Ts,U) = strip_type env T
   1.574 +        and js = length ts - 1  downto 0
   1.575 +        val args = sort arg_less
   1.576 +                (foldr (change_arg banned) (flexargs (js,ts,Ts), []))
   1.577 +        val ts' = map (#t) args
   1.578      in
   1.579      if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   1.580      else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
   1.581 -	     val body = list_comb(v', map (Bound o #j) args)
   1.582 -	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
   1.583 -	     (*the vupdate affects ts' if they contain v*)
   1.584 -	 in  
   1.585 -	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
   1.586 +             val body = list_comb(v', map (Bound o #j) args)
   1.587 +             val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
   1.588 +             (*the vupdate affects ts' if they contain v*)
   1.589 +         in  
   1.590 +             (env2, Envir.norm_term env2 (list_comb(v',ts')))
   1.591           end
   1.592      end;
   1.593  
   1.594 @@ -583,8 +583,8 @@
   1.595    let val loot = loose_bnos t  and  loou = loose_bnos u
   1.596        fun add_index (((a,T), j), (bnos, newbinder)) = 
   1.597              if  j mem loot  andalso  j mem loou 
   1.598 -            then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
   1.599 -            else  (j::bnos, newbinder);		(*remove*)
   1.600 +            then  (bnos, (a,T)::newbinder)      (*needed by both: keep*)
   1.601 +            else  (j::bnos, newbinder);         (*remove*)
   1.602        val indices = 0 upto (length rbinder - 1);
   1.603        val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
   1.604        val (env', t') = clean_term banned (env, t);
   1.605 @@ -605,11 +605,11 @@
   1.606    let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   1.607    in  case  (head_of t, head_of u) of
   1.608        (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
   1.609 -	if v=w then		(*...occur check would falsely return true!*)
   1.610 -	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   1.611 -	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
   1.612 -	else if xless(v,w) then (*prefer to update the LARGER variable*)
   1.613 -	     clean_ffpair ((rbinder, u, t), (env,tpairs))
   1.614 +        if v=w then             (*...occur check would falsely return true!*)
   1.615 +            if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   1.616 +            else raise TERM ("add_ffpair: Var name confusion", [t,u])
   1.617 +        else if xless(v,w) then (*prefer to update the LARGER variable*)
   1.618 +             clean_ffpair ((rbinder, u, t), (env,tpairs))
   1.619          else clean_ffpair ((rbinder, t, u), (env,tpairs))
   1.620      | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
   1.621    end;
   1.622 @@ -634,26 +634,26 @@
   1.623  fun hounifiers (sg,env, tus : (term*term)list) 
   1.624    : (Envir.env * (term*term)list)Sequence.seq =
   1.625    let fun add_unify tdepth ((env,dpairs), reseq) =
   1.626 -	  Sequence.seqof (fn()=>
   1.627 -	  let val (env',flexflex,flexrigid) = 
   1.628 -	       (if tdepth> !trace_bound andalso !trace_simp
   1.629 -		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   1.630 -		SIMPL (env,dpairs))
   1.631 -	  in case flexrigid of
   1.632 -	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
   1.633 -	    | dp::frigid' => 
   1.634 -		if tdepth > !search_bound then
   1.635 -		    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
   1.636 -		else
   1.637 -		(if tdepth > !trace_bound then
   1.638 -		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
   1.639 -		 else ();
   1.640 -		 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
   1.641 -			   (MATCH (env',dp, frigid'@flexflex), reseq)))
   1.642 -	  end
   1.643 -	  handle CANTUNIFY => 
   1.644 -	    (if tdepth > !trace_bound then writeln"Failure node" else ();
   1.645 -	     Sequence.pull reseq));
   1.646 +          Sequence.seqof (fn()=>
   1.647 +          let val (env',flexflex,flexrigid) = 
   1.648 +               (if tdepth> !trace_bound andalso !trace_simp
   1.649 +                then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   1.650 +                SIMPL (env,dpairs))
   1.651 +          in case flexrigid of
   1.652 +              [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
   1.653 +            | dp::frigid' => 
   1.654 +                if tdepth > !search_bound then
   1.655 +                    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
   1.656 +                else
   1.657 +                (if tdepth > !trace_bound then
   1.658 +                    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
   1.659 +                 else ();
   1.660 +                 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
   1.661 +                           (MATCH (env',dp, frigid'@flexflex), reseq)))
   1.662 +          end
   1.663 +          handle CANTUNIFY => 
   1.664 +            (if tdepth > !trace_bound then writeln"Failure node" else ();
   1.665 +             Sequence.pull reseq));
   1.666       val dps = map (fn(t,u)=> ([],t,u)) tus
   1.667    in sgr := sg;
   1.668       add_unify 1 ((env,dps), Sequence.null) 
   1.669 @@ -675,7 +675,7 @@
   1.670  (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   1.671    Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   1.672    Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, 
   1.673 -	though just ?g->?f is a more general unifier.
   1.674 +        though just ?g->?f is a more general unifier.
   1.675    Unlike Huet (1975), does not smash together all variables of same type --
   1.676      requires more work yet gives a less general unifier (fewer variables).
   1.677    Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)