diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-05-16 15:55:15 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-16 15:55:15 -0400 |
| commit | ac6a31d08025c413f89961a17b35321be8a41fc7 (patch) | |
| tree | 42c21054472ff028fbeaba0f8af6534d23662ad0 /src/monoize.sml | |
| parent | 3d77d43fda3acfa1d5f1e12c836718d79fdf84db (diff) | |
Mutual datatypes through Pathcheck
Diffstat (limited to 'src/monoize.sml')
| -rw-r--r-- | src/monoize.sml | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/src/monoize.sml b/src/monoize.sml index e4175015..50bd04e8 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -3045,27 +3045,30 @@ fun monoDecl (env, fm) (all as (d, loc)) = in case d of L.DCon _ => NONE - | L.DDatatype _ => raise Fail "Monoize DDatatype" - (*| L.DDatatype (x, n, [], xncs) => + | L.DDatatype [("list", n, [_], [("Nil", _, NONE), + ("Cons", _, SOME (L.TRecord (L.CRecord (_, + [((L.CName "1", _), + (L.CRel 0, _)), + ((L.CName "2", _), + (L.CApp ((L.CNamed n', _), + (L.CRel 0, _)), + _))]), _), _))])] => + if n = n' then + NONE + else + poly () + | L.DDatatype dts => let val env' = Env.declBinds env all - val d = (L'.DDatatype (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env') to)) xncs), loc) + val dts = map (fn (x, n, [], xncs) => + (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env') to)) xncs) + | _ => (E.errorAt loc "Polymorphic datatype needed too late"; + Print.eprefaces' [("Declaration", CorePrint.p_decl env all)]; + ("", 0, []))) dts + val d = (L'.DDatatype dts, loc) in SOME (env', fm, [d]) end - | L.DDatatype ("list", n, [_], [("Nil", _, NONE), - ("Cons", _, SOME (L.TRecord (L.CRecord (_, - [((L.CName "1", _), - (L.CRel 0, _)), - ((L.CName "2", _), - (L.CApp ((L.CNamed n', _), - (L.CRel 0, _)), - _))]), _), _))]) => - if n = n' then - NONE - else - poly () - | L.DDatatype _ => poly ()*) | L.DVal (x, n, t, e, s) => let val (e, fm) = monoExp (env, St.empty, fm) e |