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