src/Pure/unify.ML
author wenzelm
Tue Jun 29 21:46:47 2010 +0200 (2010-06-29)
changeset 37635 484efa650907
parent 36787 f60e4dd6d76f
child 37636 ab50854da897
permissions -rw-r--r--
recovered some indentation from the depths of time;
     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 (T as 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 (_, _, body) => 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 name (binder: typ list, 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, uary) =>
   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 (*Flex argument: a term, its type, and the index that refers to it.*)
   455 type flarg = {t: term, T: typ, j: int};
   456 
   457 (*Form the arguments into records for deletion/sorting.*)
   458 fun flexargs ([], [], []) = [] : flarg list
   459   | flexargs (j :: js, t :: ts, T :: Ts) = {j = j, t = t, T = T} :: flexargs (js, ts, Ts)
   460   | flexargs _ = error "flexargs";
   461 
   462 
   463 (*If an argument contains a banned Bound, then it should be deleted.
   464   But if the only path is flexible, this is difficult; the code gives up!
   465   In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
   466 exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
   467 
   468 
   469 (*Check whether the 'banned' bound var indices occur rigidly in t*)
   470 fun rigid_bound (lev, banned) t =
   471   let val (head,args) = strip_comb t in
   472     (case head of
   473       Bound i =>
   474         member (op =) banned (i - lev) orelse exists (rigid_bound (lev, banned)) args
   475     | Var _ => false  (*no rigid occurrences here!*)
   476     | Abs (_, _, u) =>
   477         rigid_bound (lev + 1, banned) u orelse
   478         exists (rigid_bound (lev, banned)) args
   479     | _ => exists (rigid_bound (lev, banned)) args)
   480   end;
   481 
   482 (*Squash down indices at level >=lev to delete the banned from a term.*)
   483 fun change_bnos banned =
   484   let
   485     fun change lev (Bound i) =
   486           if i < lev then Bound i
   487           else if member (op =) banned (i - lev) then
   488             raise CHANGE_FAIL (**flexible occurrence: give up**)
   489           else Bound (i - length (filter (fn j => j < i - lev) banned))
   490       | change lev (Abs (a, T, t)) = Abs (a, T, change(lev + 1) t)
   491       | change lev (t $ u) = change lev t $ change lev u
   492       | change lev t = t;
   493   in change 0 end;
   494 
   495 (*Change indices, delete the argument if it contains a banned Bound*)
   496 fun change_arg banned ({j, t, T}, args) : flarg list =
   497   if rigid_bound (0, banned) t then args  (*delete argument!*)
   498   else {j = j, t = change_bnos banned t, T = T} :: args;
   499 
   500 
   501 (*Sort the arguments to create assignments if possible:
   502   create eta-terms like ?g(B.1,B.0) *)
   503 fun arg_less ({t = Bound i1, ...}, {t = Bound i2, ...}) = (i2 < i1)
   504   | arg_less (_: flarg, _: flarg) = false;
   505 
   506 (*Test whether the new term would be eta-equivalent to a variable --
   507   if so then there is no point in creating a new variable*)
   508 fun decreasing n ([]: flarg list) = (n = 0)
   509   | decreasing n ({j, ...} :: args) = j = n - 1 andalso decreasing (n - 1) args;
   510 
   511 (*Delete banned indices in the term, simplifying it.
   512   Force an assignment, if possible, by sorting the arguments.
   513   Update its head; squash indices in arguments. *)
   514 fun clean_term banned (env,t) =
   515   let
   516     val (Var (v, T), ts) = strip_comb t;
   517     val (Ts, U) = strip_type env T
   518     and js = length ts - 1  downto 0;
   519     val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts)))
   520     val ts' = map #t args;
   521   in
   522     if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts')))
   523     else
   524       let
   525         val (env', v') = Envir.genvar (#1 v) (env, map #T args ---> U);
   526         val body = list_comb (v', map (Bound o #j) args);
   527         val env2 = Envir.vupdate ((((v, T), types_abs (Ts, body)), env'));
   528         (*the vupdate affects ts' if they contain v*)
   529       in (env2, Envir.norm_term env2 (list_comb (v', ts'))) end
   530   end;
   531 
   532 
   533 (*Add tpair if not trivial or already there.
   534   Should check for swapped pairs??*)
   535 fun add_tpair (rbinder, (t0, u0), tpairs) : (term * term) list =
   536   if t0 aconv u0 then tpairs
   537   else
   538     let
   539       val t = Logic.rlist_abs (rbinder, t0)
   540       and u = Logic.rlist_abs (rbinder, u0);
   541       fun same (t', u') = (t aconv t') andalso (u aconv u')
   542     in if exists same tpairs then tpairs else (t, u) :: tpairs end;
   543 
   544 
   545 (*Simplify both terms and check for assignments.
   546   Bound vars in the binder are "banned" unless used in both t AND u *)
   547 fun clean_ffpair thy ((rbinder, t, u), (env, tpairs)) =
   548   let
   549     val loot = loose_bnos t and loou = loose_bnos u
   550     fun add_index (j, (a, T)) (bnos, newbinder) =
   551       if member (op =) loot j andalso member (op =) loou j
   552       then (bnos, (a, T) :: newbinder)  (*needed by both: keep*)
   553       else (j :: bnos, newbinder);   (*remove*)
   554     val (banned, rbin') = fold_rev add_index ((0 upto (length rbinder - 1)) ~~ rbinder) ([], []);
   555     val (env', t') = clean_term banned (env, t);
   556     val (env'',u') = clean_term banned (env',u);
   557   in
   558     (ff_assign thy (env'', rbin', t', u'), tpairs)
   559       handle ASSIGN =>
   560         (ff_assign thy (env'', rbin', u', t'), tpairs)
   561           handle ASSIGN => (env'', add_tpair (rbin', (t', u'), tpairs))
   562   end
   563   handle CHANGE_FAIL => (env, add_tpair (rbinder, (t, u), tpairs));
   564 
   565 
   566 (*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   567   eliminates trivial tpairs like t=t, as well as repeated ones
   568   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t
   569   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
   570 fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) : Envir.env * (term * term) list =
   571   let
   572     val t = Envir.norm_term env t0
   573     and u = Envir.norm_term env u0;
   574   in
   575     (case (head_of t, head_of u) of
   576       (Var (v, T), Var (w, U)) =>  (*Check for identical variables...*)
   577         if Term.eq_ix (v, w) then     (*...occur check would falsely return true!*)
   578           if T = U then (env, add_tpair (rbinder, (t, u), tpairs))
   579           else raise TERM ("add_ffpair: Var name confusion", [t, u])
   580         else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
   581           clean_ffpair thy ((rbinder, u, t), (env, tpairs))
   582         else clean_ffpair thy ((rbinder, t, u), (env, tpairs))
   583     | _ => raise TERM ("add_ffpair: Vars expected", [t, u]))
   584   end;
   585 
   586 
   587 (*Print a tracing message + list of dpairs.
   588   In t==u print u first because it may be rigid or flexible --
   589     t is always flexible.*)
   590 fun print_dpairs thy msg (env, dpairs) =
   591   let
   592     fun pdp (rbinder, t, u) =
   593       let
   594         fun termT t =
   595           Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
   596         val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, termT t];
   597       in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
   598   in tracing msg; List.app pdp dpairs end;
   599 
   600 
   601 (*Unify the dpairs in the environment.
   602   Returns flex-flex disagreement pairs NOT IN normal form.
   603   SIMPL may raise exception CANTUNIFY. *)
   604 fun hounifiers (thy, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq =
   605   let
   606     val trace_bnd = Config.get_global thy trace_bound;
   607     val search_bnd = Config.get_global thy search_bound;
   608     val trace_smp = Config.get_global thy trace_simp;
   609     fun add_unify tdepth ((env, dpairs), reseq) =
   610       Seq.make (fn () =>
   611         let
   612           val (env', flexflex, flexrigid) =
   613            (if tdepth > trace_bnd andalso trace_smp
   614             then print_dpairs thy "Enter SIMPL" (env, dpairs) else ();
   615             SIMPL thy (env, dpairs));
   616         in
   617           (case flexrigid of
   618             [] => SOME (List.foldr (add_ffpair thy) (env', []) flexflex, reseq)
   619           | dp :: frigid' =>
   620               if tdepth > search_bnd then
   621                 (warning "Unification bound exceeded"; Seq.pull reseq)
   622               else
   623                (if tdepth > trace_bnd then
   624                   print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
   625                 else ();
   626                 Seq.pull (Seq.it_right
   627                     (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
   628         end
   629         handle CANTUNIFY =>
   630          (if tdepth > trace_bnd then tracing"Failure node" else ();
   631           Seq.pull reseq));
   632     val dps = map (fn (t, u) => ([], t, u)) tus;
   633   in add_unify 1 ((env, dps), Seq.empty) end;
   634 
   635 fun unifiers (params as (thy, env, tus)) =
   636   Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
   637     handle Pattern.Unif => Seq.empty
   638       | Pattern.Pattern => hounifiers params;
   639 
   640 
   641 (*For smash_flexflex1*)
   642 fun var_head_of (env,t) : indexname * typ =
   643   (case head_of (strip_abs_body (Envir.norm_term env t)) of
   644     Var (v, T) => (v, T)
   645   | _ => raise CANTUNIFY);  (*not flexible, cannot use trivial substitution*)
   646 
   647 
   648 (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
   649   Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
   650   Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a,
   651   though just ?g->?f is a more general unifier.
   652   Unlike Huet (1975), does not smash together all variables of same type --
   653     requires more work yet gives a less general unifier (fewer variables).
   654   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
   655 fun smash_flexflex1 ((t,u), env) : Envir.env =
   656   let
   657     val vT as (v, T) = var_head_of (env, t)
   658     and wU as (w, U) = var_head_of (env, u);
   659     val (env', var) = Envir.genvar (#1 v) (env, body_type env T);
   660     val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env');
   661   in
   662     if vT = wU then env''  (*the other update would be identical*)
   663     else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
   664   end;
   665 
   666 
   667 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   668 fun smash_flexflex (env,tpairs) : Envir.env =
   669   List.foldr smash_flexflex1 env tpairs;
   670 
   671 (*Returns unifiers with no remaining disagreement pairs*)
   672 fun smash_unifiers thy tus env =
   673   Seq.map smash_flexflex (unifiers (thy, env, tus));
   674 
   675 
   676 (*Pattern matching*)
   677 fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
   678   let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
   679   in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
   680   handle Pattern.MATCH => Seq.empty;
   681 
   682 (*General matching -- keeps variables disjoint*)
   683 fun matchers _ [] = Seq.single (Envir.empty ~1)
   684   | matchers thy pairs =
   685       let
   686         val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
   687         val offset = maxidx + 1;
   688         val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
   689         val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
   690 
   691         val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
   692         val pat_vars = fold (Term.add_vars o #1) pairs' [];
   693 
   694         val decr_indexesT =
   695           Term.map_atyps (fn T as TVar ((x, i), S) =>
   696             if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
   697         val decr_indexes =
   698           Term.map_types decr_indexesT #>
   699           Term.map_aterms (fn t as Var ((x, i), T) =>
   700             if i > maxidx then Var ((x, i - offset), T) else t | t => t);
   701 
   702         fun norm_tvar env ((x, i), S) =
   703           ((x, i - offset),
   704             (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
   705         fun norm_var env ((x, i), T) =
   706           let
   707             val tyenv = Envir.type_env env;
   708             val T' = Envir.norm_type tyenv T;
   709             val t' = Envir.norm_term env (Var ((x, i), T'));
   710           in ((x, i - offset), (decr_indexesT T', decr_indexes t')) 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 (norm_tvar env) pat_tvars),
   716               tenv = Vartab.make (map (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;