author  clasohm 
Mon, 29 Jan 1996 13:56:41 +0100  
changeset 1458  fd510875fb71 
parent 1435  aefcd255ed4a 
child 1460  5a6f2aabd538 
permissions  rwrr 
1458  1 
(* Title: unify 
0  2 
ID: $Id$ 
1458  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 = 

18 
sig 

19 
structure Sign: SIGN 

20 
structure Envir : ENVIR 

21 
structure Sequence : SEQUENCE 

22 
(*references for control and tracing*) 

23 
val trace_bound: int ref 

24 
val trace_simp: bool ref 

25 
val trace_types: bool ref 

26 
val search_bound: int ref 

27 
(*other exports*) 

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

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

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

1458  31 
> (Envir.env Sequence.seq) 
0  32 
val unifiers: Sign.sg * Envir.env * ((term*term)list) 
1458  33 
> (Envir.env * (term * term)list) Sequence.seq 
0  34 
end; 
35 

36 
functor UnifyFun (structure Sign: SIGN and Envir: ENVIR and Sequence: SEQUENCE 

37 
and Pattern:PATTERN 

38 
sharing type Sign.sg = Pattern.sg 

39 
and type Envir.env = Pattern.env) 

1458  40 
: UNIFY = 
0  41 
struct 
42 

43 
structure Sign = Sign; 

44 
structure Envir = Envir; 

45 
structure Sequence = Sequence; 

46 
structure Pretty = Sign.Syntax.Pretty; 

47 

48 
(*Unification options*) 

49 

1458  50 
val trace_bound = ref 10 (*tracing starts above this depth, 0 for full*) 
51 
and search_bound = ref 20 (*unification quits above this depth*) 

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

53 
and trace_types = ref false (*announce potential incompleteness 

54 
of type unification*) 

0  55 

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

56 
val sgr = ref(Sign.proto_pure); 
0  57 

58 
type binderlist = (string*typ) list; 

59 

60 
type dpair = binderlist * term * term; 

61 

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

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

64 
 bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of 

1458  65 
None => T  Some(T') => bT T') 
0  66 
 bT T = T 
67 
in bT end; 

68 

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

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

71 
 bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of 

1458  72 
None => []  Some(T') => bTs T') 
0  73 
 bTs _ = [] 
74 
in bTs end; 

75 

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

77 

78 

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

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

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

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

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

84 
For 

1458  85 
rbinder = [(x1,T),...,(xm,Tm)] (user's var names preserved!) 
0  86 
args = [arg1,...,argn] 
87 
the value of 

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

89 
*) 

90 

91 
local exception SAME 

92 
in 

93 
fun head_norm (env,t) : term = 

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

1458  95 
(case Envir.lookup (env,v) of 
96 
Some u => head_norm (env, u) 

97 
 None => raise SAME) 

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

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

100 
head_norm (env, subst_bounds([t], body)) 

101 
 hnorm (f $ t) = 

102 
(case hnorm f of 

103 
Abs(_,_,body) => 

104 
head_norm (env, subst_bounds([t], body)) 

105 
 nf => nf $ t) 

106 
 hnorm _ = raise SAME 

0  107 
in hnorm t handle SAME=> t end 
108 
end; 

109 

110 

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

112 
rbinder holds types of bound variables*) 

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

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

115 
fun fast(rbinder, f$u) = 

1458  116 
(case (fast (rbinder, f)) of 
117 
Type("fun",[_,T]) => T 

118 
 TVar(ixn,_) => 

119 
(case assoc(iTs,ixn) of 

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

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

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

0  123 
 fast (rbinder, Const (_,T)) = T 
124 
 fast (rbinder, Free (_,T)) = T 

125 
 fast (rbinder, Bound i) = 

1458  126 
(#2 (nth_elem (i,rbinder)) 
127 
handle LIST _=> raise TERM("fastype: Bound", [Bound i])) 

0  128 
 fast (rbinder, Var (_,T)) = T 
129 
 fast (rbinder, Abs (_,T,u)) = T > fast (("",T) :: rbinder, u) 

130 
in fast end; 

131 

132 

133 
(*Eta normal form*) 

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

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

1458  136 
Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) 
137 
 etif (TVar(ixn,_),t) = 

138 
(case assoc(iTs,ixn) of 

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

140 
 etif (_,t) = t; 

0  141 
fun eta_nm (rbinder, Abs(a,T,body)) = 
1458  142 
Abs(a, T, eta_nm ((a,T)::rbinder, body)) 
143 
 eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t) 

0  144 
in eta_nm end; 
145 

146 

147 
(*OCCURS CHECK 

148 
Does the uvar occur in the term t? 

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

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

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

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

1458  153 
env: Envir.env, v: indexname, ts: term list): bool = 
0  154 
let fun occurs [] = false 
1458  155 
 occurs (t::ts) = occur t orelse occurs ts 
0  156 
and occur (Const _) = false 
1458  157 
 occur (Bound _) = false 
158 
 occur (Free _) = false 

159 
 occur (Var (w,_)) = 

160 
if w mem !seen then false 

161 
else if v=w then true 

162 
(*no need to lookup: v has no assignment*) 

163 
else (seen := w:: !seen; 

164 
case Envir.lookup(env,w) of 

165 
None => false 

166 
 Some t => occur t) 

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

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

0  169 
in occurs ts end; 
170 

171 

172 

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

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

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

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

1458  177 
Some u => head_of_in(env,u)  None => t) 
0  178 
 _ => t; 
179 

180 

181 
datatype occ = NoOcc  Nonrigid  Rigid; 

182 

183 
(* Rigid occur check 

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

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

186 
NoOcc otherwise. 

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

188 

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

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

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

192 
reject ALL rigid paths to the variable. 

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

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

195 

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

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

198 
for arg1,...,argn. 

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

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

201 
term is not in normal form. 

202 

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

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

205 
*) 

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

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

1458  208 
else NoOcc 
0  209 
fun occurs [] = NoOcc 
1458  210 
 occurs (t::ts) = 
0  211 
(case occur t of 
212 
Rigid => Rigid 

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

214 
and occomb (f$t) = 

215 
(case occur t of 

216 
Rigid => Rigid 

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

218 
 occomb t = occur t 

219 
and occur (Const _) = NoOcc 

1458  220 
 occur (Bound _) = NoOcc 
221 
 occur (Free _) = NoOcc 

222 
 occur (Var (w,_)) = 

223 
if w mem !seen then NoOcc 

224 
else if v=w then Rigid 

225 
else (seen := w:: !seen; 

226 
case Envir.lookup(env,w) of 

227 
None => NoOcc 

228 
 Some t => occur t) 

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

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

231 
(case head_of_in (env,f) of 

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

233 
if v=w then Rigid 

234 
else nonrigid t 

235 
 Abs(_,_,body) => nonrigid t (*not in normal form*) 

236 
 _ => occomb t) 

0  237 
in occur t end; 
238 

239 

1458  240 
exception CANTUNIFY; (*Signals nonunifiability. Does not signal errors!*) 
241 
exception ASSIGN; (*Raised if not an assignment*) 

0  242 

243 

244 
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

245 
if T=U then env 
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
922
diff
changeset

246 
else let val (iTs',maxidx') = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr))) 
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
922
diff
changeset

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

248 
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end 
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
922
diff
changeset

249 
handle Sign.Type.TUNIFY => raise CANTUNIFY; 
0  250 

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

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

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

254 
val env' = unify_types(args) 

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

256 
env' 

257 
end; 

258 

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

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

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

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

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

1458  264 
if n=i then get_eta_var (rbinder, n+1, f) 
265 
else raise ASSIGN 

0  266 
 get_eta_var _ = raise ASSIGN; 
267 

268 

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

270 
fun rlist_abs ([], body) = body 

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

272 

273 

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

275 
If v occurs rigidly then nonunifiable. 

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

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

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

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

1458  280 
NoOcc => let val env = unify_types(body_type env T, 
281 
fastype env (rbinder,u),env) 

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

283 
 Nonrigid => raise ASSIGN 

284 
 Rigid => raise CANTUNIFY 

0  285 
end; 
286 

287 

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

289 
Tries to unify types of the bound variables! 

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

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

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

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

1458  294 
let val env' = unify_types(T,U,env) 
295 
val c = if a="" then b else a 

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

0  297 
 new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", []) 
298 
 new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", []) 

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

300 

301 

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

303 
new_dpair (rbinder, 

1458  304 
eta_norm env (rbinder, head_norm(env,t)), 
305 
eta_norm env (rbinder, head_norm(env,u)), env); 

0  306 

307 

308 

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

310 
Does not perform assignments for flexflex pairs: 

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

313 
do so caused numerous problems with no compensating advantage. 

314 
*) 

0  315 
fun SIMPL0 (dp0, (env,flexflex,flexrigid)) 
1458  316 
: Envir.env * dpair list * dpair list = 
0  317 
let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0); 
1458  318 
fun SIMRANDS(f$t, g$u, env) = 
319 
SIMPL0((rbinder,t,u), SIMRANDS(f,g,env)) 

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

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

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

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

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

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

1458  327 
let val T' = body_type env T and U' = body_type env U; 
328 
val env = unify_types(T',U',env) 

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

0  330 
 (Var _, _) => 
1458  331 
((assignment (env,rbinder,t,u), flexflex, flexrigid) 
332 
handle ASSIGN => (env, flexflex, dp::flexrigid)) 

0  333 
 (_, Var _) => 
1458  334 
((assignment (env,rbinder,u,t), flexflex, flexrigid) 
335 
handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid)) 

0  336 
 (Const(a,T), Const(b,U)) => 
1458  337 
if a=b then SIMRANDS(t,u, unify_types(T,U,env)) 
338 
else raise CANTUNIFY 

0  339 
 (Bound i, Bound j) => 
1458  340 
if i=j then SIMRANDS(t,u,env) else raise CANTUNIFY 
0  341 
 (Free(a,T), Free(b,U)) => 
1458  342 
if a=b then SIMRANDS(t,u, unify_types(T,U,env)) 
343 
else raise CANTUNIFY 

0  344 
 _ => raise CANTUNIFY 
345 
end; 

346 

347 

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

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

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

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

352 
 changed _ = false; 

353 

354 

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

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

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

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

1458  359 
foldr SIMPL0 (dpairs, (env,[],[])); 
360 
val dps = flexrigid@flexflex 

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

363 
end; 

364 

365 

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

367 
fun combound (t, n, k) = 

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

369 

370 

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

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

373 
The B.j are bound vars of binder. 

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

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

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

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

378 
let fun funtype T = binder>T; 

1458  379 
val (env', vars) = Envir.genvars name (env, map funtype Ts) 
0  380 
in (env', map (fn var=> combound(var, 0, length binder)) vars) end; 
381 

382 

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

384 
fun types_abs ([],u) = u 

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

386 

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

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

389 

390 

391 
(*MATCH taking "big steps". 

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

393 
A projection is allowed unless SIMPL raises an exception. 

394 
Allocates new variables in projection on a higherorder argument, 

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

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

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

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

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

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

1458  401 
: (term * (Envir.env * dpair list))Sequence.seq = 
0  402 
let (*Produce copies of uarg and cons them in front of uargs*) 
403 
fun copycons uarg (uargs, (env, dpairs)) = 

1458  404 
Sequence.maps(fn (uarg', ed') => (uarg'::uargs, ed')) 
405 
(mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)), 

406 
(env, dpairs))); 

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

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

1458  410 
Sequence.flats (Sequence.maps (copycons uarg) (copyargs uargs)); 
0  411 
val (uhead,uargs) = strip_comb u; 
412 
val base = body_type env (fastype env (rbinder,uhead)); 

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

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

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

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

1458  417 
let val env = if !trace_types then test_unify_types(base,bary,env) 
418 
else unify_types(base,bary,env) 

419 
in Sequence.seqof (fn () => 

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

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

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

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

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

425 
(*may raise exception CANTUNIFY*) 

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

427 
tail) 

428 
end handle CANTUNIFY => Sequence.pull tail) 

429 
end handle CANTUNIFY => tail; 

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

1458  432 
(Bound(length Ts), T, targ) :: make_projs (Ts,targs) 
0  433 
 make_projs ([],[]) = [] 
434 
 make_projs _ = raise TERM ("make_projs", u::targs); 

435 
(*try projections and imitation*) 

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

1458  437 
(projenv(bvar, strip_type env T, targ, matchfun projs)) 
0  438 
 matchfun [] = (*imitation last of all*) 
1458  439 
(case uhead of 
440 
Const _ => Sequence.maps joinargs (copyargs uargs) 

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

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

0  443 
in case uhead of 
1458  444 
Abs(a, T, body) => 
445 
Sequence.maps(fn (body', ed') => (Abs (a,T,body'), ed')) 

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

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

0  448 
 Var (w,uary) => 
1458  449 
(*a flexflex dpair: make variable for t*) 
450 
let val (env', newhd) = Envir.genvar (#1 w) (env, Ts> base) 

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

452 
val tsub = list_comb(newhd,targs) 

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

454 
end 

0  455 
 _ => matchfun(rev(make_projs(Ts, targs))) 
456 
end 

457 
in mc end; 

458 

459 

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

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

1458  462 
: (Envir.env * dpair list)Sequence.seq = 
0  463 
let val (Var(v,T), targs) = strip_comb t; 
464 
val Ts = binder_types env T; 

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

1458  466 
(*if v was updated to s, must unify s with u' *) 
467 
case Envir.lookup(env',v) of 

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

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

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

472 
end; 

473 

474 

475 

476 
(**** Flexflex processing ****) 

477 

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

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

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

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

482 
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

483 
else let val env = unify_types(body_type env T, 
1458  484 
fastype env (rbinder,u), 
485 
env) 

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

0  487 
end; 
488 

489 

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

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

492 

493 

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

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

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

497 
 flexargs _ = error"flexargs"; 

498 

499 

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

501 
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

502 
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

503 
exception CHANGE_FAIL; (*flexible occurrence of banned variable*) 
0  504 

505 

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

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

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

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

510 
case head of 
1458  511 
Bound i => (ilev) mem banned orelse 
512 
exists (rigid_bound (lev, banned)) args 

513 
 Var _ => false (*no rigid occurrences here!*) 

514 
 Abs (_,_,u) => 

515 
rigid_bound(lev+1, banned) u orelse 

516 
exists (rigid_bound (lev, banned)) args 

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

0  518 
end; 
519 

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

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

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

522 
let fun change lev (Bound i) = 
1458  523 
if i<lev then Bound i 
524 
else if (ilev) mem banned 

525 
then raise CHANGE_FAIL (**flexible occurrence: give up**) 

526 
else Bound (i  length (filter (fn j => j < ilev) banned)) 

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

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

529 
 change lev t = t 

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

530 
in change 0 end; 
0  531 

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

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

535 
else {j=j, t= change_bnos banned t, T=T} :: args; 
0  536 

537 

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

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

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

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

542 

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

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

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

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

547 

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

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

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

551 
fun clean_term banned (env,t) = 

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

1458  553 
val (Ts,U) = strip_type env T 
554 
and js = length ts  1 downto 0 

555 
val args = sort arg_less 

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

557 
val ts' = map (#t) args 

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

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

1458  561 
val body = list_comb(v', map (Bound o #j) args) 
562 
val env2 = Envir.vupdate (((v, types_abs(Ts, body)), env')) 

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

564 
in 

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

0  566 
end 
567 
end; 

568 

569 

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

571 
Should check for swapped pairs??*) 

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

573 
if t0 aconv u0 then tpairs 

574 
else 

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

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

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

578 

579 

580 
(*Simplify both terms and check for assignments. 

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

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

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

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

585 
if j mem loot andalso j mem loou 

1458  586 
then (bnos, (a,T)::newbinder) (*needed by both: keep*) 
587 
else (j::bnos, newbinder); (*remove*) 

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

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

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

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

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

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

595 
end 

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

597 

598 

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

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

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

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

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

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

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

606 
in case (head_of t, head_of u) of 

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

1458  608 
if v=w then (*...occur check would falsely return true!*) 
609 
if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) 

610 
else raise TERM ("add_ffpair: Var name confusion", [t,u]) 

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

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

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

615 
end; 

616 

617 

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

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

620 
t is always flexible.*) 

621 
fun print_dpairs msg (env,dpairs) = 

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

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

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

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

626 
termT t]; 

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

628 
in writeln msg; seq pdp dpairs end; 

629 

630 

631 
(*Unify the dpairs in the environment. 

632 
Returns flexflex disagreement pairs NOT IN normal form. 

633 
SIMPL may raise exception CANTUNIFY. *) 

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

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

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

1458  637 
Sequence.seqof (fn()=> 
638 
let val (env',flexflex,flexrigid) = 

639 
(if tdepth> !trace_bound andalso !trace_simp 

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

641 
SIMPL (env,dpairs)) 

642 
in case flexrigid of 

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

644 
 dp::frigid' => 

645 
if tdepth > !search_bound then 

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

647 
else 

648 
(if tdepth > !trace_bound then 

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

650 
else (); 

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

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

653 
end 

654 
handle CANTUNIFY => 

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

656 
Sequence.pull reseq)); 

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

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

660 
end; 

661 

662 
fun unifiers(params) = 

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

664 
handle Pattern.Unif => Sequence.null 

665 
 Pattern.Pattern => hounifiers(params); 

666 

667 

668 
(*For smash_flexflex1*) 

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

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

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

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

673 

674 

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

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

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

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

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

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

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

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

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

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

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

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

689 
end; 

690 

691 

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

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

694 
foldr smash_flexflex1 (tpairs, env); 

695 

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

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

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

699 

700 
end; 