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