Mercurial > urweb

comparison src/elab_util.sml @ 1302:d008c4c43a0a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Flex kinds for type-level tuples; ::_ notation
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 13:07:38 -0400
parents b4480a56cab7
children c7b9a33c26c8
comparison
equal deleted inserted replaced
1301:4359e185d3af 1302:d008c4c43a0a
76 | KError => S.return2 kAll 76 | KError => S.return2 kAll
77 77
78 | KUnif (_, _, ref (SOME k)) => mfk' ctx k 78 | KUnif (_, _, ref (SOME k)) => mfk' ctx k
79 | KUnif _ => S.return2 kAll 79 | KUnif _ => S.return2 kAll
80 80
81 | KTupleUnif (_, _, ref (SOME k)) => mfk' ctx k
82 | KTupleUnif (loc, nks, r) =>
83 S.map2 (ListUtil.mapfold (fn (n, k) =>
84 S.map2 (mfk ctx k,
85 fn k' =>
86 (n, k'))) nks,
87 fn nks' =>
88 (KTupleUnif (loc, nks', r), loc))
89
90
81 | KRel _ => S.return2 kAll 91 | KRel _ => S.return2 kAll
82 | KFun (x, k) => 92 | KFun (x, k) =>
83 S.map2 (mfk (bind (ctx, x)) k, 93 S.map2 (mfk (bind (ctx, x)) k,
84 fn k' => 94 fn k' =>
85 (KFun (x, k'), loc)) 95 (KFun (x, k'), loc))
205 (CProj (c', n), loc)) 215 (CProj (c', n), loc))
206 216
207 | CError => S.return2 cAll 217 | CError => S.return2 cAll
208 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c 218 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
209 | CUnif _ => S.return2 cAll 219 | CUnif _ => S.return2 cAll
210 220
211 | CKAbs (x, c) => 221 | CKAbs (x, c) =>
212 S.map2 (mfc (bind (ctx, RelK x)) c, 222 S.map2 (mfc (bind (ctx, RelK x)) c,
213 fn c' => 223 fn c' =>
214 (CKAbs (x, c'), loc)) 224 (CKAbs (x, c'), loc))
215 | CKApp (c, k) => 225 | CKApp (c, k) =>