Mercurial > urweb

comparison src/elab_util.sml @ 1639:6c00d8af6239

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 ()