Disjointness assumptions

10 files changed, 64 insertions, 10 deletions

diff --git a/src/disjoint.sml b/src/disjoint.sml
index fa4c8618..c9f6d2e9 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -114,7 +114,7 @@ fun decomposeRow env c =
                 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 @@ fun decomposeRow env c =
               | 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) =
 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)
diff --git a/src/elab.sml b/src/elab.sml
index a7085fee..fe7c989e 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -55,6 +55,7 @@ datatype con' =
        | CModProj of int * string list * string
        | CApp of con * con
        | CAbs of string * kind * con
+       | CDisjoint of con * con * con
 
        | CName of string
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 01472ca7..05d216ca 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -126,6 +126,15 @@ fun p_con' par env (c, _) =
                                             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]
 
diff --git a/src/elab_util.sml b/src/elab_util.sml
index e9b7ddd9..63d035e8 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -124,6 +124,14 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                          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
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 73ebc43b..e311726a 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -306,6 +306,23 @@ fun elabCon (env, denv) (c, loc) =
              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 @@ fun kindof env (c, loc) =
            | 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 @@ fun elabFile basis env file =
 
         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
diff --git a/src/explify.sml b/src/explify.sml
index af655eb4..2ed66843 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -56,6 +56,7 @@ fun explifyCon (c, loc) =
 
       | 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)
 
diff --git a/src/lacweb.grm b/src/lacweb.grm
index b961ba85..39d30349 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -43,7 +43,7 @@ val s = ErrorMsg.spanOf
  | 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 @@ val s = ErrorMsg.spanOf
 %right COMMA
 %right ARROW LARROW
 %right PLUSPLUS
+%nonassoc TWIDDLE
 %nonassoc DOLLAR
 %left DOT
 
@@ -194,6 +195,7 @@ cexp   : capps                          (capps)
 
        | 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))
 
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 45e2f1f2..3fa0b45c 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -142,6 +142,7 @@ realconst = [0-9]+\.[0-9]*;
 <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));
diff --git a/src/source.sml b/src/source.sml
index e55e5901..10d174ab 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -53,6 +53,7 @@ datatype con' =
        | CVar of string list * string
        | CApp of con * con
        | CAbs of string * kind option * con
+       | CDisjoint of con * con * con
 
        | CName of string
 
diff --git a/src/source_print.sml b/src/source_print.sml
index 80b077d0..3e83dbe8 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -111,6 +111,15 @@ fun p_con' par (c, _) =
                                                  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]