diff src/lacweb.grm @ 83:0a1baddd8ab2

Threading disjointness conditions through Elaborate
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 11:39:14 -0400
parents b4f2a258e52c
children e86370850c30
line wrap: on
line diff
--- a/src/lacweb.grm	Tue Jul 01 10:55:38 2008 -0400
+++ b/src/lacweb.grm	Tue Jul 01 11:39:14 2008 -0400
@@ -70,6 +70,7 @@
  | cterm of con
  | ident of con
  | rcon of (con * con) list
+ | rconn of (con * con) list
  | rcone of (con * con) list
 
  | eexp of exp
@@ -209,6 +210,7 @@
 
 cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
        | LBRACK rcon RBRACK             (CRecord rcon, s (LBRACKleft, RBRACKright))
+       | LBRACK rconn RBRACK            (CRecord rconn, s (LBRACKleft, RBRACKright))
        | LBRACE rcone RBRACE            (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)),
 					 s (LBRACEleft, RBRACEright))
        | DOLLAR cterm                   (TRecord cterm, s (DOLLARleft, ctermright))
@@ -223,6 +225,9 @@
        | ident EQ cexp                  ([(ident, cexp)])
        | ident EQ cexp COMMA rcon       ((ident, cexp) :: rcon)
 
+rconn  : ident                          ([(ident, (CUnit, s (identleft, identright)))])
+       | ident COMMA rconn              ((ident, (CUnit, s (identleft, identright))) :: rconn)
+
 rcone  :                                ([])
        | ident COLON cexp               ([(ident, cexp)])
        | ident COLON cexp COMMA rcone   ((ident, cexp) :: rcone)