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