diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-07-01 10:55:38 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-01 10:55:38 -0400 |
| commit | 43116f69ce9330eb09d42a25d4afc746e7c3f3ef (patch) | |
| tree | e57ed0ff271cf35d5dbf88ecb90ce150a877e454 /src/lacweb.grm | |
| parent | cc2b6499cd2ea61f8882419cc5915c3428d5f5b7 (diff) | |
Initial disjointness prover
Diffstat (limited to 'src/lacweb.grm')
| -rw-r--r-- | src/lacweb.grm | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/lacweb.grm b/src/lacweb.grm index c42b5eb5..91285e4c 100644 --- a/src/lacweb.grm +++ b/src/lacweb.grm @@ -40,7 +40,7 @@ val s = ErrorMsg.spanOf | SYMBOL of string | CSYMBOL of string | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER - | CON | LTYPE | VAL | FOLD + | CON | LTYPE | VAL | FOLD | UNIT | KUNIT | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR @@ -179,6 +179,7 @@ kind : TYPE (KType, s (TYPEleft, TYPEright)) | LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright)) | kind ARROW kind (KArrow (kind1, kind2), s (kind1left, kind2right)) | LPAREN kind RPAREN (#1 kind, s (LPARENleft, RPARENright)) + | KUNIT (KUnit, s (KUNITleft, KUNITright)) | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright)) capps : cterm (cterm) @@ -216,6 +217,7 @@ cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) | path (CVar path, s (pathleft, pathright)) | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) | FOLD (CFold, s (FOLDleft, FOLDright)) + | UNIT (CUnit, s (UNITleft, UNITright)) rcon : ([]) | ident EQ cexp ([(ident, cexp)]) |