Mercurial > urweb

annotate src/expl_env.sml @ 275:73456bfde988

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Validating schema of a live database
author Adam Chlipala <adamc@hcoop.net>
date Tue, 02 Sep 2008 14:40:57 -0400
parents 3aa010e97db9
children e976b187d73a
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@162 239 fun declBinds env (d, loc) =
adamc@38 240 case d of
adamc@38 241 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@191 242 | DDatatype (x, n, xs, xncs) =>
adamc@162 243 let
adamc@162 244 val env = pushCNamed env x n (KType, loc) NONE
adamc@162 245 in
adamc@191 246 foldl (fn ((x', n', to), env) =>
adamc@191 247 let
adamc@191 248 val t =
adamc@191 249 case to of
adamc@191 250 NONE => (CNamed n, loc)
adamc@191 251 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 252 val k = (KType, loc)
adamc@191 253 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 254 in
adamc@191 255 pushENamed env x' n' t
adamc@191 256 end)
adamc@191 257 env xncs
adamc@162 258 end
adamc@191 259 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
adamc@162 260 let
adamc@162 261 val t = (CModProj (m, ms, x'), loc)
adamc@162 262 val env = pushCNamed env x n (KType, loc) (SOME t)
adamc@162 263
adamc@162 264 val t = (CNamed n, loc)
adamc@162 265 in
adamc@191 266 foldl (fn ((x', n', to), env) =>
adamc@191 267 let
adamc@191 268 val t =
adamc@191 269 case to of
adamc@191 270 NONE => (CNamed n, loc)
adamc@191 271 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 272 val k = (KType, loc)
adamc@191 273 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 274 in
adamc@191 275 pushENamed env x' n' t
adamc@191 276 end)
adamc@191 277 env xncs
adamc@162 278 end
adamc@38 279 | DVal (x, n, t, _) => pushENamed env x n t
adamc@124 280 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
adamc@38 281 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 282 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
adamc@48 283 | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@109 284 | DExport _ => env
adamc@246 285 | DTable (tn, x, n, c) =>
adamc@246 286 let
adamc@246 287 val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
adamc@246 288 in
adamc@246 289 pushENamed env x n t
adamc@246 290 end
adamc@275 291 | DDatabase _ => env
adamc@38 292
adamc@162 293 fun sgiBinds env (sgi, loc) =
adamc@38 294 case sgi of
adamc@38 295 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
adamc@38 296 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@191 297 | SgiDatatype (x, n, xs, xncs) =>
adamc@162 298 let
adamc@162 299 val env = pushCNamed env x n (KType, loc) NONE
adamc@162 300 in
adamc@191 301 foldl (fn ((x', n', to), env) =>
adamc@191 302 let
adamc@191 303 val t =
adamc@191 304 case to of
adamc@191 305 NONE => (CNamed n, loc)
adamc@191 306 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 307 val k = (KType, loc)
adamc@191 308 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 309 in
adamc@191 310 pushENamed env x' n' t
adamc@191 311 end)
adamc@191 312 env xncs
adamc@162 313 end
adamc@191 314 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@162 315 let
adamc@191 316 val t = (CModProj (m1, ms, x'), loc)
adamc@191 317 val env = pushCNamed env x n (KType, loc) (SOME t)
adamc@191 318
adamc@191 319 val t = (CNamed n, loc)
adamc@162 320 in
adamc@191 321 foldl (fn ((x', n', to), env) =>
adamc@191 322 let
adamc@191 323 val t =
adamc@191 324 case to of
adamc@191 325 NONE => (CNamed n, loc)
adamc@191 326 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 327 val k = (KType, loc)
adamc@191 328 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 329 in
adamc@191 330 pushENamed env x' n' t
adamc@191 331 end)
adamc@191 332 env xncs
adamc@162 333 end
adamc@38 334 | SgiVal (x, n, t) => pushENamed env x n t
adamc@64 335 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 336 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@38 337
adamc@246 338 | SgiTable (tn, x, n, c) =>
adamc@246 339 let
adamc@246 340 val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
adamc@246 341 in
adamc@246 342 pushENamed env x n t
adamc@246 343 end
adamc@246 344
adamc@38 345 end