--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/disjoint.sig	Tue Jul 01 10:55:38 2008 -0400
@@ -0,0 +1,38 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature DISJOINT = sig
+    
+    type env
+
+    val empty : env
+    val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env
+    val enter : env -> env
+
+    val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> (Elab.con * Elab.con) list
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/disjoint.sml	Tue Jul 01 10:55:38 2008 -0400
@@ -0,0 +1,294 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure Disjoint :> DISJOINT = struct
+
+open Elab
+open ElabOps
+
+structure SS = BinarySetFn(struct
+                           type ord_key = string
+                           val compare = String.compare
+                           end)
+
+structure IS = IntBinarySet
+structure IM = IntBinaryMap
+
+type name_ineqs = {
+     namesC : SS.set,
+     namesR : IS.set,
+     namesN : IS.set
+}
+
+val name_default = {
+    namesC = SS.empty,
+    namesR = IS.empty,
+    namesN = IS.empty
+}
+
+type row_ineqs = {
+     namesC : SS.set,
+     namesR : IS.set,
+     namesN : IS.set,
+     rowsR : IS.set,
+     rowsN : IS.set
+}
+
+val row_default = {
+    namesC = SS.empty,
+    namesR = IS.empty,
+    namesN = IS.empty,
+    rowsR = IS.empty,
+    rowsN = IS.empty
+}
+
+fun nameToRow_ineqs {namesC, namesR, namesN} =
+    {namesC = namesC,
+     namesR = namesR,
+     namesN = namesN,
+     rowsR = IS.empty,
+     rowsN = IS.empty}
+
+type env = {
+     namesR : name_ineqs IM.map,
+     namesN : name_ineqs IM.map,
+     rowsR : row_ineqs IM.map,
+     rowsN : row_ineqs IM.map
+}
+
+val empty = {
+    namesR = IM.empty,
+    namesN = IM.empty,
+    rowsR = IM.empty,
+    rowsN = IM.empty
+}
+
+datatype piece =
+         NameC of string
+       | NameR of int
+       | NameN of int
+       | RowR of int
+       | RowN of int
+       | Unknown
+
+fun nameToRow (c, loc) =
+    (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
+
+fun pieceToRow (p, loc) =
+    case p of
+        NameC s => nameToRow (CName s, loc)
+      | NameR n => nameToRow (CRel n, loc)
+      | NameN n => nameToRow (CNamed n, loc)
+      | RowR n => (CRel n, loc)
+      | RowN n => (CRel n, loc)
+      | Unknown => raise Fail "Unknown to row"
+
+fun decomposeRow env c =
+    let
+        fun decomposeName (c, acc) =
+            case #1 (hnormCon env c) of
+                CName s => NameC s :: acc
+              | CRel n => NameR n :: acc
+              | CNamed n => NameN n :: acc
+              | _ => Unknown :: acc
+                     
+        fun decomposeRow (c, acc) =
+            case #1 (hnormCon env c) of
+                CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
+              | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
+              | CRel n => RowR n :: acc
+              | CNamed n => RowN n :: acc
+              | _ => Unknown :: acc
+    in
+        decomposeRow (c, [])
+    end
+
+fun assertPiece_name (ps, ineqs : name_ineqs) =
+    {namesC = foldl (fn (p', namesC) =>
+                        case p' of
+                            NameC s => SS.add (namesC, s)
+                          | _ => namesC) (#namesC ineqs) ps,
+     namesR = foldl (fn (p', namesR) =>
+                        case p' of
+                            NameR n => IS.add (namesR, n)
+                          | _ => namesR) (#namesR ineqs) ps,
+     namesN = foldl (fn (p', namesN) =>
+                        case p' of
+                            NameN n => IS.add (namesN, n)
+                          | _ => namesN) (#namesN ineqs) ps}
+
+fun assertPiece_row (ps, ineqs : row_ineqs) =
+    {namesC = foldl (fn (p', namesC) =>
+                        case p' of
+                            NameC s => SS.add (namesC, s)
+                          | _ => namesC) (#namesC ineqs) ps,
+     namesR = foldl (fn (p', namesR) =>
+                        case p' of
+                            NameR n => IS.add (namesR, n)
+                          | _ => namesR) (#namesR ineqs) ps,
+     namesN = foldl (fn (p', namesN) =>
+                        case p' of
+                            NameN n => IS.add (namesN, n)
+                          | _ => namesN) (#namesN ineqs) ps,
+     rowsR = foldl (fn (p', rowsR) =>
+                        case p' of
+                            RowR n => IS.add (rowsR, n)
+                          | _ => rowsR) (#rowsR ineqs) ps,
+     rowsN = foldl (fn (p', rowsN) =>
+                        case p' of
+                            RowN n => IS.add (rowsN, n)
+                          | _ => rowsN) (#rowsN ineqs) ps}
+
+fun assertPiece ps (p, denv) =
+    case p of
+        Unknown => denv
+      | NameC _ => denv
+
+      | NameR n =>
+        let
+            val ineqs = Option.getOpt (IM.find (#namesR denv, n), name_default)
+            val ineqs = assertPiece_name (ps, ineqs)
+        in
+            {namesR = IM.insert (#namesR denv, n, ineqs),
+             namesN = #namesN denv,
+             rowsR = #rowsR denv,
+             rowsN = #rowsN denv}
+        end
+
+      | NameN n =>
+        let
+            val ineqs = Option.getOpt (IM.find (#namesN denv, n), name_default)
+            val ineqs = assertPiece_name (ps, ineqs)
+        in
+            {namesR = #namesR denv,
+             namesN = IM.insert (#namesN denv, n, ineqs),
+             rowsR = #rowsR denv,
+             rowsN = #rowsN denv}
+        end
+
+      | RowR n =>
+        let
+            val ineqs = Option.getOpt (IM.find (#rowsR denv, n), row_default)
+            val ineqs = assertPiece_row (ps, ineqs)
+        in
+            {namesR = #namesR denv,
+             namesN = #namesN denv,
+             rowsR = IM.insert (#rowsR denv, n, ineqs),
+             rowsN = #rowsN denv}
+        end
+
+      | RowN n =>
+        let
+            val ineqs = Option.getOpt (IM.find (#rowsN denv, n), row_default)
+            val ineqs = assertPiece_row (ps, ineqs)
+        in
+            {namesR = #namesR denv,
+             namesN = #namesN denv,
+             rowsR = #rowsR denv,
+             rowsN = IM.insert (#rowsN denv, n, ineqs)}
+        end
+
+fun assert env denv (c1, c2) =
+    let
+        val ps1 = decomposeRow env c1
+        val ps2 = decomposeRow env c2
+
+        val denv = foldl (assertPiece ps2) denv ps1
+    in
+        foldl (assertPiece ps1) denv ps2
+    end
+
+fun nameEnter {namesC, namesR, namesN} =
+    {namesC = namesC,
+     namesR = IS.map (fn n => n + 1) namesR,
+     namesN = namesN}
+
+fun rowEnter {namesC, namesR, namesN, rowsR, rowsN} =
+    {namesC = namesC,
+     namesR = IS.map (fn n => n + 1) namesR,
+     namesN = namesN,
+     rowsR = IS.map (fn n => n + 1) rowsR,
+     rowsN = rowsN}
+
+fun enter {namesR, namesN, rowsR, rowsN} =
+    {namesR = IM.foldli (fn (n, ineqs, namesR) => IM.insert (namesR, n+1, nameEnter ineqs)) IM.empty namesR,
+     namesN = IM.map nameEnter namesN,
+     rowsR = IM.foldli (fn (n, ineqs, rowsR) => IM.insert (rowsR, n+1, rowEnter ineqs)) IM.empty rowsR,
+     rowsN = IM.map rowEnter rowsN}
+
+fun getIneqs (denv : env) p =
+    case p of
+        Unknown => raise Fail "getIneqs: Unknown"
+      | NameC _ => raise Fail "getIneqs: NameC"
+      | NameR n => nameToRow_ineqs (Option.getOpt (IM.find (#namesR denv, n), name_default))
+      | NameN n => nameToRow_ineqs (Option.getOpt (IM.find (#namesN denv, n), name_default))
+      | RowR n => Option.getOpt (IM.find (#rowsR denv, n), row_default)
+      | RowN n => Option.getOpt (IM.find (#rowsN denv, n), row_default)
+
+fun prove1' denv (p1, p2) =
+    let
+        val {namesC, namesR, namesN, rowsR, rowsN} = getIneqs denv p1
+    in
+        case p2 of
+            Unknown => raise Fail "prove1': Unknown"
+          | NameC s => SS.member (namesC, s)
+          | NameR n => IS.member (namesR, n)
+          | NameN n => IS.member (namesN, n)
+          | RowR n => IS.member (rowsR, n)
+          | RowN n => IS.member (rowsN, n)
+    end
+
+fun prove1 denv (p1, p2) =
+    case (p1, p2) of
+        (NameC s1, NameC s2) => s1 <> s2
+      | (_, RowR _) => prove1' denv (p2, p1)
+      | (_, RowN _) => prove1' denv (p2, p1)
+      | _ => prove1' denv (p1, p2)
+
+fun prove env denv (c1, c2, loc) =
+    let
+        val ps1 = decomposeRow env c1
+        val ps2 = decomposeRow env c2
+
+        val hasUnknown = List.exists (fn p => p = Unknown)
+    in
+        if hasUnknown ps1 orelse hasUnknown ps2 then
+            (ErrorMsg.errorAt loc "Structure of row is too complicated to prove disjointness";
+             Print.eprefaces' [("Row 1", ElabPrint.p_con env c1),
+                               ("Row 2", ElabPrint.p_con env c2)];
+             [])
+        else
+            foldl (fn (p1, rem) =>
+                      foldl (fn (p2, rem) =>
+                                if prove1 denv (p1, p2) then
+                                    rem
+                                else
+                                    (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
+            [] ps1
+    end
+
+end

--- a/src/elab.sml	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/elab.sml	Tue Jul 01 10:55:38 2008 -0400
@@ -34,6 +34,7 @@
        | KArrow of kind * kind
        | KName
        | KRecord of kind
+       | KUnit
 
        | KError
        | KUnif of ErrorMsg.span * string * kind option ref
@@ -61,6 +62,8 @@
        | CConcat of con * con
        | CFold of kind * kind
 
+       | CUnit
+
        | CError
        | CUnif of ErrorMsg.span * kind * string * con option ref
 

--- a/src/elab_print.sml	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/elab_print.sml	Tue Jul 01 10:55:38 2008 -0400
@@ -48,6 +48,7 @@
                                              p_kind k2])
       | KName => string "Name"
       | KRecord k => box [string "{", p_kind k, string "}"]
+      | KUnit => string "Unit"
 
       | KError => string "<ERROR>"
       | KUnif (_, _, ref (SOME k)) => p_kind' par k
@@ -155,6 +156,8 @@
                                               p_con env c2])
       | CFold _ => string "fold"
 
+      | CUnit => string "()"
+
       | CError => string "<ERROR>"
       | CUnif (_, _, _, ref (SOME c)) => p_con' par env c
       | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),

--- a/src/elab_util.sml	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/elab_util.sml	Tue Jul 01 10:55:38 2008 -0400
@@ -56,6 +56,8 @@
                         fn k' =>
                            (KRecord k', loc))
 
+              | KUnit => S.return2 kAll
+
               | KError => S.return2 kAll
 
               | KUnif (_, _, ref (SOME k)) => mfk' k
@@ -150,6 +152,8 @@
                                     fn k2' =>
                                        (CFold (k1', k2'), loc)))
 
+              | CUnit => S.return2 cAll
+
               | CError => S.return2 cAll
               | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
               | CUnif _ => S.return2 cAll

--- a/src/elaborate.sml	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/elaborate.sml	Tue Jul 01 10:55:38 2008 -0400
@@ -32,6 +32,7 @@
 structure L' = Elab
 structure E = ElabEnv
 structure U = ElabUtil
+structure D = Disjoint
 
 open Print
 open ElabPrint
@@ -73,6 +74,8 @@
     in
         case (k1, k2) of
             (L'.KType, L'.KType) => ()
+          | (L'.KUnit, L'.KUnit) => ()
+
           | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
             (unifyKinds' d1 d2;
              unifyKinds' r1 r2)
@@ -199,6 +202,7 @@
       | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
       | L.KName => (L'.KName, loc)
       | L.KRecord k => (L'.KRecord (elabKind k), loc)
+      | L.KUnit => (L'.KUnit, loc)
       | L.KWild => kunif loc
 
 fun foldKind (dom, ran, loc)=
@@ -330,6 +334,10 @@
             val ku = kunif loc
             val k = (L'.KRecord ku, loc)
         in
+            case D.prove env D.empty (c1', c2', loc) of
+                [] => ()
+              | _ => raise Fail "Can't prove disjointness";
+
             checkKind env c1' k1 k;
             checkKind env c2' k2 k;
             ((L'.CConcat (c1', c2'), loc), k)
@@ -343,6 +351,8 @@
              foldKind (dom, ran, loc))
         end
 
+      | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc))
+
       | L.CWild k =>
         let
             val k' = elabKind k
@@ -478,6 +488,8 @@
       | L'.CConcat (c, _) => kindof env c
       | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
 
+      | L'.CUnit => (L'.KUnit, loc)
+
       | L'.CError => kerror
       | L'.CUnif (_, k, _, _) => k
 

--- a/src/explify.sml	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/explify.sml	Tue Jul 01 10:55:38 2008 -0400
@@ -38,6 +38,8 @@
       | L.KName => (L'.KName, loc)
       | L.KRecord k => (L'.KRecord (explifyKind k), loc)
 
+      | L.KUnit => raise Fail "Explify KUnit"
+
       | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
       | L.KUnif (_, _, ref (SOME k)) => explifyKind k
       | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
@@ -61,6 +63,8 @@
       | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)
       | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc)
 
+      | L.CUnit => raise Fail "Explify CUnit"
+
       | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
       | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
       | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)

--- a/src/lacweb.grm	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/lacweb.grm	Tue Jul 01 10:55:38 2008 -0400
@@ -40,7 +40,7 @@
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
- | CON | LTYPE | VAL | FOLD
+ | CON | LTYPE | VAL | FOLD | UNIT | KUNIT
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | DOLLAR
@@ -179,6 +179,7 @@
        | LBRACE kind RBRACE             (KRecord kind, s (LBRACEleft, RBRACEright))
        | kind ARROW kind                (KArrow (kind1, kind2), s (kind1left, kind2right))
        | LPAREN kind RPAREN             (#1 kind, s (LPARENleft, RPARENright))
+       | KUNIT                          (KUnit, s (KUNITleft, KUNITright))
        | UNDERUNDER                     (KWild, s (UNDERUNDERleft, UNDERUNDERright))
 
 capps  : cterm                          (cterm)
@@ -216,6 +217,7 @@
        | path                           (CVar path, s (pathleft, pathright))
        | UNDER                          (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
        | FOLD                           (CFold, s (FOLDleft, FOLDright))
+       | UNIT                           (CUnit, s (UNITleft, UNITright))
 
 rcon   :                                ([])
        | ident EQ cexp                  ([(ident, cexp)])

--- a/src/lacweb.lex	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/lacweb.lex	Tue Jul 01 10:55:38 2008 -0400
@@ -120,6 +120,7 @@
 			  str := #"\n" :: !str; continue());
 <STRING> .            => (str := String.sub (yytext, 0) :: !str; continue());
 
+<INITIAL> "()"        => (Tokens.UNIT (pos yypos, pos yypos + size yytext));
 <INITIAL> "("         => (Tokens.LPAREN (pos yypos, pos yypos + size yytext));
 <INITIAL> ")"         => (Tokens.RPAREN (pos yypos, pos yypos + size yytext));
 <INITIAL> "["         => (Tokens.LBRACK (pos yypos, pos yypos + size yytext));
@@ -161,6 +162,7 @@
 
 <INITIAL> "Type"      => (Tokens.TYPE (pos yypos, pos yypos + size yytext));
 <INITIAL> "Name"      => (Tokens.NAME (pos yypos, pos yypos + size yytext));
+<INITIAL> "Unit"      => (Tokens.KUNIT (pos yypos, pos yypos + size yytext));
 
 <INITIAL> {id}        => (Tokens.SYMBOL (yytext, pos yypos, pos yypos + size yytext));
 <INITIAL> {cid}       => (Tokens.CSYMBOL (yytext, pos yypos, pos yypos + size yytext));

--- a/src/source.sml	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/source.sml	Tue Jul 01 10:55:38 2008 -0400
@@ -34,6 +34,7 @@
        | KArrow of kind * kind
        | KName
        | KRecord of kind
+       | KUnit
        | KWild
 
 withtype kind = kind' located
@@ -59,6 +60,8 @@
        | CConcat of con * con
        | CFold
 
+       | CUnit
+
        | CWild of kind
 
 withtype con = con' located

--- a/src/source_print.sml	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/source_print.sml	Tue Jul 01 10:55:38 2008 -0400
@@ -44,6 +44,7 @@
                                              p_kind k2])
       | KName => string "Name"
       | KRecord k => box [string "{", p_kind k, string "}"]
+      | KUnit => string "Unit"
       | KWild => string "_"
 
 and p_kind k = p_kind' false k
@@ -127,6 +128,9 @@
                                               space,
                                               p_con c2])
       | CFold => string "fold"
+
+      | CUnit => string "()"
+
       | CWild k => box [string "(_",
                         space,
                         string "::",

--- a/src/sources	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/sources	Tue Jul 01 10:55:38 2008 -0400
@@ -35,6 +35,9 @@
 elab_ops.sig
 elab_ops.sml
 
+disjoint.sig
+disjoint.sml
+
 elaborate.sig
 elaborate.sml
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/disjoint.lac	Tue Jul 01 10:55:38 2008 -0400
@@ -0,0 +1,1 @@
+con c = [A = ()] ++ [A = ()]