Mercurial > urweb

comparison src/elab_env.sml @ 171:c7a6e6dbc318

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating some basic pattern matching
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 10:06:27 -0400
parents 06a98129b23f
children 7ee424760d2f
comparison
equal deleted inserted replaced
170:a158f8c5aa55 171:c7a6e6dbc318
79 renameC : kind var' SM.map, 79 renameC : kind var' SM.map,
80 relC : (string * kind) list, 80 relC : (string * kind) list,
81 namedC : (string * kind * con option) IM.map, 81 namedC : (string * kind * con option) IM.map,
82 82
83 datatypes : datatyp IM.map, 83 datatypes : datatyp IM.map,
84 constructors : (int * con option * int) SM.map,
84 85
85 renameE : con var' SM.map, 86 renameE : con var' SM.map,
86 relE : (string * con) list, 87 relE : (string * con) list,
87 namedE : (string * con) IM.map, 88 namedE : (string * con) IM.map,
88 89
107 renameC = SM.empty, 108 renameC = SM.empty,
108 relC = [], 109 relC = [],
109 namedC = IM.empty, 110 namedC = IM.empty,
110 111
111 datatypes = IM.empty, 112 datatypes = IM.empty,
113 constructors = SM.empty,
112 114
113 renameE = SM.empty, 115 renameE = SM.empty,
114 relE = [], 116 relE = [],
115 namedE = IM.empty, 117 namedE = IM.empty,
116 118
129 {renameC = SM.insert (renameC, x, Rel' (0, k)), 131 {renameC = SM.insert (renameC, x, Rel' (0, k)),
130 relC = (x, k) :: #relC env, 132 relC = (x, k) :: #relC env,
131 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 133 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
132 134
133 datatypes = #datatypes env, 135 datatypes = #datatypes env,
136 constructors = #constructors env,
134 137
135 renameE = #renameE env, 138 renameE = #renameE env,
136 relE = map (fn (x, c) => (x, lift c)) (#relE env), 139 relE = map (fn (x, c) => (x, lift c)) (#relE env),
137 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), 140 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
138 141
152 {renameC = SM.insert (#renameC env, x, Named' (n, k)), 155 {renameC = SM.insert (#renameC env, x, Named' (n, k)),
153 relC = #relC env, 156 relC = #relC env,
154 namedC = IM.insert (#namedC env, n, (x, k, co)), 157 namedC = IM.insert (#namedC env, n, (x, k, co)),
155 158
156 datatypes = #datatypes env, 159 datatypes = #datatypes env,
160 constructors = #constructors env,
157 161
158 renameE = #renameE env, 162 renameE = #renameE env,
159 relE = #relE env, 163 relE = #relE env,
160 namedE = #namedE env, 164 namedE = #namedE env,
161 165
190 namedC = #namedC env, 194 namedC = #namedC env,
191 195
192 datatypes = IM.insert (#datatypes env, n, 196 datatypes = IM.insert (#datatypes env, n,
193 foldl (fn ((x, n, to), cons) => 197 foldl (fn ((x, n, to), cons) =>
194 IM.insert (cons, n, (x, to))) IM.empty xncs), 198 IM.insert (cons, n, (x, to))) IM.empty xncs),
199 constructors = foldl (fn ((x, n', to), cmap) =>
200 SM.insert (cmap, x, (n', to, n)))
201 (#constructors env) xncs,
195 202
196 renameE = #renameE env, 203 renameE = #renameE env,
197 relE = #relE env, 204 relE = #relE env,
198 namedE = #namedE env, 205 namedE = #namedE env,
199 206
206 fun lookupDatatype (env : env) n = 213 fun lookupDatatype (env : env) n =
207 case IM.find (#datatypes env, n) of 214 case IM.find (#datatypes env, n) of
208 NONE => raise UnboundNamed n 215 NONE => raise UnboundNamed n
209 | SOME x => x 216 | SOME x => x
210 217
211 fun lookupConstructor dt n = 218 fun lookupDatatypeConstructor dt n =
212 case IM.find (dt, n) of 219 case IM.find (dt, n) of
213 NONE => raise UnboundNamed n 220 NONE => raise UnboundNamed n
214 | SOME x => x 221 | SOME x => x
215 222
223 fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
224
216 fun constructors dt = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt 225 fun constructors dt = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
217 226
218 fun pushERel (env : env) x t = 227 fun pushERel (env : env) x t =
219 let 228 let
220 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) 229 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
223 {renameC = #renameC env, 232 {renameC = #renameC env,
224 relC = #relC env, 233 relC = #relC env,
225 namedC = #namedC env, 234 namedC = #namedC env,
226 235
227 datatypes = #datatypes env, 236 datatypes = #datatypes env,
237 constructors = #constructors env,
228 238
229 renameE = SM.insert (renameE, x, Rel' (0, t)), 239 renameE = SM.insert (renameE, x, Rel' (0, t)),
230 relE = (x, t) :: #relE env, 240 relE = (x, t) :: #relE env,
231 namedE = #namedE env, 241 namedE = #namedE env,
232 242
245 {renameC = #renameC env, 255 {renameC = #renameC env,
246 relC = #relC env, 256 relC = #relC env,
247 namedC = #namedC env, 257 namedC = #namedC env,
248 258
249 datatypes = #datatypes env, 259 datatypes = #datatypes env,
260 constructors = #constructors env,
250 261
251 renameE = SM.insert (#renameE env, x, Named' (n, t)), 262 renameE = SM.insert (#renameE env, x, Named' (n, t)),
252 relE = #relE env, 263 relE = #relE env,
253 namedE = IM.insert (#namedE env, n, (x, t)), 264 namedE = IM.insert (#namedE env, n, (x, t)),
254 265
281 {renameC = #renameC env, 292 {renameC = #renameC env,
282 relC = #relC env, 293 relC = #relC env,
283 namedC = #namedC env, 294 namedC = #namedC env,
284 295
285 datatypes = #datatypes env, 296 datatypes = #datatypes env,
297 constructors = #constructors env,
286 298
287 renameE = #renameE env, 299 renameE = #renameE env,
288 relE = #relE env, 300 relE = #relE env,
289 namedE = #namedE env, 301 namedE = #namedE env,
290 302
313 {renameC = #renameC env, 325 {renameC = #renameC env,
314 relC = #relC env, 326 relC = #relC env,
315 namedC = #namedC env, 327 namedC = #namedC env,
316 328
317 datatypes = #datatypes env, 329 datatypes = #datatypes env,
330 constructors = #constructors env,
318 331
319 renameE = #renameE env, 332 renameE = #renameE env,
320 relE = #relE env, 333 relE = #relE env,
321 namedE = #namedE env, 334 namedE = #namedE env,
322 335