diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-06-22 19:10:38 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-06-22 19:10:38 -0400 |
commit | e4a1bf8af62cb275bf5f5ae2f83b7197b1b58461 (patch) | |
tree | f3be22e5bbf731f7e45263b40f58a3cf5be686ea /src/lacweb.grm | |
parent | 5eee5f4a3b11c467c853f8397c7f679e5d5acc7a (diff) |
Subsignatures
Diffstat (limited to 'src/lacweb.grm')
-rw-r--r-- | src/lacweb.grm | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/lacweb.grm b/src/lacweb.grm index 021e862e..4c3ed51e 100644 --- a/src/lacweb.grm +++ b/src/lacweb.grm @@ -63,6 +63,7 @@ val s = ErrorMsg.spanOf | path of string list * string | spath of str + | mpath of string list | cexp of con | capps of con @@ -128,7 +129,13 @@ sgn : sgntm (sgntm) (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 @@ sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, k | 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 @@ kcolon : DCOLON (Explicit) 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)), |