Mercurial > urweb
comparison 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 |
comparison
equal
deleted
inserted
replaced
84:e86370850c30 | 85:1f85890c9846 |
---|---|
194 | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) | 194 | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) |
195 | 195 |
196 | FN SYMBOL DARROW cexp (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright)) | 196 | FN SYMBOL DARROW cexp (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright)) |
197 | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright)) | 197 | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright)) |
198 | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) | 198 | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) |
199 | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) | |
199 | 200 |
200 | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) | 201 | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) |
201 | 202 |
202 | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright)) | 203 | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright)) |
203 | 204 |
243 | 244 |
244 eexp : eapps (eapps) | 245 eexp : eapps (eapps) |
245 | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright)) | 246 | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright)) |
246 | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright)) | 247 | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright)) |
247 | FN SYMBOL DARROW eexp (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright)) | 248 | FN SYMBOL DARROW eexp (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright)) |
249 | FN cterm TWIDDLE cterm DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (cterm1left, eexpright)) | |
248 | 250 |
249 | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright)) | 251 | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright)) |
250 | eterm DOT ident (EField (eterm, ident), s (etermleft, identright)) | 252 | eterm DOT ident (EField (eterm, ident), s (etermleft, identright)) |
251 | 253 |
252 eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) | 254 eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) |