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