Mercurial > urweb
comparison src/cjrize.sml @ 809:81fce435e255
Mutual datatypes through Cjrize
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 16 May 2009 16:02:17 -0400 |
parents | d8f58d488cfb |
children | 493f44759879 |
comparison
equal
deleted
inserted
replaced
808:d8f58d488cfb | 809:81fce435e255 |
---|---|
481 | L.ERecv _ => raise Fail "Cjrize ERecv" | 481 | L.ERecv _ => raise Fail "Cjrize ERecv" |
482 | L.ESleep _ => raise Fail "Cjrize ESleep" | 482 | L.ESleep _ => raise Fail "Cjrize ESleep" |
483 | 483 |
484 fun cifyDecl ((d, loc), sm) = | 484 fun cifyDecl ((d, loc), sm) = |
485 case d of | 485 case d of |
486 L.DDatatype _ => raise Fail "Cjrize DDatatype" | 486 L.DDatatype dts => |
487 (*L.DDatatype (x, n, xncs) => | 487 let |
488 let | 488 val (dts, sm) = ListUtil.foldlMap |
489 val dk = ElabUtil.classifyDatatype xncs | 489 (fn ((x, n, xncs), sm) => |
490 val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) => | 490 let |
491 case to of | 491 val dk = ElabUtil.classifyDatatype xncs |
492 NONE => ((x, n, NONE), sm) | 492 val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) => |
493 | SOME t => | 493 case to of |
494 let | 494 NONE => ((x, n, NONE), sm) |
495 val (t, sm) = cifyTyp (t, sm) | 495 | SOME t => |
496 in | 496 let |
497 ((x, n, SOME t), sm) | 497 val (t, sm) = cifyTyp (t, sm) |
498 end) sm xncs | 498 in |
499 in | 499 ((x, n, SOME t), sm) |
500 (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm) | 500 end) sm xncs |
501 end*) | 501 in |
502 ((dk, x, n, xncs), sm) | |
503 end) | |
504 sm dts | |
505 in | |
506 (SOME (L'.DDatatype dts, loc), NONE, sm) | |
507 end | |
502 | 508 |
503 | L.DVal (x, n, t, e, _) => | 509 | L.DVal (x, n, t, e, _) => |
504 let | 510 let |
505 val (t, sm) = cifyTyp (t, sm) | 511 val (t, sm) = cifyTyp (t, sm) |
506 | 512 |
641 val (dsF, ds, ps, sm) = foldl (fn (d, (dsF, ds, ps, sm)) => | 647 val (dsF, ds, ps, sm) = foldl (fn (d, (dsF, ds, ps, sm)) => |
642 let | 648 let |
643 val (dop, pop, sm) = cifyDecl (d, sm) | 649 val (dop, pop, sm) = cifyDecl (d, sm) |
644 | 650 |
645 val dsF = case dop of | 651 val dsF = case dop of |
646 SOME (L'.DDatatype (dk, x, n, _), loc) => | 652 SOME (L'.DDatatype dts, loc) => |
647 (L'.DDatatypeForward (dk, x, n), loc) :: dsF | 653 map (fn (dk, x, n, _) => |
654 (L'.DDatatypeForward (dk, x, n), loc)) dts @ dsF | |
648 | _ => dsF | 655 | _ => dsF |
649 | 656 |
650 val dsF = map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm) | 657 val dsF = map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm) |
651 @ dsF | 658 @ dsF |
652 | 659 |