src/Pure/unify.ML
author lcp
Wed Oct 19 09:48:13 1994 +0100 (1994-10-19)
changeset 646 7928c9760667
parent 0 a5a9c433f639
child 651 4b0455fbcc49
permissions -rw-r--r--
new comments explaining abandoned change
     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,fastype env (rbinder,u),env)
   483 	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
   484 end;
   485 
   486 
   487 (*Flex argument: a term, its type, and the index that refers to it.*)
   488 type flarg = {t: term,  T: typ,  j: int};
   489 
   490 
   491 (*Form the arguments into records for deletion/sorting.*)
   492 fun flexargs ([],[],[]) = [] : flarg list
   493   | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
   494   | flexargs _ = error"flexargs";
   495 
   496 
   497 (*If an argument contains a banned Bound, then it should be deleted.
   498   But if the path is flexible, this is difficult; the code gives up!*)
   499 exception CHANGE and CHANGE_FAIL;   (*rigid and flexible occurrences*)
   500 
   501 
   502 (*Squash down indices at level >=lev to delete the js from a term.
   503   flex should initially be false, since the empty path is rigid.*)
   504 fun change_bnos (lev, js, flex) t = 
   505   let val (head,args) = strip_comb t 
   506       val flex' = flex orelse is_Var head
   507       val head' = case head of
   508 	    Bound i => 
   509 		if i<lev then Bound i
   510 		else  if (i-lev) mem js  
   511                       then  if flex then raise CHANGE_FAIL
   512                                     else raise CHANGE
   513 		else  Bound (i - length (filter (fn j => j < i-lev) js))
   514 	  | Abs (a,T,t) => Abs (a, T, change_bnos(lev+1, js, flex) t)
   515 	  | _ => head
   516   in  list_comb (head', map (change_bnos (lev, js, flex')) args)
   517   end;
   518 
   519 
   520 (*Change indices, delete the argument if it contains a banned Bound*)
   521 fun change_arg js ({j,t,T}, args) : flarg list =
   522     {j=j, t= change_bnos(0,js,false)t, T=T} :: args    handle CHANGE => args;
   523 
   524 
   525 (*Sort the arguments to create assignments if possible:
   526   create eta-terms like ?g(B.1,B.0) *)
   527 fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
   528   | arg_less (_:flarg, _:flarg) = false;
   529 
   530 (*Test whether the new term would be eta-equivalent to a variable --
   531   if so then there is no point in creating a new variable*)
   532 fun decreasing n ([]: flarg list) = (n=0)
   533   | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
   534 
   535 (*Delete banned indices in the term, simplifying it.
   536   Force an assignment, if possible, by sorting the arguments.
   537   Update its head; squash indices in arguments. *)
   538 fun clean_term banned (env,t) =
   539     let val (Var(v,T), ts) = strip_comb t
   540 	val (Ts,U) = strip_type env T
   541 	and js = length ts - 1  downto 0
   542 	val args = sort arg_less
   543 		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
   544 	val ts' = map (#t) args
   545     in
   546     if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   547     else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
   548 	     val body = list_comb(v', map (Bound o #j) args)
   549 	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
   550 	     (*the vupdate affects ts' if they contain v*)
   551 	 in  
   552 	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
   553          end
   554     end;
   555 
   556 
   557 (*Add tpair if not trivial or already there.
   558   Should check for swapped pairs??*)
   559 fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
   560   if t0 aconv u0 then tpairs  
   561   else
   562   let val t = rlist_abs(rbinder, t0)  and  u = rlist_abs(rbinder, u0);
   563       fun same(t',u') = (t aconv t') andalso (u aconv u')
   564   in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
   565 
   566 
   567 (*Simplify both terms and check for assignments.
   568   Bound vars in the binder are "banned" unless used in both t AND u *)
   569 fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 
   570   let val loot = loose_bnos t  and  loou = loose_bnos u
   571       fun add_index (((a,T), j), (bnos, newbinder)) = 
   572             if  j mem loot  andalso  j mem loou 
   573             then  (bnos, (a,T)::newbinder)
   574             else  (j::bnos, newbinder);
   575       val indices = 0 upto (length rbinder - 1);
   576       val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
   577       val (env', t') = clean_term banned (env, t);
   578       val (env'',u') = clean_term banned (env',u)
   579   in  (ff_assign(env'', rbin', t', u'), tpairs)
   580       handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
   581       handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
   582   end
   583   handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
   584 
   585 
   586 (*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   587   eliminates trivial tpairs like t=t, as well as repeated ones
   588   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t 
   589   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
   590 fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 
   591       : Envir.env * (term*term)list =
   592   let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   593   in  case  (head_of t, head_of u) of
   594       (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
   595 	if v=w then		(*...occur check would falsely return true!*)
   596 	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   597 	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
   598 	else if xless(v,w) then (*prefer to update the LARGER variable*)
   599 	     clean_ffpair ((rbinder, u, t), (env,tpairs))
   600         else clean_ffpair ((rbinder, t, u), (env,tpairs))
   601     | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
   602   end;
   603 
   604 
   605 (*Print a tracing message + list of dpairs.
   606   In t==u print u first because it may be rigid or flexible --
   607     t is always flexible.*)
   608 fun print_dpairs msg (env,dpairs) =
   609   let fun pdp (rbinder,t,u) =
   610         let fun termT t = Sign.pretty_term (!sgr)
   611                               (Envir.norm_term env (rlist_abs(rbinder,t)))
   612             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
   613                           termT t];
   614         in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   615   in  writeln msg;  seq pdp dpairs  end;
   616 
   617 
   618 (*Unify the dpairs in the environment.
   619   Returns flex-flex disagreement pairs NOT IN normal form. 
   620   SIMPL may raise exception CANTUNIFY. *)
   621 fun hounifiers (sg,env, tus : (term*term)list) 
   622   : (Envir.env * (term*term)list)Sequence.seq =
   623   let fun add_unify tdepth ((env,dpairs), reseq) =
   624 	  Sequence.seqof (fn()=>
   625 	  let val (env',flexflex,flexrigid) = 
   626 	       (if tdepth> !trace_bound andalso !trace_simp
   627 		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   628 		SIMPL (env,dpairs))
   629 	  in case flexrigid of
   630 	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
   631 	    | dp::frigid' => 
   632 		if tdepth > !search_bound then
   633 		    (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
   634 		else
   635 		(if tdepth > !trace_bound then
   636 		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
   637 		 else ();
   638 		 Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
   639 			   (MATCH (env',dp, frigid'@flexflex), reseq)))
   640 	  end
   641 	  handle CANTUNIFY => 
   642 	    (if tdepth > !trace_bound then writeln"Failure node" else ();
   643 	     Sequence.pull reseq));
   644      val dps = map (fn(t,u)=> ([],t,u)) tus
   645   in sgr := sg;
   646      add_unify 1 ((env,dps), Sequence.null) 
   647   end;
   648 
   649 fun unifiers(params) =
   650       Sequence.cons((Pattern.unify(params), []),   Sequence.null)
   651       handle Pattern.Unif => Sequence.null
   652            | Pattern.Pattern => hounifiers(params);
   653 
   654 
   655 (*For smash_flexflex1*)
   656 fun var_head_of (env,t) : indexname * typ =
   657   case head_of (strip_abs_body (Envir.norm_term env t)) of
   658       Var(v,T) => (v,T)
   659     | _ => raise CANTUNIFY;  (*not flexible, cannot use trivial substitution*)
   660 
   661 
   662 (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   663   Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   664   Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, 
   665 	though just ?g->?f is a more general unifier.
   666   Unlike Huet (1975), does not smash together all variables of same type --
   667     requires more work yet gives a less general unifier (fewer variables).
   668   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   669 fun smash_flexflex1 ((t,u), env) : Envir.env =
   670   let val (v,T) = var_head_of (env,t)
   671       and (w,U) = var_head_of (env,u);
   672       val (env', var) = Envir.genvar (#1v) (env, body_type env T)
   673       val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
   674   in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
   675       else Envir.vupdate((v, type_abs(env',T,var)), env'')
   676   end;
   677 
   678 
   679 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   680 fun smash_flexflex (env,tpairs) : Envir.env =
   681   foldr smash_flexflex1 (tpairs, env);
   682 
   683 (*Returns unifiers with no remaining disagreement pairs*)
   684 fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
   685     Sequence.maps smash_flexflex (unifiers(sg,env,tus));
   686 
   687 end;