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