1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/unify.ML Thu Sep 16 12:20:38 1993 +0200
1.3 @@ -0,0 +1,680 @@
1.4 +(* Title: unify
1.5 + ID: $Id$
1.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 + Copyright Cambridge University 1992
1.8 +
1.9 +Higher-Order Unification
1.10 +
1.11 +Potential problem: type of Vars is often ignored, so two Vars with same
1.12 +indexname but different types can cause errors!
1.13 +*)
1.14 +
1.15 +
1.16 +signature UNIFY =
1.17 +sig
1.18 + structure Sign: SIGN
1.19 + structure Envir : ENVIR
1.20 + structure Sequence : SEQUENCE
1.21 + (*references for control and tracing*)
1.22 + val trace_bound: int ref
1.23 + val trace_simp: bool ref
1.24 + val trace_types: bool ref
1.25 + val search_bound: int ref
1.26 + (*other exports*)
1.27 + val combound : (term*int*int) -> term
1.28 + val rlist_abs: (string*typ)list * term -> term
1.29 + val smash_unifiers : Sign.sg * Envir.env * (term*term)list
1.30 + -> (Envir.env Sequence.seq)
1.31 + val unifiers: Sign.sg * Envir.env * ((term*term)list)
1.32 + -> (Envir.env * (term * term)list) Sequence.seq
1.33 +end;
1.34 +
1.35 +functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE
1.36 + and Pattern:PATTERN
1.37 + sharing type Sign.sg = Pattern.sg
1.38 + and type Envir.env = Pattern.env)
1.39 + : UNIFY =
1.40 +struct
1.41 +
1.42 +structure Sign = Sign;
1.43 +structure Envir = Envir;
1.44 +structure Sequence = Sequence;
1.45 +structure Pretty = Sign.Syntax.Pretty;
1.46 +
1.47 +(*Unification options*)
1.48 +
1.49 +val trace_bound = ref 10 (*tracing starts above this depth, 0 for full*)
1.50 +and search_bound = ref 20 (*unification quits above this depth*)
1.51 +and trace_simp = ref false (*print dpairs before calling SIMPL*)
1.52 +and trace_types = ref false (*announce potential incompleteness
1.53 + of type unification*)
1.54 +
1.55 +val sgr = ref(Sign.pure);
1.56 +
1.57 +type binderlist = (string*typ) list;
1.58 +
1.59 +type dpair = binderlist * term * term;
1.60 +
1.61 +fun body_type(Envir.Envir{iTs,...}) =
1.62 +let fun bT(Type("fun",[_,T])) = bT T
1.63 + | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
1.64 + None => T | Some(T') => bT T')
1.65 + | bT T = T
1.66 +in bT end;
1.67 +
1.68 +fun binder_types(Envir.Envir{iTs,...}) =
1.69 +let fun bTs(Type("fun",[T,U])) = T :: bTs U
1.70 + | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
1.71 + None => [] | Some(T') => bTs T')
1.72 + | bTs _ = []
1.73 +in bTs end;
1.74 +
1.75 +fun strip_type env T = (binder_types env T, body_type env T);
1.76 +
1.77 +
1.78 +(*Put a term into head normal form for unification.
1.79 + Operands need not be in normal form. Does eta-expansions on the head,
1.80 + which involves renumbering (thus copying) the args. To avoid this
1.81 + inefficiency, avoid partial application: if an atom is applied to
1.82 + any arguments at all, apply it to its full number of arguments.
1.83 + For
1.84 + rbinder = [(x1,T),...,(xm,Tm)] (user's var names preserved!)
1.85 + args = [arg1,...,argn]
1.86 + the value of
1.87 + (xm,...,x1)(head(arg1,...,argn)) remains invariant.
1.88 +*)
1.89 +
1.90 +local exception SAME
1.91 +in
1.92 + fun head_norm (env,t) : term =
1.93 + let fun hnorm (Var (v,T)) =
1.94 + (case Envir.lookup (env,v) of
1.95 + Some u => head_norm (env, u)
1.96 + | None => raise SAME)
1.97 + | hnorm (Abs(a,T,body)) = Abs(a, T, hnorm body)
1.98 + | hnorm (Abs(_,_,body) $ t) =
1.99 + head_norm (env, subst_bounds([t], body))
1.100 + | hnorm (f $ t) =
1.101 + (case hnorm f of
1.102 + Abs(_,_,body) =>
1.103 + head_norm (env, subst_bounds([t], body))
1.104 + | nf => nf $ t)
1.105 + | hnorm _ = raise SAME
1.106 + in hnorm t handle SAME=> t end
1.107 +end;
1.108 +
1.109 +
1.110 +(*finds type of term without checking that combinations are consistent
1.111 + rbinder holds types of bound variables*)
1.112 +fun fastype (Envir.Envir{iTs,...}) =
1.113 +let val funerr = "fastype: expected function type";
1.114 + fun fast(rbinder, f$u) =
1.115 + (case (fast (rbinder, f)) of
1.116 + Type("fun",[_,T]) => T
1.117 + | TVar(ixn,_) =>
1.118 + (case assoc(iTs,ixn) of
1.119 + Some(Type("fun",[_,T])) => T
1.120 + | _ => raise TERM(funerr, [f$u]))
1.121 + | _ => raise TERM(funerr, [f$u]))
1.122 + | fast (rbinder, Const (_,T)) = T
1.123 + | fast (rbinder, Free (_,T)) = T
1.124 + | fast (rbinder, Bound i) =
1.125 + (#2 (nth_elem (i,rbinder))
1.126 + handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
1.127 + | fast (rbinder, Var (_,T)) = T
1.128 + | fast (rbinder, Abs (_,T,u)) = T --> fast (("",T) :: rbinder, u)
1.129 +in fast end;
1.130 +
1.131 +
1.132 +(*Eta normal form*)
1.133 +fun eta_norm(env as Envir.Envir{iTs,...}) =
1.134 + let fun etif (Type("fun",[T,U]), t) =
1.135 + Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
1.136 + | etif (TVar(ixn,_),t) =
1.137 + (case assoc(iTs,ixn) of
1.138 + None => t | Some(T) => etif(T,t))
1.139 + | etif (_,t) = t;
1.140 + fun eta_nm (rbinder, Abs(a,T,body)) =
1.141 + Abs(a, T, eta_nm ((a,T)::rbinder, body))
1.142 + | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
1.143 + in eta_nm end;
1.144 +
1.145 +
1.146 +(*OCCURS CHECK
1.147 + Does the uvar occur in the term t?
1.148 + two forms of search, for whether there is a rigid path to the current term.
1.149 + "seen" is list of variables passed thru, is a memo variable for sharing.
1.150 + This version searches for nonrigid occurrence, returns true if found. *)
1.151 +fun occurs_terms (seen: (indexname list) ref,
1.152 + env: Envir.env, v: indexname, ts: term list): bool =
1.153 + let fun occurs [] = false
1.154 + | occurs (t::ts) = occur t orelse occurs ts
1.155 + and occur (Const _) = false
1.156 + | occur (Bound _) = false
1.157 + | occur (Free _) = false
1.158 + | occur (Var (w,_)) =
1.159 + if w mem !seen then false
1.160 + else if v=w then true
1.161 + (*no need to lookup: v has no assignment*)
1.162 + else (seen := w:: !seen;
1.163 + case Envir.lookup(env,w) of
1.164 + None => false
1.165 + | Some t => occur t)
1.166 + | occur (Abs(_,_,body)) = occur body
1.167 + | occur (f$t) = occur t orelse occur f
1.168 + in occurs ts end;
1.169 +
1.170 +
1.171 +
1.172 +(* f(a1,...,an) ----> (f, [a1,...,an]) using the assignments*)
1.173 +fun head_of_in (env,t) : term = case t of
1.174 + f$_ => head_of_in(env,f)
1.175 + | Var (v,_) => (case Envir.lookup(env,v) of
1.176 + Some u => head_of_in(env,u) | None => t)
1.177 + | _ => t;
1.178 +
1.179 +
1.180 +datatype occ = NoOcc | Nonrigid | Rigid;
1.181 +
1.182 +(* Rigid occur check
1.183 +Returns Rigid if it finds a rigid occurrence of the variable,
1.184 + Nonrigid if it finds a nonrigid path to the variable.
1.185 + NoOcc otherwise.
1.186 + Continues searching for a rigid occurrence even if it finds a nonrigid one.
1.187 +
1.188 +Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ]
1.189 + a rigid path to the variable, appearing with no arguments.
1.190 +Here completeness is sacrificed in order to reduce danger of divergence:
1.191 + reject ALL rigid paths to the variable.
1.192 +Could check for rigid paths to bound variables that are out of scope.
1.193 +Not necessary because the assignment test looks at variable's ENTIRE rbinder.
1.194 +
1.195 +Treatment of head(arg1,...,argn):
1.196 +If head is a variable then no rigid path, switch to nonrigid search
1.197 +for arg1,...,argn.
1.198 +If head is an abstraction then possibly no rigid path (head could be a
1.199 + constant function) so again use nonrigid search. Happens only if
1.200 + term is not in normal form.
1.201 +
1.202 +Warning: finds a rigid occurrence of ?f in ?f(t).
1.203 + Should NOT be called in this case: there is a flex-flex unifier
1.204 +*)
1.205 +fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
1.206 + let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
1.207 + else NoOcc
1.208 + fun occurs [] = NoOcc
1.209 + | occurs (t::ts) =
1.210 + (case occur t of
1.211 + Rigid => Rigid
1.212 + | oc => (case occurs ts of NoOcc => oc | oc2 => oc2))
1.213 + and occomb (f$t) =
1.214 + (case occur t of
1.215 + Rigid => Rigid
1.216 + | oc => (case occomb f of NoOcc => oc | oc2 => oc2))
1.217 + | occomb t = occur t
1.218 + and occur (Const _) = NoOcc
1.219 + | occur (Bound _) = NoOcc
1.220 + | occur (Free _) = NoOcc
1.221 + | occur (Var (w,_)) =
1.222 + if w mem !seen then NoOcc
1.223 + else if v=w then Rigid
1.224 + else (seen := w:: !seen;
1.225 + case Envir.lookup(env,w) of
1.226 + None => NoOcc
1.227 + | Some t => occur t)
1.228 + | occur (Abs(_,_,body)) = occur body
1.229 + | occur (t as f$_) = (*switch to nonrigid search?*)
1.230 + (case head_of_in (env,f) of
1.231 + Var (w,_) => (*w is not assigned*)
1.232 + if v=w then Rigid
1.233 + else nonrigid t
1.234 + | Abs(_,_,body) => nonrigid t (*not in normal form*)
1.235 + | _ => occomb t)
1.236 + in occur t end;
1.237 +
1.238 +
1.239 +exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*)
1.240 +exception ASSIGN; (*Raised if not an assignment*)
1.241 +
1.242 +
1.243 +fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
1.244 + if T=U then env else
1.245 + let val iTs' = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr))) ((U,T),iTs)
1.246 + in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'}
1.247 + end handle Sign.Type.TUNIFY => raise CANTUNIFY;
1.248 +
1.249 +fun test_unify_types(args as (T,U,_)) =
1.250 +let val sot = Sign.string_of_typ (!sgr);
1.251 + fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T);
1.252 + val env' = unify_types(args)
1.253 +in if is_TVar(T) orelse is_TVar(U) then warn() else ();
1.254 + env'
1.255 +end;
1.256 +
1.257 +(*Is the term eta-convertible to a single variable with the given rbinder?
1.258 + Examples: ?a ?f(B.0) ?g(B.1,B.0)
1.259 + Result is var a for use in SIMPL. *)
1.260 +fun get_eta_var ([], _, Var vT) = vT
1.261 + | get_eta_var (_::rbinder, n, f $ Bound i) =
1.262 + if n=i then get_eta_var (rbinder, n+1, f)
1.263 + else raise ASSIGN
1.264 + | get_eta_var _ = raise ASSIGN;
1.265 +
1.266 +
1.267 +(* ([xn,...,x1], t) ======> (x1,...,xn)t *)
1.268 +fun rlist_abs ([], body) = body
1.269 + | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
1.270 +
1.271 +
1.272 +(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
1.273 + If v occurs rigidly then nonunifiable.
1.274 + If v occurs nonrigidly then must use full algorithm. *)
1.275 +fun assignment (env, rbinder, t, u) =
1.276 + let val (v,T) = get_eta_var(rbinder,0,t)
1.277 + in case rigid_occurs_term (ref[], env, v, u) of
1.278 + NoOcc => let val env = unify_types(body_type env T,
1.279 + fastype env (rbinder,u),env)
1.280 + in Envir.update ((v, rlist_abs(rbinder,u)), env) end
1.281 + | Nonrigid => raise ASSIGN
1.282 + | Rigid => raise CANTUNIFY
1.283 + end;
1.284 +
1.285 +
1.286 +(*Extends an rbinder with a new disagreement pair, if both are abstractions.
1.287 + Tries to unify types of the bound variables!
1.288 + Checks that binders have same length, since terms should be eta-normal;
1.289 + if not, raises TERM, probably indicating type mismatch.
1.290 + Uses variable a (unless the null string) to preserve user's naming.*)
1.291 +fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
1.292 + let val env' = unify_types(T,U,env)
1.293 + val c = if a="" then b else a
1.294 + in new_dpair((c,T) :: rbinder, body1, body2, env') end
1.295 + | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
1.296 + | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
1.297 + | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
1.298 +
1.299 +
1.300 +fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
1.301 + new_dpair (rbinder,
1.302 + eta_norm env (rbinder, head_norm(env,t)),
1.303 + eta_norm env (rbinder, head_norm(env,u)), env);
1.304 +
1.305 +
1.306 +
1.307 +(*flexflex: the flex-flex pairs, flexrigid: the flex-rigid pairs
1.308 + Does not perform assignments for flex-flex pairs:
1.309 + may create nonrigid paths, which prevent other assignments*)
1.310 +fun SIMPL0 (dp0, (env,flexflex,flexrigid))
1.311 + : Envir.env * dpair list * dpair list =
1.312 + let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
1.313 + fun SIMRANDS(f$t, g$u, env) =
1.314 + SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
1.315 + | SIMRANDS (t as _$_, _, _) =
1.316 + raise TERM ("SIMPL: operands mismatch", [t,u])
1.317 + | SIMRANDS (t, u as _$_, _) =
1.318 + raise TERM ("SIMPL: operands mismatch", [t,u])
1.319 + | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
1.320 + in case (head_of t, head_of u) of
1.321 + (Var(_,T), Var(_,U)) =>
1.322 + let val T' = body_type env T and U' = body_type env U;
1.323 + val env = unify_types(T',U',env)
1.324 + in (env, dp::flexflex, flexrigid) end
1.325 + | (Var _, _) =>
1.326 + ((assignment (env,rbinder,t,u), flexflex, flexrigid)
1.327 + handle ASSIGN => (env, flexflex, dp::flexrigid))
1.328 + | (_, Var _) =>
1.329 + ((assignment (env,rbinder,u,t), flexflex, flexrigid)
1.330 + handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
1.331 + | (Const(a,T), Const(b,U)) =>
1.332 + if a=b then SIMRANDS(t,u, unify_types(T,U,env))
1.333 + else raise CANTUNIFY
1.334 + | (Bound i, Bound j) =>
1.335 + if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY
1.336 + | (Free(a,T), Free(b,U)) =>
1.337 + if a=b then SIMRANDS(t,u, unify_types(T,U,env))
1.338 + else raise CANTUNIFY
1.339 + | _ => raise CANTUNIFY
1.340 + end;
1.341 +
1.342 +
1.343 +(* changed(env,t) checks whether the head of t is a variable assigned in env*)
1.344 +fun changed (env, f$_) = changed (env,f)
1.345 + | changed (env, Var (v,_)) =
1.346 + (case Envir.lookup(env,v) of None=>false | _ => true)
1.347 + | changed _ = false;
1.348 +
1.349 +
1.350 +(*Recursion needed if any of the 'head variables' have been updated
1.351 + Clever would be to re-do just the affected dpairs*)
1.352 +fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
1.353 + let val all as (env',flexflex,flexrigid) =
1.354 + foldr SIMPL0 (dpairs, (env,[],[]));
1.355 + val dps = flexrigid@flexflex
1.356 + in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
1.357 + then SIMPL(env',dps) else all
1.358 + end;
1.359 +
1.360 +
1.361 +(*computes t(Bound(n+k-1),...,Bound(n)) *)
1.362 +fun combound (t, n, k) =
1.363 + if k>0 then combound (t,n+1,k-1) $ (Bound n) else t;
1.364 +
1.365 +
1.366 +(*Makes the terms E1,...,Em, where Ts = [T...Tm].
1.367 + Each Ei is ?Gi(B.(n-1),...,B.0), and has type Ti
1.368 + The B.j are bound vars of binder.
1.369 + The terms are not made in eta-normal-form, SIMPL does that later.
1.370 + If done here, eta-expansion must be recursive in the arguments! *)
1.371 +fun make_args name (binder: typ list, env, []) = (env, []) (*frequent case*)
1.372 + | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
1.373 + let fun funtype T = binder--->T;
1.374 + val (env', vars) = Envir.genvars name (env, map funtype Ts)
1.375 + in (env', map (fn var=> combound(var, 0, length binder)) vars) end;
1.376 +
1.377 +
1.378 +(*Abstraction over a list of types, like list_abs*)
1.379 +fun types_abs ([],u) = u
1.380 + | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
1.381 +
1.382 +(*Abstraction over the binder of a type*)
1.383 +fun type_abs (env,T,t) = types_abs(binder_types env T, t);
1.384 +
1.385 +
1.386 +(*MATCH taking "big steps".
1.387 + Copies u into the Var v, using projection on targs or imitation.
1.388 + A projection is allowed unless SIMPL raises an exception.
1.389 + Allocates new variables in projection on a higher-order argument,
1.390 + or if u is a variable (flex-flex dpair).
1.391 + Returns long sequence of every way of copying u, for backtracking
1.392 + For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
1.393 + The order for trying projections is crucial in ?b'(?a)
1.394 + NB "vname" is only used in the call to make_args!! *)
1.395 +fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
1.396 + : (term * (Envir.env * dpair list))Sequence.seq =
1.397 +let (*Produce copies of uarg and cons them in front of uargs*)
1.398 + fun copycons uarg (uargs, (env, dpairs)) =
1.399 + Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed'))
1.400 + (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
1.401 + (env, dpairs)));
1.402 + (*Produce sequence of all possible ways of copying the arg list*)
1.403 + fun copyargs [] = Sequence.cons( ([],ed), Sequence.null)
1.404 + | copyargs (uarg::uargs) =
1.405 + Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs));
1.406 + val (uhead,uargs) = strip_comb u;
1.407 + val base = body_type env (fastype env (rbinder,uhead));
1.408 + fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
1.409 + (*attempt projection on argument with given typ*)
1.410 + val Ts = map (curry (fastype env) rbinder) targs;
1.411 + fun projenv (head, (Us,bary), targ, tail) =
1.412 + let val env = if !trace_types then test_unify_types(base,bary,env)
1.413 + else unify_types(base,bary,env)
1.414 + in Sequence.seqof (fn () =>
1.415 + let val (env',args) = make_args vname (Ts,env,Us);
1.416 + (*higher-order projection: plug in targs for bound vars*)
1.417 + fun plugin arg = list_comb(head_of arg, targs);
1.418 + val dp = (rbinder, list_comb(targ, map plugin args), u);
1.419 + val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
1.420 + (*may raise exception CANTUNIFY*)
1.421 + in Some ((list_comb(head,args), (env2, frigid@fflex)),
1.422 + tail)
1.423 + end handle CANTUNIFY => Sequence.pull tail)
1.424 + end handle CANTUNIFY => tail;
1.425 + (*make a list of projections*)
1.426 + fun make_projs (T::Ts, targ::targs) =
1.427 + (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
1.428 + | make_projs ([],[]) = []
1.429 + | make_projs _ = raise TERM ("make_projs", u::targs);
1.430 + (*try projections and imitation*)
1.431 + fun matchfun ((bvar,T,targ)::projs) =
1.432 + (projenv(bvar, strip_type env T, targ, matchfun projs))
1.433 + | matchfun [] = (*imitation last of all*)
1.434 + (case uhead of
1.435 + Const _ => Sequence.maps joinargs (copyargs uargs)
1.436 + | Free _ => Sequence.maps joinargs (copyargs uargs)
1.437 + | _ => Sequence.null) (*if Var, would be a loop!*)
1.438 +in case uhead of
1.439 + Abs(a, T, body) =>
1.440 + Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed'))
1.441 + (mc ((a,T)::rbinder,
1.442 + (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
1.443 + | Var (w,uary) =>
1.444 + (*a flex-flex dpair: make variable for t*)
1.445 + let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
1.446 + val tabs = combound(newhd, 0, length Ts)
1.447 + val tsub = list_comb(newhd,targs)
1.448 + in Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs))
1.449 + end
1.450 + | _ => matchfun(rev(make_projs(Ts, targs)))
1.451 +end
1.452 +in mc end;
1.453 +
1.454 +
1.455 +(*Call matchcopy to produce assignments to the variable in the dpair*)
1.456 +fun MATCH (env, (rbinder,t,u), dpairs)
1.457 + : (Envir.env * dpair list)Sequence.seq =
1.458 + let val (Var(v,T), targs) = strip_comb t;
1.459 + val Ts = binder_types env T;
1.460 + fun new_dset (u', (env',dpairs')) =
1.461 + (*if v was updated to s, must unify s with u' *)
1.462 + case Envir.lookup(env',v) of
1.463 + None => (Envir.update ((v, types_abs(Ts, u')), env'), dpairs')
1.464 + | Some s => (env', ([], s, types_abs(Ts, u'))::dpairs')
1.465 + in Sequence.maps new_dset
1.466 + (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
1.467 + end;
1.468 +
1.469 +
1.470 +
1.471 +(**** Flex-flex processing ****)
1.472 +
1.473 +(*At end of unification, do flex-flex assignments like ?a -> ?f(?b)
1.474 + Attempts to update t with u, raising ASSIGN if impossible*)
1.475 +fun ff_assign(env, rbinder, t, u) : Envir.env =
1.476 +let val (v,T) = get_eta_var(rbinder,0,t)
1.477 +in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
1.478 + else let val env = unify_types(body_type env T,fastype env (rbinder,u),env)
1.479 + in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
1.480 +end;
1.481 +
1.482 +
1.483 +(*Flex argument: a term, its type, and the index that refers to it.*)
1.484 +type flarg = {t: term, T: typ, j: int};
1.485 +
1.486 +
1.487 +(*Form the arguments into records for deletion/sorting.*)
1.488 +fun flexargs ([],[],[]) = [] : flarg list
1.489 + | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
1.490 + | flexargs _ = error"flexargs";
1.491 +
1.492 +
1.493 +(*If an argument contains a banned Bound, then it should be deleted.
1.494 + But if the path is flexible, this is difficult; the code gives up!*)
1.495 +exception CHANGE and CHANGE_FAIL; (*rigid and flexible occurrences*)
1.496 +
1.497 +
1.498 +(*Squash down indices at level >=lev to delete the js from a term.
1.499 + flex should initially be false, since the empty path is rigid.*)
1.500 +fun change_bnos (lev, js, flex) t =
1.501 + let val (head,args) = strip_comb t
1.502 + val flex' = flex orelse is_Var head
1.503 + val head' = case head of
1.504 + Bound i =>
1.505 + if i<lev then Bound i
1.506 + else if (i-lev) mem js
1.507 + then if flex then raise CHANGE_FAIL
1.508 + else raise CHANGE
1.509 + else Bound (i - length (filter (fn j => j < i-lev) js))
1.510 + | Abs (a,T,t) => Abs (a, T, change_bnos(lev+1, js, flex) t)
1.511 + | _ => head
1.512 + in list_comb (head', map (change_bnos (lev, js, flex')) args)
1.513 + end;
1.514 +
1.515 +
1.516 +(*Change indices, delete the argument if it contains a banned Bound*)
1.517 +fun change_arg js ({j,t,T}, args) : flarg list =
1.518 + {j=j, t= change_bnos(0,js,false)t, T=T} :: args handle CHANGE => args;
1.519 +
1.520 +
1.521 +(*Sort the arguments to create assignments if possible:
1.522 + create eta-terms like ?g(B.1,B.0) *)
1.523 +fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
1.524 + | arg_less (_:flarg, _:flarg) = false;
1.525 +
1.526 +(*Test whether the new term would be eta-equivalent to a variable --
1.527 + if so then there is no point in creating a new variable*)
1.528 +fun decreasing n ([]: flarg list) = (n=0)
1.529 + | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
1.530 +
1.531 +(*Delete banned indices in the term, simplifying it.
1.532 + Force an assignment, if possible, by sorting the arguments.
1.533 + Update its head; squash indices in arguments. *)
1.534 +fun clean_term banned (env,t) =
1.535 + let val (Var(v,T), ts) = strip_comb t
1.536 + val (Ts,U) = strip_type env T
1.537 + and js = length ts - 1 downto 0
1.538 + val args = sort arg_less
1.539 + (foldr (change_arg banned) (flexargs (js,ts,Ts), []))
1.540 + val ts' = map (#t) args
1.541 + in
1.542 + if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
1.543 + else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
1.544 + val body = list_comb(v', map (Bound o #j) args)
1.545 + val env2 = Envir.vupdate (((v, types_abs(Ts, body)), env'))
1.546 + (*the vupdate affects ts' if they contain v*)
1.547 + in
1.548 + (env2, Envir.norm_term env2 (list_comb(v',ts')))
1.549 + end
1.550 + end;
1.551 +
1.552 +
1.553 +(*Add tpair if not trivial or already there.
1.554 + Should check for swapped pairs??*)
1.555 +fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
1.556 + if t0 aconv u0 then tpairs
1.557 + else
1.558 + let val t = rlist_abs(rbinder, t0) and u = rlist_abs(rbinder, u0);
1.559 + fun same(t',u') = (t aconv t') andalso (u aconv u')
1.560 + in if exists same tpairs then tpairs else (t,u)::tpairs end;
1.561 +
1.562 +
1.563 +(*Simplify both terms and check for assignments.
1.564 + Bound vars in the binder are "banned" unless used in both t AND u *)
1.565 +fun clean_ffpair ((rbinder, t, u), (env,tpairs)) =
1.566 + let val loot = loose_bnos t and loou = loose_bnos u
1.567 + fun add_index (((a,T), j), (bnos, newbinder)) =
1.568 + if j mem loot andalso j mem loou
1.569 + then (bnos, (a,T)::newbinder)
1.570 + else (j::bnos, newbinder);
1.571 + val indices = 0 upto (length rbinder - 1);
1.572 + val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
1.573 + val (env', t') = clean_term banned (env, t);
1.574 + val (env'',u') = clean_term banned (env',u)
1.575 + in (ff_assign(env'', rbin', t', u'), tpairs)
1.576 + handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
1.577 + handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
1.578 + end
1.579 + handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
1.580 +
1.581 +
1.582 +(*IF the flex-flex dpair is an assignment THEN do it ELSE put in tpairs
1.583 + eliminates trivial tpairs like t=t, as well as repeated ones
1.584 + trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t
1.585 + Resulting tpairs MAY NOT be in normal form: assignments may occur here.*)
1.586 +fun add_ffpair ((rbinder,t0,u0), (env,tpairs))
1.587 + : Envir.env * (term*term)list =
1.588 + let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0
1.589 + in case (head_of t, head_of u) of
1.590 + (Var(v,T), Var(w,U)) => (*Check for identical variables...*)
1.591 + if v=w then (*...occur check would falsely return true!*)
1.592 + if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
1.593 + else raise TERM ("add_ffpair: Var name confusion", [t,u])
1.594 + else if xless(v,w) then (*prefer to update the LARGER variable*)
1.595 + clean_ffpair ((rbinder, u, t), (env,tpairs))
1.596 + else clean_ffpair ((rbinder, t, u), (env,tpairs))
1.597 + | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
1.598 + end;
1.599 +
1.600 +
1.601 +(*Print a tracing message + list of dpairs.
1.602 + In t==u print u first because it may be rigid or flexible --
1.603 + t is always flexible.*)
1.604 +fun print_dpairs msg (env,dpairs) =
1.605 + let fun pdp (rbinder,t,u) =
1.606 + let fun termT t = Sign.pretty_term (!sgr)
1.607 + (Envir.norm_term env (rlist_abs(rbinder,t)))
1.608 + val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
1.609 + termT t];
1.610 + in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
1.611 + in writeln msg; seq pdp dpairs end;
1.612 +
1.613 +
1.614 +(*Unify the dpairs in the environment.
1.615 + Returns flex-flex disagreement pairs NOT IN normal form.
1.616 + SIMPL may raise exception CANTUNIFY. *)
1.617 +fun hounifiers (sg,env, tus : (term*term)list)
1.618 + : (Envir.env * (term*term)list)Sequence.seq =
1.619 + let fun add_unify tdepth ((env,dpairs), reseq) =
1.620 + Sequence.seqof (fn()=>
1.621 + let val (env',flexflex,flexrigid) =
1.622 + (if tdepth> !trace_bound andalso !trace_simp
1.623 + then print_dpairs "Enter SIMPL" (env,dpairs) else ();
1.624 + SIMPL (env,dpairs))
1.625 + in case flexrigid of
1.626 + [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
1.627 + | dp::frigid' =>
1.628 + if tdepth > !search_bound then
1.629 + (prs"***Unification bound exceeded\n"; Sequence.pull reseq)
1.630 + else
1.631 + (if tdepth > !trace_bound then
1.632 + print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
1.633 + else ();
1.634 + Sequence.pull (Sequence.its_right (add_unify (tdepth+1))
1.635 + (MATCH (env',dp, frigid'@flexflex), reseq)))
1.636 + end
1.637 + handle CANTUNIFY =>
1.638 + (if tdepth > !trace_bound then writeln"Failure node" else ();
1.639 + Sequence.pull reseq));
1.640 + val dps = map (fn(t,u)=> ([],t,u)) tus
1.641 + in sgr := sg;
1.642 + add_unify 1 ((env,dps), Sequence.null)
1.643 + end;
1.644 +
1.645 +fun unifiers(params) =
1.646 + Sequence.cons((Pattern.unify(params), []), Sequence.null)
1.647 + handle Pattern.Unif => Sequence.null
1.648 + | Pattern.Pattern => hounifiers(params);
1.649 +
1.650 +
1.651 +(*For smash_flexflex1*)
1.652 +fun var_head_of (env,t) : indexname * typ =
1.653 + case head_of (strip_abs_body (Envir.norm_term env t)) of
1.654 + Var(v,T) => (v,T)
1.655 + | _ => raise CANTUNIFY; (*not flexible, cannot use trivial substitution*)
1.656 +
1.657 +
1.658 +(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
1.659 + Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
1.660 + Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a,
1.661 + though just ?g->?f is a more general unifier.
1.662 + Unlike Huet (1975), does not smash together all variables of same type --
1.663 + requires more work yet gives a less general unifier (fewer variables).
1.664 + Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
1.665 +fun smash_flexflex1 ((t,u), env) : Envir.env =
1.666 + let val (v,T) = var_head_of (env,t)
1.667 + and (w,U) = var_head_of (env,u);
1.668 + val (env', var) = Envir.genvar (#1v) (env, body_type env T)
1.669 + val env'' = Envir.vupdate((w, type_abs(env',U,var)), env')
1.670 + in if (v,T)=(w,U) then env'' (*the other update would be identical*)
1.671 + else Envir.vupdate((v, type_abs(env',T,var)), env'')
1.672 + end;
1.673 +
1.674 +
1.675 +(*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*)
1.676 +fun smash_flexflex (env,tpairs) : Envir.env =
1.677 + foldr smash_flexflex1 (tpairs, env);
1.678 +
1.679 +(*Returns unifiers with no remaining disagreement pairs*)
1.680 +fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq =
1.681 + Sequence.maps smash_flexflex (unifiers(sg,env,tus));
1.682 +
1.683 +end;