diff options
author | 2008-07-01 12:25:12 -0400 | |
---|---|---|
committer | 2008-07-01 12:25:12 -0400 | |
commit | f7d2bdce780d0333431829a8a788bdb208c0dcbc (patch) | |
tree | 5316084519f313741563c016ac6733d03f892475 | |
parent | 7628e1d8f7f8199531c9bc08a774c9a9e2bc5d63 (diff) |
Disjointness assumptions in expressions
-rw-r--r-- | src/elab.sml | 1 | ||||
-rw-r--r-- | src/elab_print.sml | 9 | ||||
-rw-r--r-- | src/elab_util.sml | 8 | ||||
-rw-r--r-- | src/elaborate.sml | 34 | ||||
-rw-r--r-- | src/explify.sml | 3 | ||||
-rw-r--r-- | src/lacweb.grm | 2 | ||||
-rw-r--r-- | src/source.sml | 2 | ||||
-rw-r--r-- | src/source_print.sml | 18 | ||||
-rw-r--r-- | tests/disjoint.lac | 2 |
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 |