Mercurial > urweb
diff src/elaborate.sml @ 85:1f85890c9846
Disjointness assumptions in expressions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 12:25:12 -0400 |
parents | e86370850c30 |
children | 7f9bcc8bfa1e |
line wrap: on
line diff
--- a/src/elaborate.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/elaborate.sml Tue Jul 01 12:25:12 2008 -0400 @@ -243,6 +243,22 @@ checkKind env t' tk ktype; ((L'.TCFun (e', x, k', t'), loc), ktype, gs) end + | L.TDisjoint (c1, c2, c) => + let + val (c1', k1, gs1) = elabCon (env, denv) c1 + val (c2', k2, gs2) = elabCon (env, denv) c2 + + val ku1 = kunif loc + val ku2 = kunif loc + + val denv' = D.assert env denv (c1', c2') + val (c', k, gs3) = elabCon (env, denv') c + in + checkKind env c1' k1 (L'.KRecord ku1, loc); + checkKind env c2' k2 (L'.KRecord ku2, loc); + + ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3) + end | L.TRecord c => let val (c', ck, gs) = elabCon (env, denv) c @@ -491,6 +507,7 @@ case c of L'.TFun _ => ktype | L'.TCFun _ => ktype + | L'.TDisjoint _ => ktype | L'.TRecord _ => ktype | L'.CRel xn => #2 (E.lookupCRel env xn) @@ -967,6 +984,23 @@ gs) end + | L.EDisjoint (c1, c2, e) => + let + val (c1', k1, gs1) = elabCon (env, denv) c1 + val (c2', k2, gs2) = elabCon (env, denv) c2 + + val ku1 = kunif loc + val ku2 = kunif loc + + val denv' = D.assert env denv (c1', c2') + val (e', t, gs3) = elabExp (env, denv') e + in + checkKind env c1' k1 (L'.KRecord ku1, loc); + checkKind env c2' k2 (L'.KRecord ku2, loc); + + (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3) + end + | L.ERecord xes => let val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>