diff src/lacweb.grm @ 85:1f85890c9846

Disjointness assumptions in expressions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 12:25:12 -0400
parents e86370850c30
children 7bab29834cd6
line wrap: on
line diff
--- a/src/lacweb.grm	Tue Jul 01 12:10:46 2008 -0400
+++ b/src/lacweb.grm	Tue Jul 01 12:25:12 2008 -0400
@@ -196,6 +196,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))
+       | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
 
        | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
 
@@ -245,6 +246,7 @@
        | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright))
        | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright))
        | FN SYMBOL DARROW eexp          (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright))
+       | FN cterm TWIDDLE cterm DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (cterm1left, eexpright))
 
        | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
        | eterm DOT ident                (EField (eterm, ident), s (etermleft, identright))