Mercurial > urweb

comparison src/lacweb.grm @ 191:aa54250f58ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 3eb53c957d10
children 85b5f663bb86
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
62 | decls of decl list 62 | decls of decl list
63 | decl of decl 63 | decl of decl
64 | vali of string * con option * exp 64 | vali of string * con option * exp
65 | valis of (string * con option * exp) list 65 | valis of (string * con option * exp) list
66 66
67 | dargs of string list
67 | barOpt of unit 68 | barOpt of unit
68 | dcons of (string * con option) list 69 | dcons of (string * con option) list
69 | dcon of string * con option 70 | dcon of string * con option
70 71
71 | sgn of sgn 72 | sgn of sgn
140 141
141 decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft, cexpright)) 142 decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft, cexpright))
142 | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)) 143 | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
143 | LTYPE SYMBOL EQ cexp (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), 144 | LTYPE SYMBOL EQ cexp (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
144 s (LTYPEleft, cexpright)) 145 s (LTYPEleft, cexpright))
145 | DATATYPE SYMBOL EQ barOpt dcons(DDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright)) 146 | DATATYPE SYMBOL dargs EQ barOpt dcons(DDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
146 | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path 147 | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
147 (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright)) 148 (case dargs of
149 [] => (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
150 | _ => raise Fail "Arguments specified for imported datatype")
148 | VAL vali (DVal vali, s (VALleft, valiright)) 151 | VAL vali (DVal vali, s (VALleft, valiright))
149 | VAL REC valis (DValRec valis, s (VALleft, valisright)) 152 | VAL REC valis (DValRec valis, s (VALleft, valisright))
150 153
151 | SIGNATURE CSYMBOL EQ sgn (DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)) 154 | SIGNATURE CSYMBOL EQ sgn (DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
152 | STRUCTURE CSYMBOL EQ str (DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright)) 155 | STRUCTURE CSYMBOL EQ str (DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright))
167 [] => raise Fail "Impossible mpath parse [3]" 170 [] => raise Fail "Impossible mpath parse [3]"
168 | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright))) 171 | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright)))
169 | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) 172 | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
170 | EXPORT spath (DExport spath, s (EXPORTleft, spathright)) 173 | EXPORT spath (DExport spath, s (EXPORTleft, spathright))
171 174
175 dargs : ([])
176 | SYMBOL dargs (SYMBOL :: dargs)
177
172 barOpt : () 178 barOpt : ()
173 | BAR () 179 | BAR ()
174 180
175 dcons : dcon ([dcon]) 181 dcons : dcon ([dcon])
176 | dcon BAR dcons (dcon :: dcons) 182 | dcon BAR dcons (dcon :: dcons)
205 s (LTYPEleft, SYMBOLright)) 211 s (LTYPEleft, SYMBOLright))
206 | CON SYMBOL EQ cexp (SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright)) 212 | CON SYMBOL EQ cexp (SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright))
207 | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)) 213 | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
208 | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), 214 | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
209 s (LTYPEleft, cexpright)) 215 s (LTYPEleft, cexpright))
210 | DATATYPE SYMBOL EQ barOpt dcons(SgiDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright)) 216 | DATATYPE SYMBOL dargs EQ barOpt dcons(SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
211 | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path 217 | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
212 (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright)) 218 (case dargs of
219 [] => (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
220 | _ => raise Fail "Arguments specified for imported datatype")
213 | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) 221 | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
214 222
215 | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) 223 | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))
216 | SIGNATURE CSYMBOL EQ sgn (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)) 224 | SIGNATURE CSYMBOL EQ sgn (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
217 | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn 225 | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn