Mercurial > urweb

comparison src/elab_env.sml @ 156:34ccd7d2bea8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of datatype support
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 15:02:03 -0400
parents e3041657d653
children adc4e42e3adc
comparison
equal deleted inserted replaced
155:4334bb734187 156:34ccd7d2bea8
290 NONE => raise UnboundNamed n 290 NONE => raise UnboundNamed n
291 | SOME x => x 291 | SOME x => x
292 292
293 fun lookupStr (env : env) x = SM.find (#renameStr env, x) 293 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
294 294
295 fun declBinds env (d, _) = 295 fun declBinds env (d, loc) =
296 case d of 296 case d of
297 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 297 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
298 | DDatatype (x, n, xncs) =>
299 let
300 val env = pushCNamedAs env x n (KType, loc) NONE
301 in
302 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
303 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
304 env xncs
305 end
306 | DDatatypeImp (x, n, m, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m, ms, x'), loc))
298 | DVal (x, n, t, _) => pushENamedAs env x n t 307 | DVal (x, n, t, _) => pushENamedAs env x n t
299 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis 308 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
300 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 309 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
301 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn 310 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
302 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn 311 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
303 | DConstraint _ => env 312 | DConstraint _ => env
304 | DExport _ => env 313 | DExport _ => env
305 314
306 fun sgiBinds env (sgi, _) = 315 fun sgiBinds env (sgi, loc) =
307 case sgi of 316 case sgi of
308 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE 317 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
309 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 318 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
319 | SgiDatatype (x, n, xncs) =>
320 let
321 val env = pushCNamedAs env x n (KType, loc) NONE
322 in
323 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
324 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
325 env xncs
326 end
327 | SgiDatatypeImp (x, n, m1, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
310 | SgiVal (x, n, t) => pushENamedAs env x n t 328 | SgiVal (x, n, t) => pushENamedAs env x n t
311 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 329 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
312 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 330 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
313 | SgiConstraint _ => env 331 | SgiConstraint _ => env
314 332
322 SOME v => SOME (v, (sgns, strs, cons)) 340 SOME v => SOME (v, (sgns, strs, cons))
323 | NONE => 341 | NONE =>
324 case sgi of 342 case sgi of
325 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 343 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
326 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 344 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
345 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
346 | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
327 | SgiVal _ => seek (sgis, sgns, strs, cons) 347 | SgiVal _ => seek (sgis, sgns, strs, cons)
328 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) 348 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
329 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) 349 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
330 | SgiConstraint _ => seek (sgis, sgns, strs, cons) 350 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
331 in 351 in
487 in 507 in
488 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc) 508 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
489 end 509 end
490 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 510 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
491 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 511 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
512 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
513 | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
492 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) 514 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
493 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) 515 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
494 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) 516 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
495 in 517 in
496 seek (sgis, IM.empty, IM.empty, IM.empty, []) 518 seek (sgis, IM.empty, IM.empty, IM.empty, [])