# HG changeset patch # User Adam Chlipala # Date 1214928646 14400 # Node ID e86370850c30f4a2012646aa323eb8ef1ff93127 # Parent 0a1baddd8ab2ca7e6ae6109fa98d7492f3b10a40 Disjointness assumptions diff -r 0a1baddd8ab2 -r e86370850c30 src/disjoint.sml --- a/src/disjoint.sml Tue Jul 01 11:39:14 2008 -0400 +++ b/src/disjoint.sml Tue Jul 01 12:10:46 2008 -0400 @@ -114,7 +114,7 @@ CName s => NameC s :: acc | CRel n => NameR n :: acc | CNamed n => NameN n :: acc - | _ => Unknown :: acc + | _ => (print "Unknown name\n"; Unknown :: acc) fun decomposeRow (c, acc) = case #1 (hnormCon env c) of @@ -122,7 +122,7 @@ | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc)) | CRel n => RowR n :: acc | CNamed n => RowN n :: acc - | _ => Unknown :: acc + | _ => (print "Unknown row\n"; Unknown :: acc) in decomposeRow (c, []) end @@ -265,6 +265,7 @@ fun prove1 denv (p1, p2) = case (p1, p2) of (NameC s1, NameC s2) => s1 <> s2 + | (NameC _, _) => prove1' denv (p2, p1) | (_, RowR _) => prove1' denv (p2, p1) | (_, RowN _) => prove1' denv (p2, p1) | _ => prove1' denv (p1, p2) diff -r 0a1baddd8ab2 -r e86370850c30 src/elab.sml --- a/src/elab.sml Tue Jul 01 11:39:14 2008 -0400 +++ b/src/elab.sml Tue Jul 01 12:10:46 2008 -0400 @@ -55,6 +55,7 @@ | CModProj of int * string list * string | CApp of con * con | CAbs of string * kind * con + | CDisjoint of con * con * con | CName of string diff -r 0a1baddd8ab2 -r e86370850c30 src/elab_print.sml --- a/src/elab_print.sml Tue Jul 01 11:39:14 2008 -0400 +++ b/src/elab_print.sml Tue Jul 01 12:10:46 2008 -0400 @@ -126,6 +126,15 @@ string "=>", space, p_con (E.pushCRel env x k) c]) + | CDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1, + space, + string "~", + space, + p_con env c2, + space, + string "=>", + space, + p_con env c3]) | CName s => box [string "#", string s] diff -r 0a1baddd8ab2 -r e86370850c30 src/elab_util.sml --- a/src/elab_util.sml Tue Jul 01 11:39:14 2008 -0400 +++ b/src/elab_util.sml Tue Jul 01 12:10:46 2008 -0400 @@ -124,6 +124,14 @@ S.map2 (mfc (bind (ctx, Rel (x, k))) c, fn c' => (CAbs (x, k', c'), loc))) + | CDisjoint (c1, c2, c3) => + S.bind2 (mfc ctx c1, + fn c1' => + S.bind2 (mfc ctx c2, + fn c2' => + S.map2 (mfc ctx c3, + fn c3' => + (CDisjoint (c1', c2', c3'), loc)))) | CName _ => S.return2 cAll diff -r 0a1baddd8ab2 -r e86370850c30 src/elaborate.sml --- a/src/elaborate.sml Tue Jul 01 11:39:14 2008 -0400 +++ b/src/elaborate.sml Tue Jul 01 12:10:46 2008 -0400 @@ -306,6 +306,23 @@ gs) end + | L.CDisjoint (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'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3) + end + | L.CName s => ((L'.CName s, loc), kname, []) @@ -498,6 +515,7 @@ | L'.KError => kerror | _ => raise CUnify' (CKindof c)) | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) + | L'.CDisjoint (_, _, c) => kindof env c | L'.CName _ => kname @@ -1761,13 +1779,16 @@ val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file in - app (fn (loc, env, denv, (c1, c2)) => - case D.prove env denv (c1, c2, loc) of - [] => () - | _ => - (ErrorMsg.errorAt loc "Remaining constraint"; - eprefaces' [("Con 1", p_con env c1), - ("Con 2", p_con env c2)])) gs; + if ErrorMsg.anyErrors () then + () + else + app (fn (loc, env, denv, (c1, c2)) => + case D.prove env denv (c1, c2, loc) of + [] => () + | _ => + (ErrorMsg.errorAt loc "Remaining constraint"; + eprefaces' [("Con 1", p_con env c1), + ("Con 2", p_con env c2)])) gs; (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file end diff -r 0a1baddd8ab2 -r e86370850c30 src/explify.sml --- a/src/explify.sml Tue Jul 01 11:39:14 2008 -0400 +++ b/src/explify.sml Tue Jul 01 12:10:46 2008 -0400 @@ -56,6 +56,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.CName s => (L'.CName s, loc) diff -r 0a1baddd8ab2 -r e86370850c30 src/lacweb.grm --- a/src/lacweb.grm Tue Jul 01 11:39:14 2008 -0400 +++ b/src/lacweb.grm Tue Jul 01 12:10:46 2008 -0400 @@ -43,7 +43,7 @@ | CON | LTYPE | VAL | FOLD | UNIT | KUNIT | TYPE | NAME | ARROW | LARROW | DARROW - | FN | PLUSPLUS | DOLLAR + | FN | PLUSPLUS | DOLLAR | TWIDDLE | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN %nonterm @@ -93,6 +93,7 @@ %right COMMA %right ARROW LARROW %right PLUSPLUS +%nonassoc TWIDDLE %nonassoc DOLLAR %left DOT @@ -194,6 +195,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)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) diff -r 0a1baddd8ab2 -r e86370850c30 src/lacweb.lex --- a/src/lacweb.lex Tue Jul 01 11:39:14 2008 -0400 +++ b/src/lacweb.lex Tue Jul 01 12:10:46 2008 -0400 @@ -142,6 +142,7 @@ "#" => (Tokens.HASH (pos yypos, pos yypos + size yytext)); "__" => (Tokens.UNDERUNDER (pos yypos, pos yypos + size yytext)); "_" => (Tokens.UNDER (pos yypos, pos yypos + size yytext)); + "~" => (Tokens.TWIDDLE (pos yypos, pos yypos + size yytext)); "con" => (Tokens.CON (pos yypos, pos yypos + size yytext)); "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext)); diff -r 0a1baddd8ab2 -r e86370850c30 src/source.sml --- a/src/source.sml Tue Jul 01 11:39:14 2008 -0400 +++ b/src/source.sml Tue Jul 01 12:10:46 2008 -0400 @@ -53,6 +53,7 @@ | CVar of string list * string | CApp of con * con | CAbs of string * kind option * con + | CDisjoint of con * con * con | CName of string diff -r 0a1baddd8ab2 -r e86370850c30 src/source_print.sml --- a/src/source_print.sml Tue Jul 01 11:39:14 2008 -0400 +++ b/src/source_print.sml Tue Jul 01 12:10:46 2008 -0400 @@ -111,6 +111,15 @@ string "=>", space, p_con c]) + | CDisjoint (c1, c2, c3) => parenIf par (box [p_con c1, + space, + string "~", + space, + p_con c2, + space, + string "=>", + space, + p_con c3]) | CName s => box [string "#", string s] diff -r 0a1baddd8ab2 -r e86370850c30 tests/disjoint.lac --- a/tests/disjoint.lac Tue Jul 01 11:39:14 2008 -0400 +++ b/tests/disjoint.lac Tue Jul 01 12:10:46 2008 -0400 @@ -1,1 +1,9 @@ -con c = fn x :: Name => [x, A] +con c1 = fn x :: Name => [x] ~ [A] => [x, A] +con c2 = fn x :: Name => [x] ~ [A] => [A, x] +con c3 = fn x :: Name => [A] ~ [x] => [x, A] +con c4 = fn x :: Name => [A] ~ [x] => [A, x] + +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