src/Pure/unify.ML
author bulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 38950 62578950e748
parent 37720 50a9e2fa4f6b
child 39116 f14735a88886
permissions -rw-r--r--
storing options for prolog code generation in the theory
     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_value: Config.value Config.T
    15   val trace_bound: int Config.T
    16   val search_bound_value: Config.value Config.T
    17   val search_bound: int Config.T
    18   val trace_simp_value: Config.value Config.T
    19   val trace_simp: bool Config.T
    20   val trace_types_value: Config.value Config.T
    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_value = Config.declare true "unify_trace_bound" (K (Config.Int 50));
    36 val trace_bound = Config.int trace_bound_value;
    37 
    38 (*unification quits above this depth*)
    39 val search_bound_value = Config.declare true "unify_search_bound" (K (Config.Int 60));
    40 val search_bound = Config.int search_bound_value;
    41 
    42 (*print dpairs before calling SIMPL*)
    43 val trace_simp_value = Config.declare true "unify_trace_simp" (K (Config.Bool false));
    44 val trace_simp = Config.bool trace_simp_value;
    45 
    46 (*announce potential incompleteness of type unification*)
    47 val trace_types_value = Config.declare true "unify_trace_types" (K (Config.Bool false));
    48 val trace_types = Config.bool trace_types_value;
    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) = List.foldr (SIMPL0 thy) (env, [], []) dpairs;
   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, like list_abs*)
   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 fun arg_less ({t = Bound i1, ...}, {t = Bound i2, ...}) = (i2 < i1)
   507   | arg_less (_: flarg, _: flarg) = false;
   508 
   509 (*Test whether the new term would be eta-equivalent to a variable --
   510   if so then there is no point in creating a new variable*)
   511 fun decreasing n ([]: flarg list) = (n = 0)
   512   | decreasing n ({j, ...} :: args) = j = n - 1 andalso decreasing (n - 1) args;
   513 
   514 (*Delete banned indices in the term, simplifying it.
   515   Force an assignment, if possible, by sorting the arguments.
   516   Update its head; squash indices in arguments. *)
   517 fun clean_term banned (env,t) =
   518   let
   519     val (Var (v, T), ts) = strip_comb t;
   520     val (Ts, U) = strip_type env T
   521     and js = length ts - 1  downto 0;
   522     val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts))) 
   523     val ts' = map #t args;
   524   in
   525     if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts')))
   526     else
   527       let
   528         val (env', v') = Envir.genvar (#1 v) (env, map #T args ---> U);
   529         val body = list_comb (v', map (Bound o #j) args);
   530         val env2 = Envir.vupdate ((((v, T), types_abs (Ts, body)), env'));
   531         (*the vupdate affects ts' if they contain v*)
   532       in (env2, Envir.norm_term env2 (list_comb (v', ts'))) end
   533   end;
   534 
   535 
   536 (*Add tpair if not trivial or already there.
   537   Should check for swapped pairs??*)
   538 fun add_tpair (rbinder, (t0, u0), tpairs) : (term * term) list =
   539   if t0 aconv u0 then tpairs
   540   else
   541     let
   542       val t = Logic.rlist_abs (rbinder, t0)
   543       and u = Logic.rlist_abs (rbinder, u0);
   544       fun same (t', u') = (t aconv t') andalso (u aconv u')
   545     in if exists same tpairs then tpairs else (t, u) :: tpairs end;
   546 
   547 
   548 (*Simplify both terms and check for assignments.
   549   Bound vars in the binder are "banned" unless used in both t AND u *)
   550 fun clean_ffpair thy ((rbinder, t, u), (env, tpairs)) =
   551   let
   552     val loot = loose_bnos t and loou = loose_bnos u
   553     fun add_index (j, (a, T)) (bnos, newbinder) =
   554       if member (op =) loot j andalso member (op =) loou j
   555       then (bnos, (a, T) :: newbinder)  (*needed by both: keep*)
   556       else (j :: bnos, newbinder);   (*remove*)
   557     val (banned, rbin') = fold_rev add_index ((0 upto (length rbinder - 1)) ~~ rbinder) ([], []);
   558     val (env', t') = clean_term banned (env, t);
   559     val (env'',u') = clean_term banned (env',u);
   560   in
   561     (ff_assign thy (env'', rbin', t', u'), tpairs)
   562       handle ASSIGN =>
   563         (ff_assign thy (env'', rbin', u', t'), tpairs)
   564           handle ASSIGN => (env'', add_tpair (rbin', (t', u'), tpairs))
   565   end
   566   handle CHANGE_FAIL => (env, add_tpair (rbinder, (t, u), tpairs));
   567 
   568 
   569 (*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   570   eliminates trivial tpairs like t=t, as well as repeated ones
   571   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t
   572   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
   573 fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) : Envir.env * (term * term) list =
   574   let
   575     val t = Envir.norm_term env t0
   576     and u = Envir.norm_term env u0;
   577   in
   578     (case (head_of t, head_of u) of
   579       (Var (v, T), Var (w, U)) =>  (*Check for identical variables...*)
   580         if Term.eq_ix (v, w) then     (*...occur check would falsely return true!*)
   581           if T = U then (env, add_tpair (rbinder, (t, u), tpairs))
   582           else raise TERM ("add_ffpair: Var name confusion", [t, u])
   583         else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
   584           clean_ffpair thy ((rbinder, u, t), (env, tpairs))
   585         else clean_ffpair thy ((rbinder, t, u), (env, tpairs))
   586     | _ => raise TERM ("add_ffpair: Vars expected", [t, u]))
   587   end;
   588 
   589 
   590 (*Print a tracing message + list of dpairs.
   591   In t==u print u first because it may be rigid or flexible --
   592     t is always flexible.*)
   593 fun print_dpairs thy msg (env, dpairs) =
   594   let
   595     fun pdp (rbinder, t, u) =
   596       let
   597         fun termT t =
   598           Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
   599         val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, termT t];
   600       in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
   601   in tracing msg; List.app pdp dpairs end;
   602 
   603 
   604 (*Unify the dpairs in the environment.
   605   Returns flex-flex disagreement pairs NOT IN normal form.
   606   SIMPL may raise exception CANTUNIFY. *)
   607 fun hounifiers (thy, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq =
   608   let
   609     val trace_bnd = Config.get_global thy trace_bound;
   610     val search_bnd = Config.get_global thy search_bound;
   611     val trace_smp = Config.get_global thy trace_simp;
   612     fun add_unify tdepth ((env, dpairs), reseq) =
   613       Seq.make (fn () =>
   614         let
   615           val (env', flexflex, flexrigid) =
   616            (if tdepth > trace_bnd andalso trace_smp
   617             then print_dpairs thy "Enter SIMPL" (env, dpairs) else ();
   618             SIMPL thy (env, dpairs));
   619         in
   620           (case flexrigid of
   621             [] => SOME (List.foldr (add_ffpair thy) (env', []) flexflex, reseq)
   622           | dp :: frigid' =>
   623               if tdepth > search_bnd then
   624                 (warning "Unification bound exceeded"; Seq.pull reseq)
   625               else
   626                (if tdepth > trace_bnd then
   627                   print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
   628                 else ();
   629                 Seq.pull (Seq.it_right
   630                     (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
   631         end
   632         handle CANTUNIFY =>
   633          (if tdepth > trace_bnd then tracing"Failure node" else ();
   634           Seq.pull reseq));
   635     val dps = map (fn (t, u) => ([], t, u)) tus;
   636   in add_unify 1 ((env, dps), Seq.empty) end;
   637 
   638 fun unifiers (params as (thy, env, tus)) =
   639   Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
   640     handle Pattern.Unif => Seq.empty
   641       | Pattern.Pattern => hounifiers params;
   642 
   643 
   644 (*For smash_flexflex1*)
   645 fun var_head_of (env,t) : indexname * typ =
   646   (case head_of (strip_abs_body (Envir.norm_term env t)) of
   647     Var (v, T) => (v, T)
   648   | _ => raise CANTUNIFY);  (*not flexible, cannot use trivial substitution*)
   649 
   650 
   651 (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   652   Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   653   Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a,
   654   though just ?g->?f is a more general unifier.
   655   Unlike Huet (1975), does not smash together all variables of same type --
   656     requires more work yet gives a less general unifier (fewer variables).
   657   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   658 fun smash_flexflex1 ((t, u), env) : Envir.env =
   659   let
   660     val vT as (v, T) = var_head_of (env, t)
   661     and wU as (w, U) = var_head_of (env, u);
   662     val (env', var) = Envir.genvar (#1 v) (env, body_type env T);
   663     val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env');
   664   in
   665     if vT = wU then env''  (*the other update would be identical*)
   666     else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
   667   end;
   668 
   669 
   670 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   671 fun smash_flexflex (env, tpairs) : Envir.env =
   672   List.foldr smash_flexflex1 env tpairs;
   673 
   674 (*Returns unifiers with no remaining disagreement pairs*)
   675 fun smash_unifiers thy tus env =
   676   Seq.map smash_flexflex (unifiers (thy, env, tus));
   677 
   678 
   679 (*Pattern matching*)
   680 fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
   681   let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
   682   in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
   683   handle Pattern.MATCH => Seq.empty;
   684 
   685 (*General matching -- keeps variables disjoint*)
   686 fun matchers _ [] = Seq.single (Envir.empty ~1)
   687   | matchers thy pairs =
   688       let
   689         val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
   690         val offset = maxidx + 1;
   691         val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
   692         val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
   693 
   694         val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
   695         val pat_vars = fold (Term.add_vars o #1) pairs' [];
   696 
   697         val decr_indexesT =
   698           Term.map_atyps (fn T as TVar ((x, i), S) =>
   699             if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
   700         val decr_indexes =
   701           Term.map_types decr_indexesT #>
   702           Term.map_aterms (fn t as Var ((x, i), T) =>
   703             if i > maxidx then Var ((x, i - offset), T) else t | t => t);
   704 
   705         fun norm_tvar env ((x, i), S) =
   706           ((x, i - offset),
   707             (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
   708         fun norm_var env ((x, i), T) =
   709           let
   710             val tyenv = Envir.type_env env;
   711             val T' = Envir.norm_type tyenv T;
   712             val t' = Envir.norm_term env (Var ((x, i), T'));
   713           in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
   714 
   715         fun result env =
   716           if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
   717             SOME (Envir.Envir {maxidx = maxidx,
   718               tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
   719               tenv = Vartab.make (map (norm_var env) pat_vars)})
   720           else NONE;
   721 
   722         val empty = Envir.empty maxidx';
   723       in
   724         Seq.append
   725           (Seq.map_filter result (smash_unifiers thy pairs' empty))
   726           (first_order_matchers thy pairs empty)
   727       end;
   728 
   729 fun matches_list thy ps os =
   730   length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os)));
   731 
   732 end;