Mercurial > urweb

annotate src/expl_env.sml @ 1554:396e8d881205

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better detection of type class witnesses in local bindings
author Adam Chlipala <adam@chlipala.net>
date Sat, 03 Sep 2011 08:57:13 -0400
parents b4480a56cab7
children 403f0cc65b9c
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
adamc@38 349
adamc@162 350 fun sgiBinds env (sgi, loc) =
adamc@38 351 case sgi of
adamc@38 352 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
adamc@38 353 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
adamc@806 354 | SgiDatatype dts =>
adamc@162 355 let
adamc@806 356 fun doOne ((x, n, xs, xncs), env) =
adamc@806 357 let
adamc@806 358 val k = (KType, loc)
adamc@806 359 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@806 360
adamc@806 361 val env = pushCNamed env x n k' NONE
adamc@806 362 in
adamc@806 363 foldl (fn ((x', n', to), env) =>
adamc@806 364 let
adamc@806 365 val t =
adamc@806 366 case to of
adamc@806 367 NONE => (CNamed n, loc)
adamc@806 368 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@806 369
adamc@806 370 val k = (KType, loc)
adamc@806 371 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@806 372 in
adamc@806 373 pushENamed env x' n' t
adamc@806 374 end)
adamc@806 375 env xncs
adamc@806 376 end
adamc@162 377 in
adamc@806 378 foldl doOne env dts
adamc@162 379 end
adamc@191 380 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@162 381 let
adamc@191 382 val t = (CModProj (m1, ms, x'), loc)
adamc@191 383 val env = pushCNamed env x n (KType, loc) (SOME t)
adamc@191 384
adamc@191 385 val t = (CNamed n, loc)
adamc@162 386 in
adamc@191 387 foldl (fn ((x', n', to), env) =>
adamc@191 388 let
adamc@191 389 val t =
adamc@191 390 case to of
adamc@191 391 NONE => (CNamed n, loc)
adamc@191 392 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 393 val k = (KType, loc)
adamc@191 394 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
adamc@191 395 in
adamc@191 396 pushENamed env x' n' t
adamc@191 397 end)
adamc@191 398 env xncs
adamc@162 399 end
adamc@38 400 | SgiVal (x, n, t) => pushENamed env x n t
adamc@64 401 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
adamc@38 402 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
adamc@38 403
adamc@1278 404 fun patBinds env (p, loc) =
adamc@1278 405 case p of
adamc@1278 406 PWild => env
adamc@1278 407 | PVar (x, t) => pushERel env x t
adamc@1278 408 | PPrim _ => env
adamc@1278 409 | PCon (_, _, _, NONE) => env
adamc@1278 410 | PCon (_, _, _, SOME p) => patBinds env p
adamc@1278 411 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
adamc@1278 412
adamc@38 413 end