### changeset 84:e86370850c30

Disjointness assumptions
author Adam Chlipala Tue, 01 Jul 2008 12:10:46 -0400 0a1baddd8ab2 1f85890c9846 src/disjoint.sml src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/disjoint.lac 11 files changed, 73 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
```--- a/src/disjoint.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/disjoint.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -114,7 +114,7 @@
CName s => NameC s :: acc
| CRel n => NameR n :: acc
| CNamed n => NameN n :: acc
-              | _ => Unknown :: acc
+              | _ => (print "Unknown name\n"; Unknown :: acc)

fun decomposeRow (c, acc) =
case #1 (hnormCon env c) of
@@ -122,7 +122,7 @@
| CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
| CRel n => RowR n :: acc
| CNamed n => RowN n :: acc
-              | _ => Unknown :: acc
+              | _ => (print "Unknown row\n"; Unknown :: acc)
in
decomposeRow (c, [])
end
@@ -265,6 +265,7 @@
fun prove1 denv (p1, p2) =
case (p1, p2) of
(NameC s1, NameC s2) => s1 <> s2
+      | (NameC _, _) => prove1' denv (p2, p1)
| (_, RowR _) => prove1' denv (p2, p1)
| (_, RowN _) => prove1' denv (p2, p1)
| _ => prove1' denv (p1, p2)```
```--- a/src/elab.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elab.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -55,6 +55,7 @@
| CModProj of int * string list * string
| CApp of con * con
| CAbs of string * kind * con
+       | CDisjoint of con * con * con

| CName of string
```
```--- a/src/elab_print.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elab_print.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -126,6 +126,15 @@
string "=>",
space,
p_con (E.pushCRel env x k) c])
+      | CDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
+                                                    space,
+                                                    string "~",
+                                                    space,
+                                                    p_con env c2,
+                                                    space,
+                                                    string "=>",
+                                                    space,
+                                                    p_con env c3])

| CName s => box [string "#", string s]
```
```--- a/src/elab_util.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elab_util.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -124,6 +124,14 @@
S.map2 (mfc (bind (ctx, Rel (x, k))) c,
fn c' =>
(CAbs (x, k', c'), loc)))
+              | CDisjoint (c1, c2, c3) =>
+                S.bind2 (mfc ctx c1,
+                      fn c1' =>
+                         S.bind2 (mfc ctx c2,
+                              fn c2' =>
+                                 S.map2 (mfc ctx c3,
+                                         fn c3' =>
+                                            (CDisjoint (c1', c2', c3'), loc))))

| CName _ => S.return2 cAll
```
```--- a/src/elaborate.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elaborate.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -306,6 +306,23 @@
gs)
end

+      | L.CDisjoint (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'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3)
+        end
+
| L.CName s =>
((L'.CName s, loc), kname, [])

@@ -498,6 +515,7 @@
| L'.KError => kerror
| _ => raise CUnify' (CKindof c))
| L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
+      | L'.CDisjoint (_, _, c) => kindof env c

| L'.CName _ => kname

@@ -1761,13 +1779,16 @@

val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
in
-        app (fn (loc, env, denv, (c1, c2)) =>
-                case D.prove env denv (c1, c2, loc) of
-                    [] => ()
-                  | _ =>
-                    (ErrorMsg.errorAt loc "Remaining constraint";
-                     eprefaces' [("Con 1", p_con env c1),
-                                 ("Con 2", p_con env c2)])) gs;
+        if ErrorMsg.anyErrors () then
+            ()
+        else
+            app (fn (loc, env, denv, (c1, c2)) =>
+                    case D.prove env denv (c1, c2, loc) of
+                        [] => ()
+                      | _ =>
+                        (ErrorMsg.errorAt loc "Remaining constraint";
+                         eprefaces' [("Con 1", p_con env c1),
+                                     ("Con 2", p_con env c2)])) gs;

(L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
end```
```--- a/src/explify.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/explify.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -56,6 +56,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.CName s => (L'.CName s, loc)
```
```--- a/src/lacweb.grm	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/lacweb.grm	Tue Jul 01 12:10:46 2008 -0400
@@ -43,7 +43,7 @@
| CON | LTYPE | VAL | FOLD | UNIT | KUNIT
| TYPE | NAME
| ARROW | LARROW | DARROW
- | FN | PLUSPLUS | DOLLAR
+ | FN | PLUSPLUS | DOLLAR | TWIDDLE
| STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN

%nonterm
@@ -93,6 +93,7 @@
%right COMMA
%right ARROW LARROW
%right PLUSPLUS
+%nonassoc TWIDDLE
%nonassoc DOLLAR
%left DOT

@@ -194,6 +195,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))

| LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
```
```--- a/src/lacweb.lex	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/lacweb.lex	Tue Jul 01 12:10:46 2008 -0400
@@ -142,6 +142,7 @@
<INITIAL> "#"         => (Tokens.HASH (pos yypos, pos yypos + size yytext));
<INITIAL> "__"        => (Tokens.UNDERUNDER (pos yypos, pos yypos + size yytext));
<INITIAL> "_"         => (Tokens.UNDER (pos yypos, pos yypos + size yytext));
+<INITIAL> "~"         => (Tokens.TWIDDLE (pos yypos, pos yypos + size yytext));

<INITIAL> "con"       => (Tokens.CON (pos yypos, pos yypos + size yytext));
<INITIAL> "type"      => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));```
```--- a/src/source.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/source.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -53,6 +53,7 @@
| CVar of string list * string
| CApp of con * con
| CAbs of string * kind option * con
+       | CDisjoint of con * con * con

| CName of string
```
```--- a/src/source_print.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/source_print.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -111,6 +111,15 @@
string "=>",
space,
p_con c])
+      | CDisjoint (c1, c2, c3) => parenIf par (box [p_con c1,
+                                                    space,
+                                                    string "~",
+                                                    space,
+                                                    p_con c2,
+                                                    space,
+                                                    string "=>",
+                                                    space,
+                                                    p_con c3])

| CName s => box [string "#", string s]
```
```--- a/tests/disjoint.lac	Tue Jul 01 11:39:14 2008 -0400
+++ b/tests/disjoint.lac	Tue Jul 01 12:10:46 2008 -0400
@@ -1,1 +1,9 @@
-con c = fn x :: Name => [x, A]
+con c1 = fn x :: Name => [x] ~ [A] => [x, A]
+con c2 = fn x :: Name => [x] ~ [A] => [A, x]
+con c3 = fn x :: Name => [A] ~ [x] => [x, A]
+con c4 = fn x :: Name => [A] ~ [x] => [A, x]
+
+con c5 = fn r1 :: {Type} => fn r2 => r1 ~ r2 => r1 ++ r2
+con c6 = fn r1 :: {Type} => fn r2 => r2 ~ r1 => r1 ++ r2
+
+con c7 = fn x :: Name => fn r => [x] ~ r => [x] ++ r```