Mercurial > urweb

annotate src/core_env.sml @ 709:0406e9cccb72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FOREIGN KEY, without ability to link NULL to NOT NULL (and with some lingering problems in row inference)
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 18:47:47 -0400
parents d8217b4cb617
children f152f215a02c
rev   line source
adamc@16 1 (* Copyright (c) 2008, Adam Chlipala
adamc@16 2 * All rights reserved.
adamc@16 3 *
adamc@16 4 * Redistribution and use in source and binary forms, with or without
adamc@16 5 * modification, are permitted provided that the following conditions are met:
adamc@16 6 *
adamc@16 7 * - Redistributions of source code must retain the above copyright notice,
adamc@16 8 * this list of conditions and the following disclaimer.
adamc@16 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@16 10 * this list of conditions and the following disclaimer in the documentation
adamc@16 11 * and/or other materials provided with the distribution.
adamc@16 12 * - The names of contributors may not be used to endorse or promote products
adamc@16 13 * derived from this software without specific prior written permission.
adamc@16 14 *
adamc@16 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@16 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@16 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@16 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@16 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@16 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@16 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@16 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@16 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@16 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@16 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@16 26 *)
adamc@16 27
adamc@16 28 structure CoreEnv :> CORE_ENV = struct
adamc@16 29
adamc@16 30 open Core
adamc@16 31
adamc@16 32 structure U = CoreUtil
adamc@16 33
adamc@16 34 structure IM = IntBinaryMap
adamc@16 35
adamc@16 36
adamc@16 37 (* AST utility functions *)
adamc@16 38
adamc@626 39 val liftKindInKind =
adamc@626 40 U.Kind.mapB {kind = fn bound => fn k =>
adamc@626 41 case k of
adamc@626 42 KRel xn =>
adamc@626 43 if xn < bound then
adamc@626 44 k
adamc@626 45 else
adamc@626 46 KRel (xn + 1)
adamc@626 47 | _ => k,
adamc@626 48 bind = fn (bound, _) => bound + 1}
adamc@626 49
adamc@626 50 val liftKindInCon =
adamc@626 51 U.Con.mapB {kind = fn bound => fn k =>
adamc@626 52 case k of
adamc@626 53 KRel xn =>
adamc@626 54 if xn < bound then
adamc@626 55 k
adamc@626 56 else
adamc@626 57 KRel (xn + 1)
adamc@626 58 | _ => k,
adamc@626 59 con = fn _ => fn c => c,
adamc@626 60 bind = fn (bound, U.Con.RelK _) => bound + 1
adamc@626 61 | (bound, _) => bound}
adamc@626 62
adamc@626 63 val liftKindInExp =
adamc@626 64 U.Exp.mapB {kind = fn bound => fn k =>
adamc@626 65 case k of
adamc@626 66 KRel xn =>
adamc@626 67 if xn < bound then
adamc@626 68 k
adamc@626 69 else
adamc@626 70 KRel (xn + 1)
adamc@626 71 | _ => k,
adamc@626 72 con = fn _ => fn c => c,
adamc@626 73 exp = fn _ => fn e => e,
adamc@626 74 bind = fn (bound, U.Exp.RelK _) => bound + 1
adamc@626 75 | (bound, _) => bound}
adamc@626 76
adamc@16 77 val liftConInCon =
adamc@626 78 U.Con.mapB {kind = fn _ => fn k => k,
adamc@16 79 con = fn bound => fn c =>
adamc@16 80 case c of
adamc@16 81 CRel xn =>
adamc@16 82 if xn < bound then
adamc@16 83 c
adamc@16 84 else
adamc@16 85 CRel (xn + 1)
adamc@16 86 | _ => c,
adamc@626 87 bind = fn (bound, U.Con.RelC _) => bound + 1
adamc@16 88 | (bound, _) => bound}
adamc@16 89
adamc@16 90 val lift = liftConInCon 0
adamc@16 91
adamc@193 92 val subConInCon =
adamc@626 93 U.Con.mapB {kind = fn _ => fn k => k,
adamc@193 94 con = fn (xn, rep) => fn c =>
adamc@193 95 case c of
adamc@193 96 CRel xn' =>
adamc@193 97 (case Int.compare (xn', xn) of
adamc@193 98 EQUAL => #1 rep
adamc@193 99 | GREATER => CRel (xn' - 1)
adamc@193 100 | LESS => c)
adamc@193 101 | _ => c,
adamc@626 102 bind = fn ((xn, rep), U.Con.RelC _) => (xn+1, liftConInCon 0 rep)
adamc@193 103 | (ctx, _) => ctx}
adamc@193 104
adamc@16 105
adamc@315 106 val liftConInExp =
adamc@626 107 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@315 108 con = fn bound => fn c =>
adamc@315 109 case c of
adamc@315 110 CRel xn =>
adamc@315 111 if xn < bound then
adamc@315 112 c
adamc@315 113 else
adamc@315 114 CRel (xn + 1)
adamc@315 115 | _ => c,
adamc@315 116 exp = fn _ => fn e => e,
adamc@315 117 bind = fn (bound, U.Exp.RelC _) => bound + 1
adamc@315 118 | (bound, _) => bound}
adamc@315 119
adamc@315 120 val subConInExp =
adamc@626 121 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@315 122 con = fn (xn, rep) => fn c =>
adamc@417 123 case c of
adamc@417 124 CRel xn' =>
adamc@417 125 (case Int.compare (xn', xn) of
adamc@417 126 EQUAL => #1 rep
adamc@417 127 | GREATER => CRel (xn' - 1)
adamc@417 128 | LESS => c)
adamc@417 129 | _ => c,
adamc@315 130 exp = fn _ => fn e => e,
adamc@315 131 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
adamc@315 132 | (ctx, _) => ctx}
adamc@315 133
adamc@443 134 val liftExpInExp =
adamc@626 135 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@443 136 con = fn _ => fn c => c,
adamc@443 137 exp = fn bound => fn e =>
adamc@443 138 case e of
adamc@443 139 ERel xn =>
adamc@443 140 if xn < bound then
adamc@443 141 e
adamc@443 142 else
adamc@443 143 ERel (xn + 1)
adamc@443 144 | _ => e,
adamc@443 145 bind = fn (bound, U.Exp.RelE _) => bound + 1
adamc@443 146 | (bound, _) => bound}
adamc@443 147
adamc@443 148 val subExpInExp =
adamc@626 149 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@443 150 con = fn _ => fn c => c,
adamc@443 151 exp = fn (xn, rep) => fn e =>
adamc@443 152 case e of
adamc@443 153 ERel xn' =>
adamc@443 154 (case Int.compare (xn', xn) of
adamc@443 155 EQUAL => #1 rep
adamc@443 156 | GREATER=> ERel (xn' - 1)
adamc@443 157 | LESS => e)
adamc@443 158 | _ => e,
adamc@443 159 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
adamc@443 160 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
adamc@443 161 | (ctx, _) => ctx}
adamc@443 162
adamc@16 163 (* Back to environments *)
adamc@16 164
adamc@16 165 exception UnboundRel of int
adamc@16 166 exception UnboundNamed of int
adamc@16 167
adamc@16 168 type env = {
adamc@626 169 relK : string list,
adamc@626 170
adamc@16 171 relC : (string * kind) list,
adamc@16 172 namedC : (string * kind * con option) IM.map,
adamc@16 173
adamc@192 174 datatypes : (string * string list * (string * int * con option) list) IM.map,
adamc@192 175 constructors : (string * string list * con option * int) IM.map,
adamc@168 176
adamc@16 177 relE : (string * con) list,
adamc@109 178 namedE : (string * con * exp option * string) IM.map
adamc@16 179 }
adamc@16 180
adamc@16 181 val empty = {
adamc@626 182 relK = [],
adamc@626 183
adamc@16 184 relC = [],
adamc@16 185 namedC = IM.empty,
adamc@16 186
adamc@168 187 datatypes = IM.empty,
adamc@177 188 constructors = IM.empty,
adamc@168 189
adamc@16 190 relE = [],
adamc@16 191 namedE = IM.empty
adamc@16 192 }
adamc@16 193
adamc@626 194 fun pushKRel (env : env) x =
adamc@626 195 {relK = x :: #relK env,
adamc@626 196
adamc@626 197 relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
adamc@626 198 namedC = #namedC env,
adamc@626 199
adamc@626 200 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
adamc@626 201 namedE = #namedE env,
adamc@626 202
adamc@626 203 datatypes = #datatypes env,
adamc@626 204 constructors = #constructors env
adamc@626 205 }
adamc@626 206
adamc@626 207 fun lookupKRel (env : env) n =
adamc@626 208 (List.nth (#relK env, n))
adamc@626 209 handle Subscript => raise UnboundRel n
adamc@626 210
adamc@16 211 fun pushCRel (env : env) x k =
adamc@626 212 {relK = #relK env,
adamc@626 213
adamc@626 214 relC = (x, k) :: #relC env,
adamc@16 215 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
adamc@16 216
adamc@168 217 datatypes = #datatypes env,
adamc@177 218 constructors = #constructors env,
adamc@168 219
adamc@16 220 relE = map (fn (x, c) => (x, lift c)) (#relE env),
adamc@109 221 namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)}
adamc@16 222
adamc@16 223 fun lookupCRel (env : env) n =
adamc@16 224 (List.nth (#relC env, n))
adamc@16 225 handle Subscript => raise UnboundRel n
adamc@16 226
adamc@16 227 fun pushCNamed (env : env) x n k co =
adamc@626 228 {relK = #relK env,
adamc@626 229
adamc@626 230 relC = #relC env,
adamc@16 231 namedC = IM.insert (#namedC env, n, (x, k, co)),
adamc@16 232
adamc@168 233 datatypes = #datatypes env,
adamc@177 234 constructors = #constructors env,
adamc@168 235
adamc@16 236 relE = #relE env,
adamc@16 237 namedE = #namedE env}
adamc@16 238
adamc@16 239 fun lookupCNamed (env : env) n =
adamc@16 240 case IM.find (#namedC env, n) of
adamc@16 241 NONE => raise UnboundNamed n
adamc@16 242 | SOME x => x
adamc@16 243
adamc@192 244 fun pushDatatype (env : env) x n xs xncs =
adamc@626 245 {relK = #relK env,
adamc@626 246
adamc@626 247 relC = #relC env,
adamc@168 248 namedC = #namedC env,
adamc@168 249
adamc@192 250 datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)),
adamc@182 251 constructors = foldl (fn ((x, n', to), constructors) =>
adamc@192 252 IM.insert (constructors, n', (x, xs, to, n)))
adamc@177 253 (#constructors env) xncs,
adamc@168 254
adamc@168 255 relE = #relE env,
adamc@168 256 namedE = #namedE env}
adamc@168 257
adamc@168 258 fun lookupDatatype (env : env) n =
adamc@168 259 case IM.find (#datatypes env, n) of
adamc@168 260 NONE => raise UnboundNamed n
adamc@168 261 | SOME x => x
adamc@168 262
adamc@177 263 fun lookupConstructor (env : env) n =
adamc@177 264 case IM.find (#constructors env, n) of
adamc@177 265 NONE => raise UnboundNamed n
adamc@177 266 | SOME x => x
adamc@177 267
adamc@16 268 fun pushERel (env : env) x t =
adamc@626 269 {relK = #relK env,
adamc@626 270
adamc@626 271 relC = #relC env,
adamc@16 272 namedC = #namedC env,
adamc@16 273
adamc@168 274 datatypes = #datatypes env,
adamc@177 275 constructors = #constructors env,
adamc@168 276
adamc@16 277 relE = (x, t) :: #relE env,
adamc@16 278 namedE = #namedE env}
adamc@16 279
adamc@16 280 fun lookupERel (env : env) n =
adamc@16 281 (List.nth (#relE env, n))
adamc@16 282 handle Subscript => raise UnboundRel n
adamc@16 283
adamc@109 284 fun pushENamed (env : env) x n t eo s =
adamc@626 285 {relK = #relK env,
adamc@626 286
adamc@626 287 relC = #relC env,
adamc@16 288 namedC = #namedC env,
adamc@16 289
adamc@168 290 datatypes = #datatypes env,
adamc@177 291 constructors = #constructors env,
adamc@168 292
adamc@16 293 relE = #relE env,
adamc@109 294 namedE = IM.insert (#namedE env, n, (x, t, eo, s))}
adamc@16 295
adamc@16 296 fun lookupENamed (env : env) n =
adamc@16 297 case IM.find (#namedE env, n) of
adamc@16 298 NONE => raise UnboundNamed n
adamc@16 299 | SOME x => x
adamc@16 300
adamc@163 301 fun declBinds env (d, loc) =
adamc@16 302 case d of
adamc@16 303 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@192 304 | DDatatype (x, n, xs, xncs) =>
adamc@163 305 let
adamc@192 306 val env = pushDatatype env x n xs xncs
adamc@163 307 val env = pushCNamed env x n (KType, loc) NONE
adamc@163 308 in
adamc@163 309 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""
adamc@163 310 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc) NONE "")
adamc@163 311 env xncs
adamc@163 312 end
adamc@109 313 | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
adamc@126 314 | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis
adamc@109 315 | DExport _ => env
adamc@707 316 | DTable (x, n, c, s, _, pc, _, cc) =>
adamc@247 317 let
adamc@705 318 val ct = (CFfi ("Basis", "sql_table"), loc)
adamc@705 319 val ct = (CApp (ct, c), loc)
adamc@707 320 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@338 321 in
adamc@705 322 pushENamed env x n ct NONE s
adamc@338 323 end
adamc@338 324 | DSequence (x, n, s) =>
adamc@338 325 let
adamc@338 326 val t = (CFfi ("Basis", "sql_sequence"), loc)
adamc@247 327 in
adamc@247 328 pushENamed env x n t NONE s
adamc@247 329 end
adamc@271 330 | DDatabase _ => env
adamc@461 331 | DCookie (x, n, c, s) =>
adamc@461 332 let
adamc@461 333 val t = (CApp ((CFfi ("Basis", "http_cookie"), loc), c), loc)
adamc@461 334 in
adamc@461 335 pushENamed env x n t NONE s
adamc@461 336 end
adamc@16 337
adamc@193 338 fun patBinds env (p, loc) =
adamc@193 339 case p of
adamc@193 340 PWild => env
adamc@193 341 | PVar (x, t) => pushERel env x t
adamc@193 342 | PPrim _ => env
adamc@193 343 | PCon (_, _, _, NONE) => env
adamc@193 344 | PCon (_, _, _, SOME p) => patBinds env p
adamc@193 345 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
adamc@193 346
adamc@642 347 fun patBindsN (p, loc) =
adamc@642 348 case p of
adamc@642 349 PWild => 0
adamc@642 350 | PVar _ => 1
adamc@642 351 | PPrim _ => 0
adamc@642 352 | PCon (_, _, _, NONE) => 0
adamc@642 353 | PCon (_, _, _, SOME p) => patBindsN p
adamc@642 354 | PRecord xps => foldl (fn ((_, p, _), count) => count + patBindsN p) 0 xps
adamc@642 355
adamc@16 356 end