From 21f2ec92093d2b00afe3d36476f20f45b4d4a194 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 24 Jul 2008 16:51:24 -0400 Subject: Normalize datatype choice during SgiDatatypeImp elaboration --- src/elaborate.sml | 48 ++++++++++++++++++++++++++---------------------- 1 file changed, 26 insertions(+), 22 deletions(-) (limited to 'src') 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) => -- cgit v1.2.3