diff src/lacweb.grm @ 88:7bab29834cd6

Constraints in modules
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 15:58:02 -0400
parents 1f85890c9846
children d3ee072fa609
line wrap: on
line diff
--- a/src/lacweb.grm	Tue Jul 01 13:23:46 2008 -0400
+++ b/src/lacweb.grm	Tue Jul 01 15:58:02 2008 -0400
@@ -44,7 +44,8 @@
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | DOLLAR | TWIDDLE
- | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN
+ | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
+ | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS
 
 %nonterm
    file of decl list
@@ -128,6 +129,10 @@
        | OPEN mpath                     (case mpath of
                                              [] => raise Fail "Impossible mpath parse [1]"
                                            | m :: ms => (DOpen (m, ms), s (OPENleft, mpathright)))
+       | OPEN CONSTRAINTS mpath         (case mpath of
+                                             [] => raise Fail "Impossible mpath parse [3]"
+                                           | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright)))
+       | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
 
 sgn    : sgntm                          (sgntm)
        | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
@@ -161,6 +166,7 @@
                                                  (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
                                          s (FUNCTORleft, sgn2right))
        | INCLUDE sgn                    (SgiInclude sgn, s (INCLUDEleft, sgnright))
+       | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
 
 sgis   :                                ([])
        | sgi sgis                       (sgi :: sgis)