comparison src/lacweb.grm @ 34:44b5405e74c7

Elaborating module projection
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Jun 2008 16:38:54 -0400
parents e6ccf961d8a3
children e3d3c2791105
comparison
equal deleted inserted replaced
33:535c324f0b35 34:44b5405e74c7
58 | str of str 58 | str of str
59 59
60 | kind of kind 60 | kind of kind
61 | kcolon of explicitness 61 | kcolon of explicitness
62 62
63 | path of string list * string
64 | spath of str
65
63 | cexp of con 66 | cexp of con
64 | capps of con 67 | capps of con
65 | cterm of con 68 | cterm of con
66 | ident of con 69 | ident of con
67 | rcon of (con * con) list 70 | rcon of (con * con) list
124 127
125 sgis : ([]) 128 sgis : ([])
126 | sgi sgis (sgi :: sgis) 129 | sgi sgis (sgi :: sgis)
127 130
128 str : STRUCT decls END (StrConst decls, s (STRUCTleft, ENDright)) 131 str : STRUCT decls END (StrConst decls, s (STRUCTleft, ENDright))
129 | CSYMBOL (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) 132 | spath (spath)
133
134 spath : CSYMBOL (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
135 | spath DOT CSYMBOL (StrProj (spath, CSYMBOL), s (spathleft, CSYMBOLright))
130 136
131 kind : TYPE (KType, s (TYPEleft, TYPEright)) 137 kind : TYPE (KType, s (TYPEleft, TYPEright))
132 | NAME (KName, s (NAMEleft, NAMEright)) 138 | NAME (KName, s (NAMEleft, NAMEright))
133 | LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright)) 139 | LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright))
134 | kind ARROW kind (KArrow (kind1, kind2), s (kind1left, kind2right)) 140 | kind ARROW kind (KArrow (kind1, kind2), s (kind1left, kind2right))
151 | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright)) 157 | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright))
152 158
153 kcolon : DCOLON (Explicit) 159 kcolon : DCOLON (Explicit)
154 | TCOLON (Implicit) 160 | TCOLON (Implicit)
155 161
162 path : SYMBOL ([], SYMBOL)
163 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
164
156 cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) 165 cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright))
157 | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright)) 166 | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright))
158 | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)), 167 | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)),
159 s (LBRACEleft, RBRACEright)) 168 s (LBRACEleft, RBRACEright))
160 | DOLLAR cterm (TRecord cterm, s (DOLLARleft, ctermright)) 169 | DOLLAR cterm (TRecord cterm, s (DOLLARleft, ctermright))
161 | HASH CSYMBOL (CName CSYMBOL, s (HASHleft, CSYMBOLright)) 170 | HASH CSYMBOL (CName CSYMBOL, s (HASHleft, CSYMBOLright))
162 171
163 | SYMBOL (CVar SYMBOL, s (SYMBOLleft, SYMBOLright)) 172 | path (CVar path, s (pathleft, pathright))
164 | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) 173 | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
165 174
166 rcon : ([]) 175 rcon : ([])
167 | ident EQ cexp ([(ident, cexp)]) 176 | ident EQ cexp ([(ident, cexp)])
168 | ident EQ cexp COMMA rcon ((ident, cexp) :: rcon) 177 | ident EQ cexp COMMA rcon ((ident, cexp) :: rcon)
170 rcone : ([]) 179 rcone : ([])
171 | ident COLON cexp ([(ident, cexp)]) 180 | ident COLON cexp ([(ident, cexp)])
172 | ident COLON cexp COMMA rcone ((ident, cexp) :: rcone) 181 | ident COLON cexp COMMA rcone ((ident, cexp) :: rcone)
173 182
174 ident : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) 183 ident : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
175 | SYMBOL (CVar SYMBOL, s (SYMBOLleft, SYMBOLright)) 184 | SYMBOL (CVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright))
176 185
177 eapps : eterm (eterm) 186 eapps : eterm (eterm)
178 | eapps eterm (EApp (eapps, eterm), s (eappsleft, etermright)) 187 | eapps eterm (EApp (eapps, eterm), s (eappsleft, etermright))
179 | eapps LBRACK cexp RBRACK (ECApp (eapps, cexp), s (eappsleft, RBRACKright)) 188 | eapps LBRACK cexp RBRACK (ECApp (eapps, cexp), s (eappsleft, RBRACKright))
180 189
186 | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright)) 195 | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
187 | eterm DOT ident (EField (eterm, ident), s (etermleft, identright)) 196 | eterm DOT ident (EField (eterm, ident), s (etermleft, identright))
188 197
189 eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) 198 eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
190 199
191 | SYMBOL (EVar SYMBOL, s (SYMBOLleft, SYMBOLright)) 200 | path (EVar path, s (pathleft, pathright))
192 | LBRACE rexp RBRACE (ERecord rexp, s (LBRACEleft, RBRACEright)) 201 | LBRACE rexp RBRACE (ERecord rexp, s (LBRACEleft, RBRACEright))
193 202
194 | INT (EPrim (Prim.Int INT), s (INTleft, INTright)) 203 | INT (EPrim (Prim.Int INT), s (INTleft, INTright))
195 | FLOAT (EPrim (Prim.Float FLOAT), s (FLOATleft, FLOATright)) 204 | FLOAT (EPrim (Prim.Float FLOAT), s (FLOATleft, FLOATright))
196 | STRING (EPrim (Prim.String STRING), s (STRINGleft, STRINGright)) 205 | STRING (EPrim (Prim.String STRING), s (STRINGleft, STRINGright))