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