diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-07-01 12:10:46 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-01 12:10:46 -0400 |
commit | 7628e1d8f7f8199531c9bc08a774c9a9e2bc5d63 (patch) | |
tree | 3d434c77c5ec6ac3660a553072e1c1ba26cd4665 /src | |
parent | d28cad7cc5881018717c7e875c99c51469da9d44 (diff) |
Disjointness assumptions
Diffstat (limited to 'src')
-rw-r--r-- | src/disjoint.sml | 5 | ||||
-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 | 35 | ||||
-rw-r--r-- | src/explify.sml | 1 | ||||
-rw-r--r-- | src/lacweb.grm | 4 | ||||
-rw-r--r-- | src/lacweb.lex | 1 | ||||
-rw-r--r-- | src/source.sml | 1 | ||||
-rw-r--r-- | src/source_print.sml | 9 |
10 files changed, 64 insertions, 10 deletions
diff --git a/src/disjoint.sml b/src/disjoint.sml index fa4c8618..c9f6d2e9 100644 --- a/src/disjoint.sml +++ b/src/disjoint.sml @@ -114,7 +114,7 @@ fun decomposeRow env c = 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 @@ fun decomposeRow env c = | 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) = 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 --git a/src/elab.sml b/src/elab.sml index a7085fee..fe7c989e 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -55,6 +55,7 @@ datatype con' = | CModProj of int * string list * string | CApp of con * con | CAbs of string * kind * con + | CDisjoint of con * con * con | CName of string diff --git a/src/elab_print.sml b/src/elab_print.sml index 01472ca7..05d216ca 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -126,6 +126,15 @@ fun p_con' par env (c, _) = 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 --git a/src/elab_util.sml b/src/elab_util.sml index e9b7ddd9..63d035e8 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -124,6 +124,14 @@ fun mapfoldB {kind = fk, con = fc, bind} = 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 --git a/src/elaborate.sml b/src/elaborate.sml index 73ebc43b..e311726a 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -306,6 +306,23 @@ fun elabCon (env, denv) (c, loc) = 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 @@ fun kindof env (c, loc) = | 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 @@ fun elabFile basis env file = 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 --git a/src/explify.sml b/src/explify.sml index af655eb4..2ed66843 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -56,6 +56,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.CName s => (L'.CName s, loc) diff --git a/src/lacweb.grm b/src/lacweb.grm index b961ba85..39d30349 100644 --- a/src/lacweb.grm +++ b/src/lacweb.grm @@ -43,7 +43,7 @@ val s = ErrorMsg.spanOf | 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 @@ val s = ErrorMsg.spanOf %right COMMA %right ARROW LARROW %right PLUSPLUS +%nonassoc TWIDDLE %nonassoc DOLLAR %left DOT @@ -194,6 +195,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)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) diff --git a/src/lacweb.lex b/src/lacweb.lex index 45e2f1f2..3fa0b45c 100644 --- a/src/lacweb.lex +++ b/src/lacweb.lex @@ -142,6 +142,7 @@ realconst = [0-9]+\.[0-9]*; <INITIAL> "#" => (Tokens.HASH (pos yypos, pos yypos + size yytext)); <INITIAL> "__" => (Tokens.UNDERUNDER (pos yypos, pos yypos + size yytext)); <INITIAL> "_" => (Tokens.UNDER (pos yypos, pos yypos + size yytext)); +<INITIAL> "~" => (Tokens.TWIDDLE (pos yypos, pos yypos + size yytext)); <INITIAL> "con" => (Tokens.CON (pos yypos, pos yypos + size yytext)); <INITIAL> "type" => (Tokens.LTYPE (pos yypos, pos yypos + size yytext)); diff --git a/src/source.sml b/src/source.sml index e55e5901..10d174ab 100644 --- a/src/source.sml +++ b/src/source.sml @@ -53,6 +53,7 @@ datatype con' = | CVar of string list * string | CApp of con * con | CAbs of string * kind option * con + | CDisjoint of con * con * con | CName of string diff --git a/src/source_print.sml b/src/source_print.sml index 80b077d0..3e83dbe8 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -111,6 +111,15 @@ fun p_con' par (c, _) = 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] |