adamc@38: (* Copyright (c) 2008, Adam Chlipala adamc@38: * All rights reserved. adamc@38: * adamc@38: * Redistribution and use in source and binary forms, with or without adamc@38: * modification, are permitted provided that the following conditions are met: adamc@38: * adamc@38: * - Redistributions of source code must retain the above copyright notice, adamc@38: * this list of conditions and the following disclaimer. adamc@38: * - Redistributions in binary form must reproduce the above copyright notice, adamc@38: * this list of conditions and the following disclaimer in the documentation adamc@38: * and/or other materials provided with the distribution. adamc@38: * - The names of contributors may not be used to endorse or promote products adamc@38: * derived from this software without specific prior written permission. adamc@38: * adamc@38: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@38: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@38: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@38: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@38: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@38: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@38: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@38: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@38: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@38: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@38: * POSSIBILITY OF SUCH DAMAGE. adamc@38: *) adamc@38: adamc@38: structure ExplEnv :> EXPL_ENV = struct adamc@38: adamc@38: open Expl adamc@38: adamc@38: structure U = ExplUtil adamc@38: adamc@38: structure IM = IntBinaryMap adamc@38: structure SM = BinaryMapFn(struct adamc@38: type ord_key = string adamc@38: val compare = String.compare adamc@38: end) adamc@38: adamc@38: exception UnboundRel of int adamc@38: exception UnboundNamed of int adamc@38: adamc@38: adamc@38: (* AST utility functions *) adamc@38: adamc@38: exception SynUnif adamc@38: adamc@38: val liftConInCon = adamc@38: U.Con.mapB {kind = fn k => k, adamc@38: con = fn bound => fn c => adamc@38: case c of adamc@38: CRel xn => adamc@38: if xn < bound then adamc@38: c adamc@38: else adamc@38: CRel (xn + 1) adamc@38: (*| CUnif _ => raise SynUnif*) adamc@38: | _ => c, adamc@38: bind = fn (bound, U.Con.Rel _) => bound + 1 adamc@38: | (bound, _) => bound} adamc@38: adamc@38: val lift = liftConInCon 0 adamc@38: adamc@38: adamc@38: (* Back to environments *) adamc@38: adamc@38: datatype 'a var' = adamc@38: Rel' of int * 'a adamc@38: | Named' of int * 'a adamc@38: adamc@38: datatype 'a var = adamc@38: NotBound adamc@38: | Rel of int * 'a adamc@38: | Named of int * 'a adamc@38: adamc@38: type env = { adamc@38: renameC : kind var' SM.map, adamc@38: relC : (string * kind) list, adamc@38: namedC : (string * kind * con option) IM.map, adamc@38: adamc@38: renameE : con var' SM.map, adamc@38: relE : (string * con) list, adamc@38: namedE : (string * con) IM.map, adamc@38: adamc@38: renameSgn : (int * sgn) SM.map, adamc@38: sgn : (string * sgn) IM.map, adamc@38: adamc@38: renameStr : (int * sgn) SM.map, adamc@38: str : (string * sgn) IM.map adamc@38: } adamc@38: adamc@38: val namedCounter = ref 0 adamc@38: adamc@38: val empty = { adamc@38: renameC = SM.empty, adamc@38: relC = [], adamc@38: namedC = IM.empty, adamc@38: adamc@38: renameE = SM.empty, adamc@38: relE = [], adamc@38: namedE = IM.empty, adamc@38: adamc@38: renameSgn = SM.empty, adamc@38: sgn = IM.empty, adamc@38: adamc@38: renameStr = SM.empty, adamc@38: str = IM.empty adamc@38: } adamc@38: adamc@38: fun pushCRel (env : env) x k = adamc@38: let adamc@38: val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) adamc@38: | x => x) (#renameC env) adamc@38: in adamc@38: {renameC = SM.insert (renameC, x, Rel' (0, k)), adamc@38: relC = (x, k) :: #relC env, adamc@38: namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), adamc@38: adamc@38: renameE = #renameE env, adamc@38: relE = map (fn (x, c) => (x, lift c)) (#relE env), adamc@38: namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), adamc@38: adamc@38: renameSgn = #renameSgn env, adamc@38: sgn = #sgn env, adamc@38: adamc@38: renameStr = #renameStr env, adamc@38: str = #str env adamc@38: } adamc@38: end adamc@38: adamc@38: fun lookupCRel (env : env) n = adamc@38: (List.nth (#relC env, n)) adamc@38: handle Subscript => raise UnboundRel n adamc@38: adamc@38: fun pushCNamed (env : env) x n k co = adamc@38: {renameC = SM.insert (#renameC env, x, Named' (n, k)), adamc@38: relC = #relC env, adamc@38: namedC = IM.insert (#namedC env, n, (x, k, co)), adamc@38: adamc@38: renameE = #renameE env, adamc@38: relE = #relE env, adamc@38: namedE = #namedE env, adamc@38: adamc@38: renameSgn = #renameSgn env, adamc@38: sgn = #sgn env, adamc@38: adamc@38: renameStr = #renameStr env, adamc@38: str = #str env} adamc@38: adamc@38: fun lookupCNamed (env : env) n = adamc@38: case IM.find (#namedC env, n) of adamc@38: NONE => raise UnboundNamed n adamc@38: | SOME x => x adamc@38: adamc@38: fun pushERel (env : env) x t = adamc@38: let adamc@38: val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) adamc@38: | x => x) (#renameE env) adamc@38: in adamc@38: {renameC = #renameC env, adamc@38: relC = #relC env, adamc@38: namedC = #namedC env, adamc@38: adamc@38: renameE = SM.insert (renameE, x, Rel' (0, t)), adamc@38: relE = (x, t) :: #relE env, adamc@38: namedE = #namedE env, adamc@38: adamc@38: renameSgn = #renameSgn env, adamc@38: sgn = #sgn env, adamc@38: adamc@38: renameStr = #renameStr env, adamc@38: str = #str env} adamc@38: end adamc@38: adamc@38: fun lookupERel (env : env) n = adamc@38: (List.nth (#relE env, n)) adamc@38: handle Subscript => raise UnboundRel n adamc@38: adamc@38: fun pushENamed (env : env) x n t = adamc@38: {renameC = #renameC env, adamc@38: relC = #relC env, adamc@38: namedC = #namedC env, adamc@38: adamc@38: renameE = SM.insert (#renameE env, x, Named' (n, t)), adamc@38: relE = #relE env, adamc@38: namedE = IM.insert (#namedE env, n, (x, t)), adamc@38: adamc@38: renameSgn = #renameSgn env, adamc@38: sgn = #sgn env, adamc@38: adamc@38: renameStr = #renameStr env, adamc@38: str = #str env} adamc@38: adamc@38: fun lookupENamed (env : env) n = adamc@38: case IM.find (#namedE env, n) of adamc@38: NONE => raise UnboundNamed n adamc@38: | SOME x => x adamc@38: adamc@38: fun pushSgnNamed (env : env) x n sgis = adamc@38: {renameC = #renameC env, adamc@38: relC = #relC env, adamc@38: namedC = #namedC env, adamc@38: adamc@38: renameE = #renameE env, adamc@38: relE = #relE env, adamc@38: namedE = #namedE env, adamc@38: adamc@38: renameSgn = SM.insert (#renameSgn env, x, (n, sgis)), adamc@38: sgn = IM.insert (#sgn env, n, (x, sgis)), adamc@38: adamc@38: renameStr = #renameStr env, adamc@38: str = #str env} adamc@38: adamc@38: fun lookupSgnNamed (env : env) n = adamc@38: case IM.find (#sgn env, n) of adamc@38: NONE => raise UnboundNamed n adamc@38: | SOME x => x adamc@38: adamc@38: fun pushStrNamed (env : env) x n sgis = adamc@38: {renameC = #renameC env, adamc@38: relC = #relC env, adamc@38: namedC = #namedC env, adamc@38: adamc@38: renameE = #renameE env, adamc@38: relE = #relE env, adamc@38: namedE = #namedE env, adamc@38: adamc@38: renameSgn = #renameSgn env, adamc@38: sgn = #sgn env, adamc@38: adamc@38: renameStr = SM.insert (#renameStr env, x, (n, sgis)), adamc@38: str = IM.insert (#str env, n, (x, sgis))} adamc@38: adamc@38: fun lookupStrNamed (env : env) n = adamc@38: case IM.find (#str env, n) of adamc@38: NONE => raise UnboundNamed n adamc@38: | SOME x => x adamc@38: adamc@162: fun declBinds env (d, loc) = adamc@38: case d of adamc@38: DCon (x, n, k, c) => pushCNamed env x n k (SOME c) adamc@191: | DDatatype (x, n, xs, xncs) => adamc@162: let adamc@162: val env = pushCNamed env x n (KType, loc) NONE adamc@162: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamed env x' n' t adamc@191: end) adamc@191: env xncs adamc@162: end adamc@191: | DDatatypeImp (x, n, m, ms, x', xs, xncs) => adamc@162: let adamc@162: val t = (CModProj (m, ms, x'), loc) adamc@162: val env = pushCNamed env x n (KType, loc) (SOME t) adamc@162: adamc@162: val t = (CNamed n, loc) adamc@162: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamed env x' n' t adamc@191: end) adamc@191: env xncs adamc@162: end adamc@38: | DVal (x, n, t, _) => pushENamed env x n t adamc@124: | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis adamc@38: | DSgn (x, n, sgn) => pushSgnNamed env x n sgn adamc@38: | DStr (x, n, sgn, _) => pushStrNamed env x n sgn adamc@48: | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn adamc@109: | DExport _ => env adamc@38: adamc@162: fun sgiBinds env (sgi, loc) = adamc@38: case sgi of adamc@38: SgiConAbs (x, n, k) => pushCNamed env x n k NONE adamc@38: | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) adamc@191: | SgiDatatype (x, n, xs, xncs) => adamc@162: let adamc@162: val env = pushCNamed env x n (KType, loc) NONE adamc@162: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamed env x' n' t adamc@191: end) adamc@191: env xncs adamc@162: end adamc@191: | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@162: let adamc@191: val t = (CModProj (m1, ms, x'), loc) adamc@191: val env = pushCNamed env x n (KType, loc) (SOME t) adamc@191: adamc@191: val t = (CNamed n, loc) adamc@162: in adamc@191: foldl (fn ((x', n', to), env) => adamc@191: let adamc@191: val t = adamc@191: case to of adamc@191: NONE => (CNamed n, loc) adamc@191: | SOME t => (TFun (t, (CNamed n, loc)), loc) adamc@191: val k = (KType, loc) adamc@191: val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs adamc@191: in adamc@191: pushENamed env x' n' t adamc@191: end) adamc@191: env xncs adamc@162: end adamc@38: | SgiVal (x, n, t) => pushENamed env x n t adamc@64: | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn adamc@38: | SgiStr (x, n, sgn) => pushStrNamed env x n sgn adamc@38: adamc@38: end