changeset 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
files src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/source.sml src/source_print.sml tests/disjoint.lac
diffstat 9 files changed, 78 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/elab.sml	Tue Jul 01 12:25:12 2008 -0400
@@ -48,6 +48,7 @@
 datatype con' =
          TFun of con * con
        | TCFun of explicitness * string * kind * con
+       | TDisjoint of con * con * con
        | TRecord of con
 
        | CRel of int
--- a/src/elab_print.sml	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/elab_print.sml	Tue Jul 01 12:25:12 2008 -0400
@@ -77,6 +77,15 @@
                                                 string "->",
                                                 space,
                                                 p_con (E.pushCRel env x k) c])
+      | TDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
+                                                    space,
+                                                    string "~",
+                                                    space,
+                                                    p_con env c2,
+                                                    space,
+                                                    string "->",
+                                                    space,
+                                                    p_con env c3])
       | TRecord (CRecord (_, xcs), _) => box [string "{",
                                               p_list (fn (x, c) =>
                                                          box [p_name env x,
--- a/src/elab_util.sml	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/elab_util.sml	Tue Jul 01 12:25:12 2008 -0400
@@ -104,6 +104,14 @@
                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
                               fn c' =>
                                  (TCFun (e, x, k', c'), loc)))
+              | TDisjoint (c1, c2, c3) =>
+                S.bind2 (mfc ctx c1,
+                      fn c1' =>
+                         S.bind2 (mfc ctx c2,
+                              fn c2' =>
+                                 S.map2 (mfc ctx c3,
+                                         fn c3' =>
+                                            (TDisjoint (c1', c2', c3'), loc))))
               | TRecord c =>
                 S.map2 (mfc ctx c,
                         fn c' =>
--- 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) =>
--- a/src/explify.sml	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/explify.sml	Tue Jul 01 12:25:12 2008 -0400
@@ -48,6 +48,7 @@
     case c of
         L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
       | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc)
+      | L.TDisjoint (_, _, c) => explifyCon c
       | L.TRecord c => (L'.TRecord (explifyCon c), loc)
 
       | L.CRel n => (L'.CRel n, loc)
@@ -56,7 +57,7 @@
 
       | L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc)
       | L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc)
-      | L.CDisjoint _ => raise Fail "Explify CDisjoint"
+      | L.CDisjoint (_, _, c) => explifyCon c
 
       | L.CName s => (L'.CName s, loc)
 
--- a/src/lacweb.grm	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/lacweb.grm	Tue Jul 01 12:25:12 2008 -0400
@@ -196,6 +196,7 @@
        | FN SYMBOL DARROW cexp          (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright))
        | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright))
        | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
+       | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
 
        | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
 
@@ -245,6 +246,7 @@
        | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright))
        | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright))
        | FN SYMBOL DARROW eexp          (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright))
+       | FN cterm TWIDDLE cterm DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (cterm1left, eexpright))
 
        | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
        | eterm DOT ident                (EField (eterm, ident), s (etermleft, identright))
--- a/src/source.sml	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/source.sml	Tue Jul 01 12:25:12 2008 -0400
@@ -48,6 +48,7 @@
 
        | TFun of con * con
        | TCFun of explicitness * string * kind * con
+       | TDisjoint of con * con * con
        | TRecord of con
 
        | CVar of string list * string
@@ -94,6 +95,7 @@
        | EAbs of string * con option * exp
        | ECApp of exp * con
        | ECAbs of explicitness * string * kind * exp
+       | EDisjoint of con * con * exp
 
        | ERecord of (con * exp) list
        | EField of exp * con
--- a/src/source_print.sml	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/source_print.sml	Tue Jul 01 12:25:12 2008 -0400
@@ -78,6 +78,15 @@
                                                 string "->",
                                                 space,
                                                 p_con c])
+      | TDisjoint (c1, c2, c3) => parenIf par (box [p_con c1,
+                                                    space,
+                                                    string "~",
+                                                    space,
+                                                    p_con c2,
+                                                    space,
+                                                    string "->",
+                                                    space,
+                                                    p_con c3])
       | TRecord (CRecord xcs, _) => box [string "{",
                                          p_list (fn (x, c) =>
                                                     box [p_name x,
@@ -202,6 +211,15 @@
                                                   string "=>",
                                                   space,
                                                   p_exp e])
+      | EDisjoint (c1, c2, e) => parenIf par (box [p_con c1,
+                                                   space,
+                                                   string "~",
+                                                   space,
+                                                   p_con c2,
+                                                   space,
+                                                   string "=>",
+                                                   space,
+                                                   p_exp e])
 
       | ERecord xes => box [string "{",
                             p_list (fn (x, e) =>
--- a/tests/disjoint.lac	Tue Jul 01 12:10:46 2008 -0400
+++ b/tests/disjoint.lac	Tue Jul 01 12:25:12 2008 -0400
@@ -7,3 +7,5 @@
 con c6 = fn r1 :: {Type} => fn r2 => r2 ~ r1 => r1 ++ r2
 
 con c7 = fn x :: Name => fn r => [x] ~ r => [x] ++ r
+
+val v1 = fn x :: Name => fn [x] ~ [A] => fn y : {x : int, A : string} => y.x