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