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