Mercurial > urweb

comparison src/elab_util.sml @ 162:06a98129b23f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add datatype import constructor annotations; datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 12:30:04 -0400
parents 34ccd7d2bea8
children c7a6e6dbc318
comparison
equal deleted inserted replaced
161:a5ae7b3e37a4 162:06a98129b23f
384 | SOME c => 384 | SOME c =>
385 S.map2 (con ctx c, 385 S.map2 (con ctx c,
386 fn c' => (x, n, SOME c'))) xncs, 386 fn c' => (x, n, SOME c'))) xncs,
387 fn xncs' => 387 fn xncs' =>
388 (SgiDatatype (x, n, xncs'), loc)) 388 (SgiDatatype (x, n, xncs'), loc))
389 | SgiDatatypeImp _ => S.return2 siAll 389 | SgiDatatypeImp (x, n, m1, ms, s, xncs) =>
390 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
391 case c of
392 NONE => S.return2 (x, n, c)
393 | SOME c =>
394 S.map2 (con ctx c,
395 fn c' => (x, n, SOME c'))) xncs,
396 fn xncs' =>
397 (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc))
390 | SgiVal (x, n, c) => 398 | SgiVal (x, n, c) =>
391 S.map2 (con ctx c, 399 S.map2 (con ctx c,
392 fn c' => 400 fn c' =>
393 (SgiVal (x, n, c'), loc)) 401 (SgiVal (x, n, c'), loc))
394 | SgiStr (x, n, s) => 402 | SgiStr (x, n, s) =>
418 bind (ctx, NamedC (x, k)) 426 bind (ctx, NamedC (x, k))
419 | SgiCon (x, _, k, _) => 427 | SgiCon (x, _, k, _) =>
420 bind (ctx, NamedC (x, k)) 428 bind (ctx, NamedC (x, k))
421 | SgiDatatype (x, n, xncs) => 429 | SgiDatatype (x, n, xncs) =>
422 bind (ctx, NamedC (x, (KType, loc))) 430 bind (ctx, NamedC (x, (KType, loc)))
423 | SgiDatatypeImp (x, _, _, _, _) => 431 | SgiDatatypeImp (x, _, _, _, _, _) =>
424 bind (ctx, NamedC (x, (KType, loc))) 432 bind (ctx, NamedC (x, (KType, loc)))
425 | SgiVal _ => ctx 433 | SgiVal _ => ctx
426 | SgiStr (x, _, sgn) => 434 | SgiStr (x, _, sgn) =>
427 bind (ctx, Str (x, sgn)) 435 bind (ctx, Str (x, sgn))
428 | SgiSgn (x, _, sgn) => 436 | SgiSgn (x, _, sgn) =>
539 in 547 in
540 bind (ctx, NamedE (x, (t, loc))) 548 bind (ctx, NamedE (x, (t, loc)))
541 end) 549 end)
542 ctx xncs 550 ctx xncs
543 end 551 end
544 | DDatatypeImp (x, n, m, ms, x') => 552 | DDatatypeImp (x, n, m, ms, x', _) =>
545 bind (ctx, NamedC (x, (KType, loc))) 553 bind (ctx, NamedC (x, (KType, loc)))
546 | DVal (x, _, c, _) => 554 | DVal (x, _, c, _) =>
547 bind (ctx, NamedE (x, c)) 555 bind (ctx, NamedE (x, c))
548 | DValRec vis => 556 | DValRec vis =>
549 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis 557 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
596 | SOME c => 604 | SOME c =>
597 S.map2 (mfc ctx c, 605 S.map2 (mfc ctx c,
598 fn c' => (x, n, SOME c'))) xncs, 606 fn c' => (x, n, SOME c'))) xncs,
599 fn xncs' => 607 fn xncs' =>
600 (DDatatype (x, n, xncs'), loc)) 608 (DDatatype (x, n, xncs'), loc))
601 | DDatatypeImp _ => S.return2 dAll 609 | DDatatypeImp (x, n, m1, ms, s, xncs) =>
610 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
611 case c of
612 NONE => S.return2 (x, n, c)
613 | SOME c =>
614 S.map2 (mfc ctx c,
615 fn c' => (x, n, SOME c'))) xncs,
616 fn xncs' =>
617 (DDatatypeImp (x, n, m1, ms, s, xncs'), loc))
602 | DVal vi => 618 | DVal vi =>
603 S.map2 (mfvi ctx vi, 619 S.map2 (mfvi ctx vi,
604 fn vi' => 620 fn vi' =>
605 (DVal vi', loc)) 621 (DVal vi', loc))
606 | DValRec vis => 622 | DValRec vis =>