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