Mercurial > urweb

annotate src/expl_rename.sml @ 2283:4afaab523213

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initialize invalidation to NULL!
author Ziv Scully <ziv@mit.edu>
date Thu, 12 Nov 2015 10:06:07 -0500
parents 403f0cc65b9c
children
rev   line source
adam@1989 1 (* Copyright (c) 2014, Adam Chlipala
adam@1989 2 * All rights reserved.
adam@1989 3 *
adam@1989 4 * Redistribution and use in source and binary forms, with or without
adam@1989 5 * modification, are permitted provided that the following conditions are met:
adam@1989 6 *
adam@1989 7 * - Redistributions of source code must retain the above copyright notice,
adam@1989 8 * this list of conditions and the following disclaimer.
adam@1989 9 * - Redistributions in binary form must reproduce the above copyright notice,
adam@1989 10 * this list of conditions and the following disclaimer in the documentation
adam@1989 11 * and/or other materials provided with the distribution.
adam@1989 12 * - The names of contributors may not be used to endorse or promote products
adam@1989 13 * derived from this software without specific prior written permission.
adam@1989 14 *
adam@1989 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adam@1989 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adam@1989 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adam@1989 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adam@1989 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adam@1989 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adam@1989 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adam@1989 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adam@1989 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adam@1989 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adam@1989 25 * POSSIBILITY OF SUCH DAMAGE.
adam@1989 26 *)
adam@1989 27
adam@1989 28 structure ExplRename :> EXPL_RENAME = struct
adam@1989 29
adam@1989 30 open Expl
adam@1989 31 structure E = ExplEnv
adam@1989 32
adam@1989 33 structure IM = IntBinaryMap
adam@1989 34
adam@1989 35 structure St :> sig
adam@1989 36 type t
adam@1989 37
adam@1989 38 val create : int -> t
adam@1989 39 val next : t -> int
adam@1989 40
adam@1989 41 val bind : t * int -> t * int
adam@1989 42 val lookup: t * int -> int option
adam@1989 43 end = struct
adam@1989 44
adam@1989 45 type t = {next : int,
adam@1989 46 renaming : int IM.map}
adam@1989 47
adam@1989 48 fun create next = {next = next,
adam@1989 49 renaming = IM.empty}
adam@1989 50
adam@1989 51 fun next (t : t) = #next t
adam@1989 52
adam@1989 53 fun bind ({next, renaming}, n) =
adam@1989 54 ({next = next + 1,
adam@1989 55 renaming = IM.insert (renaming, n, next)}, next)
adam@1989 56
adam@1989 57 fun lookup ({next, renaming}, n) =
adam@1989 58 IM.find (renaming, n)
adam@1989 59
adam@1989 60 end
adam@1989 61
adam@1989 62 fun renameCon st (all as (c, loc)) =
adam@1989 63 case c of
adam@1989 64 TFun (c1, c2) => (TFun (renameCon st c1, renameCon st c2), loc)
adam@1989 65 | TCFun (x, k, c) => (TCFun (x, k, renameCon st c), loc)
adam@1989 66 | TRecord c => (TRecord (renameCon st c), loc)
adam@1989 67 | CRel _ => all
adam@1989 68 | CNamed n =>
adam@1989 69 (case St.lookup (st, n) of
adam@1989 70 NONE => all
adam@1989 71 | SOME n' => (CNamed n', loc))
adam@1989 72 | CModProj (n, ms, x) =>
adam@1989 73 (case St.lookup (st, n) of
adam@1989 74 NONE => all
adam@1989 75 | SOME n' => (CModProj (n', ms, x), loc))
adam@1989 76 | CApp (c1, c2) => (CApp (renameCon st c1, renameCon st c2), loc)
adam@1989 77 | CAbs (x, k, c) => (CAbs (x, k, renameCon st c), loc)
adam@1989 78 | CKAbs (x, c) => (CKAbs (x, renameCon st c), loc)
adam@1989 79 | CKApp (c, k) => (CKApp (renameCon st c, k), loc)
adam@1989 80 | TKFun (x, c) => (TKFun (x, renameCon st c), loc)
adam@1989 81 | CName _ => all
adam@1989 82 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (renameCon st x, renameCon st c)) xcs), loc)
adam@1989 83 | CConcat (c1, c2) => (CConcat (renameCon st c1, renameCon st c2), loc)
adam@1989 84 | CMap _ => all
adam@1989 85 | CUnit => all
adam@1989 86 | CTuple cs => (CTuple (map (renameCon st) cs), loc)
adam@1989 87 | CProj (c, n) => (CProj (renameCon st c, n), loc)
adam@1989 88
adam@1989 89 fun renamePatCon st pc =
adam@1989 90 case pc of
adam@1989 91 PConVar n =>
adam@1989 92 (case St.lookup (st, n) of
adam@1989 93 NONE => pc
adam@1989 94 | SOME n' => PConVar n')
adam@1989 95 | PConProj (n, ms, x) =>
adam@1989 96 (case St.lookup (st, n) of
adam@1989 97 NONE => pc
adam@1989 98 | SOME n' => PConProj (n', ms, x))
adam@1989 99
adam@1989 100 fun renamePat st (all as (p, loc)) =
adam@1989 101 case p of
adam@1989 102 PWild => all
adam@1989 103 | PVar (x, c) => (PVar (x, renameCon st c), loc)
adam@1989 104 | PPrim _ => all
adam@1989 105 | PCon (dk, pc, cs, po) => (PCon (dk, renamePatCon st pc,
adam@1989 106 map (renameCon st) cs,
adam@1989 107 Option.map (renamePat st) po), loc)
adam@1989 108 | PRecord xpcs => (PRecord (map (fn (x, p, c) =>
adam@1989 109 (x, renamePat st p, renameCon st c)) xpcs), loc)
adam@1989 110
adam@1989 111 fun renameExp st (all as (e, loc)) =
adam@1989 112 case e of
adam@1989 113 EPrim _ => all
adam@1989 114 | ERel _ => all
adam@1989 115 | ENamed n =>
adam@1989 116 (case St.lookup (st, n) of
adam@1989 117 NONE => all
adam@1989 118 | SOME n' => (ENamed n', loc))
adam@1989 119 | EModProj (n, ms, x) =>
adam@1989 120 (case St.lookup (st, n) of
adam@1989 121 NONE => all
adam@1989 122 | SOME n' => (EModProj (n', ms, x), loc))
adam@1989 123 | EApp (e1, e2) => (EApp (renameExp st e1, renameExp st e2), loc)
adam@1989 124 | EAbs (x, dom, ran, e) => (EAbs (x, renameCon st dom, renameCon st ran, renameExp st e), loc)
adam@1989 125 | ECApp (e, c) => (ECApp (renameExp st e, renameCon st c), loc)
adam@1989 126 | ECAbs (x, k, e) => (ECAbs (x, k, renameExp st e), loc)
adam@1989 127 | EKAbs (x, e) => (EKAbs (x, renameExp st e), loc)
adam@1989 128 | EKApp (e, k) => (EKApp (renameExp st e, k), loc)
adam@1989 129 | ERecord xecs => (ERecord (map (fn (x, e, c) => (renameCon st x,
adam@1989 130 renameExp st e,
adam@1989 131 renameCon st c)) xecs), loc)
adam@1989 132 | EField (e, c, {field, rest}) => (EField (renameExp st e,
adam@1989 133 renameCon st c,
adam@1989 134 {field = renameCon st field,
adam@1989 135 rest = renameCon st rest}), loc)
adam@1989 136 | EConcat (e1, c1, e2, c2) => (EConcat (renameExp st e1,
adam@1989 137 renameCon st c1,
adam@1989 138 renameExp st e2,
adam@1989 139 renameCon st c2), loc)
adam@1989 140 | ECut (e, c, {field, rest}) => (ECut (renameExp st e,
adam@1989 141 renameCon st c,
adam@1989 142 {field = renameCon st field,
adam@1989 143 rest = renameCon st rest}), loc)
adam@1989 144 | ECutMulti (e, c, {rest}) => (ECutMulti (renameExp st e,
adam@1989 145 renameCon st c,
adam@1989 146 {rest = renameCon st rest}), loc)
adam@1989 147 | ECase (e, pes, {disc, result}) => (ECase (renameExp st e,
adam@1989 148 map (fn (p, e) => (renamePat st p, renameExp st e)) pes,
adam@1989 149 {disc = renameCon st disc,
adam@1989 150 result = renameCon st result}), loc)
adam@1989 151 | EWrite e => (EWrite (renameExp st e), loc)
adam@1989 152 | ELet (x, c1, e1, e2) => (ELet (x, renameCon st c1,
adam@1989 153 renameExp st e1,
adam@1989 154 renameExp st e2), loc)
adam@1989 155
adam@1989 156 fun renameSitem st (all as (si, loc)) =
adam@1989 157 case si of
adam@1989 158 SgiConAbs _ => all
adam@1989 159 | SgiCon (x, n, k, c) => (SgiCon (x, n, k, renameCon st c), loc)
adam@1989 160 | SgiDatatype dts => (SgiDatatype (map (fn (x, n, xs, cns) =>
adam@1989 161 (x, n, xs,
adam@1989 162 map (fn (x, n, co) =>
adam@1989 163 (x, n, Option.map (renameCon st) co)) cns)) dts),
adam@1989 164 loc)
adam@1989 165 | SgiDatatypeImp (x, n, n', xs, x', xs', cns) =>
adam@1989 166 (SgiDatatypeImp (x, n, n', xs, x', xs',
adam@1989 167 map (fn (x, n, co) =>
adam@1989 168 (x, n, Option.map (renameCon st) co)) cns), loc)
adam@1989 169 | SgiVal (x, n, c) => (SgiVal (x, n, renameCon st c), loc)
adam@1989 170 | SgiSgn (x, n, sg) => (SgiSgn (x, n, renameSgn st sg), loc)
adam@1989 171 | SgiStr (x, n, sg) => (SgiStr (x, n, renameSgn st sg), loc)
adam@1989 172
adam@1989 173 and renameSgn st (all as (sg, loc)) =
adam@1989 174 case sg of
adam@1989 175 SgnConst sis => (SgnConst (map (renameSitem st) sis), loc)
adam@1989 176 | SgnVar n =>
adam@1989 177 (case St.lookup (st, n) of
adam@1989 178 NONE => all
adam@1989 179 | SOME n' => (SgnVar n', loc))
adam@1989 180 | SgnFun (x, n, dom, ran) => (SgnFun (x, n, renameSgn st dom, renameSgn st ran), loc)
adam@1989 181 | SgnWhere (sg, xs, s, c) => (SgnWhere (renameSgn st sg, xs, s, renameCon st c), loc)
adam@1989 182 | SgnProj (n, ms, x) =>
adam@1989 183 (case St.lookup (st, n) of
adam@1989 184 NONE => all
adam@1989 185 | SOME n' => (SgnProj (n', ms, x), loc))
adam@1989 186
adam@1989 187 fun renameDecl st (all as (d, loc)) =
adam@1989 188 case d of
adam@1989 189 DCon (x, n, k, c) => (DCon (x, n, k, renameCon st c), loc)
adam@1989 190 | DDatatype dts => (DDatatype (map (fn (x, n, xs, cns) =>
adam@1989 191 (x, n, xs,
adam@1989 192 map (fn (x, n, co) =>
adam@1989 193 (x, n, Option.map (renameCon st) co)) cns)) dts),
adam@1989 194 loc)
adam@1989 195 | DDatatypeImp (x, n, n', xs, x', xs', cns) =>
adam@1989 196 (DDatatypeImp (x, n, n', xs, x', xs',
adam@1989 197 map (fn (x, n, co) =>
adam@1989 198 (x, n, Option.map (renameCon st) co)) cns), loc)
adam@1989 199 | DVal (x, n, c, e) => (DVal (x, n, renameCon st c, renameExp st e), loc)
adam@1989 200 | DValRec vis => (DValRec (map (fn (x, n, c, e) => (x, n, renameCon st c, renameExp st e)) vis), loc)
adam@1989 201 | DSgn (x, n, sg) => (DSgn (x, n, renameSgn st sg), loc)
adam@1989 202 | DStr (x, n, sg, str) => (DStr (x, n, renameSgn st sg, renameStr st str), loc)
adam@1989 203 | DFfiStr (x, n, sg) => (DFfiStr (x, n, renameSgn st sg), loc)
adam@1989 204 | DExport (n, sg, str) =>
adam@1989 205 (case St.lookup (st, n) of
adam@1989 206 NONE => all
adam@1989 207 | SOME n' => (DExport (n', renameSgn st sg, renameStr st str), loc))
adam@1989 208 | DTable (n, x, m, c1, e1, c2, e2, c3) =>
adam@1989 209 (DTable (n, x, m, renameCon st c1, renameExp st e1, renameCon st c2,
adam@1989 210 renameExp st e2, renameCon st c3), loc)
adam@1989 211 | DSequence _ => all
adam@1989 212 | DView (n, x, n', e, c) => (DView (n, x, n', renameExp st e, renameCon st c), loc)
adam@1989 213 | DDatabase _ => all
adam@1989 214 | DCookie (n, x, n', c) => (DCookie (n, x, n', renameCon st c), loc)
adam@1989 215 | DStyle _ => all
adam@1989 216 | DTask (e1, e2) => (DTask (renameExp st e1, renameExp st e2), loc)
adam@1989 217 | DPolicy e => (DPolicy (renameExp st e), loc)
adam@1989 218 | DOnError (n, xs, x) =>
adam@1989 219 (case St.lookup (st, n) of
adam@1989 220 NONE => all
adam@1989 221 | SOME n' => (DOnError (n', xs, x), loc))
adam@2010 222 | DFfi (x, n, modes, t) => (DFfi (x, n, modes, renameCon st t), loc)
adam@1989 223
adam@1989 224 and renameStr st (all as (str, loc)) =
adam@1989 225 case str of
adam@1989 226 StrConst ds => (StrConst (map (renameDecl st) ds), loc)
adam@1989 227 | StrVar n =>
adam@1989 228 (case St.lookup (st, n) of
adam@1989 229 NONE => all
adam@1989 230 | SOME n' => (StrVar n', loc))
adam@1989 231 | StrProj (str, x) => (StrProj (renameStr st str, x), loc)
adam@1989 232 | StrFun (x, n, dom, ran, str) => (StrFun (x, n, renameSgn st dom,
adam@1989 233 renameSgn st ran,
adam@1989 234 renameStr st str), loc)
adam@1989 235 | StrApp (str1, str2) => (StrApp (renameStr st str1, renameStr st str2), loc)
adam@1989 236
adam@1989 237
adam@1989 238
adam@1989 239 fun fromArity (n, loc) =
adam@1989 240 case n of
adam@1989 241 0 => (KType, loc)
adam@1989 242 | _ => (KArrow ((KType, loc), fromArity (n - 1, loc)), loc)
adam@1989 243
adam@1989 244 fun dupDecl (all as (d, loc), st) =
adam@1989 245 case d of
adam@1989 246 DCon (x, n, k, c) =>
adam@1989 247 let
adam@1989 248 val (st, n') = St.bind (st, n)
adam@1989 249 in
adam@1989 250 ([(DCon (x, n, k, renameCon st c), loc),
adam@1989 251 (DCon (x, n', k, (CNamed n, loc)), loc)],
adam@1989 252 st)
adam@1989 253 end
adam@1989 254 | DDatatype dts =>
adam@1989 255 let
adam@1990 256 val d = (DDatatype (map (fn (x, n, xs, cns) =>
adam@1990 257 (x, n, xs,
adam@1990 258 map (fn (x, n, co) =>
adam@1990 259 (x, n, Option.map (renameCon st) co)) cns)) dts),
adam@1990 260 loc)
adam@1990 261
adam@1989 262 val (dts', st) = ListUtil.foldlMap (fn ((x, n, xs, cns), st) =>
adam@1989 263 let
adam@1989 264 val (st, n') = St.bind (st, n)
adam@1989 265
adam@1989 266 val (cns', st) = ListUtil.foldlMap
adam@1989 267 (fn ((x, n, _), st) =>
adam@1989 268 let
adam@1989 269 val (st, n') =
adam@1989 270 St.bind (st, n)
adam@1989 271 in
adam@1989 272 ((x, n, n'), st)
adam@1989 273 end) st cns
adam@1989 274 in
adam@1989 275 ((x, n, length xs, n', cns'), st)
adam@1989 276 end) st dts
adam@1989 277
adam@1989 278 val env = E.declBinds E.empty d
adam@1989 279 in
adam@1989 280 (d
adam@1989 281 :: map (fn (x, n, arity, n', _) =>
adam@1989 282 (DCon (x, n', fromArity (arity, loc), (CNamed n, loc)), loc)) dts'
adam@1989 283 @ ListUtil.mapConcat (fn (_, _, _, _, cns') =>
adam@1989 284 map (fn (x, n, n') =>
adam@1989 285 (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)),
adam@1989 286 loc)) cns') dts',
adam@1989 287 st)
adam@1989 288 end
adam@1989 289 | DDatatypeImp (x, n, n', xs, x', xs', cns) =>
adam@1989 290 let
adam@1990 291 val d = (DDatatypeImp (x, n, n', xs, x', xs',
adam@1990 292 map (fn (x, n, co) =>
adam@1990 293 (x, n, Option.map (renameCon st) co)) cns), loc)
adam@1990 294
adam@1989 295 val (cns', st) = ListUtil.foldlMap
adam@1989 296 (fn ((x, n, _), st) =>
adam@1989 297 let
adam@1989 298 val (st, n') =
adam@1989 299 St.bind (st, n)
adam@1989 300 in
adam@1989 301 ((x, n, n'), st)
adam@1989 302 end) st cns
adam@1989 303
adam@1989 304 val (st, n') = St.bind (st, n)
adam@1989 305
adam@1989 306 val env = E.declBinds E.empty d
adam@1989 307 in
adam@1989 308 (d
adam@1989 309 :: (DCon (x, n', fromArity (length xs, loc), (CNamed n, loc)), loc)
adam@1989 310 :: map (fn (x, n, n') =>
adam@1989 311 (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)),
adam@1989 312 loc)) cns',
adam@1989 313 st)
adam@1989 314 end
adam@1989 315 | DVal (x, n, c, e) =>
adam@1989 316 let
adam@1989 317 val (st, n') = St.bind (st, n)
adam@1989 318 val c' = renameCon st c
adam@1989 319 in
adam@1989 320 ([(DVal (x, n, c', renameExp st e), loc),
adam@1989 321 (DVal (x, n', c', (ENamed n, loc)), loc)],
adam@1989 322 st)
adam@1989 323 end
adam@1989 324 | DValRec vis =>
adam@1989 325 let
adam@1989 326 val d = (DValRec (map (fn (x, n, c, e) => (x, n, renameCon st c, renameExp st e)) vis), loc)
adam@1989 327
adam@1989 328 val (vis', st) = ListUtil.foldlMap (fn ((x, n, _, _), st) =>
adam@1989 329 let
adam@1989 330 val (st, n') = St.bind (st, n)
adam@1989 331 in
adam@1989 332 ((x, n, n'), st)
adam@1989 333 end) st vis
adam@1989 334
adam@1989 335 val env = E.declBinds E.empty d
adam@1989 336 in
adam@1989 337 (d
adam@1989 338 :: map (fn (x, n, n') => (DVal (x, n', #2 (E.lookupENamed env n), (ENamed n, loc)), loc)) vis',
adam@1989 339 st)
adam@1989 340 end
adam@1989 341 | DSgn (x, n, sg) =>
adam@1989 342 let
adam@1989 343 val (st, n') = St.bind (st, n)
adam@1989 344 in
adam@1989 345 ([(DSgn (x, n, renameSgn st sg), loc),
adam@1989 346 (DSgn (x, n', (SgnVar n, loc)), loc)],
adam@1989 347 st)
adam@1989 348 end
adam@1989 349 | DStr (x, n, sg, str) =>
adam@1989 350 let
adam@1989 351 val (st, n') = St.bind (st, n)
adam@1989 352 val sg' = renameSgn st sg
adam@1989 353 in
adam@1989 354 ([(DStr (x, n, sg', renameStr st str), loc),
adam@1989 355 (DStr (x, n', sg', (StrVar n, loc)), loc)],
adam@1989 356 st)
adam@1989 357 end
adam@1989 358 | DFfiStr (x, n, sg) => ([(DFfiStr (x, n, renameSgn st sg), loc)], st)
adam@1989 359 | DExport (n, sg, str) =>
adam@1989 360 (case St.lookup (st, n) of
adam@1989 361 NONE => ([all], st)
adam@1989 362 | SOME n' => ([(DExport (n', renameSgn st sg, renameStr st str), loc)], st))
adam@1989 363 | DTable (n, x, m, c1, e1, c2, e2, c3) =>
adam@1989 364 let
adam@1989 365 val (st, m') = St.bind (st, m)
adam@1989 366
adam@1989 367 val d = (DTable (n, x, m, renameCon st c1, renameExp st e1, renameCon st c2,
adam@1989 368 renameExp st e2, renameCon st c3), loc)
adam@1989 369
adam@1989 370 val env = E.declBinds E.empty d
adam@1989 371 in
adam@1989 372 ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989 373 end
adam@1989 374 | DSequence (n, x, m) =>
adam@1989 375 let
adam@1989 376 val (st, m') = St.bind (st, m)
adam@1989 377
adam@1989 378 val env = E.declBinds E.empty all
adam@1989 379 in
adam@1989 380 ([all, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989 381 end
adam@1989 382 | DView (n, x, m, e, c) =>
adam@1989 383 let
adam@1989 384 val (st, m') = St.bind (st, m)
adam@1989 385
adam@1989 386 val d = (DView (n, x, m, renameExp st e, renameCon st c), loc)
adam@1989 387
adam@1989 388 val env = E.declBinds E.empty d
adam@1989 389 in
adam@1989 390 ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989 391 end
adam@1989 392 | DDatabase _ => ([all], st)
adam@1989 393 | DCookie (n, x, m, c) =>
adam@1989 394 let
adam@1989 395 val (st, m') = St.bind (st, m)
adam@1989 396
adam@1989 397 val d = (DCookie (n, x, m, renameCon st c), loc)
adam@1989 398
adam@1989 399 val env = E.declBinds E.empty d
adam@1989 400 in
adam@1989 401 ([d, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989 402 end
adam@1989 403 | DStyle (n, x, m) =>
adam@1989 404 let
adam@1989 405 val (st, m') = St.bind (st, m)
adam@1989 406
adam@1989 407 val env = E.declBinds E.empty all
adam@1989 408 in
adam@1989 409 ([all, (DVal (x, m', #2 (E.lookupENamed env m), (ENamed m, loc)), loc)], st)
adam@1989 410 end
adam@1989 411 | DTask (e1, e2) => ([(DTask (renameExp st e1, renameExp st e2), loc)], st)
adam@1989 412 | DPolicy e => ([(DPolicy (renameExp st e), loc)], st)
adam@1989 413 | DOnError (n, xs, x) =>
adam@1989 414 (case St.lookup (st, n) of
adam@1989 415 NONE => ([all], st)
adam@1989 416 | SOME n' => ([(DOnError (n', xs, x), loc)], st))
adam@2010 417 | DFfi (x, n, modes, t) =>
adam@2010 418 let
adam@2010 419 val (st, n') = St.bind (st, n)
adam@2010 420 val t' = renameCon st t
adam@2010 421 in
adam@2010 422 ([(DFfi (x, n, modes, t'), loc),
adam@2010 423 (DVal (x, n', t', (ENamed n, loc)), loc)],
adam@2010 424 st)
adam@2010 425 end
adam@1989 426
adam@1989 427 fun rename {NextId, FormalName, FormalId, Body = all as (str, loc)} =
adam@1989 428 case str of
adam@1989 429 StrConst ds =>
adam@1989 430 let
adam@1989 431 val st = St.create NextId
adam@1989 432 val (st, n) = St.bind (st, FormalId)
adam@1989 433
adam@1989 434 val (ds, st) = ListUtil.foldlMapConcat dupDecl st ds
adam@1991 435
adam@1991 436 (* Revenge of the functor parameter renamer!
adam@1991 437 * See comment in elaborate.sml for the start of the saga.
adam@1991 438 * We need to alpha-rename the argument to allow sufficient shadowing in the body. *)
adam@1991 439
adam@1991 440 fun mungeName m =
adam@1991 441 if List.exists (fn (DStr (x, _, _, _), _) => x = m
adam@1991 442 | _ => false) ds then
adam@1991 443 mungeName ("?" ^ m)
adam@1991 444 else
adam@1991 445 m
adam@1991 446
adam@1991 447 val FormalName = mungeName FormalName
adam@1991 448
adam@1989 449 val ds = (DStr (FormalName, n, (SgnConst [], loc), (StrVar FormalId, loc)), loc) :: ds
adam@1989 450 in
adam@1989 451 (St.next st, (StrConst ds, loc))
adam@1989 452 end
adam@1989 453 | _ => (NextId, all)
adam@1989 454
adam@1989 455 end