Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- a/src/cjrize.sml Sat May 16 15:55:15 2009 -0400 +++ b/src/cjrize.sml Sat May 16 16:02:17 2009 -0400 @@ -483,22 +483,28 @@ fun cifyDecl ((d, loc), sm) = case d of - L.DDatatype _ => raise Fail "Cjrize DDatatype" - (*L.DDatatype (x, n, xncs) => + L.DDatatype dts => let - val dk = ElabUtil.classifyDatatype xncs - val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) => - case to of - NONE => ((x, n, NONE), sm) - | SOME t => - let - val (t, sm) = cifyTyp (t, sm) - in - ((x, n, SOME t), sm) - end) sm xncs + val (dts, sm) = ListUtil.foldlMap + (fn ((x, n, xncs), sm) => + let + val dk = ElabUtil.classifyDatatype xncs + val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) => + case to of + NONE => ((x, n, NONE), sm) + | SOME t => + let + val (t, sm) = cifyTyp (t, sm) + in + ((x, n, SOME t), sm) + end) sm xncs + in + ((dk, x, n, xncs), sm) + end) + sm dts in - (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm) - end*) + (SOME (L'.DDatatype dts, loc), NONE, sm) + end | L.DVal (x, n, t, e, _) => let @@ -643,8 +649,9 @@ val (dop, pop, sm) = cifyDecl (d, sm) val dsF = case dop of - SOME (L'.DDatatype (dk, x, n, _), loc) => - (L'.DDatatypeForward (dk, x, n), loc) :: dsF + SOME (L'.DDatatype dts, loc) => + map (fn (dk, x, n, _) => + (L'.DDatatypeForward (dk, x, n), loc)) dts @ dsF | _ => dsF val dsF = map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm)