Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- a/src/lacweb.grm Sun Jun 22 18:17:21 2008 -0400 +++ b/src/lacweb.grm Sun Jun 22 19:10:38 2008 -0400 @@ -63,6 +63,7 @@ | path of string list * string | spath of str + | mpath of string list | cexp of con | capps of con @@ -128,7 +129,13 @@ (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right)) sgntm : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright)) - | CSYMBOL (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) + | mpath (case mpath of + [] => raise Fail "Impossible mpath parse" + | [x] => SgnVar x + | m :: ms => SgnProj (m, + List.take (ms, length ms - 1), + List.nth (ms, length ms - 1)), + s (mpathleft, mpathright)) | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) | LPAREN sgn RPAREN (sgn) @@ -143,6 +150,7 @@ | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) + | SIGNATURE CSYMBOL EQ sgn (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)) | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn (SgiStr (CSYMBOL1, (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))), @@ -191,6 +199,9 @@ path : SYMBOL ([], SYMBOL) | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) +mpath : CSYMBOL ([CSYMBOL]) + | CSYMBOL DOT mpath (CSYMBOL :: mpath) + cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright)) | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)),