comparison 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
comparison
equal deleted inserted replaced
87:275aaeb73f1f 88:7bab29834cd6
42 | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER 42 | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
43 | CON | LTYPE | VAL | FOLD | UNIT | KUNIT 43 | CON | LTYPE | VAL | FOLD | UNIT | KUNIT
44 | TYPE | NAME 44 | TYPE | NAME
45 | ARROW | LARROW | DARROW 45 | ARROW | LARROW | DARROW
46 | FN | PLUSPLUS | DOLLAR | TWIDDLE 46 | FN | PLUSPLUS | DOLLAR | TWIDDLE
47 | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN 47 | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
48 | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS
48 49
49 %nonterm 50 %nonterm
50 file of decl list 51 file of decl list
51 | decls of decl list 52 | decls of decl list
52 | decl of decl 53 | decl of decl
126 s (FUNCTORleft, strright)) 127 s (FUNCTORleft, strright))
127 | EXTERN STRUCTURE CSYMBOL COLON sgn (DFfiStr (CSYMBOL, sgn), s (EXTERNleft, sgnright)) 128 | EXTERN STRUCTURE CSYMBOL COLON sgn (DFfiStr (CSYMBOL, sgn), s (EXTERNleft, sgnright))
128 | OPEN mpath (case mpath of 129 | OPEN mpath (case mpath of
129 [] => raise Fail "Impossible mpath parse [1]" 130 [] => raise Fail "Impossible mpath parse [1]"
130 | m :: ms => (DOpen (m, ms), s (OPENleft, mpathright))) 131 | m :: ms => (DOpen (m, ms), s (OPENleft, mpathright)))
132 | OPEN CONSTRAINTS mpath (case mpath of
133 [] => raise Fail "Impossible mpath parse [3]"
134 | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright)))
135 | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
131 136
132 sgn : sgntm (sgntm) 137 sgn : sgntm (sgntm)
133 | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn 138 | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
134 (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right)) 139 (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right))
135 140
159 | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn 164 | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
160 (SgiStr (CSYMBOL1, 165 (SgiStr (CSYMBOL1,
161 (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))), 166 (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
162 s (FUNCTORleft, sgn2right)) 167 s (FUNCTORleft, sgn2right))
163 | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright)) 168 | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright))
169 | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
164 170
165 sgis : ([]) 171 sgis : ([])
166 | sgi sgis (sgi :: sgis) 172 | sgi sgis (sgi :: sgis)
167 173
168 str : STRUCT decls END (StrConst decls, s (STRUCTleft, ENDright)) 174 str : STRUCT decls END (StrConst decls, s (STRUCTleft, ENDright))