Mercurial > urweb

annotate src/expl_env.sml @ 2291:50ad02829abd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make cache flushes happen immediately instead of at end of transaction.
author Ziv Scully <ziv@mit.edu>
date Tue, 17 Nov 2015 02:44:37 -0500
parents 403f0cc65b9c
children
rev   line source
adamc@1278 1 (* Copyright (c) 2008-2010, 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@624 48 val liftKindInKind =
adamc@624 49 U.Kind.mapB {kind = fn bound => fn k =>
adamc@624 50 case k of
adamc@624 51 KRel xn =>
adamc@624 52 if xn < bound then
adamc@624 53 k
adamc@624 54 else
adamc@624 55 KRel (xn + 1)
adamc@624 56 | _ => k,
adamc@624 57 bind = fn (bound, _) => bound + 1}
adamc@624 58
adamc@624 59 val liftKindInCon =
adamc@624 60 U.Con.mapB {kind = fn bound => fn k =>
adamc@624 61 case k of
adamc@624 62 KRel xn =>
adamc@624 63 if xn < bound then
adamc@624 64 k
adamc@624 65 else
adamc@624 66 KRel (xn + 1)
adamc@624 67 | _ => k,
adamc@624 68 con = fn _ => fn c => c,
adamc@624 69 bind = fn (bound, U.Con.RelK _) => bound + 1
adamc@624 70 | (bound, _) => bound}
adamc@624 71
adamc@38 72 val liftConInCon =
adamc@624 73 U.Con.mapB {kind = fn _ => fn k => k,
adamc@38 74 con = fn bound => fn c =>
adamc@38 75 case c of
adamc@38 76 CRel xn =>
adamc@38 77 if xn < bound then
adamc@38 78 c
adamc@38 79 else
adamc@38 80 CRel (xn + 1)
adamc@38 81 (*| CUnif _ => raise SynUnif*)
adamc@38 82 | _ => c,
adamc@624 83 bind = fn (bound, U.Con.RelC _) => bound + 1
adamc@38 84 | (bound, _) => bound}
adamc@38 85
adamc@38 86 val lift = liftConInCon 0
adamc@38 87
adamc@38 88
adamc@38 89 (* Back to environments *)
adamc@38 90
adamc@38 91 datatype 'a var' =
adamc@38 92 Rel' of int * 'a
adamc@38 93 | Named' of int * 'a
adamc@38 94
adamc@38 95 datatype 'a var =
adamc@38 96 NotBound
adamc@38 97 | Rel of int * 'a
adamc@38 98 | Named of int * 'a
adamc@38 99
adamc@38 100 type env = {
adamc@624 101 relK : string list,
adamc@624 102
adamc@38 103 relC : (string * kind) list,
adamc@38 104 namedC : (string * kind * con option) IM.map,
adamc@38 105
adamc@38 106 relE : (string * con) list,
adamc@38 107 namedE : (string * con) IM.map,
adamc@38 108
adamc@38 109 sgn : (string * sgn) IM.map,
adamc@38 110
adamc@38 111 str : (string * sgn) IM.map
adamc@38 112 }
adamc@38 113
adamc@38 114 val namedCounter = ref 0
adamc@38 115
adamc@38 116 val empty = {
adamc@624 117 relK = [],
adamc@624 118
adamc@38 119 relC = [],
adamc@38 120 namedC = IM.empty,
adamc@38 121
adamc@38 122 relE = [],
adamc@38 123 namedE = IM.empty,
adamc@38 124
adamc@38 125 sgn = IM.empty,
adamc@38 126
adamc@38 127 str = IM.empty
adamc@38 128 }
adamc@38 129
adamc@624 130 fun pushKRel (env : env) x =
adamc@624 131 {relK = x :: #relK env,
adamc@624 132
adamc@624 133 relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
adamc@624 134 namedC = #namedC env,
adamc@624 135
adamc@624 136 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
adamc@624 137 namedE = #namedE env,
adamc@624 138
adamc@624 139 sgn = #sgn env,
adamc@624 140
adamc@624 141 str = #str env
adamc@624 142 }
adamc@624 143
adamc@624 144 fun lookupKRel (env : env) n =
adamc@624 145 (List.nth (#relK env, n))
adamc@624 146 handle Subscript => raise UnboundRel n
adamc@624 147
adamc@38 148 fun pushCRel (env : env) x k =
adamc@624 149 {relK = #relK env,
adamc@38 150
adamc@624 151 relC = (x, k) :: #relC env,
adamc@624 152 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
adamc@38 153
adamc@624 154 relE = map (fn (x, c) => (x, lift c)) (#relE env),
adamc@624 155 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
adamc@38 156
adamc@624 157 sgn = #sgn env,
adamc@624 158
adamc@624 159 str = #str env
adamc@624 160 }
adamc@38 161
adamc@38 162 fun lookupCRel (env : env) n =
adamc@38 163 (List.nth (#relC env, n))
adamc@38 164 handle Subscript => raise UnboundRel n
adamc@38 165
adamc@38 166 fun pushCNamed (env : env) x n k co =
adamc@624 167 {relK = #relK env,
adamc@624 168
adamc@38 169 relC = #relC env,
adamc@38 170 namedC = IM.insert (#namedC env, n, (x, k, co)),
adamc@38 171
adamc@38 172 relE = #relE env,
adamc@38 173 namedE = #namedE env,
adamc@38 174
adamc@38 175 sgn = #sgn env,
adamc@38 176
adamc@38 177 str = #str env}
adamc@38 178
adamc@38 179 fun lookupCNamed (env : env) n =
adamc@38 180 case IM.find (#namedC env, n) of
adamc@38 181 NONE => raise UnboundNamed n
adamc@38 182 | SOME x => x
adamc@38 183
adamc@38 184 fun pushERel (env : env) x t =
adamc@624 185 {relK = #relK env,
adamc@38 186
adamc@624 187 relC = #relC env,
adamc@624 188 namedC = #namedC env,
adamc@38 189
adamc@624 190 relE = (x, t) :: #relE env,
adamc@624 191 namedE = #namedE env,
adamc@38 192
adamc@624 193 sgn = #sgn env,
adamc@624 194
adamc@624 195 str = #str env}
adamc@38 196
adamc@38 197 fun lookupERel (env : env) n =
adamc@38 198 (List.nth (#relE env, n))
adamc@38 199 handle Subscript => raise UnboundRel n
adamc@38 200
adamc@38 201 fun pushENamed (env : env) x n t =
adamc@624 202 {relK = #relK env,
adamc@624 203
adamc@38 204 relC = #relC env,
adamc@38 205 namedC = #namedC env,
adamc@38 206
adamc@38 207 relE = #relE env,
adamc@38 208 namedE = IM.insert (#namedE env, n, (x, t)),
adamc@38 209
adamc@38 210 sgn = #sgn env,
adamc@38 211
adamc@38 212 str = #str env}
adamc@38 213
adamc@38 214 fun lookupENamed (env : env) n =
adamc@38 215 case IM.find (#namedE env, n) of
adamc@38 216 NONE => raise UnboundNamed n
adamc@38 217 | SOME x => x
adamc@38 218
adamc@38 219 fun pushSgnNamed (env : env) x n sgis =
adamc@624 220 {relK = #relK env,
adamc@624 221
adamc@38 222 relC = #relC env,
adamc@38 223 namedC = #namedC env,
adamc@38 224
adamc@38 225 relE = #relE env,
adamc@38 226 namedE = #namedE env,
adamc@38 227
adamc@38 228 sgn = IM.insert (#sgn env, n, (x, sgis)),
adamc@38 229
adamc@38 230 str = #str env}
adamc@38 231
adamc@38 232 fun lookupSgnNamed (env : env) n =
adamc@38 233 case IM.find (#sgn env, n) of
adamc@38 234 NONE => raise UnboundNamed n
adamc@38 235 | SOME x => x
adamc@38 236
adamc@38 237 fun pushStrNamed (env : env) x n sgis =
adamc@624 238 {relK = #relK env,
adamc@624 239
adamc@38 240 relC = #relC env,
adamc@38 241 namedC = #namedC env,
adamc@38 242
adamc@38 243 relE = #relE env,
adamc@38 244 namedE = #namedE env,
adamc@38 245
adamc@38 246 sgn = #sgn env,
adamc@38 247
adamc@38 248 str = IM.insert (#str env, n, (x, sgis))}
adamc@38 249
adamc@38 250 fun lookupStrNamed (env : env) n =
adamc@38 251 case IM.find (#str env, n) of
adamc@38 252 NONE => raise UnboundNamed n
adamc@38 253 | SOME x => x
adamc@38 254
adamc@162 255 fun declBinds env (d, loc) =
adamc@38 256 case d of
adamc@38 257 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@806 258 | DDatatype dts =>
adamc@162 259 let
adamc@806 260 fun doOne ((x, n, xs, xncs), env) =
adamc@806 261 let
adamc@806 262 val k = (KType, loc)
adamc@806 263 val nxs = length xs
adamc@806 264 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
adamc@806 265 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
adamc@806 266 (KArrow (k, kb), loc)))
adamc@806 267 ((CNamed n, loc), k) xs
adamc@806 268
adamc@806 269 val env = pushCNamed env x n kb NONE
adamc@806 270 in
adamc@806 271 foldl (fn ((x', n', to), env) =>
adamc@806 272 let
adamc@806 273 val t =
adamc@806 274 case to of
adamc@806 275 NONE => tb
adamc@806 276 | SOME t => (TFun (t, tb), loc)
adamc@806 277 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@806 278 in
adamc@806 279 pushENamed env x' n' t
adamc@806 280 end)
adamc@806 281 env xncs
adamc@806 282 end
adamc@162 283 in
adamc@806 284 foldl doOne env dts
adamc@162 285 end
adamc@191 286 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
adamc@162 287 let
adamc@162 288 val t = (CModProj (m, ms, x'), loc)
adamc@162 289 val env = pushCNamed env x n (KType, loc) (SOME t)
adamc@162 290
adamc@162 291 val t = (CNamed n, loc)
adamc@162 292 in
adamc@191 293 foldl (fn ((x', n', to), env) =>
adamc@191 294 let
adamc@191 295 val t =
adamc@191 296 case to of
adamc@191 297 NONE => (CNamed n, loc)
adamc@191 298 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 299 val k = (KType, loc)
adamc@191 300 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 301 in
adamc@191 302 pushENamed env x' n' t
adamc@191 303 end)
adamc@191 304 env xncs
adamc@162 305 end
adamc@38 306 | DVal (x, n, t, _) => pushENamed env x n t
adamc@124 307 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
adamc@38 308 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 309 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
adamc@48 310 | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@109 311 | DExport _ => env
adamc@707 312 | DTable (tn, x, n, c, _, pc, _, cc) =>
adamc@246 313 let
adamc@705 314 val ct = (CModProj (tn, [], "sql_table"), loc)
adamc@705 315 val ct = (CApp (ct, c), loc)
adamc@707 316 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@338 317 in
adamc@705 318 pushENamed env x n ct
adamc@338 319 end
adamc@338 320 | DSequence (tn, x, n) =>
adamc@338 321 let
adamc@338 322 val t = (CModProj (tn, [], "sql_sequence"), loc)
adamc@246 323 in
adamc@246 324 pushENamed env x n t
adamc@246 325 end
adamc@754 326 | DView (tn, x, n, _, c) =>
adamc@754 327 let
adamc@754 328 val ct = (CModProj (tn, [], "sql_view"), loc)
adamc@754 329 val ct = (CApp (ct, c), loc)
adamc@754 330 in
adamc@754 331 pushENamed env x n ct
adamc@754 332 end
adamc@275 333 | DDatabase _ => env
adamc@460 334 | DCookie (tn, x, n, c) =>
adamc@460 335 let
adamc@460 336 val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc)
adamc@460 337 in
adamc@460 338 pushENamed env x n t
adamc@460 339 end
adamc@720 340 | DStyle (tn, x, n) =>
adamc@718 341 let
adamc@720 342 val t = (CModProj (tn, [], "css_class"), loc)
adamc@718 343 in
adamc@718 344 pushENamed env x n t
adamc@718 345 end
adamc@1075 346 | DTask _ => env
adamc@1199 347 | DPolicy _ => env
adam@1294 348 | DOnError _ => env
adam@2010 349 | DFfi (x, n, _, t) => pushENamed env x n t
adamc@38 350
adamc@162 351 fun sgiBinds env (sgi, loc) =
adamc@38 352 case sgi of
adamc@38 353 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
adamc@38 354 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@806 355 | SgiDatatype dts =>
adamc@162 356 let
adamc@806 357 fun doOne ((x, n, xs, xncs), env) =
adamc@806 358 let
adamc@806 359 val k = (KType, loc)
adamc@806 360 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@806 361
adamc@806 362 val env = pushCNamed env x n k' NONE
adamc@806 363 in
adamc@806 364 foldl (fn ((x', n', to), env) =>
adamc@806 365 let
adamc@806 366 val t =
adamc@806 367 case to of
adamc@806 368 NONE => (CNamed n, loc)
adamc@806 369 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@806 370
adamc@806 371 val k = (KType, loc)
adamc@806 372 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@806 373 in
adamc@806 374 pushENamed env x' n' t
adamc@806 375 end)
adamc@806 376 env xncs
adamc@806 377 end
adamc@162 378 in
adamc@806 379 foldl doOne env dts
adamc@162 380 end
adamc@191 381 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@162 382 let
adamc@191 383 val t = (CModProj (m1, ms, x'), loc)
adamc@191 384 val env = pushCNamed env x n (KType, loc) (SOME t)
adamc@191 385
adamc@191 386 val t = (CNamed n, loc)
adamc@162 387 in
adamc@191 388 foldl (fn ((x', n', to), env) =>
adamc@191 389 let
adamc@191 390 val t =
adamc@191 391 case to of
adamc@191 392 NONE => (CNamed n, loc)
adamc@191 393 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 394 val k = (KType, loc)
adamc@191 395 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 396 in
adamc@191 397 pushENamed env x' n' t
adamc@191 398 end)
adamc@191 399 env xncs
adamc@162 400 end
adamc@38 401 | SgiVal (x, n, t) => pushENamed env x n t
adamc@64 402 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 403 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@38 404
adamc@1278 405 fun patBinds env (p, loc) =
adamc@1278 406 case p of
adamc@1278 407 PWild => env
adamc@1278 408 | PVar (x, t) => pushERel env x t
adamc@1278 409 | PPrim _ => env
adamc@1278 410 | PCon (_, _, _, NONE) => env
adamc@1278 411 | PCon (_, _, _, SOME p) => patBinds env p
adamc@1278 412 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
adamc@1278 413
adamc@38 414 end