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