src/Pure/unify.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15574 b1d1b5bfc464
child 16425 2427be27cc60
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     1 (*  Title:      Pure/unify.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Higher-Order Unification
     7 
     8 Types as well as terms are unified.  The outermost functions assume the
     9 terms to be unified already have the same type.  In resolution, this is
    10 assured because both have type "prop".
    11 *)
    12 
    13 
    14 signature UNIFY = 
    15   sig
    16   (*references for control and tracing*)
    17   val trace_bound: int ref
    18   val trace_simp: bool ref
    19   val trace_types: bool ref
    20   val search_bound: int ref
    21   (*other exports*)
    22   val combound : (term*int*int) -> term
    23   val rlist_abs: (string*typ)list * term -> term   
    24   val smash_unifiers : Sign.sg * Envir.env * (term*term)list
    25 	-> (Envir.env Seq.seq)
    26   val unifiers: Sign.sg * Envir.env * ((term*term)list)
    27 	-> (Envir.env * (term * term)list) Seq.seq
    28   end;
    29 
    30 structure Unify	: UNIFY = 
    31 struct
    32 
    33 (*Unification options*)
    34 
    35 val trace_bound = ref 25	(*tracing starts above this depth, 0 for full*)
    36 and search_bound = ref 30	(*unification quits above this depth*)
    37 and trace_simp = ref false	(*print dpairs before calling SIMPL*)
    38 and trace_types = ref false	(*announce potential incompleteness
    39 				  of type unification*)
    40 
    41 val sgr = ref(Sign.pre_pure);
    42 
    43 type binderlist = (string*typ) list;
    44 
    45 type dpair = binderlist * term * term;
    46 
    47 fun body_type(Envir.Envir{iTs,...}) = 
    48 let fun bT(Type("fun",[_,T])) = bT T
    49       | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
    50 		NONE => T | SOME(T') => bT T')
    51       | bT T = T
    52 in bT end;
    53 
    54 fun binder_types(Envir.Envir{iTs,...}) = 
    55 let fun bTs(Type("fun",[T,U])) = T :: bTs U
    56       | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
    57 		NONE => [] | SOME(T') => bTs T')
    58       | bTs _ = []
    59 in bTs end;
    60 
    61 fun strip_type env T = (binder_types env T, body_type env T);
    62 
    63 fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
    64 
    65 
    66 (*Eta normal form*)
    67 fun eta_norm(env as Envir.Envir{iTs,...}) =
    68   let fun etif (Type("fun",[T,U]), t) =
    69 	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    70 	| etif (TVar ixnS, t) = 
    71 	    (case Type.lookup (iTs, ixnS) of
    72 		  NONE => t | SOME(T) => etif(T,t))
    73 	| etif (_,t) = t;
    74       fun eta_nm (rbinder, Abs(a,T,body)) =
    75 	    Abs(a, T, eta_nm ((a,T)::rbinder, body))
    76 	| eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
    77   in eta_nm end;
    78 
    79 
    80 (*OCCURS CHECK
    81   Does the uvar occur in the term t?  
    82   two forms of search, for whether there is a rigid path to the current term.
    83   "seen" is list of variables passed thru, is a memo variable for sharing.
    84   This version searches for nonrigid occurrence, returns true if found.
    85   Since terms may contain variables with same name and different types,
    86   the occurs check must ignore the types of variables. This avoids
    87   that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
    88   substitution when ?'a is instantiated with T later. *)
    89 fun occurs_terms (seen: (indexname list) ref,
    90  		  env: Envir.env, v: indexname, ts: term list): bool =
    91   let fun occurs [] = false
    92 	| occurs (t::ts) =  occur t  orelse  occurs ts
    93       and occur (Const _)  = false
    94 	| occur (Bound _)  = false
    95 	| occur (Free _)  = false
    96 	| occur (Var (w, T))  = 
    97 	    if mem_ix (w, !seen) then false
    98 	    else if eq_ix(v,w) then true
    99 	      (*no need to lookup: v has no assignment*)
   100 	    else (seen := w:: !seen;  
   101 	          case Envir.lookup (env, (w, T)) of
   102 		      NONE    => false
   103 		    | SOME t => occur t)
   104 	| occur (Abs(_,_,body)) = occur body
   105 	| occur (f$t) = occur t  orelse   occur f
   106   in  occurs ts  end;
   107 
   108 
   109 
   110 (* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
   111 fun head_of_in (env,t) : term = case t of
   112     f$_ => head_of_in(env,f)
   113   | Var vT => (case Envir.lookup (env, vT) of  
   114 			SOME u => head_of_in(env,u)  |  NONE   => t)
   115   | _ => t;
   116 
   117 
   118 datatype occ = NoOcc | Nonrigid | Rigid;
   119 
   120 (* Rigid occur check
   121 Returns Rigid    if it finds a rigid occurrence of the variable,
   122         Nonrigid if it finds a nonrigid path to the variable.
   123         NoOcc    otherwise.
   124   Continues searching for a rigid occurrence even if it finds a nonrigid one.
   125 
   126 Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ]
   127    a rigid path to the variable, appearing with no arguments.
   128 Here completeness is sacrificed in order to reduce danger of divergence:
   129    reject ALL rigid paths to the variable.
   130 Could check for rigid paths to bound variables that are out of scope.  
   131 Not necessary because the assignment test looks at variable's ENTIRE rbinder.
   132 
   133 Treatment of head(arg1,...,argn):
   134 If head is a variable then no rigid path, switch to nonrigid search
   135 for arg1,...,argn. 
   136 If head is an abstraction then possibly no rigid path (head could be a 
   137    constant function) so again use nonrigid search.  Happens only if
   138    term is not in normal form. 
   139 
   140 Warning: finds a rigid occurrence of ?f in ?f(t).
   141   Should NOT be called in this case: there is a flex-flex unifier
   142 *)
   143 fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 
   144   let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 
   145 		       else NoOcc
   146       fun occurs [] = NoOcc
   147 	| occurs (t::ts) =
   148             (case occur t of
   149                Rigid => Rigid
   150              | oc =>  (case occurs ts of NoOcc => oc  |  oc2 => oc2))
   151       and occomb (f$t) =
   152             (case occur t of
   153                Rigid => Rigid
   154              | oc =>  (case occomb f of NoOcc => oc  |  oc2 => oc2))
   155         | occomb t = occur t
   156       and occur (Const _)  = NoOcc
   157 	| occur (Bound _)  = NoOcc
   158 	| occur (Free _)  = NoOcc
   159 	| occur (Var (w, T))  = 
   160 	    if mem_ix (w, !seen) then NoOcc
   161 	    else if eq_ix(v,w) then Rigid
   162 	    else (seen := w:: !seen;  
   163 	          case Envir.lookup (env, (w, T)) of
   164 		      NONE    => NoOcc
   165 		    | SOME t => occur t)
   166 	| occur (Abs(_,_,body)) = occur body
   167 	| occur (t as f$_) =  (*switch to nonrigid search?*)
   168 	   (case head_of_in (env,f) of
   169 	      Var (w,_) => (*w is not assigned*)
   170 		if eq_ix(v,w) then Rigid  
   171 		else  nonrigid t
   172 	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
   173 	    | _ => occomb t)
   174   in  occur t  end;
   175 
   176 
   177 exception CANTUNIFY;	(*Signals non-unifiability.  Does not signal errors!*)
   178 exception ASSIGN;	(*Raised if not an assignment*)
   179 
   180 
   181 fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   182   if T=U then env
   183   else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (!sgr)) (iTs, maxidx) (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() = tracing ("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 vT as (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 ((vT, 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 (env,[],[]) dpairs;
   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 (vT as (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', vT) of
   404 	      NONE => (Envir.update ((vT, 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 vT as (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 ((vT, 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 (List.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, T), 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 tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   564   in  tracing msg;  List.app 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 (env',[]) flexflex, 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 tracing"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 vT as (v,T) = var_head_of (env,t)
   620       and wU as (w,U) = var_head_of (env,u);
   621       val (env', var) = Envir.genvar (#1v) (env, body_type env T)
   622       val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env')
   623   in  if vT = wU then env''  (*the other update would be identical*)
   624       else Envir.vupdate ((vT, 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 env tpairs;
   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;