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@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@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