Mercurial > urweb
changeset 1968:2c075e875a47
Fix a subtle renaming problem in elaborating functor applications
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 14 Feb 2014 15:11:22 -0500 |
| parents | fca98a6cbe23 |
| children | f463c773ed6a 5195378deeca |
| files | src/elaborate.sml |
| diffstat | 1 files changed, 22 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Sun Feb 09 19:29:50 2014 -0500 +++ b/src/elaborate.sml Fri Feb 14 15:11:22 2014 -0500 @@ -4481,9 +4481,28 @@ 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, []))