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