comparison src/monoize.sml @ 808:d8f58d488cfb

Mutual datatypes through Pathcheck
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:55:15 -0400
parents 61a1f5c5ae2c
children 7b380e2b9e68
comparison
equal deleted inserted replaced
807:61a1f5c5ae2c 808:d8f58d488cfb
3043 Print.eprefaces' [("Declaration", CorePrint.p_decl env all)]; 3043 Print.eprefaces' [("Declaration", CorePrint.p_decl env all)];
3044 NONE) 3044 NONE)
3045 in 3045 in
3046 case d of 3046 case d of
3047 L.DCon _ => NONE 3047 L.DCon _ => NONE
3048 | L.DDatatype _ => raise Fail "Monoize DDatatype" 3048 | L.DDatatype [("list", n, [_], [("Nil", _, NONE),
3049 (*| L.DDatatype (x, n, [], xncs) => 3049 ("Cons", _, SOME (L.TRecord (L.CRecord (_,
3050 let 3050 [((L.CName "1", _),
3051 val env' = Env.declBinds env all 3051 (L.CRel 0, _)),
3052 val d = (L'.DDatatype (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env') to)) xncs), loc) 3052 ((L.CName "2", _),
3053 in 3053 (L.CApp ((L.CNamed n', _),
3054 SOME (env', fm, [d]) 3054 (L.CRel 0, _)),
3055 end 3055 _))]), _), _))])] =>
3056 | L.DDatatype ("list", n, [_], [("Nil", _, NONE),
3057 ("Cons", _, SOME (L.TRecord (L.CRecord (_,
3058 [((L.CName "1", _),
3059 (L.CRel 0, _)),
3060 ((L.CName "2", _),
3061 (L.CApp ((L.CNamed n', _),
3062 (L.CRel 0, _)),
3063 _))]), _), _))]) =>
3064 if n = n' then 3056 if n = n' then
3065 NONE 3057 NONE
3066 else 3058 else
3067 poly () 3059 poly ()
3068 | L.DDatatype _ => poly ()*) 3060 | L.DDatatype dts =>
3061 let
3062 val env' = Env.declBinds env all
3063 val dts = map (fn (x, n, [], xncs) =>
3064 (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env') to)) xncs)
3065 | _ => (E.errorAt loc "Polymorphic datatype needed too late";
3066 Print.eprefaces' [("Declaration", CorePrint.p_decl env all)];
3067 ("", 0, []))) dts
3068 val d = (L'.DDatatype dts, loc)
3069 in
3070 SOME (env', fm, [d])
3071 end
3069 | L.DVal (x, n, t, e, s) => 3072 | L.DVal (x, n, t, e, s) =>
3070 let 3073 let
3071 val (e, fm) = monoExp (env, St.empty, fm) e 3074 val (e, fm) = monoExp (env, St.empty, fm) e
3072 in 3075 in
3073 SOME (Env.pushENamed env x n t NONE s, 3076 SOME (Env.pushENamed env x n t NONE s,