Mercurial > urweb

annotate src/expl_rename.sml @ 2112:b4702145f8de

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Treat getHeader and getenv as vectors for reading request data supplied implicitly by browsers
author Adam Chlipala <adam@chlipala.net>
date Thu, 05 Feb 2015 11:09:25 -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