Mercurial > urweb
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, |