Mercurial > urweb
comparison src/lacweb.grm @ 59:abb2b32c19fb
Subsignatures
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Jun 2008 19:10:38 -0400 |
parents | fd8a81ecd598 |
children | 48b6d2c3df46 |
comparison
equal
deleted
inserted
replaced
58:fd8a81ecd598 | 59:abb2b32c19fb |
---|---|
61 | kind of kind | 61 | kind of kind |
62 | kcolon of explicitness | 62 | kcolon of explicitness |
63 | 63 |
64 | path of string list * string | 64 | path of string list * string |
65 | spath of str | 65 | spath of str |
66 | mpath of string list | |
66 | 67 |
67 | cexp of con | 68 | cexp of con |
68 | capps of con | 69 | capps of con |
69 | cterm of con | 70 | cterm of con |
70 | ident of con | 71 | ident of con |
126 sgn : sgntm (sgntm) | 127 sgn : sgntm (sgntm) |
127 | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn | 128 | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn |
128 (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right)) | 129 (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right)) |
129 | 130 |
130 sgntm : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright)) | 131 sgntm : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright)) |
131 | CSYMBOL (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) | 132 | mpath (case mpath of |
133 [] => raise Fail "Impossible mpath parse" | |
134 | [x] => SgnVar x | |
135 | m :: ms => SgnProj (m, | |
136 List.take (ms, length ms - 1), | |
137 List.nth (ms, length ms - 1)), | |
138 s (mpathleft, mpathright)) | |
132 | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) | 139 | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) |
133 | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) | 140 | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) |
134 | LPAREN sgn RPAREN (sgn) | 141 | LPAREN sgn RPAREN (sgn) |
135 | 142 |
136 sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, kindright)) | 143 sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, kindright)) |
141 | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), | 148 | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), |
142 s (LTYPEleft, cexpright)) | 149 s (LTYPEleft, cexpright)) |
143 | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) | 150 | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) |
144 | 151 |
145 | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) | 152 | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) |
153 | SIGNATURE CSYMBOL EQ sgn (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)) | |
146 | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn | 154 | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn |
147 (SgiStr (CSYMBOL1, | 155 (SgiStr (CSYMBOL1, |
148 (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))), | 156 (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))), |
149 s (FUNCTORleft, sgn2right)) | 157 s (FUNCTORleft, sgn2right)) |
150 | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright)) | 158 | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright)) |
189 | TCOLON (Implicit) | 197 | TCOLON (Implicit) |
190 | 198 |
191 path : SYMBOL ([], SYMBOL) | 199 path : SYMBOL ([], SYMBOL) |
192 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) | 200 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) |
193 | 201 |
202 mpath : CSYMBOL ([CSYMBOL]) | |
203 | CSYMBOL DOT mpath (CSYMBOL :: mpath) | |
204 | |
194 cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) | 205 cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) |
195 | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright)) | 206 | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright)) |
196 | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)), | 207 | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)), |
197 s (LBRACEleft, RBRACEright)) | 208 s (LBRACEleft, RBRACEright)) |
198 | DOLLAR cterm (TRecord cterm, s (DOLLARleft, ctermright)) | 209 | DOLLAR cterm (TRecord cterm, s (DOLLARleft, ctermright)) |