summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/disjoint.sig38
-rw-r--r--src/disjoint.sml294
-rw-r--r--src/elab.sml3
-rw-r--r--src/elab_print.sml3
-rw-r--r--src/elab_util.sml4
-rw-r--r--src/elaborate.sml12
-rw-r--r--src/explify.sml4
-rw-r--r--src/lacweb.grm4
-rw-r--r--src/lacweb.lex2
-rw-r--r--src/source.sml3
-rw-r--r--src/source_print.sml4
-rw-r--r--src/sources3
-rw-r--r--tests/disjoint.lac1
13 files changed, 374 insertions, 1 deletions
diff --git a/src/disjoint.sig b/src/disjoint.sig
new file mode 100644
index 00000000..16afa885
--- /dev/null
+++ b/src/disjoint.sig
@@ -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
diff --git a/src/disjoint.sml b/src/disjoint.sml
new file mode 100644
index 00000000..784bd635
--- /dev/null
+++ b/src/disjoint.sml
@@ -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
diff --git a/src/elab.sml b/src/elab.sml
index 1b0e3ea1..a7085fee 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -34,6 +34,7 @@ datatype kind' =
| KArrow of kind * kind
| KName
| KRecord of kind
+ | KUnit
| KError
| KUnif of ErrorMsg.span * string * kind option ref
@@ -61,6 +62,8 @@ datatype con' =
| CConcat of con * con
| CFold of kind * kind
+ | CUnit
+
| CError
| CUnif of ErrorMsg.span * kind * string * con option ref
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 8c51be11..01472ca7 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -48,6 +48,7 @@ fun p_kind' par (k, _) =
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 @@ fun p_con' par env (c, _) =
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 ^ "::"),
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 45446a4e..e9b7ddd9 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -56,6 +56,8 @@ fun mapfold f =
fn k' =>
(KRecord k', loc))
+ | KUnit => S.return2 kAll
+
| KError => S.return2 kAll
| KUnif (_, _, ref (SOME k)) => mfk' k
@@ -150,6 +152,8 @@ fun mapfoldB {kind = fk, con = fc, bind} =
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
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 4323677d..0e9696b9 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -32,6 +32,7 @@ structure L = Source
structure L' = Elab
structure E = ElabEnv
structure U = ElabUtil
+structure D = Disjoint
open Print
open ElabPrint
@@ -73,6 +74,8 @@ fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
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 @@ fun elabKind (k, loc) =
| 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 @@ fun elabCon env (c, loc) =
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 @@ fun elabCon env (c, loc) =
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 @@ fun kindof env (c, loc) =
| 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
diff --git a/src/explify.sml b/src/explify.sml
index 0f416067..af655eb4 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -38,6 +38,8 @@ fun explifyKind (k, loc) =
| 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 @@ fun explifyCon (c, loc) =
| 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)
diff --git a/src/lacweb.grm b/src/lacweb.grm
index c42b5eb5..91285e4c 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -40,7 +40,7 @@ val s = ErrorMsg.spanOf
| 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 @@ kind : TYPE (KType, s (TYPEleft, TYPEright))
| 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 @@ cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright))
| 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)])
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 038e591f..45e2f1f2 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -120,6 +120,7 @@ realconst = [0-9]+\.[0-9]*;
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 @@ realconst = [0-9]+\.[0-9]*;
<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));
diff --git a/src/source.sml b/src/source.sml
index d36e86ca..e55e5901 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -34,6 +34,7 @@ datatype kind' =
| KArrow of kind * kind
| KName
| KRecord of kind
+ | KUnit
| KWild
withtype kind = kind' located
@@ -59,6 +60,8 @@ datatype con' =
| CConcat of con * con
| CFold
+ | CUnit
+
| CWild of kind
withtype con = con' located
diff --git a/src/source_print.sml b/src/source_print.sml
index aa880e08..80b077d0 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -44,6 +44,7 @@ fun p_kind' par (k, _) =
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 @@ fun p_con' par (c, _) =
space,
p_con c2])
| CFold => string "fold"
+
+ | CUnit => string "()"
+
| CWild k => box [string "(_",
space,
string "::",
diff --git a/src/sources b/src/sources
index 03b8f344..20bb2011 100644
--- a/src/sources
+++ b/src/sources
@@ -35,6 +35,9 @@ elab_print.sml
elab_ops.sig
elab_ops.sml
+disjoint.sig
+disjoint.sml
+
elaborate.sig
elaborate.sml
diff --git a/tests/disjoint.lac b/tests/disjoint.lac
new file mode 100644
index 00000000..805b9674
--- /dev/null
+++ b/tests/disjoint.lac
@@ -0,0 +1 @@
+con c = [A = ()] ++ [A = ()]
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 12:51:24 +0000