summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_print.sml9
-rw-r--r--src/elab_util.sml8
-rw-r--r--src/elaborate.sml34
-rw-r--r--src/explify.sml3
-rw-r--r--src/lacweb.grm2
-rw-r--r--src/source.sml2
-rw-r--r--src/source_print.sml18
-rw-r--r--tests/disjoint.lac2
9 files changed, 78 insertions, 1 deletions
diff --git a/src/elab.sml b/src/elab.sml
index fe7c989e..cf9a7e7a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -48,6 +48,7 @@ datatype explicitness =
datatype con' =
TFun of con * con
| TCFun of explicitness * string * kind * con
+ | TDisjoint of con * con * con
| TRecord of con
| CRel of int
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 05d216ca..c90a0494 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -77,6 +77,15 @@ fun p_con' par env (c, _) =
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,
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 63d035e8..65906c72 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -104,6 +104,14 @@ fun mapfoldB {kind = fk, con = fc, bind} =
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' =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index e311726a..7d238368 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -243,6 +243,22 @@ fun elabCon (env, denv) (c, loc) =
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 @@ fun kindof env (c, loc) =
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 @@ fun elabExp (env, denv) (e, loc) =
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) =>
diff --git a/src/explify.sml b/src/explify.sml
index 2ed66843..0fa3698b 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -48,6 +48,7 @@ fun explifyCon (c, loc) =
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 @@ 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.CDisjoint (_, _, c) => explifyCon c
| L.CName s => (L'.CName s, loc)
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 39d30349..4bf03388 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -196,6 +196,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))
+ | 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 @@ eexp : eapps (eapps)
| 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))
diff --git a/src/source.sml b/src/source.sml
index 10d174ab..0b168dd0 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -48,6 +48,7 @@ datatype con' =
| 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 @@ datatype exp' =
| 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
diff --git a/src/source_print.sml b/src/source_print.sml
index 3e83dbe8..41051c81 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -78,6 +78,15 @@ fun p_con' par (c, _) =
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 @@ fun p_exp' par (e, _) =
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) =>
diff --git a/tests/disjoint.lac b/tests/disjoint.lac
index 4fd70d63..fcc86fa5 100644
--- a/tests/disjoint.lac
+++ b/tests/disjoint.lac
@@ -7,3 +7,5 @@ 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
+
+val v1 = fn x :: Name => fn [x] ~ [A] => fn y : {x : int, A : string} => y.x
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-10 17:09:07 +0000