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) =>