Mercurial > urweb
comparison src/elab_util.sml @ 1639:6c00d8af6239
Add a new scoping check for unification variables, to fix a type inference bug
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 18 Dec 2011 11:29:13 -0500 |
parents | c37d8341940a |
children | 4a03aa3251cb |
comparison
equal
deleted
inserted
replaced
1638:3bf727a08db8 | 1639:6c00d8af6239 |
---|---|
73 fn ks' => | 73 fn ks' => |
74 (KTuple ks', loc)) | 74 (KTuple ks', loc)) |
75 | 75 |
76 | KError => S.return2 kAll | 76 | KError => S.return2 kAll |
77 | 77 |
78 | KUnif (_, _, ref (SOME k)) => mfk' ctx k | 78 | KUnif (_, _, ref (KKnown k)) => mfk' ctx k |
79 | KUnif _ => S.return2 kAll | 79 | KUnif _ => S.return2 kAll |
80 | 80 |
81 | KTupleUnif (_, _, ref (SOME k)) => mfk' ctx k | 81 | KTupleUnif (_, _, ref (KKnown k)) => mfk' ctx k |
82 | KTupleUnif (loc, nks, r) => | 82 | KTupleUnif (loc, nks, r) => |
83 S.map2 (ListUtil.mapfold (fn (n, k) => | 83 S.map2 (ListUtil.mapfold (fn (n, k) => |
84 S.map2 (mfk ctx k, | 84 S.map2 (mfk ctx k, |
85 fn k' => | 85 fn k' => |
86 (n, k'))) nks, | 86 (n, k'))) nks, |
215 S.map2 (mfc ctx c, | 215 S.map2 (mfc ctx c, |
216 fn c' => | 216 fn c' => |
217 (CProj (c', n), loc)) | 217 (CProj (c', n), loc)) |
218 | 218 |
219 | CError => S.return2 cAll | 219 | CError => S.return2 cAll |
220 | CUnif (nl, _, _, _, ref (SOME c)) => mfc' ctx (!mliftConInCon nl c) | 220 | CUnif (nl, _, _, _, ref (Known c)) => mfc' ctx (!mliftConInCon nl c) |
221 | CUnif _ => S.return2 cAll | 221 | CUnif _ => S.return2 cAll |
222 | 222 |
223 | CKAbs (x, c) => | 223 | CKAbs (x, c) => |
224 S.map2 (mfc (bind (ctx, RelK x)) c, | 224 S.map2 (mfc (bind (ctx, RelK x)) c, |
225 fn c' => | 225 fn c' => |
253 fun map {kind, con} s = | 253 fun map {kind, con} s = |
254 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), | 254 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), |
255 con = fn c => fn () => S.Continue (con c, ())} s () of | 255 con = fn c => fn () => S.Continue (con c, ())} s () of |
256 S.Return () => raise Fail "ElabUtil.Con.map: Impossible" | 256 S.Return () => raise Fail "ElabUtil.Con.map: Impossible" |
257 | S.Continue (s, ()) => s | 257 | S.Continue (s, ()) => s |
258 | |
259 fun appB {kind, con, bind} ctx c = | |
260 case mapfoldB {kind = fn ctx => fn k => fn () => (kind ctx k; S.Continue (k, ())), | |
261 con = fn ctx => fn c => fn () => (con ctx c; S.Continue (c, ())), | |
262 bind = bind} ctx c () of | |
263 S.Continue _ => () | |
264 | S.Return _ => raise Fail "ElabUtil.Con.appB: Impossible" | |
265 | |
266 fun app {kind, con} s = | |
267 case mapfold {kind = fn k => fn () => (kind k; S.Continue (k, ())), | |
268 con = fn c => fn () => (con c; S.Continue (c, ()))} s () of | |
269 S.Return () => raise Fail "ElabUtil.Con.app: Impossible" | |
270 | S.Continue _ => () | |
258 | 271 |
259 fun existsB {kind, con, bind} ctx c = | 272 fun existsB {kind, con, bind} ctx c = |
260 case mapfoldB {kind = fn ctx => fn k => fn () => | 273 case mapfoldB {kind = fn ctx => fn k => fn () => |
261 if kind (ctx, k) then | 274 if kind (ctx, k) then |
262 S.Return () | 275 S.Return () |