src/Pure/unify.ML
author lcp
Fri Oct 21 09:53:38 1994 +0100 (1994-10-21)
changeset 651 4b0455fbcc49
parent 646 7928c9760667
child 922 196ca0973a6d
permissions -rw-r--r--
Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
to simplfy %x y.?a(x) =?= %x y.?b(f(?c(y), y)) because it found the flexible
path to y before the rigid path. New code simplifies this to
%x.?a(x) =?= %x.?d, eliminating ?a.

Pure/Unify/rigid_bound: preliminary check for rigid paths to the banned
bound variables

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