comparison 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
comparison
equal deleted inserted replaced
82:b4f2a258e52c 83:0a1baddd8ab2
68 | cexp of con 68 | cexp of con
69 | capps of con 69 | capps of con
70 | cterm of con 70 | cterm of con
71 | ident of con 71 | ident of con
72 | rcon of (con * con) list 72 | rcon of (con * con) list
73 | rconn of (con * con) list
73 | rcone of (con * con) list 74 | rcone of (con * con) list
74 75
75 | eexp of exp 76 | eexp of exp
76 | eapps of exp 77 | eapps of exp
77 | eterm of exp 78 | eterm of exp
207 mpath : CSYMBOL ([CSYMBOL]) 208 mpath : CSYMBOL ([CSYMBOL])
208 | CSYMBOL DOT mpath (CSYMBOL :: mpath) 209 | CSYMBOL DOT mpath (CSYMBOL :: mpath)
209 210
210 cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) 211 cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright))
211 | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright)) 212 | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright))
213 | LBRACK rconn RBRACK (CRecord rconn, s (LBRACKleft, RBRACKright))
212 | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)), 214 | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)),
213 s (LBRACEleft, RBRACEright)) 215 s (LBRACEleft, RBRACEright))
214 | DOLLAR cterm (TRecord cterm, s (DOLLARleft, ctermright)) 216 | DOLLAR cterm (TRecord cterm, s (DOLLARleft, ctermright))
215 | HASH CSYMBOL (CName CSYMBOL, s (HASHleft, CSYMBOLright)) 217 | HASH CSYMBOL (CName CSYMBOL, s (HASHleft, CSYMBOLright))
216 218
221 223
222 rcon : ([]) 224 rcon : ([])
223 | ident EQ cexp ([(ident, cexp)]) 225 | ident EQ cexp ([(ident, cexp)])
224 | ident EQ cexp COMMA rcon ((ident, cexp) :: rcon) 226 | ident EQ cexp COMMA rcon ((ident, cexp) :: rcon)
225 227
228 rconn : ident ([(ident, (CUnit, s (identleft, identright)))])
229 | ident COMMA rconn ((ident, (CUnit, s (identleft, identright))) :: rconn)
230
226 rcone : ([]) 231 rcone : ([])
227 | ident COLON cexp ([(ident, cexp)]) 232 | ident COLON cexp ([(ident, cexp)])
228 | ident COLON cexp COMMA rcone ((ident, cexp) :: rcone) 233 | ident COLON cexp COMMA rcone ((ident, cexp) :: rcone)
229 234
230 ident : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) 235 ident : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))