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/lacweb.grm | |
| parent | d28cad7cc5881018717c7e875c99c51469da9d44 (diff) | |
Disjointness assumptions
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 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)) |