Mercurial > urweb

annotate src/core_env.sml @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents 230654093b51
children 4a125bbc602d
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@247 316 | DTable (x, n, c, s) =>
adamc@247 317 let
adamc@338 318 val t = (CApp ((CFfi ("Basis", "sql_table"), loc), c), loc)
adamc@338 319 in
adamc@338 320 pushENamed env x n t NONE s
adamc@338 321 end
adamc@338 322 | DSequence (x, n, s) =>
adamc@338 323 let
adamc@338 324 val t = (CFfi ("Basis", "sql_sequence"), loc)
adamc@247 325 in
adamc@247 326 pushENamed env x n t NONE s
adamc@247 327 end
adamc@271 328 | DDatabase _ => env
adamc@461 329 | DCookie (x, n, c, s) =>
adamc@461 330 let
adamc@461 331 val t = (CApp ((CFfi ("Basis", "http_cookie"), loc), c), loc)
adamc@461 332 in
adamc@461 333 pushENamed env x n t NONE s
adamc@461 334 end
adamc@16 335
adamc@193 336 fun patBinds env (p, loc) =
adamc@193 337 case p of
adamc@193 338 PWild => env
adamc@193 339 | PVar (x, t) => pushERel env x t
adamc@193 340 | PPrim _ => env
adamc@193 341 | PCon (_, _, _, NONE) => env
adamc@193 342 | PCon (_, _, _, SOME p) => patBinds env p
adamc@193 343 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
adamc@193 344
adamc@16 345 end