diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-07-24 16:51:24 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-07-24 16:51:24 -0400 |
| commit | 21f2ec92093d2b00afe3d36476f20f45b4d4a194 (patch) | |
| tree | 8de7577779ac35e209b858774c748dd1261bd3d5 /src | |
| parent | f9f2ae472f9c0ef861df8d087529b26b734bf191 (diff) | |
Normalize datatype choice during SgiDatatypeImp elaboration
Diffstat (limited to 'src')
| -rw-r--r-- | src/elaborate.sml | 48 |
1 files changed, 26 insertions, 22 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 1753313f..802cef7b 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1337,28 +1337,32 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | 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 - - 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 + 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, gs)) + end) + | _ => (strError env (NotDatatype loc); + ([], (env, denv, []))) end) | L.SgiVal (x, c) => |