author  wenzelm 
Tue, 18 Dec 2001 02:17:20 +0100  
changeset 12527  d6c91bc3e49c 
parent 12262  11ff5f47df6e 
child 14643  130076a81b84 
permissions  rwrr 
1460  1 
(* Title: unify 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright Cambridge University 1992 
5 

6 
HigherOrder Unification 

7 

8 
Potential problem: type of Vars is often ignored, so two Vars with same 

9 
indexname but different types can cause errors! 

646  10 

11 
Types as well as terms are unified. The outermost functions assume the 

12 
terms to be unified already have the same type. In resolution, this is 

13 
assured because both have type "prop". 

0  14 
*) 
15 

16 

17 
signature UNIFY = 

1505  18 
sig 
0  19 
(*references for control and tracing*) 
20 
val trace_bound: int ref 

21 
val trace_simp: bool ref 

22 
val trace_types: bool ref 

23 
val search_bound: int ref 

24 
(*other exports*) 

25 
val combound : (term*int*int) > term 

26 
val rlist_abs: (string*typ)list * term > term 

27 
val smash_unifiers : Sign.sg * Envir.env * (term*term)list 

4270  28 
> (Envir.env Seq.seq) 
0  29 
val unifiers: Sign.sg * Envir.env * ((term*term)list) 
4270  30 
> (Envir.env * (term * term)list) Seq.seq 
1505  31 
end; 
0  32 

1505  33 
structure Unify : UNIFY = 
0  34 
struct 
35 

36 
(*Unification options*) 

37 

1460  38 
val trace_bound = ref 10 (*tracing starts above this depth, 0 for full*) 
39 
and search_bound = ref 20 (*unification quits above this depth*) 

40 
and trace_simp = ref false (*print dpairs before calling SIMPL*) 

41 
and trace_types = ref false (*announce potential incompleteness 

42 
of type unification*) 

0  43 

3991  44 
val sgr = ref(Sign.pre_pure); 
0  45 

46 
type binderlist = (string*typ) list; 

47 

48 
type dpair = binderlist * term * term; 

49 

50 
fun body_type(Envir.Envir{iTs,...}) = 

51 
let fun bT(Type("fun",[_,T])) = bT T 

8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
4438
diff
changeset

52 
 bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of 
1460  53 
None => T  Some(T') => bT T') 
0  54 
 bT T = T 
55 
in bT end; 

56 

57 
fun binder_types(Envir.Envir{iTs,...}) = 

58 
let fun bTs(Type("fun",[T,U])) = T :: bTs U 

8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
4438
diff
changeset

59 
 bTs(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of 
1460  60 
None => []  Some(T') => bTs T') 
0  61 
 bTs _ = [] 
62 
in bTs end; 

63 

64 
fun strip_type env T = (binder_types env T, body_type env T); 

65 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

66 
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; 
0  67 

68 

69 
(*Eta normal form*) 

70 
fun eta_norm(env as Envir.Envir{iTs,...}) = 

71 
let fun etif (Type("fun",[T,U]), t) = 

1460  72 
Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) 
73 
 etif (TVar(ixn,_),t) = 

8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
4438
diff
changeset

74 
(case Vartab.lookup (iTs,ixn) of 
1460  75 
None => t  Some(T) => etif(T,t)) 
76 
 etif (_,t) = t; 

0  77 
fun eta_nm (rbinder, Abs(a,T,body)) = 
1460  78 
Abs(a, T, eta_nm ((a,T)::rbinder, body)) 
79 
 eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t) 

0  80 
in eta_nm end; 
81 

82 

83 
(*OCCURS CHECK 

84 
Does the uvar occur in the term t? 

85 
two forms of search, for whether there is a rigid path to the current term. 

86 
"seen" is list of variables passed thru, is a memo variable for sharing. 

87 
This version searches for nonrigid occurrence, returns true if found. *) 

88 
fun occurs_terms (seen: (indexname list) ref, 

1460  89 
env: Envir.env, v: indexname, ts: term list): bool = 
0  90 
let fun occurs [] = false 
1460  91 
 occurs (t::ts) = occur t orelse occurs ts 
0  92 
and occur (Const _) = false 
1460  93 
 occur (Bound _) = false 
94 
 occur (Free _) = false 

95 
 occur (Var (w,_)) = 

2178  96 
if mem_ix (w, !seen) then false 
2753  97 
else if eq_ix(v,w) then true 
1460  98 
(*no need to lookup: v has no assignment*) 
99 
else (seen := w:: !seen; 

100 
case Envir.lookup(env,w) of 

101 
None => false 

102 
 Some t => occur t) 

103 
 occur (Abs(_,_,body)) = occur body 

104 
 occur (f$t) = occur t orelse occur f 

0  105 
in occurs ts end; 
106 

107 

108 

109 
(* f(a1,...,an) > (f, [a1,...,an]) using the assignments*) 

110 
fun head_of_in (env,t) : term = case t of 

111 
f$_ => head_of_in(env,f) 

112 
 Var (v,_) => (case Envir.lookup(env,v) of 

1460  113 
Some u => head_of_in(env,u)  None => t) 
0  114 
 _ => t; 
115 

116 

117 
datatype occ = NoOcc  Nonrigid  Rigid; 

118 

119 
(* Rigid occur check 

120 
Returns Rigid if it finds a rigid occurrence of the variable, 

121 
Nonrigid if it finds a nonrigid path to the variable. 

122 
NoOcc otherwise. 

123 
Continues searching for a rigid occurrence even if it finds a nonrigid one. 

124 

125 
Condition for detecting nonunifable terms: [ section 5.3 of Huet (1975) ] 

126 
a rigid path to the variable, appearing with no arguments. 

127 
Here completeness is sacrificed in order to reduce danger of divergence: 

128 
reject ALL rigid paths to the variable. 

129 
Could check for rigid paths to bound variables that are out of scope. 

130 
Not necessary because the assignment test looks at variable's ENTIRE rbinder. 

131 

132 
Treatment of head(arg1,...,argn): 

133 
If head is a variable then no rigid path, switch to nonrigid search 

134 
for arg1,...,argn. 

135 
If head is an abstraction then possibly no rigid path (head could be a 

136 
constant function) so again use nonrigid search. Happens only if 

137 
term is not in normal form. 

138 

139 
Warning: finds a rigid occurrence of ?f in ?f(t). 

140 
Should NOT be called in this case: there is a flexflex unifier 

141 
*) 

142 
fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) = 

143 
let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid 

1460  144 
else NoOcc 
0  145 
fun occurs [] = NoOcc 
1460  146 
 occurs (t::ts) = 
0  147 
(case occur t of 
148 
Rigid => Rigid 

149 
 oc => (case occurs ts of NoOcc => oc  oc2 => oc2)) 

150 
and occomb (f$t) = 

151 
(case occur t of 

152 
Rigid => Rigid 

153 
 oc => (case occomb f of NoOcc => oc  oc2 => oc2)) 

154 
 occomb t = occur t 

155 
and occur (Const _) = NoOcc 

1460  156 
 occur (Bound _) = NoOcc 
157 
 occur (Free _) = NoOcc 

158 
 occur (Var (w,_)) = 

2178  159 
if mem_ix (w, !seen) then NoOcc 
2753  160 
else if eq_ix(v,w) then Rigid 
1460  161 
else (seen := w:: !seen; 
162 
case Envir.lookup(env,w) of 

163 
None => NoOcc 

164 
 Some t => occur t) 

165 
 occur (Abs(_,_,body)) = occur body 

166 
 occur (t as f$_) = (*switch to nonrigid search?*) 

167 
(case head_of_in (env,f) of 

168 
Var (w,_) => (*w is not assigned*) 

2753  169 
if eq_ix(v,w) then Rigid 
1460  170 
else nonrigid t 
171 
 Abs(_,_,body) => nonrigid t (*not in normal form*) 

172 
 _ => occomb t) 

0  173 
in occur t end; 
174 

175 

1460  176 
exception CANTUNIFY; (*Signals nonunifiability. Does not signal errors!*) 
177 
exception ASSIGN; (*Raised if not an assignment*) 

0  178 

179 

180 
fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) = 

1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
922
diff
changeset

181 
if T=U then env 
12527  182 
else let val (iTs',maxidx') = Type.unify (#tsig(Sign.rep_sg (!sgr))) (iTs, maxidx) (U, T) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
922
diff
changeset

183 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
1505  184 
handle Type.TUNIFY => raise CANTUNIFY; 
0  185 

186 
fun test_unify_types(args as (T,U,_)) = 

187 
let val sot = Sign.string_of_typ (!sgr); 

12262  188 
fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T); 
0  189 
val env' = unify_types(args) 
190 
in if is_TVar(T) orelse is_TVar(U) then warn() else (); 

191 
env' 

192 
end; 

193 

194 
(*Is the term etaconvertible to a single variable with the given rbinder? 

195 
Examples: ?a ?f(B.0) ?g(B.1,B.0) 

196 
Result is var a for use in SIMPL. *) 

197 
fun get_eta_var ([], _, Var vT) = vT 

198 
 get_eta_var (_::rbinder, n, f $ Bound i) = 

1460  199 
if n=i then get_eta_var (rbinder, n+1, f) 
200 
else raise ASSIGN 

0  201 
 get_eta_var _ = raise ASSIGN; 
202 

203 

204 
(* ([xn,...,x1], t) ======> (x1,...,xn)t *) 

205 
fun rlist_abs ([], body) = body 

206 
 rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); 

207 

208 

209 
(*Solve v=u by assignment  "fixedpoint" to Huet  if v not in u. 

210 
If v occurs rigidly then nonunifiable. 

211 
If v occurs nonrigidly then must use full algorithm. *) 

212 
fun assignment (env, rbinder, t, u) = 

213 
let val (v,T) = get_eta_var(rbinder,0,t) 

214 
in case rigid_occurs_term (ref[], env, v, u) of 

1460  215 
NoOcc => let val env = unify_types(body_type env T, 
216 
fastype env (rbinder,u),env) 

217 
in Envir.update ((v, rlist_abs(rbinder,u)), env) end 

218 
 Nonrigid => raise ASSIGN 

219 
 Rigid => raise CANTUNIFY 

0  220 
end; 
221 

222 

223 
(*Extends an rbinder with a new disagreement pair, if both are abstractions. 

224 
Tries to unify types of the bound variables! 

225 
Checks that binders have same length, since terms should be etanormal; 

226 
if not, raises TERM, probably indicating type mismatch. 

227 
Uses variable a (unless the null string) to preserve user's naming.*) 

228 
fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) = 

1460  229 
let val env' = unify_types(T,U,env) 
230 
val c = if a="" then b else a 

231 
in new_dpair((c,T) :: rbinder, body1, body2, env') end 

0  232 
 new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", []) 
233 
 new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", []) 

234 
 new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env); 

235 

236 

237 
fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env = 

238 
new_dpair (rbinder, 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

239 
eta_norm env (rbinder, Envir.head_norm env t), 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

240 
eta_norm env (rbinder, Envir.head_norm env u), env); 
0  241 

242 

243 

244 
(*flexflex: the flexflex pairs, flexrigid: the flexrigid pairs 

245 
Does not perform assignments for flexflex pairs: 

646  246 
may create nonrigid paths, which prevent other assignments. 
247 
Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to 

248 
do so caused numerous problems with no compensating advantage. 

249 
*) 

0  250 
fun SIMPL0 (dp0, (env,flexflex,flexrigid)) 
1460  251 
: Envir.env * dpair list * dpair list = 
0  252 
let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0); 
1460  253 
fun SIMRANDS(f$t, g$u, env) = 
254 
SIMPL0((rbinder,t,u), SIMRANDS(f,g,env)) 

255 
 SIMRANDS (t as _$_, _, _) = 

256 
raise TERM ("SIMPL: operands mismatch", [t,u]) 

257 
 SIMRANDS (t, u as _$_, _) = 

258 
raise TERM ("SIMPL: operands mismatch", [t,u]) 

259 
 SIMRANDS(_,_,env) = (env,flexflex,flexrigid); 

0  260 
in case (head_of t, head_of u) of 
261 
(Var(_,T), Var(_,U)) => 

1460  262 
let val T' = body_type env T and U' = body_type env U; 
263 
val env = unify_types(T',U',env) 

264 
in (env, dp::flexflex, flexrigid) end 

0  265 
 (Var _, _) => 
1460  266 
((assignment (env,rbinder,t,u), flexflex, flexrigid) 
267 
handle ASSIGN => (env, flexflex, dp::flexrigid)) 

0  268 
 (_, Var _) => 
1460  269 
((assignment (env,rbinder,u,t), flexflex, flexrigid) 
270 
handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) 

0  271 
 (Const(a,T), Const(b,U)) => 
1460  272 
if a=b then SIMRANDS(t,u, unify_types(T,U,env)) 
273 
else raise CANTUNIFY 

0  274 
 (Bound i, Bound j) => 
1460  275 
if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY 
0  276 
 (Free(a,T), Free(b,U)) => 
1460  277 
if a=b then SIMRANDS(t,u, unify_types(T,U,env)) 
278 
else raise CANTUNIFY 

0  279 
 _ => raise CANTUNIFY 
280 
end; 

281 

282 

283 
(* changed(env,t) checks whether the head of t is a variable assigned in env*) 

284 
fun changed (env, f$_) = changed (env,f) 

285 
 changed (env, Var (v,_)) = 

286 
(case Envir.lookup(env,v) of None=>false  _ => true) 

287 
 changed _ = false; 

288 

289 

290 
(*Recursion needed if any of the 'head variables' have been updated 

291 
Clever would be to redo just the affected dpairs*) 

292 
fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list = 

293 
let val all as (env',flexflex,flexrigid) = 

1460  294 
foldr SIMPL0 (dpairs, (env,[],[])); 
295 
val dps = flexrigid@flexflex 

0  296 
in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps 
297 
then SIMPL(env',dps) else all 

298 
end; 

299 

300 

301 
(*computes t(Bound(n+k1),...,Bound(n)) *) 

302 
fun combound (t, n, k) = 

303 
if k>0 then combound (t,n+1,k1) $ (Bound n) else t; 

304 

305 

306 
(*Makes the terms E1,...,Em, where Ts = [T...Tm]. 

307 
Each Ei is ?Gi(B.(n1),...,B.0), and has type Ti 

308 
The B.j are bound vars of binder. 

309 
The terms are not made in etanormalform, SIMPL does that later. 

310 
If done here, etaexpansion 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; 

1460  314 
val (env', vars) = Envir.genvars name (env, map funtype Ts) 
0  315 
in (env', map (fn var=> 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 higherorder argument, 

330 
or if u is a variable (flexflex 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 vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 

4270  336 
: (term * (Envir.env * dpair list))Seq.seq = 
0  337 
let (*Produce copies of uarg and cons them in front of uargs*) 
338 
fun copycons uarg (uargs, (env, dpairs)) = 

4270  339 
Seq.map(fn (uarg', ed') => (uarg'::uargs, ed')) 
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

340 
(mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), 
1460  341 
(env, dpairs))); 
342 
(*Produce sequence of all possible ways of copying the arg list*) 

4270  343 
fun copyargs [] = Seq.cons( ([],ed), Seq.empty) 
0  344 
 copyargs (uarg::uargs) = 
4270  345 
Seq.flat (Seq.map (copycons uarg) (copyargs uargs)); 
0  346 
val (uhead,uargs) = strip_comb u; 
347 
val base = body_type env (fastype env (rbinder,uhead)); 

348 
fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed'); 

349 
(*attempt projection on argument with given typ*) 

350 
val Ts = map (curry (fastype env) rbinder) targs; 

351 
fun projenv (head, (Us,bary), targ, tail) = 

1460  352 
let val env = if !trace_types then test_unify_types(base,bary,env) 
353 
else unify_types(base,bary,env) 

4270  354 
in Seq.make (fn () => 
1460  355 
let val (env',args) = make_args vname (Ts,env,Us); 
356 
(*higherorder projection: plug in targs for bound vars*) 

357 
fun plugin arg = list_comb(head_of arg, targs); 

358 
val dp = (rbinder, list_comb(targ, map plugin args), u); 

359 
val (env2,frigid,fflex) = SIMPL (env', dp::dpairs) 

360 
(*may raise exception CANTUNIFY*) 

361 
in Some ((list_comb(head,args), (env2, frigid@fflex)), 

362 
tail) 

4270  363 
end handle CANTUNIFY => Seq.pull tail) 
1460  364 
end handle CANTUNIFY => tail; 
0  365 
(*make a list of projections*) 
366 
fun make_projs (T::Ts, targ::targs) = 

1460  367 
(Bound(length Ts), T, targ) :: make_projs (Ts,targs) 
0  368 
 make_projs ([],[]) = [] 
369 
 make_projs _ = raise TERM ("make_projs", u::targs); 

370 
(*try projections and imitation*) 

371 
fun matchfun ((bvar,T,targ)::projs) = 

1460  372 
(projenv(bvar, strip_type env T, targ, matchfun projs)) 
0  373 
 matchfun [] = (*imitation last of all*) 
1460  374 
(case uhead of 
4270  375 
Const _ => Seq.map joinargs (copyargs uargs) 
376 
 Free _ => Seq.map joinargs (copyargs uargs) 

377 
 _ => Seq.empty) (*if Var, would be a loop!*) 

0  378 
in case uhead of 
1460  379 
Abs(a, T, body) => 
4270  380 
Seq.map(fn (body', ed') => (Abs (a,T,body'), ed')) 
1460  381 
(mc ((a,T)::rbinder, 
382 
(map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) 

0  383 
 Var (w,uary) => 
1460  384 
(*a flexflex dpair: make variable for t*) 
385 
let val (env', newhd) = Envir.genvar (#1 w) (env, Ts> base) 

386 
val tabs = combound(newhd, 0, length Ts) 

387 
val tsub = list_comb(newhd,targs) 

4270  388 
in Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
1460  389 
end 
0  390 
 _ => matchfun(rev(make_projs(Ts, targs))) 
391 
end 

392 
in mc end; 

393 

394 

395 
(*Call matchcopy to produce assignments to the variable in the dpair*) 

396 
fun MATCH (env, (rbinder,t,u), dpairs) 

4270  397 
: (Envir.env * dpair list)Seq.seq = 
0  398 
let val (Var(v,T), targs) = strip_comb t; 
399 
val Ts = binder_types env T; 

400 
fun new_dset (u', (env',dpairs')) = 

1460  401 
(*if v was updated to s, must unify s with u' *) 
402 
case Envir.lookup(env',v) of 

403 
None => (Envir.update ((v, types_abs(Ts, u')), env'), dpairs') 

404 
 Some s => (env', ([], s, types_abs(Ts, u'))::dpairs') 

4270  405 
in Seq.map new_dset 
0  406 
(matchcopy (#1 v) (rbinder, targs, u, (env,dpairs))) 
407 
end; 

408 

409 

410 

411 
(**** Flexflex processing ****) 

412 

413 
(*At end of unification, do flexflex assignments like ?a > ?f(?b) 

414 
Attempts to update t with u, raising ASSIGN if impossible*) 

415 
fun ff_assign(env, rbinder, t, u) : Envir.env = 

416 
let val (v,T) = get_eta_var(rbinder,0,t) 

417 
in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

418 
else let val env = unify_types(body_type env T, 
1460  419 
fastype env (rbinder,u), 
420 
env) 

421 
in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end 

0  422 
end; 
423 

424 

425 
(*Flex argument: a term, its type, and the index that refers to it.*) 

426 
type flarg = {t: term, T: typ, j: int}; 

427 

428 

429 
(*Form the arguments into records for deletion/sorting.*) 

430 
fun flexargs ([],[],[]) = [] : flarg list 

431 
 flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts) 

432 
 flexargs _ = error"flexargs"; 

433 

434 

435 
(*If an argument contains a banned Bound, then it should be deleted. 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

436 
But if the only path is flexible, this is difficult; the code gives up! 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

437 
In %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *) 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

438 
exception CHANGE_FAIL; (*flexible occurrence of banned variable*) 
0  439 

440 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

441 
(*Check whether the 'banned' bound var indices occur rigidly in t*) 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

442 
fun rigid_bound (lev, banned) t = 
0  443 
let val (head,args) = strip_comb t 
651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

444 
in 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

445 
case head of 
2140
eaa7ab39889d
Changed some mem calls to mem_int for greater efficiency (not that it could matter)
paulson
parents:
1505
diff
changeset

446 
Bound i => (ilev) mem_int banned orelse 
1460  447 
exists (rigid_bound (lev, banned)) args 
448 
 Var _ => false (*no rigid occurrences here!*) 

449 
 Abs (_,_,u) => 

450 
rigid_bound(lev+1, banned) u orelse 

451 
exists (rigid_bound (lev, banned)) args 

452 
 _ => exists (rigid_bound (lev, banned)) args 

0  453 
end; 
454 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

455 
(*Squash down indices at level >=lev to delete the banned from a term.*) 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

456 
fun change_bnos banned = 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

457 
let fun change lev (Bound i) = 
1460  458 
if i<lev then Bound i 
2140
eaa7ab39889d
Changed some mem calls to mem_int for greater efficiency (not that it could matter)
paulson
parents:
1505
diff
changeset

459 
else if (ilev) mem_int banned 
1460  460 
then raise CHANGE_FAIL (**flexible occurrence: give up**) 
461 
else Bound (i  length (filter (fn j => j < ilev) banned)) 

462 
 change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) 

463 
 change lev (t$u) = change lev t $ change lev u 

464 
 change lev t = t 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

465 
in change 0 end; 
0  466 

467 
(*Change indices, delete the argument if it contains a banned Bound*) 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

468 
fun change_arg banned ({j,t,T}, args) : flarg list = 
1460  469 
if rigid_bound (0, banned) t then args (*delete argument!*) 
651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

470 
else {j=j, t= change_bnos banned t, T=T} :: args; 
0  471 

472 

473 
(*Sort the arguments to create assignments if possible: 

474 
create etaterms like ?g(B.1,B.0) *) 

475 
fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1) 

476 
 arg_less (_:flarg, _:flarg) = false; 

477 

478 
(*Test whether the new term would be etaequivalent to a variable  

479 
if so then there is no point in creating a new variable*) 

480 
fun decreasing n ([]: flarg list) = (n=0) 

481 
 decreasing n ({j,...}::args) = j=n1 andalso decreasing (n1) args; 

482 

483 
(*Delete banned indices in the term, simplifying it. 

484 
Force an assignment, if possible, by sorting the arguments. 

485 
Update its head; squash indices in arguments. *) 

486 
fun clean_term banned (env,t) = 

487 
let val (Var(v,T), ts) = strip_comb t 

1460  488 
val (Ts,U) = strip_type env T 
489 
and js = length ts  1 downto 0 

4438  490 
val args = sort (make_ord arg_less) 
1460  491 
(foldr (change_arg banned) (flexargs (js,ts,Ts), [])) 
492 
val ts' = map (#t) args 

0  493 
in 
494 
if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts'))) 

495 
else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args > U) 

1460  496 
val body = list_comb(v', map (Bound o #j) args) 
497 
val env2 = Envir.vupdate (((v, types_abs(Ts, body)), env')) 

498 
(*the vupdate affects ts' if they contain v*) 

499 
in 

500 
(env2, Envir.norm_term env2 (list_comb(v',ts'))) 

0  501 
end 
502 
end; 

503 

504 

505 
(*Add tpair if not trivial or already there. 

506 
Should check for swapped pairs??*) 

507 
fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list = 

508 
if t0 aconv u0 then tpairs 

509 
else 

510 
let val t = rlist_abs(rbinder, t0) and u = rlist_abs(rbinder, u0); 

511 
fun same(t',u') = (t aconv t') andalso (u aconv u') 

512 
in if exists same tpairs then tpairs else (t,u)::tpairs end; 

513 

514 

515 
(*Simplify both terms and check for assignments. 

516 
Bound vars in the binder are "banned" unless used in both t AND u *) 

517 
fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 

518 
let val loot = loose_bnos t and loou = loose_bnos u 

519 
fun add_index (((a,T), j), (bnos, newbinder)) = 

2140
eaa7ab39889d
Changed some mem calls to mem_int for greater efficiency (not that it could matter)
paulson
parents:
1505
diff
changeset

520 
if j mem_int loot andalso j mem_int loou 
1460  521 
then (bnos, (a,T)::newbinder) (*needed by both: keep*) 
522 
else (j::bnos, newbinder); (*remove*) 

0  523 
val indices = 0 upto (length rbinder  1); 
524 
val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[])); 

525 
val (env', t') = clean_term banned (env, t); 

526 
val (env'',u') = clean_term banned (env',u) 

527 
in (ff_assign(env'', rbin', t', u'), tpairs) 

528 
handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs) 

529 
handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs)) 

530 
end 

531 
handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs)); 

532 

533 

534 
(*IF the flexflex dpair is an assignment THEN do it ELSE put in tpairs 

535 
eliminates trivial tpairs like t=t, as well as repeated ones 

536 
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t 

537 
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) 

538 
fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 

539 
: Envir.env * (term*term)list = 

540 
let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0 

541 
in case (head_of t, head_of u) of 

542 
(Var(v,T), Var(w,U)) => (*Check for identical variables...*) 

2753  543 
if eq_ix(v,w) then (*...occur check would falsely return true!*) 
1460  544 
if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) 
545 
else raise TERM ("add_ffpair: Var name confusion", [t,u]) 

546 
else if xless(v,w) then (*prefer to update the LARGER variable*) 

547 
clean_ffpair ((rbinder, u, t), (env,tpairs)) 

0  548 
else clean_ffpair ((rbinder, t, u), (env,tpairs)) 
549 
 _ => raise TERM ("add_ffpair: Vars expected", [t,u]) 

550 
end; 

551 

552 

553 
(*Print a tracing message + list of dpairs. 

554 
In t==u print u first because it may be rigid or flexible  

555 
t is always flexible.*) 

556 
fun print_dpairs msg (env,dpairs) = 

557 
let fun pdp (rbinder,t,u) = 

558 
let fun termT t = Sign.pretty_term (!sgr) 

559 
(Envir.norm_term env (rlist_abs(rbinder,t))) 

560 
val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, 

561 
termT t]; 

12262  562 
in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end; 
563 
in tracing msg; seq pdp dpairs end; 

0  564 

565 

566 
(*Unify the dpairs in the environment. 

567 
Returns flexflex disagreement pairs NOT IN normal form. 

568 
SIMPL may raise exception CANTUNIFY. *) 

569 
fun hounifiers (sg,env, tus : (term*term)list) 

4270  570 
: (Envir.env * (term*term)list)Seq.seq = 
0  571 
let fun add_unify tdepth ((env,dpairs), reseq) = 
4270  572 
Seq.make (fn()=> 
1460  573 
let val (env',flexflex,flexrigid) = 
574 
(if tdepth> !trace_bound andalso !trace_simp 

575 
then print_dpairs "Enter SIMPL" (env,dpairs) else (); 

576 
SIMPL (env,dpairs)) 

577 
in case flexrigid of 

578 
[] => Some (foldr add_ffpair (flexflex, (env',[])), reseq) 

579 
 dp::frigid' => 

580 
if tdepth > !search_bound then 

4314  581 
(warning "Unification bound exceeded"; Seq.pull reseq) 
1460  582 
else 
583 
(if tdepth > !trace_bound then 

584 
print_dpairs "Enter MATCH" (env',flexrigid@flexflex) 

585 
else (); 

4270  586 
Seq.pull (Seq.it_right (add_unify (tdepth+1)) 
1460  587 
(MATCH (env',dp, frigid'@flexflex), reseq))) 
588 
end 

589 
handle CANTUNIFY => 

12262  590 
(if tdepth > !trace_bound then tracing"Failure node" else (); 
4270  591 
Seq.pull reseq)); 
0  592 
val dps = map (fn(t,u)=> ([],t,u)) tus 
593 
in sgr := sg; 

4270  594 
add_unify 1 ((env,dps), Seq.empty) 
0  595 
end; 
596 

597 
fun unifiers(params) = 

4270  598 
Seq.cons((Pattern.unify(params), []), Seq.empty) 
599 
handle Pattern.Unif => Seq.empty 

0  600 
 Pattern.Pattern => hounifiers(params); 
601 

602 

603 
(*For smash_flexflex1*) 

604 
fun var_head_of (env,t) : indexname * typ = 

605 
case head_of (strip_abs_body (Envir.norm_term env t)) of 

606 
Var(v,T) => (v,T) 

607 
 _ => raise CANTUNIFY; (*not flexible, cannot use trivial substitution*) 

608 

609 

610 
(*Eliminate a flexflex pair by the trivial substitution, see Huet (1975) 

611 
Unifies ?f(t1...rm) with ?g(u1...un) by ?f > %x1...xm.?a, ?g > %x1...xn.?a 

612 
Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g > %(x,y)?a, 

1460  613 
though just ?g>?f is a more general unifier. 
0  614 
Unlike Huet (1975), does not smash together all variables of same type  
615 
requires more work yet gives a less general unifier (fewer variables). 

616 
Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *) 

617 
fun smash_flexflex1 ((t,u), env) : Envir.env = 

618 
let val (v,T) = var_head_of (env,t) 

619 
and (w,U) = var_head_of (env,u); 

620 
val (env', var) = Envir.genvar (#1v) (env, body_type env T) 

621 
val env'' = Envir.vupdate((w, type_abs(env',U,var)), env') 

622 
in if (v,T)=(w,U) then env'' (*the other update would be identical*) 

623 
else Envir.vupdate((v, type_abs(env',T,var)), env'') 

624 
end; 

625 

626 

627 
(*Smash all flexflexpairs. Should allow selection of pairs by a predicate?*) 

628 
fun smash_flexflex (env,tpairs) : Envir.env = 

629 
foldr smash_flexflex1 (tpairs, env); 

630 

631 
(*Returns unifiers with no remaining disagreement pairs*) 

4270  632 
fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq = 
633 
Seq.map smash_flexflex (unifiers(sg,env,tus)); 

0  634 

635 
end; 