src/Pure/unify.ML
author clasohm
Mon Jan 29 13:56:41 1996 +0100 (1996-01-29)
changeset 1458 fd510875fb71
parent 1435 aefcd255ed4a
child 1460 5a6f2aabd538
permissions -rw-r--r--
removed tabs
     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.proto_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
   246   else let val (iTs',maxidx') = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr)))
   247                                                 maxidx iTs (U,T)
   248        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
   249        handle Sign.Type.TUNIFY => raise CANTUNIFY;
   250 
   251 fun test_unify_types(args as (T,U,_)) =
   252 let val sot = Sign.string_of_typ (!sgr);
   253     fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
   254     val env' = unify_types(args)
   255 in if is_TVar(T) orelse is_TVar(U) then warn() else ();
   256    env'
   257 end;
   258 
   259 (*Is the term eta-convertible to a single variable with the given rbinder?
   260   Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
   261   Result is var a for use in SIMPL. *)
   262 fun get_eta_var ([], _, Var vT)  =  vT
   263   | get_eta_var (_::rbinder, n, f $ Bound i) =
   264         if  n=i  then  get_eta_var (rbinder, n+1, f) 
   265                  else  raise ASSIGN
   266   | get_eta_var _ = raise ASSIGN;
   267 
   268 
   269 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   270 fun rlist_abs ([], body) = body
   271   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   272 
   273 
   274 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
   275   If v occurs rigidly then nonunifiable.
   276   If v occurs nonrigidly then must use full algorithm. *)
   277 fun assignment (env, rbinder, t, u) =
   278     let val (v,T) = get_eta_var(rbinder,0,t)
   279     in  case rigid_occurs_term (ref[], env, v, u) of
   280               NoOcc => let val env = unify_types(body_type env T,
   281                                                  fastype env (rbinder,u),env)
   282                 in Envir.update ((v, rlist_abs(rbinder,u)), env) end
   283             | Nonrigid =>  raise ASSIGN
   284             | Rigid =>  raise CANTUNIFY
   285     end;
   286 
   287 
   288 (*Extends an rbinder with a new disagreement pair, if both are abstractions.
   289   Tries to unify types of the bound variables!
   290   Checks that binders have same length, since terms should be eta-normal;
   291     if not, raises TERM, probably indicating type mismatch.
   292   Uses variable a (unless the null string) to preserve user's naming.*) 
   293 fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
   294         let val env' = unify_types(T,U,env)
   295             val c = if a="" then b else a
   296         in new_dpair((c,T) :: rbinder, body1, body2, env') end
   297     | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
   298     | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
   299     | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
   300 
   301 
   302 fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
   303      new_dpair (rbinder,
   304                 eta_norm env (rbinder, head_norm(env,t)),
   305                 eta_norm env (rbinder, head_norm(env,u)), env);
   306 
   307 
   308 
   309 (*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
   310   Does not perform assignments for flex-flex pairs:
   311     may create nonrigid paths, which prevent other assignments.
   312   Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
   313     do so caused numerous problems with no compensating advantage.
   314 *)
   315 fun SIMPL0 (dp0, (env,flexflex,flexrigid))
   316         : Envir.env * dpair list * dpair list =
   317     let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
   318             fun SIMRANDS(f$t, g$u, env) =
   319                         SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
   320               | SIMRANDS (t as _$_, _, _) =
   321                 raise TERM ("SIMPL: operands mismatch", [t,u])
   322               | SIMRANDS (t, u as _$_, _) =
   323                 raise TERM ("SIMPL: operands mismatch", [t,u])
   324               | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
   325     in case (head_of t, head_of u) of
   326        (Var(_,T), Var(_,U)) =>
   327             let val T' = body_type env T and U' = body_type env U;
   328                 val env = unify_types(T',U',env)
   329             in (env, dp::flexflex, flexrigid) end
   330      | (Var _, _) =>
   331             ((assignment (env,rbinder,t,u), flexflex, flexrigid)
   332              handle ASSIGN => (env, flexflex, dp::flexrigid))
   333      | (_, Var _) =>
   334             ((assignment (env,rbinder,u,t), flexflex, flexrigid)
   335              handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
   336      | (Const(a,T), Const(b,U)) =>
   337             if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   338             else raise CANTUNIFY
   339      | (Bound i,    Bound j)    =>
   340             if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
   341      | (Free(a,T),  Free(b,U))  =>
   342             if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   343             else raise CANTUNIFY
   344      | _ => raise CANTUNIFY
   345     end;
   346 
   347 
   348 (* changed(env,t) checks whether the head of t is a variable assigned in env*)
   349 fun changed (env, f$_) = changed (env,f)
   350   | changed (env, Var (v,_)) =
   351       (case Envir.lookup(env,v) of None=>false  |  _ => true)
   352   | changed _ = false;
   353 
   354 
   355 (*Recursion needed if any of the 'head variables' have been updated
   356   Clever would be to re-do just the affected dpairs*)
   357 fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
   358     let val all as (env',flexflex,flexrigid) =
   359             foldr SIMPL0 (dpairs, (env,[],[]));
   360         val dps = flexrigid@flexflex
   361     in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
   362        then SIMPL(env',dps) else all
   363     end;
   364 
   365 
   366 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   367 fun combound (t, n, k) = 
   368     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   369 
   370 
   371 (*Makes the terms E1,...,Em,    where Ts = [T...Tm]. 
   372   Each Ei is   ?Gi(B.(n-1),...,B.0), and has type Ti
   373   The B.j are bound vars of binder.
   374   The terms are not made in eta-normal-form, SIMPL does that later.  
   375   If done here, eta-expansion must be recursive in the arguments! *)
   376 fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
   377   | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
   378        let fun funtype T = binder--->T;
   379            val (env', vars) = Envir.genvars name (env, map funtype Ts)
   380        in  (env',  map (fn var=> combound(var, 0, length binder)) vars)  end;
   381 
   382 
   383 (*Abstraction over a list of types, like list_abs*)
   384 fun types_abs ([],u) = u
   385   | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
   386 
   387 (*Abstraction over the binder of a type*)
   388 fun type_abs (env,T,t) = types_abs(binder_types env T, t);
   389 
   390 
   391 (*MATCH taking "big steps".
   392   Copies u into the Var v, using projection on targs or imitation.
   393   A projection is allowed unless SIMPL raises an exception.
   394   Allocates new variables in projection on a higher-order argument,
   395     or if u is a variable (flex-flex dpair).
   396   Returns long sequence of every way of copying u, for backtracking
   397   For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
   398   The order for trying projections is crucial in ?b'(?a)   
   399   NB "vname" is only used in the call to make_args!!   *)
   400 fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
   401         : (term * (Envir.env * dpair list))Sequence.seq =
   402 let (*Produce copies of uarg and cons them in front of uargs*)
   403     fun copycons uarg (uargs, (env, dpairs)) =
   404         Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
   405             (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
   406                  (env, dpairs)));
   407         (*Produce sequence of all possible ways of copying the arg list*)
   408     fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
   409       | copyargs (uarg::uargs) =
   410             Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
   411     val (uhead,uargs) = strip_comb u;
   412     val base = body_type env (fastype env (rbinder,uhead));
   413     fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
   414     (*attempt projection on argument with given typ*)
   415     val Ts = map (curry (fastype env) rbinder) targs;
   416     fun projenv (head, (Us,bary), targ, tail) = 
   417         let val env = if !trace_types then test_unify_types(base,bary,env)
   418                       else unify_types(base,bary,env)
   419         in Sequence.seqof (fn () =>  
   420             let val (env',args) = make_args vname (Ts,env,Us);
   421                 (*higher-order projection: plug in targs for bound vars*)
   422                 fun plugin arg = list_comb(head_of arg, targs);
   423                 val dp = (rbinder, list_comb(targ, map plugin args), u);
   424                 val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
   425                     (*may raise exception CANTUNIFY*)
   426             in  Some ((list_comb(head,args), (env2, frigid@fflex)),
   427                         tail)
   428             end  handle CANTUNIFY => Sequence.pull tail)
   429         end handle CANTUNIFY => tail;
   430     (*make a list of projections*)
   431     fun make_projs (T::Ts, targ::targs) =
   432               (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
   433       | make_projs ([],[]) = []
   434       | make_projs _ = raise TERM ("make_projs", u::targs);
   435     (*try projections and imitation*)
   436     fun matchfun ((bvar,T,targ)::projs) =
   437                (projenv(bvar, strip_type env T, targ, matchfun projs))
   438       | matchfun [] = (*imitation last of all*)
   439               (case uhead of
   440                  Const _ => Sequence.maps joinargs (copyargs uargs)
   441                | Free _  => Sequence.maps joinargs (copyargs uargs)
   442                | _ => Sequence.null)  (*if Var, would be a loop!*)
   443 in case uhead of
   444         Abs(a, T, body) =>
   445             Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 
   446                 (mc ((a,T)::rbinder,
   447                         (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
   448       | Var (w,uary) => 
   449             (*a flex-flex dpair: make variable for t*)
   450             let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
   451                 val tabs = combound(newhd, 0, length Ts)
   452                 val tsub = list_comb(newhd,targs)
   453             in  Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
   454             end
   455       | _ =>  matchfun(rev(make_projs(Ts, targs)))
   456 end
   457 in mc end;
   458 
   459 
   460 (*Call matchcopy to produce assignments to the variable in the dpair*)
   461 fun MATCH (env, (rbinder,t,u), dpairs)
   462         : (Envir.env * dpair list)Sequence.seq = 
   463   let val (Var(v,T), targs) = strip_comb t;
   464       val Ts = binder_types env T;
   465       fun new_dset (u', (env',dpairs')) =
   466           (*if v was updated to s, must unify s with u' *)
   467           case Envir.lookup(env',v) of
   468               None => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
   469             | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   470   in Sequence.maps new_dset
   471          (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   472   end;
   473 
   474 
   475 
   476 (**** Flex-flex processing ****)
   477 
   478 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
   479   Attempts to update t with u, raising ASSIGN if impossible*)
   480 fun ff_assign(env, rbinder, t, u) : Envir.env = 
   481 let val (v,T) = get_eta_var(rbinder,0,t)
   482 in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
   483    else let val env = unify_types(body_type env T,
   484                                   fastype env (rbinder,u),
   485                                   env)
   486         in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
   487 end;
   488 
   489 
   490 (*Flex argument: a term, its type, and the index that refers to it.*)
   491 type flarg = {t: term,  T: typ,  j: int};
   492 
   493 
   494 (*Form the arguments into records for deletion/sorting.*)
   495 fun flexargs ([],[],[]) = [] : flarg list
   496   | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
   497   | flexargs _ = error"flexargs";
   498 
   499 
   500 (*If an argument contains a banned Bound, then it should be deleted.
   501   But if the only path is flexible, this is difficult; the code gives up!
   502   In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
   503 exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
   504 
   505 
   506 (*Check whether the 'banned' bound var indices occur rigidly in t*)
   507 fun rigid_bound (lev, banned) t = 
   508   let val (head,args) = strip_comb t 
   509   in  
   510       case head of
   511           Bound i => (i-lev) mem banned  orelse
   512                      exists (rigid_bound (lev, banned)) args
   513         | Var _ => false        (*no rigid occurrences here!*)
   514         | Abs (_,_,u) => 
   515                rigid_bound(lev+1, banned) u  orelse
   516                exists (rigid_bound (lev, banned)) args
   517         | _ => exists (rigid_bound (lev, banned)) args
   518   end;
   519 
   520 (*Squash down indices at level >=lev to delete the banned from a term.*)
   521 fun change_bnos banned =
   522   let fun change lev (Bound i) = 
   523             if i<lev then Bound i
   524             else  if (i-lev) mem banned  
   525                   then raise CHANGE_FAIL (**flexible occurrence: give up**)
   526             else  Bound (i - length (filter (fn j => j < i-lev) banned))
   527         | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
   528         | change lev (t$u) = change lev t $ change lev u
   529         | change lev t = t
   530   in  change 0  end;
   531 
   532 (*Change indices, delete the argument if it contains a banned Bound*)
   533 fun change_arg banned ({j,t,T}, args) : flarg list =
   534     if rigid_bound (0, banned) t  then  args    (*delete argument!*)
   535     else  {j=j, t= change_bnos banned t, T=T} :: args;
   536 
   537 
   538 (*Sort the arguments to create assignments if possible:
   539   create eta-terms like ?g(B.1,B.0) *)
   540 fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
   541   | arg_less (_:flarg, _:flarg) = false;
   542 
   543 (*Test whether the new term would be eta-equivalent to a variable --
   544   if so then there is no point in creating a new variable*)
   545 fun decreasing n ([]: flarg list) = (n=0)
   546   | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
   547 
   548 (*Delete banned indices in the term, simplifying it.
   549   Force an assignment, if possible, by sorting the arguments.
   550   Update its head; squash indices in arguments. *)
   551 fun clean_term banned (env,t) =
   552     let val (Var(v,T), ts) = strip_comb t
   553         val (Ts,U) = strip_type env T
   554         and js = length ts - 1  downto 0
   555         val args = sort arg_less
   556                 (foldr (change_arg banned) (flexargs (js,ts,Ts), []))
   557         val ts' = map (#t) args
   558     in
   559     if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   560     else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
   561              val body = list_comb(v', map (Bound o #j) args)
   562              val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
   563              (*the vupdate affects ts' if they contain v*)
   564          in  
   565              (env2, Envir.norm_term env2 (list_comb(v',ts')))
   566          end
   567     end;
   568 
   569 
   570 (*Add tpair if not trivial or already there.
   571   Should check for swapped pairs??*)
   572 fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
   573   if t0 aconv u0 then tpairs  
   574   else
   575   let val t = rlist_abs(rbinder, t0)  and  u = rlist_abs(rbinder, u0);
   576       fun same(t',u') = (t aconv t') andalso (u aconv u')
   577   in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
   578 
   579 
   580 (*Simplify both terms and check for assignments.
   581   Bound vars in the binder are "banned" unless used in both t AND u *)
   582 fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 
   583   let val loot = loose_bnos t  and  loou = loose_bnos u
   584       fun add_index (((a,T), j), (bnos, newbinder)) = 
   585             if  j mem loot  andalso  j mem loou 
   586             then  (bnos, (a,T)::newbinder)      (*needed by both: keep*)
   587             else  (j::bnos, newbinder);         (*remove*)
   588       val indices = 0 upto (length rbinder - 1);
   589       val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
   590       val (env', t') = clean_term banned (env, t);
   591       val (env'',u') = clean_term banned (env',u)
   592   in  (ff_assign(env'', rbin', t', u'), tpairs)
   593       handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
   594       handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
   595   end
   596   handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
   597 
   598 
   599 (*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   600   eliminates trivial tpairs like t=t, as well as repeated ones
   601   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t 
   602   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
   603 fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 
   604       : Envir.env * (term*term)list =
   605   let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   606   in  case  (head_of t, head_of u) of
   607       (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
   608         if v=w then             (*...occur check would falsely return true!*)
   609             if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   610             else raise TERM ("add_ffpair: Var name confusion", [t,u])
   611         else if xless(v,w) then (*prefer to update the LARGER variable*)
   612              clean_ffpair ((rbinder, u, t), (env,tpairs))
   613         else clean_ffpair ((rbinder, t, u), (env,tpairs))
   614     | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
   615   end;
   616 
   617 
   618 (*Print a tracing message + list of dpairs.
   619   In t==u print u first because it may be rigid or flexible --
   620     t is always flexible.*)
   621 fun print_dpairs msg (env,dpairs) =
   622   let fun pdp (rbinder,t,u) =
   623         let fun termT t = Sign.pretty_term (!sgr)
   624                               (Envir.norm_term env (rlist_abs(rbinder,t)))
   625             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
   626                           termT t];
   627         in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   628   in  writeln msg;  seq pdp dpairs  end;
   629 
   630 
   631 (*Unify the dpairs in the environment.
   632   Returns flex-flex disagreement pairs NOT IN normal form. 
   633   SIMPL may raise exception CANTUNIFY. *)
   634 fun hounifiers (sg,env, tus : (term*term)list) 
   635   : (Envir.env * (term*term)list)Sequence.seq =
   636   let fun add_unify tdepth ((env,dpairs), reseq) =
   637           Sequence.seqof (fn()=>
   638           let val (env',flexflex,flexrigid) = 
   639                (if tdepth> !trace_bound andalso !trace_simp
   640                 then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   641                 SIMPL (env,dpairs))
   642           in case flexrigid of
   643               [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
   644             | dp::frigid' => 
   645                 if tdepth > !search_bound then
   646                     (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
   647                 else
   648                 (if tdepth > !trace_bound then
   649                     print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
   650                  else ();
   651                  Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
   652                            (MATCH (env',dp, frigid'@flexflex), reseq)))
   653           end
   654           handle CANTUNIFY => 
   655             (if tdepth > !trace_bound then writeln"Failure node" else ();
   656              Sequence.pull reseq));
   657      val dps = map (fn(t,u)=> ([],t,u)) tus
   658   in sgr := sg;
   659      add_unify 1 ((env,dps), Sequence.null) 
   660   end;
   661 
   662 fun unifiers(params) =
   663       Sequence.cons((Pattern.unify(params), []),   Sequence.null)
   664       handle Pattern.Unif => Sequence.null
   665            | Pattern.Pattern => hounifiers(params);
   666 
   667 
   668 (*For smash_flexflex1*)
   669 fun var_head_of (env,t) : indexname * typ =
   670   case head_of (strip_abs_body (Envir.norm_term env t)) of
   671       Var(v,T) => (v,T)
   672     | _ => raise CANTUNIFY;  (*not flexible, cannot use trivial substitution*)
   673 
   674 
   675 (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   676   Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   677   Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, 
   678         though just ?g->?f is a more general unifier.
   679   Unlike Huet (1975), does not smash together all variables of same type --
   680     requires more work yet gives a less general unifier (fewer variables).
   681   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   682 fun smash_flexflex1 ((t,u), env) : Envir.env =
   683   let val (v,T) = var_head_of (env,t)
   684       and (w,U) = var_head_of (env,u);
   685       val (env', var) = Envir.genvar (#1v) (env, body_type env T)
   686       val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
   687   in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
   688       else Envir.vupdate((v, type_abs(env',T,var)), env'')
   689   end;
   690 
   691 
   692 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   693 fun smash_flexflex (env,tpairs) : Envir.env =
   694   foldr smash_flexflex1 (tpairs, env);
   695 
   696 (*Returns unifiers with no remaining disagreement pairs*)
   697 fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
   698     Sequence.maps smash_flexflex (unifiers(sg,env,tus));
   699 
   700 end;