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