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