author  paulson 
Fri, 07 Mar 1997 10:26:02 +0100  
changeset 2753  bcde71e5f371 
parent 2193  b7e59795c75b 
child 3991  4cb2f2422695 
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 

1460  28 
> (Envir.env Sequence.seq) 
0  29 
val unifiers: Sign.sg * Envir.env * ((term*term)list) 
1460  30 
> (Envir.env * (term * term)list) Sequence.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 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
651
diff
changeset

44 
val sgr = ref(Sign.proto_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 

52 
 bT(T as TVar(ixn,_)) = (case assoc(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 

59 
 bTs(T as TVar(ixn,_)) = (case assoc(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 

66 

67 
(*Put a term into head normal form for unification. 

68 
Operands need not be in normal form. Does etaexpansions on the head, 

69 
which involves renumbering (thus copying) the args. To avoid this 

70 
inefficiency, avoid partial application: if an atom is applied to 

71 
any arguments at all, apply it to its full number of arguments. 

72 
For 

1460  73 
rbinder = [(x1,T),...,(xm,Tm)] (user's var names preserved!) 
0  74 
args = [arg1,...,argn] 
75 
the value of 

76 
(xm,...,x1)(head(arg1,...,argn)) remains invariant. 

77 
*) 

78 

79 
local exception SAME 

80 
in 

81 
fun head_norm (env,t) : term = 

82 
let fun hnorm (Var (v,T)) = 

1460  83 
(case Envir.lookup (env,v) of 
84 
Some u => head_norm (env, u) 

85 
 None => raise SAME) 

86 
 hnorm (Abs(a,T,body)) = Abs(a, T, hnorm body) 

87 
 hnorm (Abs(_,_,body) $ t) = 

2193
b7e59795c75b
Changed subst_bounds to subst_bound, to run faster
paulson
parents:
2178
diff
changeset

88 
head_norm (env, subst_bound (t, body)) 
1460  89 
 hnorm (f $ t) = 
90 
(case hnorm f of 

91 
Abs(_,_,body) => 

2193
b7e59795c75b
Changed subst_bounds to subst_bound, to run faster
paulson
parents:
2178
diff
changeset

92 
head_norm (env, subst_bound (t, body)) 
1460  93 
 nf => nf $ t) 
94 
 hnorm _ = raise SAME 

0  95 
in hnorm t handle SAME=> t end 
96 
end; 

97 

98 

99 
(*finds type of term without checking that combinations are consistent 

100 
rbinder holds types of bound variables*) 

101 
fun fastype (Envir.Envir{iTs,...}) = 

102 
let val funerr = "fastype: expected function type"; 

103 
fun fast(rbinder, f$u) = 

1460  104 
(case (fast (rbinder, f)) of 
105 
Type("fun",[_,T]) => T 

106 
 TVar(ixn,_) => 

107 
(case assoc(iTs,ixn) of 

108 
Some(Type("fun",[_,T])) => T 

109 
 _ => raise TERM(funerr, [f$u])) 

110 
 _ => raise TERM(funerr, [f$u])) 

0  111 
 fast (rbinder, Const (_,T)) = T 
112 
 fast (rbinder, Free (_,T)) = T 

113 
 fast (rbinder, Bound i) = 

1460  114 
(#2 (nth_elem (i,rbinder)) 
115 
handle LIST _=> raise TERM("fastype: Bound", [Bound i])) 

0  116 
 fast (rbinder, Var (_,T)) = T 
117 
 fast (rbinder, Abs (_,T,u)) = T > fast (("",T) :: rbinder, u) 

118 
in fast end; 

119 

120 

121 
(*Eta normal form*) 

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

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

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

126 
(case assoc(iTs,ixn) of 

127 
None => t  Some(T) => etif(T,t)) 

128 
 etif (_,t) = t; 

0  129 
fun eta_nm (rbinder, Abs(a,T,body)) = 
1460  130 
Abs(a, T, eta_nm ((a,T)::rbinder, body)) 
131 
 eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t) 

0  132 
in eta_nm end; 
133 

134 

135 
(*OCCURS CHECK 

136 
Does the uvar occur in the term t? 

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

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

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

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

1460  141 
env: Envir.env, v: indexname, ts: term list): bool = 
0  142 
let fun occurs [] = false 
1460  143 
 occurs (t::ts) = occur t orelse occurs ts 
0  144 
and occur (Const _) = false 
1460  145 
 occur (Bound _) = false 
146 
 occur (Free _) = false 

147 
 occur (Var (w,_)) = 

2178  148 
if mem_ix (w, !seen) then false 
2753  149 
else if eq_ix(v,w) then true 
1460  150 
(*no need to lookup: v has no assignment*) 
151 
else (seen := w:: !seen; 

152 
case Envir.lookup(env,w) of 

153 
None => false 

154 
 Some t => occur t) 

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

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

0  157 
in occurs ts end; 
158 

159 

160 

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

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

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

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

1460  165 
Some u => head_of_in(env,u)  None => t) 
0  166 
 _ => t; 
167 

168 

169 
datatype occ = NoOcc  Nonrigid  Rigid; 

170 

171 
(* Rigid occur check 

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

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

174 
NoOcc otherwise. 

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

176 

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

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

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

180 
reject ALL rigid paths to the variable. 

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

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

183 

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

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

186 
for arg1,...,argn. 

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

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

189 
term is not in normal form. 

190 

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

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

193 
*) 

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

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

1460  196 
else NoOcc 
0  197 
fun occurs [] = NoOcc 
1460  198 
 occurs (t::ts) = 
0  199 
(case occur t of 
200 
Rigid => Rigid 

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

202 
and occomb (f$t) = 

203 
(case occur t of 

204 
Rigid => Rigid 

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

206 
 occomb t = occur t 

207 
and occur (Const _) = NoOcc 

1460  208 
 occur (Bound _) = NoOcc 
209 
 occur (Free _) = NoOcc 

210 
 occur (Var (w,_)) = 

2178  211 
if mem_ix (w, !seen) then NoOcc 
2753  212 
else if eq_ix(v,w) then Rigid 
1460  213 
else (seen := w:: !seen; 
214 
case Envir.lookup(env,w) of 

215 
None => NoOcc 

216 
 Some t => occur t) 

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

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

219 
(case head_of_in (env,f) of 

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

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

224 
 _ => occomb t) 

0  225 
in occur t end; 
226 

227 

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

0  230 

231 

232 
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

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

235 
maxidx iTs (U,T) 
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
922
diff
changeset

236 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
1505  237 
handle Type.TUNIFY => raise CANTUNIFY; 
0  238 

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

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

241 
fun warn() = writeln("Potential loss of completeness: "^sot U^" = "^sot T); 

242 
val env' = unify_types(args) 

243 
in if is_TVar(T) orelse is_TVar(U) then warn() else (); 

244 
env' 

245 
end; 

246 

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

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

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

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

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

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

0  254 
 get_eta_var _ = raise ASSIGN; 
255 

256 

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

258 
fun rlist_abs ([], body) = body 

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

260 

261 

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

263 
If v occurs rigidly then nonunifiable. 

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

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

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

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

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

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

271 
 Nonrigid => raise ASSIGN 

272 
 Rigid => raise CANTUNIFY 

0  273 
end; 
274 

275 

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

277 
Tries to unify types of the bound variables! 

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

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

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

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

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

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

0  285 
 new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", []) 
286 
 new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", []) 

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

288 

289 

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

291 
new_dpair (rbinder, 

1460  292 
eta_norm env (rbinder, head_norm(env,t)), 
293 
eta_norm env (rbinder, head_norm(env,u)), env); 

0  294 

295 

296 

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

298 
Does not perform assignments for flexflex pairs: 

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

301 
do so caused numerous problems with no compensating advantage. 

302 
*) 

0  303 
fun SIMPL0 (dp0, (env,flexflex,flexrigid)) 
1460  304 
: Envir.env * dpair list * dpair list = 
0  305 
let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0); 
1460  306 
fun SIMRANDS(f$t, g$u, env) = 
307 
SIMPL0((rbinder,t,u), SIMRANDS(f,g,env)) 

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

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

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

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

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

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

1460  315 
let val T' = body_type env T and U' = body_type env U; 
316 
val env = unify_types(T',U',env) 

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

0  318 
 (Var _, _) => 
1460  319 
((assignment (env,rbinder,t,u), flexflex, flexrigid) 
320 
handle ASSIGN => (env, flexflex, dp::flexrigid)) 

0  321 
 (_, Var _) => 
1460  322 
((assignment (env,rbinder,u,t), flexflex, flexrigid) 
323 
handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) 

0  324 
 (Const(a,T), Const(b,U)) => 
1460  325 
if a=b then SIMRANDS(t,u, unify_types(T,U,env)) 
326 
else raise CANTUNIFY 

0  327 
 (Bound i, Bound j) => 
1460  328 
if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY 
0  329 
 (Free(a,T), Free(b,U)) => 
1460  330 
if a=b then SIMRANDS(t,u, unify_types(T,U,env)) 
331 
else raise CANTUNIFY 

0  332 
 _ => raise CANTUNIFY 
333 
end; 

334 

335 

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

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

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

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

340 
 changed _ = false; 

341 

342 

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

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

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

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

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

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

351 
end; 

352 

353 

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

355 
fun combound (t, n, k) = 

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

357 

358 

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

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

361 
The B.j are bound vars of binder. 

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

363 
If done here, etaexpansion must be recursive in the arguments! *) 

364 
fun make_args name (binder: typ list, env, []) = (env, []) (*frequent case*) 

365 
 make_args name (binder: typ list, env, Ts) : Envir.env * term list = 

366 
let fun funtype T = binder>T; 

1460  367 
val (env', vars) = Envir.genvars name (env, map funtype Ts) 
0  368 
in (env', map (fn var=> combound(var, 0, length binder)) vars) end; 
369 

370 

371 
(*Abstraction over a list of types, like list_abs*) 

372 
fun types_abs ([],u) = u 

373 
 types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u)); 

374 

375 
(*Abstraction over the binder of a type*) 

376 
fun type_abs (env,T,t) = types_abs(binder_types env T, t); 

377 

378 

379 
(*MATCH taking "big steps". 

380 
Copies u into the Var v, using projection on targs or imitation. 

381 
A projection is allowed unless SIMPL raises an exception. 

382 
Allocates new variables in projection on a higherorder argument, 

383 
or if u is a variable (flexflex dpair). 

384 
Returns long sequence of every way of copying u, for backtracking 

385 
For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a. 

386 
The order for trying projections is crucial in ?b'(?a) 

387 
NB "vname" is only used in the call to make_args!! *) 

388 
fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 

1460  389 
: (term * (Envir.env * dpair list))Sequence.seq = 
0  390 
let (*Produce copies of uarg and cons them in front of uargs*) 
391 
fun copycons uarg (uargs, (env, dpairs)) = 

1460  392 
Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed')) 
393 
(mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)), 

394 
(env, dpairs))); 

395 
(*Produce sequence of all possible ways of copying the arg list*) 

0  396 
fun copyargs [] = Sequence.cons( ([],ed), Sequence.null) 
397 
 copyargs (uarg::uargs) = 

1460  398 
Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs)); 
0  399 
val (uhead,uargs) = strip_comb u; 
400 
val base = body_type env (fastype env (rbinder,uhead)); 

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

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

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

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

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

407 
in Sequence.seqof (fn () => 

408 
let val (env',args) = make_args vname (Ts,env,Us); 

409 
(*higherorder projection: plug in targs for bound vars*) 

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

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

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

413 
(*may raise exception CANTUNIFY*) 

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

415 
tail) 

416 
end handle CANTUNIFY => Sequence.pull tail) 

417 
end handle CANTUNIFY => tail; 

0  418 
(*make a list of projections*) 
419 
fun make_projs (T::Ts, targ::targs) = 

1460  420 
(Bound(length Ts), T, targ) :: make_projs (Ts,targs) 
0  421 
 make_projs ([],[]) = [] 
422 
 make_projs _ = raise TERM ("make_projs", u::targs); 

423 
(*try projections and imitation*) 

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

1460  425 
(projenv(bvar, strip_type env T, targ, matchfun projs)) 
0  426 
 matchfun [] = (*imitation last of all*) 
1460  427 
(case uhead of 
428 
Const _ => Sequence.maps joinargs (copyargs uargs) 

429 
 Free _ => Sequence.maps joinargs (copyargs uargs) 

430 
 _ => Sequence.null) (*if Var, would be a loop!*) 

0  431 
in case uhead of 
1460  432 
Abs(a, T, body) => 
433 
Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 

434 
(mc ((a,T)::rbinder, 

435 
(map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) 

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

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

440 
val tsub = list_comb(newhd,targs) 

441 
in Sequence.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 

442 
end 

0  443 
 _ => matchfun(rev(make_projs(Ts, targs))) 
444 
end 

445 
in mc end; 

446 

447 

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

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

1460  450 
: (Envir.env * dpair list)Sequence.seq = 
0  451 
let val (Var(v,T), targs) = strip_comb t; 
452 
val Ts = binder_types env T; 

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

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

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

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

0  458 
in Sequence.maps new_dset 
459 
(matchcopy (#1 v) (rbinder, targs, u, (env,dpairs))) 

460 
end; 

461 

462 

463 

464 
(**** Flexflex processing ****) 

465 

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

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

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

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

470 
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

471 
else let val env = unify_types(body_type env T, 
1460  472 
fastype env (rbinder,u), 
473 
env) 

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

0  475 
end; 
476 

477 

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

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

480 

481 

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

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

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

485 
 flexargs _ = error"flexargs"; 

486 

487 

488 
(*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

489 
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

490 
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

491 
exception CHANGE_FAIL; (*flexible occurrence of banned variable*) 
0  492 

493 

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

494 
(*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

495 
fun rigid_bound (lev, banned) t = 
0  496 
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

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

498 
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

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

502 
 Abs (_,_,u) => 

503 
rigid_bound(lev+1, banned) u orelse 

504 
exists (rigid_bound (lev, banned)) args 

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

0  506 
end; 
507 

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

508 
(*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

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

510 
let fun change lev (Bound i) = 
1460  511 
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

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

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

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

517 
 change lev t = t 

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

518 
in change 0 end; 
0  519 

520 
(*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

521 
fun change_arg banned ({j,t,T}, args) : flarg list = 
1460  522 
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

523 
else {j=j, t= change_bnos banned t, T=T} :: args; 
0  524 

525 

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

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

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

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

530 

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

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

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

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

535 

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

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

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

539 
fun clean_term banned (env,t) = 

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

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

543 
val args = sort arg_less 

544 
(foldr (change_arg banned) (flexargs (js,ts,Ts), [])) 

545 
val ts' = map (#t) args 

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

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

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

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

552 
in 

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

0  554 
end 
555 
end; 

556 

557 

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

559 
Should check for swapped pairs??*) 

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

561 
if t0 aconv u0 then tpairs 

562 
else 

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

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

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

566 

567 

568 
(*Simplify both terms and check for assignments. 

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

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

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

572 
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

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

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

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

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

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

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

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

583 
end 

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

585 

586 

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

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

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

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

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

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

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

594 
in case (head_of t, head_of u) of 

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

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

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

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

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

603 
end; 

604 

605 

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

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

608 
t is always flexible.*) 

609 
fun print_dpairs msg (env,dpairs) = 

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

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

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

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

614 
termT t]; 

615 
in writeln(Pretty.string_of(Pretty.blk(0,bsymbs))) end; 

616 
in writeln msg; seq pdp dpairs end; 

617 

618 

619 
(*Unify the dpairs in the environment. 

620 
Returns flexflex disagreement pairs NOT IN normal form. 

621 
SIMPL may raise exception CANTUNIFY. *) 

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

623 
: (Envir.env * (term*term)list)Sequence.seq = 

624 
let fun add_unify tdepth ((env,dpairs), reseq) = 

1460  625 
Sequence.seqof (fn()=> 
626 
let val (env',flexflex,flexrigid) = 

627 
(if tdepth> !trace_bound andalso !trace_simp 

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

629 
SIMPL (env,dpairs)) 

630 
in case flexrigid of 

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

632 
 dp::frigid' => 

633 
if tdepth > !search_bound then 

634 
(prs"***Unification bound exceeded\n"; Sequence.pull reseq) 

635 
else 

636 
(if tdepth > !trace_bound then 

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

638 
else (); 

639 
Sequence.pull (Sequence.its_right (add_unify (tdepth+1)) 

640 
(MATCH (env',dp, frigid'@flexflex), reseq))) 

641 
end 

642 
handle CANTUNIFY => 

643 
(if tdepth > !trace_bound then writeln"Failure node" else (); 

644 
Sequence.pull reseq)); 

0  645 
val dps = map (fn(t,u)=> ([],t,u)) tus 
646 
in sgr := sg; 

647 
add_unify 1 ((env,dps), Sequence.null) 

648 
end; 

649 

650 
fun unifiers(params) = 

651 
Sequence.cons((Pattern.unify(params), []), Sequence.null) 

652 
handle Pattern.Unif => Sequence.null 

653 
 Pattern.Pattern => hounifiers(params); 

654 

655 

656 
(*For smash_flexflex1*) 

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

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

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

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

661 

662 

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

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

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

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

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

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

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

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

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

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

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

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

677 
end; 

678 

679 

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

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

682 
foldr smash_flexflex1 (tpairs, env); 

683 

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

685 
fun smash_unifiers (sg, env, tus) : Envir.env Sequence.seq = 

686 
Sequence.maps smash_flexflex (unifiers(sg,env,tus)); 

687 

688 
end; 