Mercurial > urweb

comparison src/cjrize.sml @ 809:81fce435e255

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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