Mercurial > urweb
changeset 85:1f85890c9846
Disjointness assumptions in expressions
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 01 Jul 2008 12:25:12 -0400 |
| parents | e86370850c30 |
| children | 7f9bcc8bfa1e |
| files | src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/source.sml src/source_print.sml tests/disjoint.lac |
| diffstat | 9 files changed, 78 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/elab.sml Tue Jul 01 12:25:12 2008 -0400 @@ -48,6 +48,7 @@ datatype con' = TFun of con * con | TCFun of explicitness * string * kind * con + | TDisjoint of con * con * con | TRecord of con | CRel of int
--- a/src/elab_print.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/elab_print.sml Tue Jul 01 12:25:12 2008 -0400 @@ -77,6 +77,15 @@ 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,
--- a/src/elab_util.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/elab_util.sml Tue Jul 01 12:25:12 2008 -0400 @@ -104,6 +104,14 @@ 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' =>
--- a/src/elaborate.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/elaborate.sml Tue Jul 01 12:25:12 2008 -0400 @@ -243,6 +243,22 @@ 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 @@ 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 @@ 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) =>
--- a/src/explify.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/explify.sml Tue Jul 01 12:25:12 2008 -0400 @@ -48,6 +48,7 @@ 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 @@ | 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)
--- a/src/lacweb.grm Tue Jul 01 12:10:46 2008 -0400 +++ b/src/lacweb.grm Tue Jul 01 12:25:12 2008 -0400 @@ -196,6 +196,7 @@ | 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 @@ | 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))
--- a/src/source.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/source.sml Tue Jul 01 12:25:12 2008 -0400 @@ -48,6 +48,7 @@ | 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 @@ | 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
--- a/src/source_print.sml Tue Jul 01 12:10:46 2008 -0400 +++ b/src/source_print.sml Tue Jul 01 12:25:12 2008 -0400 @@ -78,6 +78,15 @@ 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 @@ 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) =>
--- a/tests/disjoint.lac Tue Jul 01 12:10:46 2008 -0400 +++ b/tests/disjoint.lac Tue Jul 01 12:25:12 2008 -0400 @@ -7,3 +7,5 @@ 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