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))