Mercurial > urweb

comparison src/elaborate.sml @ 85:1f85890c9846

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness assumptions in expressions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 12:25:12 -0400
parents e86370850c30
children 7f9bcc8bfa1e
comparison
equal deleted inserted replaced
84:e86370850c30 85:1f85890c9846
241 val (t', tk, gs) = elabCon (env', D.enter denv) t 241 val (t', tk, gs) = elabCon (env', D.enter denv) t
242 in 242 in
243 checkKind env t' tk ktype; 243 checkKind env t' tk ktype;
244 ((L'.TCFun (e', x, k', t'), loc), ktype, gs) 244 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
245 end 245 end
246 | L.TDisjoint (c1, c2, c) =>
247 let
248 val (c1', k1, gs1) = elabCon (env, denv) c1
249 val (c2', k2, gs2) = elabCon (env, denv) c2
250
251 val ku1 = kunif loc
252 val ku2 = kunif loc
253
254 val denv' = D.assert env denv (c1', c2')
255 val (c', k, gs3) = elabCon (env, denv') c
256 in
257 checkKind env c1' k1 (L'.KRecord ku1, loc);
258 checkKind env c2' k2 (L'.KRecord ku2, loc);
259
260 ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3)
261 end
246 | L.TRecord c => 262 | L.TRecord c =>
247 let 263 let
248 val (c', ck, gs) = elabCon (env, denv) c 264 val (c', ck, gs) = elabCon (env, denv) c
249 val k = (L'.KRecord ktype, loc) 265 val k = (L'.KRecord ktype, loc)
250 in 266 in
489 505
490 fun kindof env (c, loc) = 506 fun kindof env (c, loc) =
491 case c of 507 case c of
492 L'.TFun _ => ktype 508 L'.TFun _ => ktype
493 | L'.TCFun _ => ktype 509 | L'.TCFun _ => ktype
510 | L'.TDisjoint _ => ktype
494 | L'.TRecord _ => ktype 511 | L'.TRecord _ => ktype
495 512
496 | L'.CRel xn => #2 (E.lookupCRel env xn) 513 | L'.CRel xn => #2 (E.lookupCRel env xn)
497 | L'.CNamed xn => #2 (E.lookupCNamed env xn) 514 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
498 | L'.CModProj (n, ms, x) => 515 | L'.CModProj (n, ms, x) =>
963 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e 980 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
964 in 981 in
965 ((L'.ECAbs (expl', x, k', e'), loc), 982 ((L'.ECAbs (expl', x, k', e'), loc),
966 (L'.TCFun (expl', x, k', et), loc), 983 (L'.TCFun (expl', x, k', et), loc),
967 gs) 984 gs)
985 end
986
987 | L.EDisjoint (c1, c2, e) =>
988 let
989 val (c1', k1, gs1) = elabCon (env, denv) c1
990 val (c2', k2, gs2) = elabCon (env, denv) c2
991
992 val ku1 = kunif loc
993 val ku2 = kunif loc
994
995 val denv' = D.assert env denv (c1', c2')
996 val (e', t, gs3) = elabExp (env, denv') e
997 in
998 checkKind env c1' k1 (L'.KRecord ku1, loc);
999 checkKind env c2' k2 (L'.KRecord ku2, loc);
1000
1001 (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3)
968 end 1002 end
969 1003
970 | L.ERecord xes => 1004 | L.ERecord xes =>
971 let 1005 let
972 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) => 1006 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>