summaryrefslogtreecommitdiff
path: root/src/lacweb.grm
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 12:10:46 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 12:10:46 -0400
commit7628e1d8f7f8199531c9bc08a774c9a9e2bc5d63 (patch)
tree3d434c77c5ec6ac3660a553072e1c1ba26cd4665 /src/lacweb.grm
parentd28cad7cc5881018717c7e875c99c51469da9d44 (diff)
Disjointness assumptions
Diffstat (limited to 'src/lacweb.grm')
-rw-r--r--src/lacweb.grm4
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))