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