Mercurial > urweb
diff src/elaborate.sml @ 161:a5ae7b3e37a4
Normalize datatype choice during SgiDatatypeImp elaboration
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 24 Jul 2008 16:51:24 -0400 |
| parents | 870e8abbe3b9 |
| children | 06a98129b23f |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jul 24 16:48:47 2008 -0400 +++ b/src/elaborate.sml Thu Jul 24 16:51:24 2008 -0400 @@ -1337,28 +1337,32 @@ | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) ((L'.StrVar n, loc), sgn) ms in - case E.projectDatatype env {sgn = sgn, str = str, field = s} of - NONE => (conError env (UnboundDatatype (loc, s)); - ([], (env, denv, gs))) - | SOME xncs => - let - val k = (L'.KType, loc) - val t = (L'.CModProj (n, ms, s), loc) - val (env, n') = E.pushCNamed env x k (SOME t) - val env = E.pushDatatype env n' xncs + case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of + ((L'.CModProj (n, ms, s), _), gs) => + (case E.projectDatatype env {sgn = sgn, str = str, field = s} of + NONE => (conError env (UnboundDatatype (loc, s)); + ([], (env, denv, gs))) + | SOME xncs => + let + val k = (L'.KType, loc) + val t = (L'.CModProj (n, ms, s), loc) + val (env, n') = E.pushCNamed env x k (SOME t) + val env = E.pushDatatype env n' xncs - val t = (L'.CNamed n', loc) - val env = foldl (fn ((x, n, to), env) => - let - val t = case to of - NONE => t - | SOME t' => (L'.TFun (t', t), loc) - in - E.pushENamedAs env x n t - end) env xncs - in - ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, [])) - end + val t = (L'.CNamed n', loc) + val env = foldl (fn ((x, n, to), env) => + let + val t = case to of + NONE => t + | SOME t' => (L'.TFun (t', t), loc) + in + E.pushENamedAs env x n t + end) env xncs + in + ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs)) + end) + | _ => (strError env (NotDatatype loc); + ([], (env, denv, []))) end) | L.SgiVal (x, c) =>