diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2014-02-14 15:11:22 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2014-02-14 15:11:22 -0500 |
| commit | 03733e0e5291ca5b07270dabd71e9773a9930721 (patch) | |
| tree | b74bb91f14dc7c250113d1f205b43a431e93f7ee /src/elaborate.sml | |
| parent | 5537bc4338b4a576b225810c5cca34d3ca7de87f (diff) | |
Fix a subtle renaming problem in elaborating functor applications
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 0c8db756..959a6cd1 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -4481,9 +4481,28 @@ and elabStr (env, denv) (str, loc) = case #1 (hnormSgn env ran) of L'.SgnError => (strerror, sgnerror, []) | L'.SgnConst sgis => - ((L'.StrApp (str1', str2'), loc), - (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), - gs1 @ gs2) + let + (* This code handles a tricky case that led to a very nasty bug. + * An invariant about signatures of elaborated modules is that no + * identifier that could appear directly in a program is defined + * twice. We add "?" in front of identifiers where necessary to + * maintain the invariant, but the code below, to extend a functor + * body with a binding for the functor argument, wasn't written + * with the invariant in mind. Luckily for us, references to + * an identifier later within a signature work by globally + * unique index, so we just need to change the string name in the + * new declaration. *) + val m = + if List.exists (fn (L'.SgiStr (x, _, _), _) => x = m + | _ => false) sgis then + "?" ^ m + else + m + in + ((L'.StrApp (str1', str2'), loc), + (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), + gs1 @ gs2) + end | _ => raise Fail "Unable to hnormSgn in functor application") | _ => (strError env (NotFunctor sgn1); (strerror, sgnerror, [])) |