src/Pure/unify.ML
changeset 0 a5a9c433f639
child 646 7928c9760667
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/unify.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,680 @@
     1.4 +(*  Title: 	unify
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   Cambridge University 1992
     1.8 +
     1.9 +Higher-Order Unification
    1.10 +
    1.11 +Potential problem: type of Vars is often ignored, so two Vars with same
    1.12 +indexname but different types can cause errors!
    1.13 +*)
    1.14 +
    1.15 +
    1.16 +signature UNIFY = 
    1.17 +sig
    1.18 +  structure Sign: SIGN
    1.19 +  structure Envir : ENVIR
    1.20 +  structure Sequence : SEQUENCE
    1.21 +  (*references for control and tracing*)
    1.22 +  val trace_bound: int ref
    1.23 +  val trace_simp: bool ref
    1.24 +  val trace_types: bool ref
    1.25 +  val search_bound: int ref
    1.26 +  (*other exports*)
    1.27 +  val combound : (term*int*int) -> term
    1.28 +  val rlist_abs: (string*typ)list * term -> term   
    1.29 +  val smash_unifiers : Sign.sg * Envir.env * (term*term)list
    1.30 +	-> (Envir.env Sequence.seq)
    1.31 +  val unifiers: Sign.sg * Envir.env * ((term*term)list)
    1.32 +	-> (Envir.env * (term * term)list) Sequence.seq
    1.33 +end;
    1.34 +
    1.35 +functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE
    1.36 +                  and Pattern:PATTERN
    1.37 +                  sharing type Sign.sg = Pattern.sg
    1.38 +                  and     type Envir.env = Pattern.env)
    1.39 +	: UNIFY = 
    1.40 +struct
    1.41 +
    1.42 +structure Sign = Sign;
    1.43 +structure Envir = Envir;
    1.44 +structure Sequence = Sequence;
    1.45 +structure Pretty = Sign.Syntax.Pretty;
    1.46 +
    1.47 +(*Unification options*)
    1.48 +
    1.49 +val trace_bound = ref 10	(*tracing starts above this depth, 0 for full*)
    1.50 +and search_bound = ref 20	(*unification quits above this depth*)
    1.51 +and trace_simp = ref false	(*print dpairs before calling SIMPL*)
    1.52 +and trace_types = ref false	(*announce potential incompleteness
    1.53 +				  of type unification*)
    1.54 +
    1.55 +val sgr = ref(Sign.pure);
    1.56 +
    1.57 +type binderlist = (string*typ) list;
    1.58 +
    1.59 +type dpair = binderlist * term * term;
    1.60 +
    1.61 +fun body_type(Envir.Envir{iTs,...}) = 
    1.62 +let fun bT(Type("fun",[_,T])) = bT T
    1.63 +      | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
    1.64 +		None => T | Some(T') => bT T')
    1.65 +      | bT T = T
    1.66 +in bT end;
    1.67 +
    1.68 +fun binder_types(Envir.Envir{iTs,...}) = 
    1.69 +let fun bTs(Type("fun",[T,U])) = T :: bTs U
    1.70 +      | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
    1.71 +		None => [] | Some(T') => bTs T')
    1.72 +      | bTs _ = []
    1.73 +in bTs end;
    1.74 +
    1.75 +fun strip_type env T = (binder_types env T, body_type env T);
    1.76 +
    1.77 +
    1.78 +(*Put a term into head normal form for unification.
    1.79 +  Operands need not be in normal form.  Does eta-expansions on the head,
    1.80 +  which involves renumbering (thus copying) the args.  To avoid this 
    1.81 +  inefficiency, avoid partial application:  if an atom is applied to
    1.82 +  any arguments at all, apply it to its full number of arguments.
    1.83 +  For
    1.84 +    rbinder = [(x1,T),...,(xm,Tm)]		(user's var names preserved!)
    1.85 +    args  =   [arg1,...,argn]
    1.86 +  the value of 
    1.87 +      (xm,...,x1)(head(arg1,...,argn))  remains invariant.
    1.88 +*)
    1.89 +
    1.90 +local exception SAME
    1.91 +in
    1.92 +  fun head_norm (env,t) : term =
    1.93 +    let fun hnorm (Var (v,T)) = 
    1.94 +	      (case Envir.lookup (env,v) of
    1.95 +		  Some u => head_norm (env, u)
    1.96 +		| None   => raise SAME)
    1.97 +	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
    1.98 +	  | hnorm (Abs(_,_,body) $ t) =
    1.99 +	      head_norm (env, subst_bounds([t], body))
   1.100 +	  | hnorm (f $ t) =
   1.101 +	      (case hnorm f of
   1.102 +		 Abs(_,_,body) =>
   1.103 +		   head_norm (env, subst_bounds([t], body))
   1.104 +	       | nf => nf $ t)
   1.105 +	  | hnorm _ =  raise SAME
   1.106 +    in  hnorm t  handle SAME=> t  end
   1.107 +end;
   1.108 +
   1.109 +
   1.110 +(*finds type of term without checking that combinations are consistent
   1.111 +  rbinder holds types of bound variables*)
   1.112 +fun fastype (Envir.Envir{iTs,...}) =
   1.113 +let val funerr = "fastype: expected function type";
   1.114 +    fun fast(rbinder, f$u) =
   1.115 +	(case (fast (rbinder, f)) of
   1.116 +	   Type("fun",[_,T]) => T
   1.117 +	 | TVar(ixn,_) =>
   1.118 +		(case assoc(iTs,ixn) of
   1.119 +		   Some(Type("fun",[_,T])) => T
   1.120 +		 | _ => raise TERM(funerr, [f$u]))
   1.121 +	 | _ => raise TERM(funerr, [f$u]))
   1.122 +      | fast (rbinder, Const (_,T)) = T
   1.123 +      | fast (rbinder, Free (_,T)) = T
   1.124 +      | fast (rbinder, Bound i) =
   1.125 +	(#2 (nth_elem (i,rbinder))
   1.126 +  	 handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
   1.127 +      | fast (rbinder, Var (_,T)) = T 
   1.128 +      | fast (rbinder, Abs (_,T,u)) =  T --> fast (("",T) :: rbinder, u)
   1.129 +in fast end;
   1.130 +
   1.131 +
   1.132 +(*Eta normal form*)
   1.133 +fun eta_norm(env as Envir.Envir{iTs,...}) =
   1.134 +  let fun etif (Type("fun",[T,U]), t) =
   1.135 +	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
   1.136 +	| etif (TVar(ixn,_),t) = 
   1.137 +	    (case assoc(iTs,ixn) of
   1.138 +		  None => t | Some(T) => etif(T,t))
   1.139 +	| etif (_,t) = t;
   1.140 +      fun eta_nm (rbinder, Abs(a,T,body)) =
   1.141 +	    Abs(a, T, eta_nm ((a,T)::rbinder, body))
   1.142 +	| eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
   1.143 +  in eta_nm end;
   1.144 +
   1.145 +
   1.146 +(*OCCURS CHECK
   1.147 +  Does the uvar occur in the term t?  
   1.148 +  two forms of search, for whether there is a rigid path to the current term.
   1.149 +  "seen" is list of variables passed thru, is a memo variable for sharing.
   1.150 +  This version searches for nonrigid occurrence, returns true if found. *)
   1.151 +fun occurs_terms (seen: (indexname list) ref,
   1.152 + 		  env: Envir.env, v: indexname, ts: term list): bool =
   1.153 +  let fun occurs [] = false
   1.154 +	| occurs (t::ts) =  occur t  orelse  occurs ts
   1.155 +      and occur (Const _)  = false
   1.156 +	| occur (Bound _)  = false
   1.157 +	| occur (Free _)  = false
   1.158 +	| occur (Var (w,_))  = 
   1.159 +	    if w mem !seen then false
   1.160 +	    else if v=w then true
   1.161 +	      (*no need to lookup: v has no assignment*)
   1.162 +	    else (seen := w:: !seen;  
   1.163 +	          case  Envir.lookup(env,w)  of
   1.164 +		      None    => false
   1.165 +		    | Some t => occur t)
   1.166 +	| occur (Abs(_,_,body)) = occur body
   1.167 +	| occur (f$t) = occur t  orelse   occur f
   1.168 +  in  occurs ts  end;
   1.169 +
   1.170 +
   1.171 +
   1.172 +(* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
   1.173 +fun head_of_in (env,t) : term = case t of
   1.174 +    f$_ => head_of_in(env,f)
   1.175 +  | Var (v,_) => (case  Envir.lookup(env,v)  of  
   1.176 +			Some u => head_of_in(env,u)  |  None   => t)
   1.177 +  | _ => t;
   1.178 +
   1.179 +
   1.180 +datatype occ = NoOcc | Nonrigid | Rigid;
   1.181 +
   1.182 +(* Rigid occur check
   1.183 +Returns Rigid    if it finds a rigid occurrence of the variable,
   1.184 +        Nonrigid if it finds a nonrigid path to the variable.
   1.185 +        NoOcc    otherwise.
   1.186 +  Continues searching for a rigid occurrence even if it finds a nonrigid one.
   1.187 +
   1.188 +Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ]
   1.189 +   a rigid path to the variable, appearing with no arguments.
   1.190 +Here completeness is sacrificed in order to reduce danger of divergence:
   1.191 +   reject ALL rigid paths to the variable.
   1.192 +Could check for rigid paths to bound variables that are out of scope.  
   1.193 +Not necessary because the assignment test looks at variable's ENTIRE rbinder.
   1.194 +
   1.195 +Treatment of head(arg1,...,argn):
   1.196 +If head is a variable then no rigid path, switch to nonrigid search
   1.197 +for arg1,...,argn. 
   1.198 +If head is an abstraction then possibly no rigid path (head could be a 
   1.199 +   constant function) so again use nonrigid search.  Happens only if
   1.200 +   term is not in normal form. 
   1.201 +
   1.202 +Warning: finds a rigid occurrence of ?f in ?f(t).
   1.203 +  Should NOT be called in this case: there is a flex-flex unifier
   1.204 +*)
   1.205 +fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 
   1.206 +  let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 
   1.207 +		       else NoOcc
   1.208 +      fun occurs [] = NoOcc
   1.209 +	| occurs (t::ts) =
   1.210 +            (case occur t of
   1.211 +               Rigid => Rigid
   1.212 +             | oc =>  (case occurs ts of NoOcc => oc  |  oc2 => oc2))
   1.213 +      and occomb (f$t) =
   1.214 +            (case occur t of
   1.215 +               Rigid => Rigid
   1.216 +             | oc =>  (case occomb f of NoOcc => oc  |  oc2 => oc2))
   1.217 +        | occomb t = occur t
   1.218 +      and occur (Const _)  = NoOcc
   1.219 +	| occur (Bound _)  = NoOcc
   1.220 +	| occur (Free _)  = NoOcc
   1.221 +	| occur (Var (w,_))  = 
   1.222 +	    if w mem !seen then NoOcc
   1.223 +	    else if v=w then Rigid
   1.224 +	    else (seen := w:: !seen;  
   1.225 +	          case  Envir.lookup(env,w)  of
   1.226 +		      None    => NoOcc
   1.227 +		    | Some t => occur t)
   1.228 +	| occur (Abs(_,_,body)) = occur body
   1.229 +	| occur (t as f$_) =  (*switch to nonrigid search?*)
   1.230 +	   (case head_of_in (env,f) of
   1.231 +	      Var (w,_) => (*w is not assigned*)
   1.232 +		if v=w then Rigid  
   1.233 +		else  nonrigid t
   1.234 +	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
   1.235 +	    | _ => occomb t)
   1.236 +  in  occur t  end;
   1.237 +
   1.238 +
   1.239 +exception CANTUNIFY;	(*Signals non-unifiability.  Does not signal errors!*)
   1.240 +exception ASSIGN;	(*Raised if not an assignment*)
   1.241 +
   1.242 +
   1.243 +fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   1.244 +	if T=U then env else
   1.245 +	let val iTs' = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr))) ((U,T),iTs)
   1.246 +	in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'}
   1.247 +	end handle Sign.Type.TUNIFY => raise CANTUNIFY;
   1.248 +
   1.249 +fun test_unify_types(args as (T,U,_)) =
   1.250 +let val sot = Sign.string_of_typ (!sgr);
   1.251 +    fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
   1.252 +    val env' = unify_types(args)
   1.253 +in if is_TVar(T) orelse is_TVar(U) then warn() else ();
   1.254 +   env'
   1.255 +end;
   1.256 +
   1.257 +(*Is the term eta-convertible to a single variable with the given rbinder?
   1.258 +  Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
   1.259 +  Result is var a for use in SIMPL. *)
   1.260 +fun get_eta_var ([], _, Var vT)  =  vT
   1.261 +  | get_eta_var (_::rbinder, n, f $ Bound i) =
   1.262 +	if  n=i  then  get_eta_var (rbinder, n+1, f) 
   1.263 +		 else  raise ASSIGN
   1.264 +  | get_eta_var _ = raise ASSIGN;
   1.265 +
   1.266 +
   1.267 +(* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   1.268 +fun rlist_abs ([], body) = body
   1.269 +  | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   1.270 +
   1.271 +
   1.272 +(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
   1.273 +  If v occurs rigidly then nonunifiable.
   1.274 +  If v occurs nonrigidly then must use full algorithm. *)
   1.275 +fun assignment (env, rbinder, t, u) =
   1.276 +    let val (v,T) = get_eta_var(rbinder,0,t)
   1.277 +    in  case rigid_occurs_term (ref[], env, v, u) of
   1.278 +	      NoOcc => let val env = unify_types(body_type env T,
   1.279 +						 fastype env (rbinder,u),env)
   1.280 +		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
   1.281 +	    | Nonrigid =>  raise ASSIGN
   1.282 +	    | Rigid =>  raise CANTUNIFY
   1.283 +    end;
   1.284 +
   1.285 +
   1.286 +(*Extends an rbinder with a new disagreement pair, if both are abstractions.
   1.287 +  Tries to unify types of the bound variables!
   1.288 +  Checks that binders have same length, since terms should be eta-normal;
   1.289 +    if not, raises TERM, probably indicating type mismatch.
   1.290 +  Uses variable a (unless the null string) to preserve user's naming.*) 
   1.291 +fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
   1.292 +	let val env' = unify_types(T,U,env)
   1.293 +	    val c = if a="" then b else a
   1.294 +	in new_dpair((c,T) :: rbinder, body1, body2, env') end
   1.295 +    | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
   1.296 +    | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
   1.297 +    | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
   1.298 +
   1.299 +
   1.300 +fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
   1.301 +     new_dpair (rbinder,
   1.302 +		eta_norm env (rbinder, head_norm(env,t)),
   1.303 +	  	eta_norm env (rbinder, head_norm(env,u)), env);
   1.304 +
   1.305 +
   1.306 +
   1.307 +(*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
   1.308 +  Does not perform assignments for flex-flex pairs:
   1.309 +    may create nonrigid paths, which prevent other assignments*)
   1.310 +fun SIMPL0 (dp0, (env,flexflex,flexrigid))
   1.311 +	: Envir.env * dpair list * dpair list =
   1.312 +    let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
   1.313 +	    fun SIMRANDS(f$t, g$u, env) =
   1.314 +			SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
   1.315 +	      | SIMRANDS (t as _$_, _, _) =
   1.316 +		raise TERM ("SIMPL: operands mismatch", [t,u])
   1.317 +	      | SIMRANDS (t, u as _$_, _) =
   1.318 +		raise TERM ("SIMPL: operands mismatch", [t,u])
   1.319 +	      | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
   1.320 +    in case (head_of t, head_of u) of
   1.321 +       (Var(_,T), Var(_,U)) =>
   1.322 +	    let val T' = body_type env T and U' = body_type env U;
   1.323 +		val env = unify_types(T',U',env)
   1.324 +	    in (env, dp::flexflex, flexrigid) end
   1.325 +     | (Var _, _) =>
   1.326 +	    ((assignment (env,rbinder,t,u), flexflex, flexrigid)
   1.327 +	     handle ASSIGN => (env, flexflex, dp::flexrigid))
   1.328 +     | (_, Var _) =>
   1.329 +	    ((assignment (env,rbinder,u,t), flexflex, flexrigid)
   1.330 +	     handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
   1.331 +     | (Const(a,T), Const(b,U)) =>
   1.332 +	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   1.333 +	    else raise CANTUNIFY
   1.334 +     | (Bound i,    Bound j)    =>
   1.335 +	    if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
   1.336 +     | (Free(a,T),  Free(b,U))  =>
   1.337 +	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   1.338 +	    else raise CANTUNIFY
   1.339 +     | _ => raise CANTUNIFY
   1.340 +    end;
   1.341 +
   1.342 +
   1.343 +(* changed(env,t) checks whether the head of t is a variable assigned in env*)
   1.344 +fun changed (env, f$_) = changed (env,f)
   1.345 +  | changed (env, Var (v,_)) =
   1.346 +      (case Envir.lookup(env,v) of None=>false  |  _ => true)
   1.347 +  | changed _ = false;
   1.348 +
   1.349 +
   1.350 +(*Recursion needed if any of the 'head variables' have been updated
   1.351 +  Clever would be to re-do just the affected dpairs*)
   1.352 +fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
   1.353 +    let val all as (env',flexflex,flexrigid) =
   1.354 +	    foldr SIMPL0 (dpairs, (env,[],[]));
   1.355 +	val dps = flexrigid@flexflex
   1.356 +    in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
   1.357 +       then SIMPL(env',dps) else all
   1.358 +    end;
   1.359 +
   1.360 +
   1.361 +(*computes t(Bound(n+k-1),...,Bound(n))  *)
   1.362 +fun combound (t, n, k) = 
   1.363 +    if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   1.364 +
   1.365 +
   1.366 +(*Makes the terms E1,...,Em,    where Ts = [T...Tm]. 
   1.367 +  Each Ei is   ?Gi(B.(n-1),...,B.0), and has type Ti
   1.368 +  The B.j are bound vars of binder.
   1.369 +  The terms are not made in eta-normal-form, SIMPL does that later.  
   1.370 +  If done here, eta-expansion must be recursive in the arguments! *)
   1.371 +fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
   1.372 +  | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
   1.373 +       let fun funtype T = binder--->T;
   1.374 +	   val (env', vars) = Envir.genvars name (env, map funtype Ts)
   1.375 +       in  (env',  map (fn var=> combound(var, 0, length binder)) vars)  end;
   1.376 +
   1.377 +
   1.378 +(*Abstraction over a list of types, like list_abs*)
   1.379 +fun types_abs ([],u) = u
   1.380 +  | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
   1.381 +
   1.382 +(*Abstraction over the binder of a type*)
   1.383 +fun type_abs (env,T,t) = types_abs(binder_types env T, t);
   1.384 +
   1.385 +
   1.386 +(*MATCH taking "big steps".
   1.387 +  Copies u into the Var v, using projection on targs or imitation.
   1.388 +  A projection is allowed unless SIMPL raises an exception.
   1.389 +  Allocates new variables in projection on a higher-order argument,
   1.390 +    or if u is a variable (flex-flex dpair).
   1.391 +  Returns long sequence of every way of copying u, for backtracking
   1.392 +  For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
   1.393 +  The order for trying projections is crucial in ?b'(?a)   
   1.394 +  NB "vname" is only used in the call to make_args!!   *)
   1.395 +fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
   1.396 +	: (term * (Envir.env * dpair list))Sequence.seq =
   1.397 +let (*Produce copies of uarg and cons them in front of uargs*)
   1.398 +    fun copycons uarg (uargs, (env, dpairs)) =
   1.399 +	Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
   1.400 +	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
   1.401 +		 (env, dpairs)));
   1.402 +	(*Produce sequence of all possible ways of copying the arg list*)
   1.403 +    fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
   1.404 +      | copyargs (uarg::uargs) =
   1.405 +	    Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
   1.406 +    val (uhead,uargs) = strip_comb u;
   1.407 +    val base = body_type env (fastype env (rbinder,uhead));
   1.408 +    fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
   1.409 +    (*attempt projection on argument with given typ*)
   1.410 +    val Ts = map (curry (fastype env) rbinder) targs;
   1.411 +    fun projenv (head, (Us,bary), targ, tail) = 
   1.412 +	let val env = if !trace_types then test_unify_types(base,bary,env)
   1.413 +		      else unify_types(base,bary,env)
   1.414 +	in Sequence.seqof (fn () =>  
   1.415 +	    let val (env',args) = make_args vname (Ts,env,Us);
   1.416 +		(*higher-order projection: plug in targs for bound vars*)
   1.417 +		fun plugin arg = list_comb(head_of arg, targs);
   1.418 +		val dp = (rbinder, list_comb(targ, map plugin args), u);
   1.419 +		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
   1.420 +		    (*may raise exception CANTUNIFY*)
   1.421 +	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
   1.422 +			tail)
   1.423 +	    end  handle CANTUNIFY => Sequence.pull tail)
   1.424 +	end handle CANTUNIFY => tail;
   1.425 +    (*make a list of projections*)
   1.426 +    fun make_projs (T::Ts, targ::targs) =
   1.427 +	      (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
   1.428 +      | make_projs ([],[]) = []
   1.429 +      | make_projs _ = raise TERM ("make_projs", u::targs);
   1.430 +    (*try projections and imitation*)
   1.431 +    fun matchfun ((bvar,T,targ)::projs) =
   1.432 +	       (projenv(bvar, strip_type env T, targ, matchfun projs))
   1.433 +      | matchfun [] = (*imitation last of all*)
   1.434 +	      (case uhead of
   1.435 +		 Const _ => Sequence.maps joinargs (copyargs uargs)
   1.436 +	       | Free _  => Sequence.maps joinargs (copyargs uargs)
   1.437 +	       | _ => Sequence.null)  (*if Var, would be a loop!*)
   1.438 +in case uhead of
   1.439 +	Abs(a, T, body) =>
   1.440 +	    Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
   1.441 +		(mc ((a,T)::rbinder,
   1.442 +			(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
   1.443 +      | Var (w,uary) => 
   1.444 +	    (*a flex-flex dpair: make variable for t*)
   1.445 +	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
   1.446 +		val tabs = combound(newhd, 0, length Ts)
   1.447 +		val tsub = list_comb(newhd,targs)
   1.448 +	    in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
   1.449 +	    end
   1.450 +      | _ =>  matchfun(rev(make_projs(Ts, targs)))
   1.451 +end
   1.452 +in mc end;
   1.453 +
   1.454 +
   1.455 +(*Call matchcopy to produce assignments to the variable in the dpair*)
   1.456 +fun MATCH (env, (rbinder,t,u), dpairs)
   1.457 +	: (Envir.env * dpair list)Sequence.seq = 
   1.458 +  let val (Var(v,T), targs) = strip_comb t;
   1.459 +      val Ts = binder_types env T;
   1.460 +      fun new_dset (u', (env',dpairs')) =
   1.461 +	  (*if v was updated to s, must unify s with u' *)
   1.462 +	  case Envir.lookup(env',v) of
   1.463 +	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
   1.464 +	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   1.465 +  in Sequence.maps new_dset
   1.466 +         (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   1.467 +  end;
   1.468 +
   1.469 +
   1.470 +
   1.471 +(**** Flex-flex processing ****)
   1.472 +
   1.473 +(*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
   1.474 +  Attempts to update t with u, raising ASSIGN if impossible*)
   1.475 +fun ff_assign(env, rbinder, t, u) : Envir.env = 
   1.476 +let val (v,T) = get_eta_var(rbinder,0,t)
   1.477 +in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
   1.478 +   else let val env = unify_types(body_type env T,fastype env (rbinder,u),env)
   1.479 +	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
   1.480 +end;
   1.481 +
   1.482 +
   1.483 +(*Flex argument: a term, its type, and the index that refers to it.*)
   1.484 +type flarg = {t: term,  T: typ,  j: int};
   1.485 +
   1.486 +
   1.487 +(*Form the arguments into records for deletion/sorting.*)
   1.488 +fun flexargs ([],[],[]) = [] : flarg list
   1.489 +  | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
   1.490 +  | flexargs _ = error"flexargs";
   1.491 +
   1.492 +
   1.493 +(*If an argument contains a banned Bound, then it should be deleted.
   1.494 +  But if the path is flexible, this is difficult; the code gives up!*)
   1.495 +exception CHANGE and CHANGE_FAIL;   (*rigid and flexible occurrences*)
   1.496 +
   1.497 +
   1.498 +(*Squash down indices at level >=lev to delete the js from a term.
   1.499 +  flex should initially be false, since the empty path is rigid.*)
   1.500 +fun change_bnos (lev, js, flex) t = 
   1.501 +  let val (head,args) = strip_comb t 
   1.502 +      val flex' = flex orelse is_Var head
   1.503 +      val head' = case head of
   1.504 +	    Bound i => 
   1.505 +		if i<lev then Bound i
   1.506 +		else  if (i-lev) mem js  
   1.507 +                      then  if flex then raise CHANGE_FAIL
   1.508 +                                    else raise CHANGE
   1.509 +		else  Bound (i - length (filter (fn j => j < i-lev) js))
   1.510 +	  | Abs (a,T,t) => Abs (a, T, change_bnos(lev+1, js, flex) t)
   1.511 +	  | _ => head
   1.512 +  in  list_comb (head', map (change_bnos (lev, js, flex')) args)
   1.513 +  end;
   1.514 +
   1.515 +
   1.516 +(*Change indices, delete the argument if it contains a banned Bound*)
   1.517 +fun change_arg js ({j,t,T}, args) : flarg list =
   1.518 +    {j=j, t= change_bnos(0,js,false)t, T=T} :: args    handle CHANGE => args;
   1.519 +
   1.520 +
   1.521 +(*Sort the arguments to create assignments if possible:
   1.522 +  create eta-terms like ?g(B.1,B.0) *)
   1.523 +fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
   1.524 +  | arg_less (_:flarg, _:flarg) = false;
   1.525 +
   1.526 +(*Test whether the new term would be eta-equivalent to a variable --
   1.527 +  if so then there is no point in creating a new variable*)
   1.528 +fun decreasing n ([]: flarg list) = (n=0)
   1.529 +  | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
   1.530 +
   1.531 +(*Delete banned indices in the term, simplifying it.
   1.532 +  Force an assignment, if possible, by sorting the arguments.
   1.533 +  Update its head; squash indices in arguments. *)
   1.534 +fun clean_term banned (env,t) =
   1.535 +    let val (Var(v,T), ts) = strip_comb t
   1.536 +	val (Ts,U) = strip_type env T
   1.537 +	and js = length ts - 1  downto 0
   1.538 +	val args = sort arg_less
   1.539 +		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
   1.540 +	val ts' = map (#t) args
   1.541 +    in
   1.542 +    if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   1.543 +    else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
   1.544 +	     val body = list_comb(v', map (Bound o #j) args)
   1.545 +	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
   1.546 +	     (*the vupdate affects ts' if they contain v*)
   1.547 +	 in  
   1.548 +	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
   1.549 +         end
   1.550 +    end;
   1.551 +
   1.552 +
   1.553 +(*Add tpair if not trivial or already there.
   1.554 +  Should check for swapped pairs??*)
   1.555 +fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
   1.556 +  if t0 aconv u0 then tpairs  
   1.557 +  else
   1.558 +  let val t = rlist_abs(rbinder, t0)  and  u = rlist_abs(rbinder, u0);
   1.559 +      fun same(t',u') = (t aconv t') andalso (u aconv u')
   1.560 +  in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
   1.561 +
   1.562 +
   1.563 +(*Simplify both terms and check for assignments.
   1.564 +  Bound vars in the binder are "banned" unless used in both t AND u *)
   1.565 +fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 
   1.566 +  let val loot = loose_bnos t  and  loou = loose_bnos u
   1.567 +      fun add_index (((a,T), j), (bnos, newbinder)) = 
   1.568 +            if  j mem loot  andalso  j mem loou 
   1.569 +            then  (bnos, (a,T)::newbinder)
   1.570 +            else  (j::bnos, newbinder);
   1.571 +      val indices = 0 upto (length rbinder - 1);
   1.572 +      val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
   1.573 +      val (env', t') = clean_term banned (env, t);
   1.574 +      val (env'',u') = clean_term banned (env',u)
   1.575 +  in  (ff_assign(env'', rbin', t', u'), tpairs)
   1.576 +      handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
   1.577 +      handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
   1.578 +  end
   1.579 +  handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
   1.580 +
   1.581 +
   1.582 +(*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   1.583 +  eliminates trivial tpairs like t=t, as well as repeated ones
   1.584 +  trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t 
   1.585 +  Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
   1.586 +fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 
   1.587 +      : Envir.env * (term*term)list =
   1.588 +  let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   1.589 +  in  case  (head_of t, head_of u) of
   1.590 +      (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
   1.591 +	if v=w then		(*...occur check would falsely return true!*)
   1.592 +	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   1.593 +	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
   1.594 +	else if xless(v,w) then (*prefer to update the LARGER variable*)
   1.595 +	     clean_ffpair ((rbinder, u, t), (env,tpairs))
   1.596 +        else clean_ffpair ((rbinder, t, u), (env,tpairs))
   1.597 +    | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
   1.598 +  end;
   1.599 +
   1.600 +
   1.601 +(*Print a tracing message + list of dpairs.
   1.602 +  In t==u print u first because it may be rigid or flexible --
   1.603 +    t is always flexible.*)
   1.604 +fun print_dpairs msg (env,dpairs) =
   1.605 +  let fun pdp (rbinder,t,u) =
   1.606 +        let fun termT t = Sign.pretty_term (!sgr)
   1.607 +                              (Envir.norm_term env (rlist_abs(rbinder,t)))
   1.608 +            val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
   1.609 +                          termT t];
   1.610 +        in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   1.611 +  in  writeln msg;  seq pdp dpairs  end;
   1.612 +
   1.613 +
   1.614 +(*Unify the dpairs in the environment.
   1.615 +  Returns flex-flex disagreement pairs NOT IN normal form. 
   1.616 +  SIMPL may raise exception CANTUNIFY. *)
   1.617 +fun hounifiers (sg,env, tus : (term*term)list) 
   1.618 +  : (Envir.env * (term*term)list)Sequence.seq =
   1.619 +  let fun add_unify tdepth ((env,dpairs), reseq) =
   1.620 +	  Sequence.seqof (fn()=>
   1.621 +	  let val (env',flexflex,flexrigid) = 
   1.622 +	       (if tdepth> !trace_bound andalso !trace_simp
   1.623 +		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   1.624 +		SIMPL (env,dpairs))
   1.625 +	  in case flexrigid of
   1.626 +	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
   1.627 +	    | dp::frigid' => 
   1.628 +		if tdepth > !search_bound then
   1.629 +		    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
   1.630 +		else
   1.631 +		(if tdepth > !trace_bound then
   1.632 +		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
   1.633 +		 else ();
   1.634 +		 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
   1.635 +			   (MATCH (env',dp, frigid'@flexflex), reseq)))
   1.636 +	  end
   1.637 +	  handle CANTUNIFY => 
   1.638 +	    (if tdepth > !trace_bound then writeln"Failure node" else ();
   1.639 +	     Sequence.pull reseq));
   1.640 +     val dps = map (fn(t,u)=> ([],t,u)) tus
   1.641 +  in sgr := sg;
   1.642 +     add_unify 1 ((env,dps), Sequence.null) 
   1.643 +  end;
   1.644 +
   1.645 +fun unifiers(params) =
   1.646 +      Sequence.cons((Pattern.unify(params), []),   Sequence.null)
   1.647 +      handle Pattern.Unif => Sequence.null
   1.648 +           | Pattern.Pattern => hounifiers(params);
   1.649 +
   1.650 +
   1.651 +(*For smash_flexflex1*)
   1.652 +fun var_head_of (env,t) : indexname * typ =
   1.653 +  case head_of (strip_abs_body (Envir.norm_term env t)) of
   1.654 +      Var(v,T) => (v,T)
   1.655 +    | _ => raise CANTUNIFY;  (*not flexible, cannot use trivial substitution*)
   1.656 +
   1.657 +
   1.658 +(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   1.659 +  Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   1.660 +  Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, 
   1.661 +	though just ?g->?f is a more general unifier.
   1.662 +  Unlike Huet (1975), does not smash together all variables of same type --
   1.663 +    requires more work yet gives a less general unifier (fewer variables).
   1.664 +  Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   1.665 +fun smash_flexflex1 ((t,u), env) : Envir.env =
   1.666 +  let val (v,T) = var_head_of (env,t)
   1.667 +      and (w,U) = var_head_of (env,u);
   1.668 +      val (env', var) = Envir.genvar (#1v) (env, body_type env T)
   1.669 +      val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
   1.670 +  in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
   1.671 +      else Envir.vupdate((v, type_abs(env',T,var)), env'')
   1.672 +  end;
   1.673 +
   1.674 +
   1.675 +(*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   1.676 +fun smash_flexflex (env,tpairs) : Envir.env =
   1.677 +  foldr smash_flexflex1 (tpairs, env);
   1.678 +
   1.679 +(*Returns unifiers with no remaining disagreement pairs*)
   1.680 +fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
   1.681 +    Sequence.maps smash_flexflex (unifiers(sg,env,tus));
   1.682 +
   1.683 +end;