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