Mercurial > urweb

annotate src/expl_env.sml @ 704:70cbdcf5989b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
UNIQUE constraints
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 12:24:31 -0400
parents 354800878b4d
children e6706a1df013
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@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@191 258 | DDatatype (x, n, xs, xncs) =>
adamc@162 259 let
adamc@162 260 val env = pushCNamed env x n (KType, loc) NONE
adamc@162 261 in
adamc@191 262 foldl (fn ((x', n', to), env) =>
adamc@191 263 let
adamc@191 264 val t =
adamc@191 265 case to of
adamc@191 266 NONE => (CNamed n, loc)
adamc@191 267 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 268 val k = (KType, loc)
adamc@191 269 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 270 in
adamc@191 271 pushENamed env x' n' t
adamc@191 272 end)
adamc@191 273 env xncs
adamc@162 274 end
adamc@191 275 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
adamc@162 276 let
adamc@162 277 val t = (CModProj (m, ms, x'), loc)
adamc@162 278 val env = pushCNamed env x n (KType, loc) (SOME t)
adamc@162 279
adamc@162 280 val t = (CNamed n, loc)
adamc@162 281 in
adamc@191 282 foldl (fn ((x', n', to), env) =>
adamc@191 283 let
adamc@191 284 val t =
adamc@191 285 case to of
adamc@191 286 NONE => (CNamed n, loc)
adamc@191 287 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 288 val k = (KType, loc)
adamc@191 289 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 290 in
adamc@191 291 pushENamed env x' n' t
adamc@191 292 end)
adamc@191 293 env xncs
adamc@162 294 end
adamc@38 295 | DVal (x, n, t, _) => pushENamed env x n t
adamc@124 296 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
adamc@38 297 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 298 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
adamc@48 299 | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@109 300 | DExport _ => env
adamc@704 301 | DTable (tn, x, n, c, _) =>
adamc@246 302 let
adamc@338 303 val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
adamc@338 304 in
adamc@338 305 pushENamed env x n t
adamc@338 306 end
adamc@338 307 | DSequence (tn, x, n) =>
adamc@338 308 let
adamc@338 309 val t = (CModProj (tn, [], "sql_sequence"), loc)
adamc@246 310 in
adamc@246 311 pushENamed env x n t
adamc@246 312 end
adamc@275 313 | DDatabase _ => env
adamc@460 314 | DCookie (tn, x, n, c) =>
adamc@460 315 let
adamc@460 316 val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc)
adamc@460 317 in
adamc@460 318 pushENamed env x n t
adamc@460 319 end
adamc@38 320
adamc@162 321 fun sgiBinds env (sgi, loc) =
adamc@38 322 case sgi of
adamc@38 323 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
adamc@38 324 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@191 325 | SgiDatatype (x, n, xs, xncs) =>
adamc@162 326 let
adamc@162 327 val env = pushCNamed env x n (KType, loc) NONE
adamc@162 328 in
adamc@191 329 foldl (fn ((x', n', to), env) =>
adamc@191 330 let
adamc@191 331 val t =
adamc@191 332 case to of
adamc@191 333 NONE => (CNamed n, loc)
adamc@191 334 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 335 val k = (KType, loc)
adamc@191 336 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 337 in
adamc@191 338 pushENamed env x' n' t
adamc@191 339 end)
adamc@191 340 env xncs
adamc@162 341 end
adamc@191 342 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@162 343 let
adamc@191 344 val t = (CModProj (m1, ms, x'), loc)
adamc@191 345 val env = pushCNamed env x n (KType, loc) (SOME t)
adamc@191 346
adamc@191 347 val t = (CNamed n, loc)
adamc@162 348 in
adamc@191 349 foldl (fn ((x', n', to), env) =>
adamc@191 350 let
adamc@191 351 val t =
adamc@191 352 case to of
adamc@191 353 NONE => (CNamed n, loc)
adamc@191 354 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 355 val k = (KType, loc)
adamc@191 356 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 357 in
adamc@191 358 pushENamed env x' n' t
adamc@191 359 end)
adamc@191 360 env xncs
adamc@162 361 end
adamc@38 362 | SgiVal (x, n, t) => pushENamed env x n t
adamc@64 363 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 364 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@38 365
adamc@38 366 end