src/Pure/unify.ML
author berghofe
Mon Nov 19 17:32:49 2001 +0100 (2001-11-19)
changeset 12231 4a25f04bea61
parent 8406 a217b0cd304d
child 12262 11ff5f47df6e
permissions -rw-r--r--
Moved head_norm and fastype from unify.ML to envir.ML
     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 (#tsig(Sign.rep_sg (!sgr)))
   183                                                 maxidx iTs (U,T)
   184        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
   185        handle Type.TUNIFY => raise CANTUNIFY;
   186 
   187 fun test_unify_types(args as (T,U,_)) =
   188 let val sot = Sign.string_of_typ (!sgr);
   189     fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
   190     val env' = unify_types(args)
   191 in if is_TVar(T) orelse is_TVar(U) then warn() else ();
   192    env'
   193 end;
   194 
   195 (*Is the term eta-convertible to a single variable with the given rbinder?
   196   Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
   197   Result is var a for use in SIMPL. *)
   198 fun get_eta_var ([], _, Var vT)  =  vT
   199   | get_eta_var (_::rbinder, n, f $ Bound i) =
   200 	if  n=i  then  get_eta_var (rbinder, n+1, f) 
   201 		 else  raise ASSIGN
   202   | get_eta_var _ = raise ASSIGN;
   203 
   204 
   205 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   206 fun rlist_abs ([], body) = body
   207   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   208 
   209 
   210 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
   211   If v occurs rigidly then nonunifiable.
   212   If v occurs nonrigidly then must use full algorithm. *)
   213 fun assignment (env, rbinder, t, u) =
   214     let val (v,T) = get_eta_var(rbinder,0,t)
   215     in  case rigid_occurs_term (ref[], env, v, u) of
   216 	      NoOcc => let val env = unify_types(body_type env T,
   217 						 fastype env (rbinder,u),env)
   218 		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
   219 	    | Nonrigid =>  raise ASSIGN
   220 	    | Rigid =>  raise CANTUNIFY
   221     end;
   222 
   223 
   224 (*Extends an rbinder with a new disagreement pair, if both are abstractions.
   225   Tries to unify types of the bound variables!
   226   Checks that binders have same length, since terms should be eta-normal;
   227     if not, raises TERM, probably indicating type mismatch.
   228   Uses variable a (unless the null string) to preserve user's naming.*) 
   229 fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
   230 	let val env' = unify_types(T,U,env)
   231 	    val c = if a="" then b else a
   232 	in new_dpair((c,T) :: rbinder, body1, body2, env') end
   233     | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
   234     | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
   235     | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
   236 
   237 
   238 fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
   239      new_dpair (rbinder,
   240 		eta_norm env (rbinder, Envir.head_norm env t),
   241 	  	eta_norm env (rbinder, Envir.head_norm env u), env);
   242 
   243 
   244 
   245 (*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
   246   Does not perform assignments for flex-flex pairs:
   247     may create nonrigid paths, which prevent other assignments.
   248   Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
   249     do so caused numerous problems with no compensating advantage.
   250 *)
   251 fun SIMPL0 (dp0, (env,flexflex,flexrigid))
   252 	: Envir.env * dpair list * dpair list =
   253     let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
   254 	    fun SIMRANDS(f$t, g$u, env) =
   255 			SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
   256 	      | SIMRANDS (t as _$_, _, _) =
   257 		raise TERM ("SIMPL: operands mismatch", [t,u])
   258 	      | SIMRANDS (t, u as _$_, _) =
   259 		raise TERM ("SIMPL: operands mismatch", [t,u])
   260 	      | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
   261     in case (head_of t, head_of u) of
   262        (Var(_,T), Var(_,U)) =>
   263 	    let val T' = body_type env T and U' = body_type env U;
   264 		val env = unify_types(T',U',env)
   265 	    in (env, dp::flexflex, flexrigid) end
   266      | (Var _, _) =>
   267 	    ((assignment (env,rbinder,t,u), flexflex, flexrigid)
   268 	     handle ASSIGN => (env, flexflex, dp::flexrigid))
   269      | (_, Var _) =>
   270 	    ((assignment (env,rbinder,u,t), flexflex, flexrigid)
   271 	     handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
   272      | (Const(a,T), Const(b,U)) =>
   273 	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   274 	    else raise CANTUNIFY
   275      | (Bound i,    Bound j)    =>
   276 	    if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
   277      | (Free(a,T),  Free(b,U))  =>
   278 	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   279 	    else raise CANTUNIFY
   280      | _ => raise CANTUNIFY
   281     end;
   282 
   283 
   284 (* changed(env,t) checks whether the head of t is a variable assigned in env*)
   285 fun changed (env, f$_) = changed (env,f)
   286   | changed (env, Var (v,_)) =
   287       (case Envir.lookup(env,v) of None=>false  |  _ => true)
   288   | changed _ = false;
   289 
   290 
   291 (*Recursion needed if any of the 'head variables' have been updated
   292   Clever would be to re-do just the affected dpairs*)
   293 fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
   294     let val all as (env',flexflex,flexrigid) =
   295 	    foldr SIMPL0 (dpairs, (env,[],[]));
   296 	val dps = flexrigid@flexflex
   297     in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
   298        then SIMPL(env',dps) else all
   299     end;
   300 
   301 
   302 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   303 fun combound (t, n, k) = 
   304     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   305 
   306 
   307 (*Makes the terms E1,...,Em,    where Ts = [T...Tm]. 
   308   Each Ei is   ?Gi(B.(n-1),...,B.0), and has type Ti
   309   The B.j are bound vars of binder.
   310   The terms are not made in eta-normal-form, SIMPL does that later.  
   311   If done here, eta-expansion must be recursive in the arguments! *)
   312 fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
   313   | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
   314        let fun funtype T = binder--->T;
   315 	   val (env', vars) = Envir.genvars name (env, map funtype Ts)
   316        in  (env',  map (fn var=> combound(var, 0, length binder)) vars)  end;
   317 
   318 
   319 (*Abstraction over a list of types, like list_abs*)
   320 fun types_abs ([],u) = u
   321   | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
   322 
   323 (*Abstraction over the binder of a type*)
   324 fun type_abs (env,T,t) = types_abs(binder_types env T, t);
   325 
   326 
   327 (*MATCH taking "big steps".
   328   Copies u into the Var v, using projection on targs or imitation.
   329   A projection is allowed unless SIMPL raises an exception.
   330   Allocates new variables in projection on a higher-order argument,
   331     or if u is a variable (flex-flex dpair).
   332   Returns long sequence of every way of copying u, for backtracking
   333   For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
   334   The order for trying projections is crucial in ?b'(?a)   
   335   NB "vname" is only used in the call to make_args!!   *)
   336 fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
   337 	: (term * (Envir.env * dpair list))Seq.seq =
   338 let (*Produce copies of uarg and cons them in front of uargs*)
   339     fun copycons uarg (uargs, (env, dpairs)) =
   340 	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
   341 	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
   342 		 (env, dpairs)));
   343 	(*Produce sequence of all possible ways of copying the arg list*)
   344     fun copyargs [] = Seq.cons( ([],ed), Seq.empty)
   345       | copyargs (uarg::uargs) =
   346 	    Seq.flat (Seq.map (copycons uarg) (copyargs uargs));
   347     val (uhead,uargs) = strip_comb u;
   348     val base = body_type env (fastype env (rbinder,uhead));
   349     fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
   350     (*attempt projection on argument with given typ*)
   351     val Ts = map (curry (fastype env) rbinder) targs;
   352     fun projenv (head, (Us,bary), targ, tail) = 
   353 	let val env = if !trace_types then test_unify_types(base,bary,env)
   354 		      else unify_types(base,bary,env)
   355 	in Seq.make (fn () =>  
   356 	    let val (env',args) = make_args vname (Ts,env,Us);
   357 		(*higher-order projection: plug in targs for bound vars*)
   358 		fun plugin arg = list_comb(head_of arg, targs);
   359 		val dp = (rbinder, list_comb(targ, map plugin args), u);
   360 		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
   361 		    (*may raise exception CANTUNIFY*)
   362 	    in  Some ((list_comb(head,args), (env2, frigid@fflex)),
   363 			tail)
   364 	    end  handle CANTUNIFY => Seq.pull tail)
   365 	end handle CANTUNIFY => tail;
   366     (*make a list of projections*)
   367     fun make_projs (T::Ts, targ::targs) =
   368 	      (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
   369       | make_projs ([],[]) = []
   370       | make_projs _ = raise TERM ("make_projs", u::targs);
   371     (*try projections and imitation*)
   372     fun matchfun ((bvar,T,targ)::projs) =
   373 	       (projenv(bvar, strip_type env T, targ, matchfun projs))
   374       | matchfun [] = (*imitation last of all*)
   375 	      (case uhead of
   376 		 Const _ => Seq.map joinargs (copyargs uargs)
   377 	       | Free _  => Seq.map joinargs (copyargs uargs)
   378 	       | _ => Seq.empty)  (*if Var, would be a loop!*)
   379 in case uhead of
   380 	Abs(a, T, body) =>
   381 	    Seq.map(fn (body', ed') => (Abs (a,T,body'), ed')) 
   382 		(mc ((a,T)::rbinder,
   383 			(map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
   384       | Var (w,uary) => 
   385 	    (*a flex-flex dpair: make variable for t*)
   386 	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
   387 		val tabs = combound(newhd, 0, length Ts)
   388 		val tsub = list_comb(newhd,targs)
   389 	    in  Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
   390 	    end
   391       | _ =>  matchfun(rev(make_projs(Ts, targs)))
   392 end
   393 in mc end;
   394 
   395 
   396 (*Call matchcopy to produce assignments to the variable in the dpair*)
   397 fun MATCH (env, (rbinder,t,u), dpairs)
   398 	: (Envir.env * dpair list)Seq.seq = 
   399   let val (Var(v,T), targs) = strip_comb t;
   400       val Ts = binder_types env T;
   401       fun new_dset (u', (env',dpairs')) =
   402 	  (*if v was updated to s, must unify s with u' *)
   403 	  case Envir.lookup(env',v) of
   404 	      None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
   405 	    | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   406   in Seq.map new_dset
   407          (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   408   end;
   409 
   410 
   411 
   412 (**** Flex-flex processing ****)
   413 
   414 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
   415   Attempts to update t with u, raising ASSIGN if impossible*)
   416 fun ff_assign(env, rbinder, t, u) : Envir.env = 
   417 let val (v,T) = get_eta_var(rbinder,0,t)
   418 in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
   419    else let val env = unify_types(body_type env T,
   420 				  fastype env (rbinder,u),
   421 				  env)
   422 	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
   423 end;
   424 
   425 
   426 (*Flex argument: a term, its type, and the index that refers to it.*)
   427 type flarg = {t: term,  T: typ,  j: int};
   428 
   429 
   430 (*Form the arguments into records for deletion/sorting.*)
   431 fun flexargs ([],[],[]) = [] : flarg list
   432   | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
   433   | flexargs _ = error"flexargs";
   434 
   435 
   436 (*If an argument contains a banned Bound, then it should be deleted.
   437   But if the only path is flexible, this is difficult; the code gives up!
   438   In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
   439 exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
   440 
   441 
   442 (*Check whether the 'banned' bound var indices occur rigidly in t*)
   443 fun rigid_bound (lev, banned) t = 
   444   let val (head,args) = strip_comb t 
   445   in  
   446       case head of
   447 	  Bound i => (i-lev) mem_int banned  orelse
   448 	      	     exists (rigid_bound (lev, banned)) args
   449 	| Var _ => false	(*no rigid occurrences here!*)
   450 	| Abs (_,_,u) => 
   451 	       rigid_bound(lev+1, banned) u  orelse
   452 	       exists (rigid_bound (lev, banned)) args
   453 	| _ => exists (rigid_bound (lev, banned)) args
   454   end;
   455 
   456 (*Squash down indices at level >=lev to delete the banned from a term.*)
   457 fun change_bnos banned =
   458   let fun change lev (Bound i) = 
   459 	    if i<lev then Bound i
   460 	    else  if (i-lev) mem_int banned  
   461 		  then raise CHANGE_FAIL (**flexible occurrence: give up**)
   462 	    else  Bound (i - length (filter (fn j => j < i-lev) banned))
   463 	| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
   464 	| change lev (t$u) = change lev t $ change lev u
   465 	| change lev t = t
   466   in  change 0  end;
   467 
   468 (*Change indices, delete the argument if it contains a banned Bound*)
   469 fun change_arg banned ({j,t,T}, args) : flarg list =
   470     if rigid_bound (0, banned) t  then  args	(*delete argument!*)
   471     else  {j=j, t= change_bnos banned t, T=T} :: args;
   472 
   473 
   474 (*Sort the arguments to create assignments if possible:
   475   create eta-terms like ?g(B.1,B.0) *)
   476 fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
   477   | arg_less (_:flarg, _:flarg) = false;
   478 
   479 (*Test whether the new term would be eta-equivalent to a variable --
   480   if so then there is no point in creating a new variable*)
   481 fun decreasing n ([]: flarg list) = (n=0)
   482   | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
   483 
   484 (*Delete banned indices in the term, simplifying it.
   485   Force an assignment, if possible, by sorting the arguments.
   486   Update its head; squash indices in arguments. *)
   487 fun clean_term banned (env,t) =
   488     let val (Var(v,T), ts) = strip_comb t
   489 	val (Ts,U) = strip_type env T
   490 	and js = length ts - 1  downto 0
   491 	val args = sort (make_ord arg_less)
   492 		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
   493 	val ts' = map (#t) args
   494     in
   495     if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   496     else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
   497 	     val body = list_comb(v', map (Bound o #j) args)
   498 	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
   499 	     (*the vupdate affects ts' if they contain v*)
   500 	 in  
   501 	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
   502          end
   503     end;
   504 
   505 
   506 (*Add tpair if not trivial or already there.
   507   Should check for swapped pairs??*)
   508 fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
   509   if t0 aconv u0 then tpairs  
   510   else
   511   let val t = rlist_abs(rbinder, t0)  and  u = rlist_abs(rbinder, u0);
   512       fun same(t',u') = (t aconv t') andalso (u aconv u')
   513   in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
   514 
   515 
   516 (*Simplify both terms and check for assignments.
   517   Bound vars in the binder are "banned" unless used in both t AND u *)
   518 fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 
   519   let val loot = loose_bnos t  and  loou = loose_bnos u
   520       fun add_index (((a,T), j), (bnos, newbinder)) = 
   521             if  j mem_int loot  andalso  j mem_int loou 
   522             then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
   523             else  (j::bnos, newbinder);		(*remove*)
   524       val indices = 0 upto (length rbinder - 1);
   525       val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
   526       val (env', t') = clean_term banned (env, t);
   527       val (env'',u') = clean_term banned (env',u)
   528   in  (ff_assign(env'', rbin', t', u'), tpairs)
   529       handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
   530       handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
   531   end
   532   handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
   533 
   534 
   535 (*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   536   eliminates trivial tpairs like t=t, as well as repeated ones
   537   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t 
   538   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
   539 fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 
   540       : Envir.env * (term*term)list =
   541   let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   542   in  case  (head_of t, head_of u) of
   543       (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
   544 	if eq_ix(v,w) then     (*...occur check would falsely return true!*)
   545 	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   546 	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
   547 	else if xless(v,w) then (*prefer to update the LARGER variable*)
   548 	     clean_ffpair ((rbinder, u, t), (env,tpairs))
   549         else clean_ffpair ((rbinder, t, u), (env,tpairs))
   550     | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
   551   end;
   552 
   553 
   554 (*Print a tracing message + list of dpairs.
   555   In t==u print u first because it may be rigid or flexible --
   556     t is always flexible.*)
   557 fun print_dpairs msg (env,dpairs) =
   558   let fun pdp (rbinder,t,u) =
   559         let fun termT t = Sign.pretty_term (!sgr)
   560                               (Envir.norm_term env (rlist_abs(rbinder,t)))
   561             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
   562                           termT t];
   563         in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   564   in  writeln msg;  seq pdp dpairs  end;
   565 
   566 
   567 (*Unify the dpairs in the environment.
   568   Returns flex-flex disagreement pairs NOT IN normal form. 
   569   SIMPL may raise exception CANTUNIFY. *)
   570 fun hounifiers (sg,env, tus : (term*term)list) 
   571   : (Envir.env * (term*term)list)Seq.seq =
   572   let fun add_unify tdepth ((env,dpairs), reseq) =
   573 	  Seq.make (fn()=>
   574 	  let val (env',flexflex,flexrigid) = 
   575 	       (if tdepth> !trace_bound andalso !trace_simp
   576 		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   577 		SIMPL (env,dpairs))
   578 	  in case flexrigid of
   579 	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
   580 	    | dp::frigid' => 
   581 		if tdepth > !search_bound then
   582 		    (warning "Unification bound exceeded"; Seq.pull reseq)
   583 		else
   584 		(if tdepth > !trace_bound then
   585 		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
   586 		 else ();
   587 		 Seq.pull (Seq.it_right (add_unify (tdepth+1))
   588 			   (MATCH (env',dp, frigid'@flexflex), reseq)))
   589 	  end
   590 	  handle CANTUNIFY => 
   591 	    (if tdepth > !trace_bound then writeln"Failure node" else ();
   592 	     Seq.pull reseq));
   593      val dps = map (fn(t,u)=> ([],t,u)) tus
   594   in sgr := sg;
   595      add_unify 1 ((env,dps), Seq.empty) 
   596   end;
   597 
   598 fun unifiers(params) =
   599       Seq.cons((Pattern.unify(params), []),   Seq.empty)
   600       handle Pattern.Unif => Seq.empty
   601            | Pattern.Pattern => hounifiers(params);
   602 
   603 
   604 (*For smash_flexflex1*)
   605 fun var_head_of (env,t) : indexname * typ =
   606   case head_of (strip_abs_body (Envir.norm_term env t)) of
   607       Var(v,T) => (v,T)
   608     | _ => raise CANTUNIFY;  (*not flexible, cannot use trivial substitution*)
   609 
   610 
   611 (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   612   Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   613   Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, 
   614 	though just ?g->?f is a more general unifier.
   615   Unlike Huet (1975), does not smash together all variables of same type --
   616     requires more work yet gives a less general unifier (fewer variables).
   617   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   618 fun smash_flexflex1 ((t,u), env) : Envir.env =
   619   let val (v,T) = var_head_of (env,t)
   620       and (w,U) = var_head_of (env,u);
   621       val (env', var) = Envir.genvar (#1v) (env, body_type env T)
   622       val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
   623   in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
   624       else Envir.vupdate((v, type_abs(env',T,var)), env'')
   625   end;
   626 
   627 
   628 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   629 fun smash_flexflex (env,tpairs) : Envir.env =
   630   foldr smash_flexflex1 (tpairs, env);
   631 
   632 (*Returns unifiers with no remaining disagreement pairs*)
   633 fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
   634     Seq.map smash_flexflex (unifiers(sg,env,tus));
   635 
   636 end;