diff options
author | Adam Chlipala <adam@chlipala.net> | 2014-02-20 15:50:33 -0500 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2014-02-20 15:50:33 -0500 |
commit | c3b5b20061b27b3533645def1a9cdea53eba2f83 (patch) | |
tree | 1a606412147d4e63047ac96534fd12868d2ae40f /src/expl_rename.sml | |
parent | 023d9ecbbc2bd1fc14098e84f5b0216da12a48a0 (diff) |
Tweaked parameter renaming for functors, so now demos and the original bug-triggering application work
Diffstat (limited to 'src/expl_rename.sml')
-rw-r--r-- | src/expl_rename.sml | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/expl_rename.sml b/src/expl_rename.sml index a17e0a3b..7e7a155a 100644 --- a/src/expl_rename.sml +++ b/src/expl_rename.sml @@ -422,6 +422,20 @@ fun rename {NextId, FormalName, FormalId, Body = all as (str, loc)} = val (st, n) = St.bind (st, FormalId) val (ds, st) = ListUtil.foldlMapConcat dupDecl st ds + + (* Revenge of the functor parameter renamer! + * See comment in elaborate.sml for the start of the saga. + * We need to alpha-rename the argument to allow sufficient shadowing in the body. *) + + fun mungeName m = + if List.exists (fn (DStr (x, _, _, _), _) => x = m + | _ => false) ds then + mungeName ("?" ^ m) + else + m + + val FormalName = mungeName FormalName + val ds = (DStr (FormalName, n, (SgnConst [], loc), (StrVar FormalId, loc)), loc) :: ds in (St.next st, (StrConst ds, loc)) |