diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-05-16 16:02:17 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-16 16:02:17 -0400 |
| commit | 2396dd1bd2bdaeb7608d88bbb2f890b5788852c0 (patch) | |
| tree | df44fd4952ee16f262cce3e4a063352e534aee25 /src/cjrize.sml | |
| parent | 30b78a96ae699fa2282c07a2dbf3e6303f99e32c (diff) | |
Mutual datatypes through Cjrize
Diffstat (limited to 'src/cjrize.sml')
| -rw-r--r-- | src/cjrize.sml | 43 |
1 files changed, 25 insertions, 18 deletions
diff --git a/src/cjrize.sml b/src/cjrize.sml index 9c2128bc..c4d916eb 100644 --- a/src/cjrize.sml +++ b/src/cjrize.sml @@ -483,22 +483,28 @@ fun cifyExp (eAll as (e, loc), sm) = fun cifyDecl ((d, loc), sm) = case d of - L.DDatatype _ => raise Fail "Cjrize DDatatype" - (*L.DDatatype (x, n, xncs) => - 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 - (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm) - end*) + L.DDatatype dts => + let + 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 dts, loc), NONE, sm) + end | L.DVal (x, n, t, e, _) => let @@ -643,8 +649,9 @@ fun cjrize ds = 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) |