adam@1989: (* Copyright (c) 2014, Adam Chlipala
adam@1989:  * All rights reserved.
adam@1989:  *
adam@1989:  * Redistribution and use in source and binary forms, with or without
adam@1989:  * modification, are permitted provided that the following conditions are met:
adam@1989:  *
adam@1989:  * - Redistributions of source code must retain the above copyright notice,
adam@1989:  *   this list of conditions and the following disclaimer.
adam@1989:  * - Redistributions in binary form must reproduce the above copyright notice,
adam@1989:  *   this list of conditions and the following disclaimer in the documentation
adam@1989:  *   and/or other materials provided with the distribution.
adam@1989:  * - The names of contributors may not be used to endorse or promote products
adam@1989:  *   derived from this software without specific prior written permission.
adam@1989:  *
adam@1989:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adam@1989:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adam@1989:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adam@1989:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adam@1989:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adam@1989:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adam@1989:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adam@1989:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adam@1989:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adam@1989:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adam@1989:  * POSSIBILITY OF SUCH DAMAGE.
adam@1989:  *)
adam@1989: 
adam@1989: structure ExplRename :> EXPL_RENAME = struct
adam@1989: 
adam@1989: open Expl
adam@1989: structure E = ExplEnv
adam@1989: 
adam@1989: structure IM = IntBinaryMap
adam@1989: 
adam@1989: structure St :> sig
adam@1989:     type t
adam@1989: 
adam@1989:     val create : int -> t
adam@1989:     val next : t -> int
adam@1989: 
adam@1989:     val bind : t * int -> t * int
adam@1989:     val lookup: t * int -> int option
adam@1989: end = struct
adam@1989: 
adam@1989: type t = {next : int,
adam@1989:           renaming : int IM.map}
adam@1989: 
adam@1989: fun create next = {next = next,
adam@1989:                    renaming = IM.empty}
adam@1989: 
adam@1989: fun next (t : t) = #next t
adam@1989: 
adam@1989: fun bind ({next, renaming}, n) =
adam@1989:     ({next = next + 1,
adam@1989:       renaming = IM.insert (renaming, n, next)}, next)
adam@1989: 
adam@1989: fun lookup ({next, renaming}, n) =
adam@1989:     IM.find (renaming, n)
adam@1989: 
adam@1989: end
adam@1989: 
adam@1989: fun renameCon st (all as (c, loc)) =
adam@1989:     case c of
adam@1989:         TFun (c1, c2) => (TFun (renameCon st c1, renameCon st c2), loc)
adam@1989:       | TCFun (x, k, c) => (TCFun (x, k, renameCon st c), loc)
adam@1989:       | TRecord c => (TRecord (renameCon st c), loc)
adam@1989:       | CRel _ => all
adam@1989:       | CNamed n =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (CNamed n', loc))
adam@1989:       | CModProj (n, ms, x) =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (CModProj (n', ms, x), loc))
adam@1989:       | CApp (c1, c2) => (CApp (renameCon st c1, renameCon st c2), loc)
adam@1989:       | CAbs (x, k, c) => (CAbs (x, k, renameCon st c), loc)
adam@1989:       | CKAbs (x, c) => (CKAbs (x, renameCon st c), loc)
adam@1989:       | CKApp (c, k) => (CKApp (renameCon st c, k), loc)
adam@1989:       | TKFun (x, c) => (TKFun (x, renameCon st c), loc)
adam@1989:       | CName _ => all
adam@1989:       | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (renameCon st x, renameCon st c)) xcs), loc)
adam@1989:       | CConcat (c1, c2) => (CConcat (renameCon st c1, renameCon st c2), loc)
adam@1989:       | CMap _ => all
adam@1989:       | CUnit => all
adam@1989:       | CTuple cs => (CTuple (map (renameCon st) cs), loc)
adam@1989:       | CProj (c, n) => (CProj (renameCon st c, n), loc)
adam@1989: 
adam@1989: fun renamePatCon st pc =
adam@1989:     case pc of
adam@1989:         PConVar n =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => pc
adam@1989:            | SOME n' => PConVar n')
adam@1989:       | PConProj (n, ms, x) =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => pc
adam@1989:            | SOME n' => PConProj (n', ms, x))
adam@1989: 
adam@1989: fun renamePat st (all as (p, loc)) =
adam@1989:     case p of
adam@1989:         PWild => all
adam@1989:       | PVar (x, c) => (PVar (x, renameCon st c), loc)
adam@1989:       | PPrim _ => all
adam@1989:       | PCon (dk, pc, cs, po) => (PCon (dk, renamePatCon st pc,
adam@1989:                                         map (renameCon st) cs,
adam@1989:                                         Option.map (renamePat st) po), loc)
adam@1989:       | PRecord xpcs => (PRecord (map (fn (x, p, c) =>
adam@1989:                                           (x, renamePat st p, renameCon st c)) xpcs), loc)
adam@1989: 
adam@1989: fun renameExp st (all as (e, loc)) =
adam@1989:     case e of
adam@1989:         EPrim _ => all
adam@1989:       | ERel _ => all
adam@1989:       | ENamed n =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (ENamed n', loc))
adam@1989:       | EModProj (n, ms, x) =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (EModProj (n', ms, x), loc))
adam@1989:       | EApp (e1, e2) => (EApp (renameExp st e1, renameExp st e2), loc)
adam@1989:       | EAbs (x, dom, ran, e) => (EAbs (x, renameCon st dom, renameCon st ran, renameExp st e), loc)
adam@1989:       | ECApp (e, c) => (ECApp (renameExp st e, renameCon st c), loc)
adam@1989:       | ECAbs (x, k, e) => (ECAbs (x, k, renameExp st e), loc)
adam@1989:       | EKAbs (x, e) => (EKAbs (x, renameExp st e), loc)
adam@1989:       | EKApp (e, k) => (EKApp (renameExp st e, k), loc)
adam@1989:       | ERecord xecs => (ERecord (map (fn (x, e, c) => (renameCon st x,
adam@1989:                                                         renameExp st e,
adam@1989:                                                         renameCon st c)) xecs), loc)
adam@1989:       | EField (e, c, {field, rest}) => (EField (renameExp st e,
adam@1989:                                                  renameCon st c,
adam@1989:                                                  {field = renameCon st field,
adam@1989:                                                   rest = renameCon st rest}), loc)
adam@1989:       | EConcat (e1, c1, e2, c2) => (EConcat (renameExp st e1,
adam@1989:                                               renameCon st c1,
adam@1989:                                               renameExp st e2,
adam@1989:                                               renameCon st c2), loc)
adam@1989:       | ECut (e, c, {field, rest}) => (ECut (renameExp st e,
adam@1989:                                              renameCon st c,
adam@1989:                                              {field = renameCon st field,
adam@1989:                                               rest = renameCon st rest}), loc)
adam@1989:       | ECutMulti (e, c, {rest}) => (ECutMulti (renameExp st e,
adam@1989:                                                 renameCon st c,
adam@1989:                                                 {rest = renameCon st rest}), loc)
adam@1989:       | ECase (e, pes, {disc, result}) => (ECase (renameExp st e,
adam@1989:                                                   map (fn (p, e) => (renamePat st p, renameExp st e)) pes,
adam@1989:                                                   {disc = renameCon st disc,
adam@1989:                                                    result = renameCon st result}), loc)
adam@1989:       | EWrite e => (EWrite (renameExp st e), loc)
adam@1989:       | ELet (x, c1, e1, e2) => (ELet (x, renameCon st c1,
adam@1989:                                       renameExp st e1,
adam@1989:                                       renameExp st e2), loc)
adam@1989: 
adam@1989: fun renameSitem st (all as (si, loc)) =
adam@1989:     case si of
adam@1989:         SgiConAbs _ => all
adam@1989:       | SgiCon (x, n, k, c) => (SgiCon (x, n, k, renameCon st c), loc)
adam@1989:       | SgiDatatype dts => (SgiDatatype (map (fn (x, n, xs, cns) =>
adam@1989:                                                  (x, n, xs,
adam@1989:                                                   map (fn (x, n, co) =>
adam@1989:                                                           (x, n, Option.map (renameCon st) co)) cns)) dts),
adam@1989:                             loc)
adam@1989:       | SgiDatatypeImp (x, n, n', xs, x', xs', cns) =>
adam@1989:         (SgiDatatypeImp (x, n, n', xs, x', xs',
adam@1989:                          map (fn (x, n, co) =>
adam@1989:                                  (x, n, Option.map (renameCon st) co)) cns), loc)
adam@1989:       | SgiVal (x, n, c) => (SgiVal (x, n, renameCon st c), loc)
adam@1989:       | SgiSgn (x, n, sg) => (SgiSgn (x, n, renameSgn st sg), loc)
adam@1989:       | SgiStr (x, n, sg) => (SgiStr (x, n, renameSgn st sg), loc)
adam@1989: 
adam@1989: and renameSgn st (all as (sg, loc)) =
adam@1989:     case sg of
adam@1989:         SgnConst sis => (SgnConst (map (renameSitem st) sis), loc)
adam@1989:       | SgnVar n =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (SgnVar n', loc))
adam@1989:       | SgnFun (x, n, dom, ran) => (SgnFun (x, n, renameSgn st dom, renameSgn st ran), loc)
adam@1989:       | SgnWhere (sg, xs, s, c) => (SgnWhere (renameSgn st sg, xs, s, renameCon st c), loc)
adam@1989:       | SgnProj (n, ms, x) =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (SgnProj (n', ms, x), loc))
adam@1989: 
adam@1989: fun renameDecl st (all as (d, loc)) =
adam@1989:     case d of
adam@1989:         DCon (x, n, k, c) => (DCon (x, n, k, renameCon st c), loc)
adam@1989:       | DDatatype dts => (DDatatype (map (fn (x, n, xs, cns) =>
adam@1989:                                              (x, n, xs,
adam@1989:                                               map (fn (x, n, co) =>
adam@1989:                                                       (x, n, Option.map (renameCon st) co)) cns)) dts),
adam@1989:                           loc)
adam@1989:       | DDatatypeImp (x, n, n', xs, x', xs', cns) =>
adam@1989:         (DDatatypeImp (x, n, n', xs, x', xs',
adam@1989:                        map (fn (x, n, co) =>
adam@1989:                                (x, n, Option.map (renameCon st) co)) cns), loc)
adam@1989:       | DVal (x, n, c, e) => (DVal (x, n, renameCon st c, renameExp st e), loc)
adam@1989:       | DValRec vis => (DValRec (map (fn (x, n, c, e) => (x, n, renameCon st c, renameExp st e)) vis), loc)
adam@1989:       | DSgn (x, n, sg) => (DSgn (x, n, renameSgn st sg), loc)
adam@1989:       | DStr (x, n, sg, str) => (DStr (x, n, renameSgn st sg, renameStr st str), loc)
adam@1989:       | DFfiStr (x, n, sg) => (DFfiStr (x, n, renameSgn st sg), loc)
adam@1989:       | DExport (n, sg, str) =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (DExport (n', renameSgn st sg, renameStr st str), loc))
adam@1989:       | DTable (n, x, m, c1, e1, c2, e2, c3) =>
adam@1989:         (DTable (n, x, m, renameCon st c1, renameExp st e1, renameCon st c2,
adam@1989:                  renameExp st e2, renameCon st c3), loc)
adam@1989:       | DSequence _ => all
adam@1989:       | DView (n, x, n', e, c) => (DView (n, x, n', renameExp st e, renameCon st c), loc)
adam@1989:       | DDatabase _ => all
adam@1989:       | DCookie (n, x, n', c) => (DCookie (n, x, n', renameCon st c), loc)
adam@1989:       | DStyle _ => all
adam@1989:       | DTask (e1, e2) => (DTask (renameExp st e1, renameExp st e2), loc)
adam@1989:       | DPolicy e => (DPolicy (renameExp st e), loc)
adam@1989:       | DOnError (n, xs, x) =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (DOnError (n', xs, x), loc))
adam@2010:       | DFfi (x, n, modes, t) => (DFfi (x, n, modes, renameCon st t), loc)
adam@1989: 
adam@1989: and renameStr st (all as (str, loc)) =
adam@1989:     case str of
adam@1989:         StrConst ds => (StrConst (map (renameDecl st) ds), loc)
adam@1989:       | StrVar n =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => all
adam@1989:            | SOME n' => (StrVar n', loc))
adam@1989:       | StrProj (str, x) => (StrProj (renameStr st str, x), loc)
adam@1989:       | StrFun (x, n, dom, ran, str) => (StrFun (x, n, renameSgn st dom,
adam@1989:                                                  renameSgn st ran,
adam@1989:                                                  renameStr st str), loc)
adam@1989:       | StrApp (str1, str2) => (StrApp (renameStr st str1, renameStr st str2), loc)
adam@1989: 
adam@1989: 
adam@1989: 
adam@1989: fun fromArity (n, loc) =
adam@1989:     case n of
adam@1989:         0 => (KType, loc)
adam@1989:       | _ => (KArrow ((KType, loc), fromArity (n - 1, loc)), loc)
adam@1989: 
adam@1989: fun dupDecl (all as (d, loc), st) =
adam@1989:     case d of
adam@1989:         DCon (x, n, k, c) =>
adam@1989:         let
adam@1989:             val (st, n') = St.bind (st, n)
adam@1989:         in
adam@1989:             ([(DCon (x, n, k, renameCon st c), loc),
adam@1989:               (DCon (x, n', k, (CNamed n, loc)), loc)],
adam@1989:              st)
adam@1989:         end
adam@1989:       | DDatatype dts =>
adam@1989:         let
adam@1990:             val d = (DDatatype (map (fn (x, n, xs, cns) =>
adam@1990:                                         (x, n, xs,
adam@1990:                                          map (fn (x, n, co) =>
adam@1990:                                                  (x, n, Option.map (renameCon st) co)) cns)) dts),
adam@1990:                      loc)
adam@1990: 
adam@1989:             val (dts', st) = ListUtil.foldlMap (fn ((x, n, xs, cns), st) =>
adam@1989:                                                    let
adam@1989:                                                        val (st, n') = St.bind (st, n)
adam@1989: 
adam@1989:                                                        val (cns', st) = ListUtil.foldlMap
adam@1989:                                                                             (fn ((x, n, _), st) =>
adam@1989:                                                                                 let
adam@1989:                                                                                     val (st, n') =
adam@1989:                                                                                         St.bind (st, n)
adam@1989:                                                                                 in
adam@1989:                                                                                     ((x, n, n'), st)
adam@1989:                                                                                 end) st cns
adam@1989:                                                    in
adam@1989:                                                        ((x, n, length xs, n', cns'), st)
adam@1989:                                                    end) st dts
adam@1989: 
adam@1989:             val env = E.declBinds E.empty d
adam@1989:         in
adam@1989:             (d
adam@1989:              :: map (fn (x, n, arity, n', _) =>
adam@1989:                         (DCon (x, n', fromArity (arity, loc), (CNamed n, loc)), loc)) dts'
adam@1989:              @ ListUtil.mapConcat (fn (_, _, _, _, cns') =>
adam@1989:                                       map (fn (x, n, n') =>
adam@1989:                                               (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)),
adam@1989:                                                loc)) cns') dts',
adam@1989:              st)
adam@1989:         end
adam@1989:       | DDatatypeImp (x, n, n', xs, x', xs', cns) =>
adam@1989:         let
adam@1990:             val d = (DDatatypeImp (x, n, n', xs, x', xs',
adam@1990:                                    map (fn (x, n, co) =>
adam@1990:                                            (x, n, Option.map (renameCon st) co)) cns), loc)
adam@1990: 
adam@1989:             val (cns', st) = ListUtil.foldlMap
adam@1989:                                  (fn ((x, n, _), st) =>
adam@1989:                                      let
adam@1989:                                          val (st, n') =
adam@1989:                                              St.bind (st, n)
adam@1989:                                      in
adam@1989:                                          ((x, n, n'), st)
adam@1989:                                      end) st cns
adam@1989: 
adam@1989:             val (st, n') = St.bind (st, n)
adam@1989: 
adam@1989:             val env = E.declBinds E.empty d
adam@1989:         in
adam@1989:             (d
adam@1989:              :: (DCon (x, n', fromArity (length xs, loc), (CNamed n, loc)), loc)
adam@1989:              :: map (fn (x, n, n') =>
adam@1989:                         (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)),
adam@1989:                          loc)) cns',
adam@1989:              st)
adam@1989:         end
adam@1989:       | DVal (x, n, c, e) =>
adam@1989:         let
adam@1989:             val (st, n') = St.bind (st, n)
adam@1989:             val c' = renameCon st c
adam@1989:         in
adam@1989:             ([(DVal (x, n, c', renameExp st e), loc),
adam@1989:               (DVal (x, n', c', (ENamed n, loc)), loc)],
adam@1989:              st)
adam@1989:         end
adam@1989:       | DValRec vis =>
adam@1989:         let
adam@1989:             val d = (DValRec (map (fn (x, n, c, e) => (x, n, renameCon st c, renameExp st e)) vis), loc)
adam@1989: 
adam@1989:             val (vis', st) = ListUtil.foldlMap (fn ((x, n, _, _), st) =>
adam@1989:                                                    let
adam@1989:                                                        val (st, n') = St.bind (st, n)
adam@1989:                                                    in
adam@1989:                                                        ((x, n, n'), st)
adam@1989:                                                    end) st vis
adam@1989: 
adam@1989:             val env = E.declBinds E.empty d
adam@1989:         in
adam@1989:             (d
adam@1989:              :: map (fn (x, n, n') => (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)), loc)) vis',
adam@1989:              st)
adam@1989:         end
adam@1989:       | DSgn (x, n, sg) =>
adam@1989:         let
adam@1989:             val (st, n') = St.bind (st, n)
adam@1989:         in
adam@1989:             ([(DSgn (x, n, renameSgn st sg), loc),
adam@1989:               (DSgn (x, n', (SgnVar n, loc)), loc)],
adam@1989:              st)
adam@1989:         end
adam@1989:       | DStr (x, n, sg, str) =>
adam@1989:         let
adam@1989:             val (st, n') = St.bind (st, n)
adam@1989:             val sg' = renameSgn st sg
adam@1989:         in
adam@1989:             ([(DStr (x, n, sg', renameStr st str), loc),
adam@1989:               (DStr (x, n', sg', (StrVar n, loc)), loc)],
adam@1989:              st)
adam@1989:         end
adam@1989:       | DFfiStr (x, n, sg) => ([(DFfiStr (x, n, renameSgn st sg), loc)], st)
adam@1989:       | DExport (n, sg, str) =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => ([all], st)
adam@1989:            | SOME n' => ([(DExport (n', renameSgn st sg, renameStr st str), loc)], st))
adam@1989:       | DTable (n, x, m, c1, e1, c2, e2, c3) =>
adam@1989:         let
adam@1989:             val (st, m') = St.bind (st, m)
adam@1989: 
adam@1989:             val d = (DTable (n, x, m, renameCon st c1, renameExp st e1, renameCon st c2,
adam@1989:                              renameExp st e2, renameCon st c3), loc)
adam@1989: 
adam@1989:             val env = E.declBinds E.empty d
adam@1989:         in
adam@1989:             ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989:         end
adam@1989:       | DSequence (n, x, m) =>
adam@1989:         let
adam@1989:             val (st, m') = St.bind (st, m)
adam@1989: 
adam@1989:             val env = E.declBinds E.empty all
adam@1989:         in
adam@1989:             ([all, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989:         end
adam@1989:       | DView (n, x, m, e, c) =>
adam@1989:         let
adam@1989:             val (st, m') = St.bind (st, m)
adam@1989: 
adam@1989:             val d = (DView (n, x, m, renameExp st e, renameCon st c), loc)
adam@1989: 
adam@1989:             val env = E.declBinds E.empty d
adam@1989:         in
adam@1989:             ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989:         end
adam@1989:       | DDatabase _ => ([all], st)
adam@1989:       | DCookie (n, x, m, c) =>
adam@1989:         let
adam@1989:             val (st, m') = St.bind (st, m)
adam@1989: 
adam@1989:             val d = (DCookie (n, x, m, renameCon st c), loc)
adam@1989: 
adam@1989:             val env = E.declBinds E.empty d
adam@1989:         in
adam@1989:             ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989:         end
adam@1989:       | DStyle (n, x, m) =>
adam@1989:         let
adam@1989:             val (st, m') = St.bind (st, m)
adam@1989: 
adam@1989:             val env = E.declBinds E.empty all
adam@1989:         in
adam@1989:             ([all, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989:         end
adam@1989:       | DTask (e1, e2) => ([(DTask (renameExp st e1, renameExp st e2), loc)], st)
adam@1989:       | DPolicy e => ([(DPolicy (renameExp st e), loc)], st)
adam@1989:       | DOnError (n, xs, x) =>
adam@1989:         (case St.lookup (st, n) of
adam@1989:              NONE => ([all], st)
adam@1989:            | SOME n' => ([(DOnError (n', xs, x), loc)], st))
adam@2010:       | DFfi (x, n, modes, t) =>
adam@2010:         let
adam@2010:             val (st, n') = St.bind (st, n)
adam@2010:             val t' = renameCon st t
adam@2010:         in
adam@2010:             ([(DFfi (x, n, modes, t'), loc),
adam@2010:               (DVal (x, n', t', (ENamed n, loc)), loc)],
adam@2010:              st)
adam@2010:         end
adam@1989: 
adam@1989: fun rename {NextId, FormalName, FormalId, Body = all as (str, loc)} =
adam@1989:     case str of
adam@1989:         StrConst ds =>
adam@1989:         let
adam@1989:             val st = St.create NextId
adam@1989:             val (st, n) = St.bind (st, FormalId)
adam@1989:                      
adam@1989:             val (ds, st) = ListUtil.foldlMapConcat dupDecl st ds
adam@1991: 
adam@1991:             (* Revenge of the functor parameter renamer!
adam@1991:              * See comment in elaborate.sml for the start of the saga.
adam@1991:              * We need to alpha-rename the argument to allow sufficient shadowing in the body. *)
adam@1991: 
adam@1991:             fun mungeName m =
adam@1991:                 if List.exists (fn (DStr (x, _, _, _), _) => x = m
adam@1991:                                  | _ => false) ds then
adam@1991:                     mungeName ("?" ^ m)
adam@1991:                 else
adam@1991:                     m
adam@1991: 
adam@1991:             val FormalName = mungeName FormalName
adam@1991: 
adam@1989:             val ds = (DStr (FormalName, n, (SgnConst [], loc), (StrVar FormalId, loc)), loc) :: ds
adam@1989:         in
adam@1989:             (St.next st, (StrConst ds, loc))
adam@1989:         end
adam@1989:       | _ => (NextId, all)
adam@1989: 
adam@1989: end