Mercurial > urweb

comparison src/expl_env.sml @ 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 06a98129b23f
children 3aa010e97db9
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
237 | SOME x => x 237 | SOME x => x
238 238
239 fun declBinds env (d, loc) = 239 fun declBinds env (d, loc) =
240 case d of 240 case d of
241 DCon (x, n, k, c) => pushCNamed env x n k (SOME c) 241 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
242 | DDatatype (x, n, xncs) => 242 | DDatatype (x, n, xs, xncs) =>
243 let 243 let
244 val env = pushCNamed env x n (KType, loc) NONE 244 val env = pushCNamed env x n (KType, loc) NONE
245 in 245 in
246 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) 246 foldl (fn ((x', n', to), env) =>
247 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc)) 247 let
248 env xncs 248 val t =
249 case to of
250 NONE => (CNamed n, loc)
251 | SOME t => (TFun (t, (CNamed n, loc)), loc)
252 val k = (KType, loc)
253 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
254 in
255 pushENamed env x' n' t
256 end)
257 env xncs
249 end 258 end
250 | DDatatypeImp (x, n, m, ms, x', xncs) => 259 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
251 let 260 let
252 val t = (CModProj (m, ms, x'), loc) 261 val t = (CModProj (m, ms, x'), loc)
253 val env = pushCNamed env x n (KType, loc) (SOME t) 262 val env = pushCNamed env x n (KType, loc) (SOME t)
254 263
255 val t = (CNamed n, loc) 264 val t = (CNamed n, loc)
256 in 265 in
257 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' t 266 foldl (fn ((x', n', to), env) =>
258 | ((x', n', SOME t'), env) => pushENamed env x' n' (TFun (t', t), loc)) 267 let
259 env xncs 268 val t =
269 case to of
270 NONE => (CNamed n, loc)
271 | SOME t => (TFun (t, (CNamed n, loc)), loc)
272 val k = (KType, loc)
273 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
274 in
275 pushENamed env x' n' t
276 end)
277 env xncs
260 end 278 end
261 | DVal (x, n, t, _) => pushENamed env x n t 279 | DVal (x, n, t, _) => pushENamed env x n t
262 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis 280 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
263 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn 281 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
264 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn 282 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
267 285
268 fun sgiBinds env (sgi, loc) = 286 fun sgiBinds env (sgi, loc) =
269 case sgi of 287 case sgi of
270 SgiConAbs (x, n, k) => pushCNamed env x n k NONE 288 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
271 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) 289 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
272 | SgiDatatype (x, n, xncs) => 290 | SgiDatatype (x, n, xs, xncs) =>
273 let 291 let
274 val env = pushCNamed env x n (KType, loc) NONE 292 val env = pushCNamed env x n (KType, loc) NONE
275 in 293 in
276 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) 294 foldl (fn ((x', n', to), env) =>
277 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc)) 295 let
278 env xncs 296 val t =
297 case to of
298 NONE => (CNamed n, loc)
299 | SOME t => (TFun (t, (CNamed n, loc)), loc)
300 val k = (KType, loc)
301 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
302 in
303 pushENamed env x' n' t
304 end)
305 env xncs
279 end 306 end
280 | SgiDatatypeImp (x, n, m1, ms, x', xncs) => 307 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
281 let 308 let
282 val env = pushCNamed env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) 309 val t = (CModProj (m1, ms, x'), loc)
310 val env = pushCNamed env x n (KType, loc) (SOME t)
311
312 val t = (CNamed n, loc)
283 in 313 in
284 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) 314 foldl (fn ((x', n', to), env) =>
285 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc)) 315 let
286 env xncs 316 val t =
317 case to of
318 NONE => (CNamed n, loc)
319 | SOME t => (TFun (t, (CNamed n, loc)), loc)
320 val k = (KType, loc)
321 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
322 in
323 pushENamed env x' n' t
324 end)
325 env xncs
287 end 326 end
288 | SgiVal (x, n, t) => pushENamed env x n t 327 | SgiVal (x, n, t) => pushENamed env x n t
289 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn 328 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
290 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn 329 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
291 330