src/Pure/unify.ML
author wenzelm
Thu Apr 22 10:52:32 2004 +0200 (2004-04-22)
changeset 14643 130076a81b84
parent 12527 d6c91bc3e49c
child 15275 baa90469961a
permissions -rw-r--r--
tuned;
     1 (*  Title: 	unify
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Higher-Order Unification
     7 
     8 Potential problem: type of Vars is often ignored, so two Vars with same
     9 indexname but different types can cause errors!
    10 
    11 Types as well as terms are unified.  The outermost functions assume the
    12 terms to be unified already have the same type.  In resolution, this is
    13 assured because both have type "prop".
    14 *)
    15 
    16 
    17 signature UNIFY = 
    18   sig
    19   (*references for control and tracing*)
    20   val trace_bound: int ref
    21   val trace_simp: bool ref
    22   val trace_types: bool ref
    23   val search_bound: int ref
    24   (*other exports*)
    25   val combound : (term*int*int) -> term
    26   val rlist_abs: (string*typ)list * term -> term   
    27   val smash_unifiers : Sign.sg * Envir.env * (term*term)list
    28 	-> (Envir.env Seq.seq)
    29   val unifiers: Sign.sg * Envir.env * ((term*term)list)
    30 	-> (Envir.env * (term * term)list) Seq.seq
    31   end;
    32 
    33 structure Unify	: UNIFY = 
    34 struct
    35 
    36 (*Unification options*)
    37 
    38 val trace_bound = ref 10	(*tracing starts above this depth, 0 for full*)
    39 and search_bound = ref 20	(*unification quits above this depth*)
    40 and trace_simp = ref false	(*print dpairs before calling SIMPL*)
    41 and trace_types = ref false	(*announce potential incompleteness
    42 				  of type unification*)
    43 
    44 val sgr = ref(Sign.pre_pure);
    45 
    46 type binderlist = (string*typ) list;
    47 
    48 type dpair = binderlist * term * term;
    49 
    50 fun body_type(Envir.Envir{iTs,...}) = 
    51 let fun bT(Type("fun",[_,T])) = bT T
    52       | bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
    53 		None => T | Some(T') => bT T')
    54       | bT T = T
    55 in bT end;
    56 
    57 fun binder_types(Envir.Envir{iTs,...}) = 
    58 let fun bTs(Type("fun",[T,U])) = T :: bTs U
    59       | bTs(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
    60 		None => [] | Some(T') => bTs T')
    61       | bTs _ = []
    62 in bTs end;
    63 
    64 fun strip_type env T = (binder_types env T, body_type env T);
    65 
    66 fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
    67 
    68 
    69 (*Eta normal form*)
    70 fun eta_norm(env as Envir.Envir{iTs,...}) =
    71   let fun etif (Type("fun",[T,U]), t) =
    72 	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    73 	| etif (TVar(ixn,_),t) = 
    74 	    (case Vartab.lookup (iTs,ixn) of
    75 		  None => t | Some(T) => etif(T,t))
    76 	| etif (_,t) = t;
    77       fun eta_nm (rbinder, Abs(a,T,body)) =
    78 	    Abs(a, T, eta_nm ((a,T)::rbinder, body))
    79 	| eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
    80   in eta_nm end;
    81 
    82 
    83 (*OCCURS CHECK
    84   Does the uvar occur in the term t?  
    85   two forms of search, for whether there is a rigid path to the current term.
    86   "seen" is list of variables passed thru, is a memo variable for sharing.
    87   This version searches for nonrigid occurrence, returns true if found. *)
    88 fun occurs_terms (seen: (indexname list) ref,
    89  		  env: Envir.env, v: indexname, ts: term list): bool =
    90   let fun occurs [] = false
    91 	| occurs (t::ts) =  occur t  orelse  occurs ts
    92       and occur (Const _)  = false
    93 	| occur (Bound _)  = false
    94 	| occur (Free _)  = false
    95 	| occur (Var (w,_))  = 
    96 	    if mem_ix (w, !seen) then false
    97 	    else if eq_ix(v,w) then true
    98 	      (*no need to lookup: v has no assignment*)
    99 	    else (seen := w:: !seen;  
   100 	          case  Envir.lookup(env,w)  of
   101 		      None    => false
   102 		    | Some t => occur t)
   103 	| occur (Abs(_,_,body)) = occur body
   104 	| occur (f$t) = occur t  orelse   occur f
   105   in  occurs ts  end;
   106 
   107 
   108 
   109 (* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
   110 fun head_of_in (env,t) : term = case t of
   111     f$_ => head_of_in(env,f)
   112   | Var (v,_) => (case  Envir.lookup(env,v)  of  
   113 			Some u => head_of_in(env,u)  |  None   => t)
   114   | _ => t;
   115 
   116 
   117 datatype occ = NoOcc | Nonrigid | Rigid;
   118 
   119 (* Rigid occur check
   120 Returns Rigid    if it finds a rigid occurrence of the variable,
   121         Nonrigid if it finds a nonrigid path to the variable.
   122         NoOcc    otherwise.
   123   Continues searching for a rigid occurrence even if it finds a nonrigid one.
   124 
   125 Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ]
   126    a rigid path to the variable, appearing with no arguments.
   127 Here completeness is sacrificed in order to reduce danger of divergence:
   128    reject ALL rigid paths to the variable.
   129 Could check for rigid paths to bound variables that are out of scope.  
   130 Not necessary because the assignment test looks at variable's ENTIRE rbinder.
   131 
   132 Treatment of head(arg1,...,argn):
   133 If head is a variable then no rigid path, switch to nonrigid search
   134 for arg1,...,argn. 
   135 If head is an abstraction then possibly no rigid path (head could be a 
   136    constant function) so again use nonrigid search.  Happens only if
   137    term is not in normal form. 
   138 
   139 Warning: finds a rigid occurrence of ?f in ?f(t).
   140   Should NOT be called in this case: there is a flex-flex unifier
   141 *)
   142 fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 
   143   let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 
   144 		       else NoOcc
   145       fun occurs [] = NoOcc
   146 	| occurs (t::ts) =
   147             (case occur t of
   148                Rigid => Rigid
   149              | oc =>  (case occurs ts of NoOcc => oc  |  oc2 => oc2))
   150       and occomb (f$t) =
   151             (case occur t of
   152                Rigid => Rigid
   153              | oc =>  (case occomb f of NoOcc => oc  |  oc2 => oc2))
   154         | occomb t = occur t
   155       and occur (Const _)  = NoOcc
   156 	| occur (Bound _)  = NoOcc
   157 	| occur (Free _)  = NoOcc
   158 	| occur (Var (w,_))  = 
   159 	    if mem_ix (w, !seen) then NoOcc
   160 	    else if eq_ix(v,w) then Rigid
   161 	    else (seen := w:: !seen;  
   162 	          case  Envir.lookup(env,w)  of
   163 		      None    => NoOcc
   164 		    | Some t => occur t)
   165 	| occur (Abs(_,_,body)) = occur body
   166 	| occur (t as f$_) =  (*switch to nonrigid search?*)
   167 	   (case head_of_in (env,f) of
   168 	      Var (w,_) => (*w is not assigned*)
   169 		if eq_ix(v,w) then Rigid  
   170 		else  nonrigid t
   171 	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
   172 	    | _ => occomb t)
   173   in  occur t  end;
   174 
   175 
   176 exception CANTUNIFY;	(*Signals non-unifiability.  Does not signal errors!*)
   177 exception ASSIGN;	(*Raised if not an assignment*)
   178 
   179 
   180 fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   181   if T=U then env
   182   else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (!sgr)) (iTs, maxidx) (U, T)
   183        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
   184        handle Type.TUNIFY => raise CANTUNIFY;
   185 
   186 fun test_unify_types(args as (T,U,_)) =
   187 let val sot = Sign.string_of_typ (!sgr);
   188     fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
   189     val env' = unify_types(args)
   190 in if is_TVar(T) orelse is_TVar(U) then warn() else ();
   191    env'
   192 end;
   193 
   194 (*Is the term eta-convertible to a single variable with the given rbinder?
   195   Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
   196   Result is var a for use in SIMPL. *)
   197 fun get_eta_var ([], _, Var vT)  =  vT
   198   | get_eta_var (_::rbinder, n, f $ Bound i) =
   199 	if  n=i  then  get_eta_var (rbinder, n+1, f) 
   200 		 else  raise ASSIGN
   201   | get_eta_var _ = raise ASSIGN;
   202 
   203 
   204 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   205 fun rlist_abs ([], body) = body
   206   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   207 
   208 
   209 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
   210   If v occurs rigidly then nonunifiable.
   211   If v occurs nonrigidly then must use full algorithm. *)
   212 fun assignment (env, rbinder, t, u) =
   213     let val (v,T) = get_eta_var(rbinder,0,t)
   214     in  case rigid_occurs_term (ref[], env, v, u) of
   215 	      NoOcc => let val env = unify_types(body_type env T,
   216 						 fastype env (rbinder,u),env)
   217 		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
   218 	    | Nonrigid =>  raise ASSIGN
   219 	    | Rigid =>  raise CANTUNIFY
   220     end;
   221 
   222 
   223 (*Extends an rbinder with a new disagreement pair, if both are abstractions.
   224   Tries to unify types of the bound variables!
   225   Checks that binders have same length, since terms should be eta-normal;
   226     if not, raises TERM, probably indicating type mismatch.
   227   Uses variable a (unless the null string) to preserve user's naming.*) 
   228 fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
   229 	let val env' = unify_types(T,U,env)
   230 	    val c = if a="" then b else a
   231 	in new_dpair((c,T) :: rbinder, body1, body2, env') end
   232     | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
   233     | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
   234     | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
   235 
   236 
   237 fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
   238      new_dpair (rbinder,
   239 		eta_norm env (rbinder, Envir.head_norm env t),
   240 	  	eta_norm env (rbinder, Envir.head_norm env u), env);
   241 
   242 
   243 
   244 (*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
   245   Does not perform assignments for flex-flex pairs:
   246     may create nonrigid paths, which prevent other assignments.
   247   Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
   248     do so caused numerous problems with no compensating advantage.
   249 *)
   250 fun SIMPL0 (dp0, (env,flexflex,flexrigid))
   251 	: Envir.env * dpair list * dpair list =
   252     let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
   253 	    fun SIMRANDS(f$t, g$u, env) =
   254 			SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
   255 	      | SIMRANDS (t as _$_, _, _) =
   256 		raise TERM ("SIMPL: operands mismatch", [t,u])
   257 	      | SIMRANDS (t, u as _$_, _) =
   258 		raise TERM ("SIMPL: operands mismatch", [t,u])
   259 	      | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
   260     in case (head_of t, head_of u) of
   261        (Var(_,T), Var(_,U)) =>
   262 	    let val T' = body_type env T and U' = body_type env U;
   263 		val env = unify_types(T',U',env)
   264 	    in (env, dp::flexflex, flexrigid) end
   265      | (Var _, _) =>
   266 	    ((assignment (env,rbinder,t,u), flexflex, flexrigid)
   267 	     handle ASSIGN => (env, flexflex, dp::flexrigid))
   268      | (_, Var _) =>
   269 	    ((assignment (env,rbinder,u,t), flexflex, flexrigid)
   270 	     handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
   271      | (Const(a,T), Const(b,U)) =>
   272 	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   273 	    else raise CANTUNIFY
   274      | (Bound i,    Bound j)    =>
   275 	    if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
   276      | (Free(a,T),  Free(b,U))  =>
   277 	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   278 	    else raise CANTUNIFY
   279      | _ => raise CANTUNIFY
   280     end;
   281 
   282 
   283 (* changed(env,t) checks whether the head of t is a variable assigned in env*)
   284 fun changed (env, f$_) = changed (env,f)
   285   | changed (env, Var (v,_)) =
   286       (case Envir.lookup(env,v) of None=>false  |  _ => true)
   287   | changed _ = false;
   288 
   289 
   290 (*Recursion needed if any of the 'head variables' have been updated
   291   Clever would be to re-do just the affected dpairs*)
   292 fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
   293     let val all as (env',flexflex,flexrigid) =
   294 	    foldr SIMPL0 (dpairs, (env,[],[]));
   295 	val dps = flexrigid@flexflex
   296     in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
   297        then SIMPL(env',dps) else all
   298     end;
   299 
   300 
   301 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   302 fun combound (t, n, k) = 
   303     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   304 
   305 
   306 (*Makes the terms E1,...,Em,    where Ts = [T...Tm]. 
   307   Each Ei is   ?Gi(B.(n-1),...,B.0), and has type Ti
   308   The B.j are bound vars of binder.
   309   The terms are not made in eta-normal-form, SIMPL does that later.  
   310   If done here, eta-expansion must be recursive in the arguments! *)
   311 fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
   312   | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
   313        let fun funtype T = binder--->T;
   314 	   val (env', vars) = Envir.genvars name (env, map funtype Ts)
   315        in  (env',  map (fn var=> combound(var, 0, length binder)) vars)  end;
   316 
   317 
   318 (*Abstraction over a list of types, like list_abs*)
   319 fun types_abs ([],u) = u
   320   | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
   321 
   322 (*Abstraction over the binder of a type*)
   323 fun type_abs (env,T,t) = types_abs(binder_types env T, t);
   324 
   325 
   326 (*MATCH taking "big steps".
   327   Copies u into the Var v, using projection on targs or imitation.
   328   A projection is allowed unless SIMPL raises an exception.
   329   Allocates new variables in projection on a higher-order argument,
   330     or if u is a variable (flex-flex dpair).
   331   Returns long sequence of every way of copying u, for backtracking
   332   For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
   333   The order for trying projections is crucial in ?b'(?a)   
   334   NB "vname" is only used in the call to make_args!!   *)
   335 fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
   336 	: (term * (Envir.env * dpair list))Seq.seq =
   337 let (*Produce copies of uarg and cons them in front of uargs*)
   338     fun copycons uarg (uargs, (env, dpairs)) =
   339 	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
   340 	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
   341 		 (env, dpairs)));
   342 	(*Produce sequence of all possible ways of copying the arg list*)
   343     fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
   344       | copyargs (uarg::uargs) =
   345 	    Seq.flat (Seq.map (copycons uarg) (copyargs uargs));
   346     val (uhead,uargs) = strip_comb u;
   347     val base = body_type env (fastype env (rbinder,uhead));
   348     fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
   349     (*attempt projection on argument with given typ*)
   350     val Ts = map (curry (fastype env) rbinder) targs;
   351     fun projenv (head, (Us,bary), targ, tail) = 
   352 	let val env = if !trace_types then test_unify_types(base,bary,env)
   353 		      else unify_types(base,bary,env)
   354 	in Seq.make (fn () =>  
   355 	    let val (env',args) = make_args vname (Ts,env,Us);
   356 		(*higher-order projection: plug in targs for bound vars*)
   357 		fun plugin arg = list_comb(head_of arg, targs);
   358 		val dp = (rbinder, list_comb(targ, map plugin args), u);
   359 		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
   360 		    (*may raise exception CANTUNIFY*)
   361 	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
   362 			tail)
   363 	    end  handle CANTUNIFY => Seq.pull tail)
   364 	end handle CANTUNIFY => tail;
   365     (*make a list of projections*)
   366     fun make_projs (T::Ts, targ::targs) =
   367 	      (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
   368       | make_projs ([],[]) = []
   369       | make_projs _ = raise TERM ("make_projs", u::targs);
   370     (*try projections and imitation*)
   371     fun matchfun ((bvar,T,targ)::projs) =
   372 	       (projenv(bvar, strip_type env T, targ, matchfun projs))
   373       | matchfun [] = (*imitation last of all*)
   374 	      (case uhead of
   375 		 Const _ => Seq.map joinargs (copyargs uargs)
   376 	       | Free _  => Seq.map joinargs (copyargs uargs)
   377 	       | _ => Seq.empty)  (*if Var, would be a loop!*)
   378 in case uhead of
   379 	Abs(a, T, body) =>
   380 	    Seq.map(fn (body', ed') => (Abs (a,T,body'), ed')) 
   381 		(mc ((a,T)::rbinder,
   382 			(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
   383       | Var (w,uary) => 
   384 	    (*a flex-flex dpair: make variable for t*)
   385 	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
   386 		val tabs = combound(newhd, 0, length Ts)
   387 		val tsub = list_comb(newhd,targs)
   388 	    in  Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
   389 	    end
   390       | _ =>  matchfun(rev(make_projs(Ts, targs)))
   391 end
   392 in mc end;
   393 
   394 
   395 (*Call matchcopy to produce assignments to the variable in the dpair*)
   396 fun MATCH (env, (rbinder,t,u), dpairs)
   397 	: (Envir.env * dpair list)Seq.seq = 
   398   let val (Var(v,T), targs) = strip_comb t;
   399       val Ts = binder_types env T;
   400       fun new_dset (u', (env',dpairs')) =
   401 	  (*if v was updated to s, must unify s with u' *)
   402 	  case Envir.lookup(env',v) of
   403 	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
   404 	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   405   in Seq.map new_dset
   406          (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   407   end;
   408 
   409 
   410 
   411 (**** Flex-flex processing ****)
   412 
   413 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
   414   Attempts to update t with u, raising ASSIGN if impossible*)
   415 fun ff_assign(env, rbinder, t, u) : Envir.env = 
   416 let val (v,T) = get_eta_var(rbinder,0,t)
   417 in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
   418    else let val env = unify_types(body_type env T,
   419 				  fastype env (rbinder,u),
   420 				  env)
   421 	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
   422 end;
   423 
   424 
   425 (*Flex argument: a term, its type, and the index that refers to it.*)
   426 type flarg = {t: term,  T: typ,  j: int};
   427 
   428 
   429 (*Form the arguments into records for deletion/sorting.*)
   430 fun flexargs ([],[],[]) = [] : flarg list
   431   | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
   432   | flexargs _ = error"flexargs";
   433 
   434 
   435 (*If an argument contains a banned Bound, then it should be deleted.
   436   But if the only path is flexible, this is difficult; the code gives up!
   437   In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
   438 exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
   439 
   440 
   441 (*Check whether the 'banned' bound var indices occur rigidly in t*)
   442 fun rigid_bound (lev, banned) t = 
   443   let val (head,args) = strip_comb t 
   444   in  
   445       case head of
   446 	  Bound i => (i-lev) mem_int banned  orelse
   447 	      	     exists (rigid_bound (lev, banned)) args
   448 	| Var _ => false	(*no rigid occurrences here!*)
   449 	| Abs (_,_,u) => 
   450 	       rigid_bound(lev+1, banned) u  orelse
   451 	       exists (rigid_bound (lev, banned)) args
   452 	| _ => exists (rigid_bound (lev, banned)) args
   453   end;
   454 
   455 (*Squash down indices at level >=lev to delete the banned from a term.*)
   456 fun change_bnos banned =
   457   let fun change lev (Bound i) = 
   458 	    if i<lev then Bound i
   459 	    else  if (i-lev) mem_int banned  
   460 		  then raise CHANGE_FAIL (**flexible occurrence: give up**)
   461 	    else  Bound (i - length (filter (fn j => j < i-lev) banned))
   462 	| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
   463 	| change lev (t$u) = change lev t $ change lev u
   464 	| change lev t = t
   465   in  change 0  end;
   466 
   467 (*Change indices, delete the argument if it contains a banned Bound*)
   468 fun change_arg banned ({j,t,T}, args) : flarg list =
   469     if rigid_bound (0, banned) t  then  args	(*delete argument!*)
   470     else  {j=j, t= change_bnos banned t, T=T} :: args;
   471 
   472 
   473 (*Sort the arguments to create assignments if possible:
   474   create eta-terms like ?g(B.1,B.0) *)
   475 fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
   476   | arg_less (_:flarg, _:flarg) = false;
   477 
   478 (*Test whether the new term would be eta-equivalent to a variable --
   479   if so then there is no point in creating a new variable*)
   480 fun decreasing n ([]: flarg list) = (n=0)
   481   | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
   482 
   483 (*Delete banned indices in the term, simplifying it.
   484   Force an assignment, if possible, by sorting the arguments.
   485   Update its head; squash indices in arguments. *)
   486 fun clean_term banned (env,t) =
   487     let val (Var(v,T), ts) = strip_comb t
   488 	val (Ts,U) = strip_type env T
   489 	and js = length ts - 1  downto 0
   490 	val args = sort (make_ord arg_less)
   491 		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
   492 	val ts' = map (#t) args
   493     in
   494     if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   495     else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
   496 	     val body = list_comb(v', map (Bound o #j) args)
   497 	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
   498 	     (*the vupdate affects ts' if they contain v*)
   499 	 in  
   500 	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
   501          end
   502     end;
   503 
   504 
   505 (*Add tpair if not trivial or already there.
   506   Should check for swapped pairs??*)
   507 fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
   508   if t0 aconv u0 then tpairs  
   509   else
   510   let val t = rlist_abs(rbinder, t0)  and  u = rlist_abs(rbinder, u0);
   511       fun same(t',u') = (t aconv t') andalso (u aconv u')
   512   in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
   513 
   514 
   515 (*Simplify both terms and check for assignments.
   516   Bound vars in the binder are "banned" unless used in both t AND u *)
   517 fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 
   518   let val loot = loose_bnos t  and  loou = loose_bnos u
   519       fun add_index (((a,T), j), (bnos, newbinder)) = 
   520             if  j mem_int loot  andalso  j mem_int loou 
   521             then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
   522             else  (j::bnos, newbinder);		(*remove*)
   523       val indices = 0 upto (length rbinder - 1);
   524       val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
   525       val (env', t') = clean_term banned (env, t);
   526       val (env'',u') = clean_term banned (env',u)
   527   in  (ff_assign(env'', rbin', t', u'), tpairs)
   528       handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
   529       handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
   530   end
   531   handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
   532 
   533 
   534 (*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   535   eliminates trivial tpairs like t=t, as well as repeated ones
   536   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t 
   537   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
   538 fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 
   539       : Envir.env * (term*term)list =
   540   let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   541   in  case  (head_of t, head_of u) of
   542       (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
   543 	if eq_ix(v,w) then     (*...occur check would falsely return true!*)
   544 	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   545 	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
   546 	else if xless(v,w) then (*prefer to update the LARGER variable*)
   547 	     clean_ffpair ((rbinder, u, t), (env,tpairs))
   548         else clean_ffpair ((rbinder, t, u), (env,tpairs))
   549     | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
   550   end;
   551 
   552 
   553 (*Print a tracing message + list of dpairs.
   554   In t==u print u first because it may be rigid or flexible --
   555     t is always flexible.*)
   556 fun print_dpairs msg (env,dpairs) =
   557   let fun pdp (rbinder,t,u) =
   558         let fun termT t = Sign.pretty_term (!sgr)
   559                               (Envir.norm_term env (rlist_abs(rbinder,t)))
   560             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
   561                           termT t];
   562         in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   563   in  tracing msg;  seq pdp dpairs  end;
   564 
   565 
   566 (*Unify the dpairs in the environment.
   567   Returns flex-flex disagreement pairs NOT IN normal form. 
   568   SIMPL may raise exception CANTUNIFY. *)
   569 fun hounifiers (sg,env, tus : (term*term)list) 
   570   : (Envir.env * (term*term)list)Seq.seq =
   571   let fun add_unify tdepth ((env,dpairs), reseq) =
   572 	  Seq.make (fn()=>
   573 	  let val (env',flexflex,flexrigid) = 
   574 	       (if tdepth> !trace_bound andalso !trace_simp
   575 		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   576 		SIMPL (env,dpairs))
   577 	  in case flexrigid of
   578 	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
   579 	    | dp::frigid' => 
   580 		if tdepth > !search_bound then
   581 		    (warning "Unification bound exceeded"; Seq.pull reseq)
   582 		else
   583 		(if tdepth > !trace_bound then
   584 		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
   585 		 else ();
   586 		 Seq.pull (Seq.it_right (add_unify (tdepth+1))
   587 			   (MATCH (env',dp, frigid'@flexflex), reseq)))
   588 	  end
   589 	  handle CANTUNIFY => 
   590 	    (if tdepth > !trace_bound then tracing"Failure node" else ();
   591 	     Seq.pull reseq));
   592      val dps = map (fn(t,u)=> ([],t,u)) tus
   593   in sgr := sg;
   594      add_unify 1 ((env,dps), Seq.empty) 
   595   end;
   596 
   597 fun unifiers(params) =
   598       Seq.cons((Pattern.unify(params), []),   Seq.empty)
   599       handle Pattern.Unif => Seq.empty
   600            | Pattern.Pattern => hounifiers(params);
   601 
   602 
   603 (*For smash_flexflex1*)
   604 fun var_head_of (env,t) : indexname * typ =
   605   case head_of (strip_abs_body (Envir.norm_term env t)) of
   606       Var(v,T) => (v,T)
   607     | _ => raise CANTUNIFY;  (*not flexible, cannot use trivial substitution*)
   608 
   609 
   610 (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   611   Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   612   Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, 
   613 	though just ?g->?f is a more general unifier.
   614   Unlike Huet (1975), does not smash together all variables of same type --
   615     requires more work yet gives a less general unifier (fewer variables).
   616   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   617 fun smash_flexflex1 ((t,u), env) : Envir.env =
   618   let val (v,T) = var_head_of (env,t)
   619       and (w,U) = var_head_of (env,u);
   620       val (env', var) = Envir.genvar (#1v) (env, body_type env T)
   621       val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
   622   in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
   623       else Envir.vupdate((v, type_abs(env',T,var)), env'')
   624   end;
   625 
   626 
   627 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   628 fun smash_flexflex (env,tpairs) : Envir.env =
   629   foldr smash_flexflex1 (tpairs, env);
   630 
   631 (*Returns unifiers with no remaining disagreement pairs*)
   632 fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
   633     Seq.map smash_flexflex (unifiers(sg,env,tus));
   634 
   635 end;