Mercurial > urweb

comparison src/lacweb.grm @ 82:b4f2a258e52c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial disjointness prover
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 10:55:38 -0400
parents 6431b315a1e3
children 0a1baddd8ab2
comparison
equal deleted inserted replaced
81:60d97de1bbe8 82:b4f2a258e52c
38 EOF 38 EOF
39 | STRING of string | INT of Int64.int | FLOAT of Real64.real 39 | STRING of string | INT of Int64.int | FLOAT of Real64.real
40 | SYMBOL of string | CSYMBOL of string 40 | SYMBOL of string | CSYMBOL of string
41 | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE 41 | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
42 | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER 42 | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
43 | CON | LTYPE | VAL | FOLD 43 | CON | LTYPE | VAL | FOLD | UNIT | KUNIT
44 | TYPE | NAME 44 | TYPE | NAME
45 | ARROW | LARROW | DARROW 45 | ARROW | LARROW | DARROW
46 | FN | PLUSPLUS | DOLLAR 46 | FN | PLUSPLUS | DOLLAR
47 | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN 47 | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN
48 48
177 kind : TYPE (KType, s (TYPEleft, TYPEright)) 177 kind : TYPE (KType, s (TYPEleft, TYPEright))
178 | NAME (KName, s (NAMEleft, NAMEright)) 178 | NAME (KName, s (NAMEleft, NAMEright))
179 | LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright)) 179 | LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright))
180 | kind ARROW kind (KArrow (kind1, kind2), s (kind1left, kind2right)) 180 | kind ARROW kind (KArrow (kind1, kind2), s (kind1left, kind2right))
181 | LPAREN kind RPAREN (#1 kind, s (LPARENleft, RPARENright)) 181 | LPAREN kind RPAREN (#1 kind, s (LPARENleft, RPARENright))
182 | KUNIT (KUnit, s (KUNITleft, KUNITright))
182 | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright)) 183 | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright))
183 184
184 capps : cterm (cterm) 185 capps : cterm (cterm)
185 | capps cterm (CApp (capps, cterm), s (cappsleft, ctermright)) 186 | capps cterm (CApp (capps, cterm), s (cappsleft, ctermright))
186 187
214 | HASH CSYMBOL (CName CSYMBOL, s (HASHleft, CSYMBOLright)) 215 | HASH CSYMBOL (CName CSYMBOL, s (HASHleft, CSYMBOLright))
215 216
216 | path (CVar path, s (pathleft, pathright)) 217 | path (CVar path, s (pathleft, pathright))
217 | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) 218 | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
218 | FOLD (CFold, s (FOLDleft, FOLDright)) 219 | FOLD (CFold, s (FOLDleft, FOLDright))
220 | UNIT (CUnit, s (UNITleft, UNITright))
219 221
220 rcon : ([]) 222 rcon : ([])
221 | ident EQ cexp ([(ident, cexp)]) 223 | ident EQ cexp ([(ident, cexp)])
222 | ident EQ cexp COMMA rcon ((ident, cexp) :: rcon) 224 | ident EQ cexp COMMA rcon ((ident, cexp) :: rcon)
223 225