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