Mercurial > urweb

annotate src/expl_env.sml @ 67:9f89f0b00b84

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating cfold
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 09:48:54 -0400
parents d609820c5834
children f0f59e918cac
rev   line source
adamc@38 1 (* Copyright (c) 2008, Adam Chlipala
adamc@38 2 * All rights reserved.
adamc@38 3 *
adamc@38 4 * Redistribution and use in source and binary forms, with or without
adamc@38 5 * modification, are permitted provided that the following conditions are met:
adamc@38 6 *
adamc@38 7 * - Redistributions of source code must retain the above copyright notice,
adamc@38 8 * this list of conditions and the following disclaimer.
adamc@38 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@38 10 * this list of conditions and the following disclaimer in the documentation
adamc@38 11 * and/or other materials provided with the distribution.
adamc@38 12 * - The names of contributors may not be used to endorse or promote products
adamc@38 13 * derived from this software without specific prior written permission.
adamc@38 14 *
adamc@38 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@38 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@38 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@38 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@38 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@38 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@38 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@38 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@38 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@38 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@38 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@38 26 *)
adamc@38 27
adamc@38 28 structure ExplEnv :> EXPL_ENV = struct
adamc@38 29
adamc@38 30 open Expl
adamc@38 31
adamc@38 32 structure U = ExplUtil
adamc@38 33
adamc@38 34 structure IM = IntBinaryMap
adamc@38 35 structure SM = BinaryMapFn(struct
adamc@38 36 type ord_key = string
adamc@38 37 val compare = String.compare
adamc@38 38 end)
adamc@38 39
adamc@38 40 exception UnboundRel of int
adamc@38 41 exception UnboundNamed of int
adamc@38 42
adamc@38 43
adamc@38 44 (* AST utility functions *)
adamc@38 45
adamc@38 46 exception SynUnif
adamc@38 47
adamc@38 48 val liftConInCon =
adamc@38 49 U.Con.mapB {kind = fn k => k,
adamc@38 50 con = fn bound => fn c =>
adamc@38 51 case c of
adamc@38 52 CRel xn =>
adamc@38 53 if xn < bound then
adamc@38 54 c
adamc@38 55 else
adamc@38 56 CRel (xn + 1)
adamc@38 57 (*| CUnif _ => raise SynUnif*)
adamc@38 58 | _ => c,
adamc@38 59 bind = fn (bound, U.Con.Rel _) => bound + 1
adamc@38 60 | (bound, _) => bound}
adamc@38 61
adamc@38 62 val lift = liftConInCon 0
adamc@38 63
adamc@38 64
adamc@38 65 (* Back to environments *)
adamc@38 66
adamc@38 67 datatype 'a var' =
adamc@38 68 Rel' of int * 'a
adamc@38 69 | Named' of int * 'a
adamc@38 70
adamc@38 71 datatype 'a var =
adamc@38 72 NotBound
adamc@38 73 | Rel of int * 'a
adamc@38 74 | Named of int * 'a
adamc@38 75
adamc@38 76 type env = {
adamc@38 77 renameC : kind var' SM.map,
adamc@38 78 relC : (string * kind) list,
adamc@38 79 namedC : (string * kind * con option) IM.map,
adamc@38 80
adamc@38 81 renameE : con var' SM.map,
adamc@38 82 relE : (string * con) list,
adamc@38 83 namedE : (string * con) IM.map,
adamc@38 84
adamc@38 85 renameSgn : (int * sgn) SM.map,
adamc@38 86 sgn : (string * sgn) IM.map,
adamc@38 87
adamc@38 88 renameStr : (int * sgn) SM.map,
adamc@38 89 str : (string * sgn) IM.map
adamc@38 90 }
adamc@38 91
adamc@38 92 val namedCounter = ref 0
adamc@38 93
adamc@38 94 val empty = {
adamc@38 95 renameC = SM.empty,
adamc@38 96 relC = [],
adamc@38 97 namedC = IM.empty,
adamc@38 98
adamc@38 99 renameE = SM.empty,
adamc@38 100 relE = [],
adamc@38 101 namedE = IM.empty,
adamc@38 102
adamc@38 103 renameSgn = SM.empty,
adamc@38 104 sgn = IM.empty,
adamc@38 105
adamc@38 106 renameStr = SM.empty,
adamc@38 107 str = IM.empty
adamc@38 108 }
adamc@38 109
adamc@38 110 fun pushCRel (env : env) x k =
adamc@38 111 let
adamc@38 112 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
adamc@38 113 | x => x) (#renameC env)
adamc@38 114 in
adamc@38 115 {renameC = SM.insert (renameC, x, Rel' (0, k)),
adamc@38 116 relC = (x, k) :: #relC env,
adamc@38 117 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
adamc@38 118
adamc@38 119 renameE = #renameE env,
adamc@38 120 relE = map (fn (x, c) => (x, lift c)) (#relE env),
adamc@38 121 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
adamc@38 122
adamc@38 123 renameSgn = #renameSgn env,
adamc@38 124 sgn = #sgn env,
adamc@38 125
adamc@38 126 renameStr = #renameStr env,
adamc@38 127 str = #str env
adamc@38 128 }
adamc@38 129 end
adamc@38 130
adamc@38 131 fun lookupCRel (env : env) n =
adamc@38 132 (List.nth (#relC env, n))
adamc@38 133 handle Subscript => raise UnboundRel n
adamc@38 134
adamc@38 135 fun pushCNamed (env : env) x n k co =
adamc@38 136 {renameC = SM.insert (#renameC env, x, Named' (n, k)),
adamc@38 137 relC = #relC env,
adamc@38 138 namedC = IM.insert (#namedC env, n, (x, k, co)),
adamc@38 139
adamc@38 140 renameE = #renameE env,
adamc@38 141 relE = #relE env,
adamc@38 142 namedE = #namedE env,
adamc@38 143
adamc@38 144 renameSgn = #renameSgn env,
adamc@38 145 sgn = #sgn env,
adamc@38 146
adamc@38 147 renameStr = #renameStr env,
adamc@38 148 str = #str env}
adamc@38 149
adamc@38 150 fun lookupCNamed (env : env) n =
adamc@38 151 case IM.find (#namedC env, n) of
adamc@38 152 NONE => raise UnboundNamed n
adamc@38 153 | SOME x => x
adamc@38 154
adamc@38 155 fun pushERel (env : env) x t =
adamc@38 156 let
adamc@38 157 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
adamc@38 158 | x => x) (#renameE env)
adamc@38 159 in
adamc@38 160 {renameC = #renameC env,
adamc@38 161 relC = #relC env,
adamc@38 162 namedC = #namedC env,
adamc@38 163
adamc@38 164 renameE = SM.insert (renameE, x, Rel' (0, t)),
adamc@38 165 relE = (x, t) :: #relE env,
adamc@38 166 namedE = #namedE env,
adamc@38 167
adamc@38 168 renameSgn = #renameSgn env,
adamc@38 169 sgn = #sgn env,
adamc@38 170
adamc@38 171 renameStr = #renameStr env,
adamc@38 172 str = #str env}
adamc@38 173 end
adamc@38 174
adamc@38 175 fun lookupERel (env : env) n =
adamc@38 176 (List.nth (#relE env, n))
adamc@38 177 handle Subscript => raise UnboundRel n
adamc@38 178
adamc@38 179 fun pushENamed (env : env) x n t =
adamc@38 180 {renameC = #renameC env,
adamc@38 181 relC = #relC env,
adamc@38 182 namedC = #namedC env,
adamc@38 183
adamc@38 184 renameE = SM.insert (#renameE env, x, Named' (n, t)),
adamc@38 185 relE = #relE env,
adamc@38 186 namedE = IM.insert (#namedE env, n, (x, t)),
adamc@38 187
adamc@38 188 renameSgn = #renameSgn env,
adamc@38 189 sgn = #sgn env,
adamc@38 190
adamc@38 191 renameStr = #renameStr env,
adamc@38 192 str = #str env}
adamc@38 193
adamc@38 194 fun lookupENamed (env : env) n =
adamc@38 195 case IM.find (#namedE env, n) of
adamc@38 196 NONE => raise UnboundNamed n
adamc@38 197 | SOME x => x
adamc@38 198
adamc@38 199 fun pushSgnNamed (env : env) x n sgis =
adamc@38 200 {renameC = #renameC env,
adamc@38 201 relC = #relC env,
adamc@38 202 namedC = #namedC env,
adamc@38 203
adamc@38 204 renameE = #renameE env,
adamc@38 205 relE = #relE env,
adamc@38 206 namedE = #namedE env,
adamc@38 207
adamc@38 208 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
adamc@38 209 sgn = IM.insert (#sgn env, n, (x, sgis)),
adamc@38 210
adamc@38 211 renameStr = #renameStr env,
adamc@38 212 str = #str env}
adamc@38 213
adamc@38 214 fun lookupSgnNamed (env : env) n =
adamc@38 215 case IM.find (#sgn env, n) of
adamc@38 216 NONE => raise UnboundNamed n
adamc@38 217 | SOME x => x
adamc@38 218
adamc@38 219 fun pushStrNamed (env : env) x n sgis =
adamc@38 220 {renameC = #renameC env,
adamc@38 221 relC = #relC env,
adamc@38 222 namedC = #namedC env,
adamc@38 223
adamc@38 224 renameE = #renameE env,
adamc@38 225 relE = #relE env,
adamc@38 226 namedE = #namedE env,
adamc@38 227
adamc@38 228 renameSgn = #renameSgn env,
adamc@38 229 sgn = #sgn env,
adamc@38 230
adamc@38 231 renameStr = SM.insert (#renameStr env, x, (n, sgis)),
adamc@38 232 str = IM.insert (#str env, n, (x, sgis))}
adamc@38 233
adamc@38 234 fun lookupStrNamed (env : env) n =
adamc@38 235 case IM.find (#str env, n) of
adamc@38 236 NONE => raise UnboundNamed n
adamc@38 237 | SOME x => x
adamc@38 238
adamc@38 239 fun declBinds env (d, _) =
adamc@38 240 case d of
adamc@38 241 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@38 242 | DVal (x, n, t, _) => pushENamed env x n t
adamc@38 243 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 244 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
adamc@48 245 | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@38 246
adamc@38 247 fun sgiBinds env (sgi, _) =
adamc@38 248 case sgi of
adamc@38 249 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
adamc@38 250 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@38 251 | SgiVal (x, n, t) => pushENamed env x n t
adamc@64 252 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 253 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@38 254
adamc@38 255 end