Mercurial > urweb

annotate src/elab_env.sml @ 213:0343557355fc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Explifying type classes
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 14:45:23 -0400
parents e86411f647c6
children 38b299373676
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 * All rights reserved.
adamc@2 3 *
adamc@2 4 * Redistribution and use in source and binary forms, with or without
adamc@2 5 * modification, are permitted provided that the following conditions are met:
adamc@2 6 *
adamc@2 7 * - Redistributions of source code must retain the above copyright notice,
adamc@2 8 * this list of conditions and the following disclaimer.
adamc@2 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@2 10 * this list of conditions and the following disclaimer in the documentation
adamc@2 11 * and/or other materials provided with the distribution.
adamc@2 12 * - The names of contributors may not be used to endorse or promote products
adamc@2 13 * derived from this software without specific prior written permission.
adamc@2 14 *
adamc@2 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@2 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@2 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@2 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@2 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@2 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@2 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@2 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@2 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@2 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@2 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@2 26 *)
adamc@2 27
adamc@2 28 structure ElabEnv :> ELAB_ENV = struct
adamc@2 29
adamc@2 30 open Elab
adamc@2 31
adamc@13 32 structure U = ElabUtil
adamc@13 33
adamc@211 34 structure IS = IntBinarySet
adamc@2 35 structure IM = IntBinaryMap
adamc@2 36 structure SM = BinaryMapFn(struct
adamc@2 37 type ord_key = string
adamc@2 38 val compare = String.compare
adamc@2 39 end)
adamc@2 40
adamc@2 41 exception UnboundRel of int
adamc@2 42 exception UnboundNamed of int
adamc@2 43
adamc@13 44
adamc@13 45 (* AST utility functions *)
adamc@13 46
adamc@13 47 exception SynUnif
adamc@13 48
adamc@13 49 val liftConInCon =
adamc@13 50 U.Con.mapB {kind = fn k => k,
adamc@13 51 con = fn bound => fn c =>
adamc@13 52 case c of
adamc@16 53 CRel xn =>
adamc@13 54 if xn < bound then
adamc@13 55 c
adamc@13 56 else
adamc@16 57 CRel (xn + 1)
adamc@17 58 (*| CUnif _ => raise SynUnif*)
adamc@13 59 | _ => c,
adamc@13 60 bind = fn (bound, U.Con.Rel _) => bound + 1
adamc@13 61 | (bound, _) => bound}
adamc@13 62
adamc@13 63 val lift = liftConInCon 0
adamc@13 64
adamc@211 65 val liftExpInExp =
adamc@211 66 U.Exp.mapB {kind = fn k => k,
adamc@211 67 con = fn _ => fn c => c,
adamc@211 68 exp = fn bound => fn e =>
adamc@211 69 case e of
adamc@211 70 ERel xn =>
adamc@211 71 if xn < bound then
adamc@211 72 e
adamc@211 73 else
adamc@211 74 ERel (xn + 1)
adamc@211 75 | _ => e,
adamc@211 76 bind = fn (bound, U.Exp.RelE _) => bound + 1
adamc@211 77 | (bound, _) => bound}
adamc@211 78
adamc@211 79
adamc@211 80 val liftExp = liftExpInExp 0
adamc@13 81
adamc@13 82 (* Back to environments *)
adamc@13 83
adamc@9 84 datatype 'a var' =
adamc@9 85 Rel' of int * 'a
adamc@9 86 | Named' of int * 'a
adamc@2 87
adamc@9 88 datatype 'a var =
adamc@9 89 NotBound
adamc@9 90 | Rel of int * 'a
adamc@9 91 | Named of int * 'a
adamc@2 92
adamc@191 93 type datatyp = string list * (string * con option) IM.map
adamc@157 94
adamc@211 95 datatype class_name =
adamc@211 96 ClNamed of int
adamc@211 97 | ClProj of int * string list * string
adamc@211 98
adamc@211 99 structure CK = struct
adamc@211 100 type ord_key = class_name
adamc@211 101 open Order
adamc@211 102 fun compare x =
adamc@211 103 case x of
adamc@211 104 (ClNamed n1, ClNamed n2) => Int.compare (n1, n2)
adamc@211 105 | (ClNamed _, _) => LESS
adamc@211 106 | (_, ClNamed _) => GREATER
adamc@211 107
adamc@211 108 | (ClProj (m1, ms1, x1), ClProj (m2, ms2, x2)) =>
adamc@211 109 join (Int.compare (m1, m2),
adamc@211 110 fn () => join (joinL String.compare (ms1, ms2),
adamc@211 111 fn () => String.compare (x1, x2)))
adamc@211 112 end
adamc@211 113
adamc@211 114 structure CM = BinaryMapFn(CK)
adamc@211 115
adamc@211 116 datatype class_key =
adamc@211 117 CkNamed of int
adamc@211 118 | CkRel of int
adamc@211 119 | CkProj of int * string list * string
adamc@211 120
adamc@211 121 structure KK = struct
adamc@211 122 type ord_key = class_key
adamc@211 123 open Order
adamc@211 124 fun compare x =
adamc@211 125 case x of
adamc@211 126 (CkNamed n1, CkNamed n2) => Int.compare (n1, n2)
adamc@211 127 | (CkNamed _, _) => LESS
adamc@211 128 | (_, CkNamed _) => GREATER
adamc@211 129
adamc@211 130 | (CkRel n1, CkRel n2) => Int.compare (n1, n2)
adamc@211 131 | (CkRel _, _) => LESS
adamc@211 132 | (_, CkRel _) => GREATER
adamc@211 133
adamc@211 134 | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) =>
adamc@211 135 join (Int.compare (m1, m2),
adamc@211 136 fn () => join (joinL String.compare (ms1, ms2),
adamc@211 137 fn () => String.compare (x1, x2)))
adamc@211 138 end
adamc@211 139
adamc@211 140 structure KM = BinaryMapFn(KK)
adamc@211 141
adamc@211 142 type class = {
adamc@211 143 ground : exp KM.map
adamc@211 144 }
adamc@211 145
adamc@211 146 val empty_class = {
adamc@211 147 ground = KM.empty
adamc@211 148 }
adamc@211 149
adamc@2 150 type env = {
adamc@9 151 renameC : kind var' SM.map,
adamc@2 152 relC : (string * kind) list,
adamc@11 153 namedC : (string * kind * con option) IM.map,
adamc@9 154
adamc@157 155 datatypes : datatyp IM.map,
adamc@191 156 constructors : (datatype_kind * int * string list * con option * int) SM.map,
adamc@157 157
adamc@211 158 classes : class CM.map,
adamc@211 159
adamc@9 160 renameE : con var' SM.map,
adamc@9 161 relE : (string * con) list,
adamc@31 162 namedE : (string * con) IM.map,
adamc@31 163
adamc@31 164 renameSgn : (int * sgn) SM.map,
adamc@31 165 sgn : (string * sgn) IM.map,
adamc@31 166
adamc@31 167 renameStr : (int * sgn) SM.map,
adamc@31 168 str : (string * sgn) IM.map
adamc@2 169 }
adamc@2 170
adamc@2 171 val namedCounter = ref 0
adamc@2 172
adamc@109 173 fun newNamed () =
adamc@109 174 let
adamc@109 175 val r = !namedCounter
adamc@109 176 in
adamc@109 177 namedCounter := r + 1;
adamc@109 178 r
adamc@109 179 end
adamc@109 180
adamc@2 181 val empty = {
adamc@2 182 renameC = SM.empty,
adamc@2 183 relC = [],
adamc@9 184 namedC = IM.empty,
adamc@9 185
adamc@157 186 datatypes = IM.empty,
adamc@171 187 constructors = SM.empty,
adamc@157 188
adamc@211 189 classes = CM.empty,
adamc@211 190
adamc@9 191 renameE = SM.empty,
adamc@9 192 relE = [],
adamc@31 193 namedE = IM.empty,
adamc@31 194
adamc@31 195 renameSgn = SM.empty,
adamc@31 196 sgn = IM.empty,
adamc@31 197
adamc@31 198 renameStr = SM.empty,
adamc@31 199 str = IM.empty
adamc@2 200 }
adamc@2 201
adamc@211 202 fun liftClassKey ck =
adamc@211 203 case ck of
adamc@211 204 CkNamed _ => ck
adamc@211 205 | CkRel n => CkRel (n + 1)
adamc@211 206 | CkProj _ => ck
adamc@211 207
adamc@2 208 fun pushCRel (env : env) x k =
adamc@2 209 let
adamc@9 210 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
adamc@2 211 | x => x) (#renameC env)
adamc@2 212 in
adamc@9 213 {renameC = SM.insert (renameC, x, Rel' (0, k)),
adamc@2 214 relC = (x, k) :: #relC env,
adamc@13 215 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
adamc@9 216
adamc@157 217 datatypes = #datatypes env,
adamc@171 218 constructors = #constructors env,
adamc@157 219
adamc@211 220 classes = CM.map (fn class => {
adamc@211 221 ground = KM.foldli (fn (ck, e, km) =>
adamc@211 222 KM.insert (km, liftClassKey ck, e))
adamc@211 223 KM.empty (#ground class)
adamc@211 224 })
adamc@211 225 (#classes env),
adamc@211 226
adamc@9 227 renameE = #renameE env,
adamc@13 228 relE = map (fn (x, c) => (x, lift c)) (#relE env),
adamc@31 229 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
adamc@31 230
adamc@31 231 renameSgn = #renameSgn env,
adamc@31 232 sgn = #sgn env,
adamc@31 233
adamc@31 234 renameStr = #renameStr env,
adamc@31 235 str = #str env
adamc@31 236 }
adamc@2 237 end
adamc@2 238
adamc@2 239 fun lookupCRel (env : env) n =
adamc@2 240 (List.nth (#relC env, n))
adamc@2 241 handle Subscript => raise UnboundRel n
adamc@2 242
adamc@11 243 fun pushCNamedAs (env : env) x n k co =
adamc@9 244 {renameC = SM.insert (#renameC env, x, Named' (n, k)),
adamc@5 245 relC = #relC env,
adamc@11 246 namedC = IM.insert (#namedC env, n, (x, k, co)),
adamc@9 247
adamc@157 248 datatypes = #datatypes env,
adamc@171 249 constructors = #constructors env,
adamc@157 250
adamc@211 251 classes = #classes env,
adamc@211 252
adamc@9 253 renameE = #renameE env,
adamc@9 254 relE = #relE env,
adamc@31 255 namedE = #namedE env,
adamc@31 256
adamc@31 257 renameSgn = #renameSgn env,
adamc@31 258 sgn = #sgn env,
adamc@31 259
adamc@31 260 renameStr = #renameStr env,
adamc@31 261 str = #str env}
adamc@5 262
adamc@11 263 fun pushCNamed env x k co =
adamc@2 264 let
adamc@2 265 val n = !namedCounter
adamc@2 266 in
adamc@2 267 namedCounter := n + 1;
adamc@11 268 (pushCNamedAs env x n k co, n)
adamc@2 269 end
adamc@2 270
adamc@2 271 fun lookupCNamed (env : env) n =
adamc@2 272 case IM.find (#namedC env, n) of
adamc@2 273 NONE => raise UnboundNamed n
adamc@2 274 | SOME x => x
adamc@2 275
adamc@2 276 fun lookupC (env : env) x =
adamc@2 277 case SM.find (#renameC env, x) of
adamc@9 278 NONE => NotBound
adamc@9 279 | SOME (Rel' x) => Rel x
adamc@9 280 | SOME (Named' x) => Named x
adamc@9 281
adamc@191 282 fun pushDatatype (env : env) n xs xncs =
adamc@188 283 let
adamc@188 284 val dk = U.classifyDatatype xncs
adamc@188 285 in
adamc@188 286 {renameC = #renameC env,
adamc@188 287 relC = #relC env,
adamc@188 288 namedC = #namedC env,
adamc@157 289
adamc@188 290 datatypes = IM.insert (#datatypes env, n,
adamc@191 291 (xs, foldl (fn ((x, n, to), cons) =>
adamc@191 292 IM.insert (cons, n, (x, to))) IM.empty xncs)),
adamc@188 293 constructors = foldl (fn ((x, n', to), cmap) =>
adamc@191 294 SM.insert (cmap, x, (dk, n', xs, to, n)))
adamc@188 295 (#constructors env) xncs,
adamc@157 296
adamc@211 297 classes = #classes env,
adamc@211 298
adamc@188 299 renameE = #renameE env,
adamc@188 300 relE = #relE env,
adamc@188 301 namedE = #namedE env,
adamc@157 302
adamc@188 303 renameSgn = #renameSgn env,
adamc@188 304 sgn = #sgn env,
adamc@157 305
adamc@188 306 renameStr = #renameStr env,
adamc@188 307 str = #str env}
adamc@188 308 end
adamc@157 309
adamc@157 310 fun lookupDatatype (env : env) n =
adamc@157 311 case IM.find (#datatypes env, n) of
adamc@157 312 NONE => raise UnboundNamed n
adamc@157 313 | SOME x => x
adamc@157 314
adamc@191 315 fun lookupDatatypeConstructor (_, dt) n =
adamc@157 316 case IM.find (dt, n) of
adamc@157 317 NONE => raise UnboundNamed n
adamc@157 318 | SOME x => x
adamc@157 319
adamc@171 320 fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
adamc@171 321
adamc@191 322 fun datatypeArgs (xs, _) = xs
adamc@191 323 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
adamc@157 324
adamc@211 325 fun pushClass (env : env) n =
adamc@211 326 {renameC = #renameC env,
adamc@211 327 relC = #relC env,
adamc@211 328 namedC = #namedC env,
adamc@211 329
adamc@211 330 datatypes = #datatypes env,
adamc@211 331 constructors = #constructors env,
adamc@211 332
adamc@211 333 classes = CM.insert (#classes env, ClNamed n, {ground = KM.empty}),
adamc@211 334
adamc@211 335 renameE = #renameE env,
adamc@211 336 relE = #relE env,
adamc@211 337 namedE = #namedE env,
adamc@211 338
adamc@211 339 renameSgn = #renameSgn env,
adamc@211 340 sgn = #sgn env,
adamc@211 341
adamc@211 342 renameStr = #renameStr env,
adamc@211 343 str = #str env}
adamc@211 344
adamc@211 345 fun class_name_in (c, _) =
adamc@211 346 case c of
adamc@211 347 CNamed n => SOME (ClNamed n)
adamc@211 348 | CModProj x => SOME (ClProj x)
adamc@211 349 | _ => NONE
adamc@211 350
adamc@211 351 fun class_key_in (c, _) =
adamc@211 352 case c of
adamc@211 353 CRel n => SOME (CkRel n)
adamc@211 354 | CNamed n => SOME (CkNamed n)
adamc@211 355 | CModProj x => SOME (CkProj x)
adamc@211 356 | _ => NONE
adamc@211 357
adamc@211 358 fun class_pair_in (c, _) =
adamc@211 359 case c of
adamc@211 360 CApp (f, x) =>
adamc@211 361 (case (class_name_in f, class_key_in x) of
adamc@211 362 (SOME f, SOME x) => SOME (f, x)
adamc@211 363 | _ => NONE)
adamc@211 364 | _ => NONE
adamc@211 365
adamc@211 366 fun resolveClass (env : env) c =
adamc@211 367 case class_pair_in c of
adamc@211 368 SOME (f, x) =>
adamc@211 369 (case CM.find (#classes env, f) of
adamc@211 370 NONE => NONE
adamc@211 371 | SOME class =>
adamc@211 372 case KM.find (#ground class, x) of
adamc@211 373 NONE => NONE
adamc@211 374 | SOME e => SOME e)
adamc@211 375 | _ => NONE
adamc@211 376
adamc@9 377 fun pushERel (env : env) x t =
adamc@9 378 let
adamc@9 379 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
adamc@9 380 | x => x) (#renameE env)
adamc@211 381
adamc@211 382 val classes = CM.map (fn class => {
adamc@211 383 ground = KM.map liftExp (#ground class)
adamc@211 384 }) (#classes env)
adamc@211 385 val classes = case class_pair_in t of
adamc@211 386 NONE => classes
adamc@211 387 | SOME (f, x) =>
adamc@211 388 let
adamc@211 389 val class = Option.getOpt (CM.find (classes, f), empty_class)
adamc@211 390 val class = {
adamc@211 391 ground = KM.insert (#ground class, x, (ERel 0, #2 t))
adamc@211 392 }
adamc@211 393 in
adamc@211 394 CM.insert (classes, f, class)
adamc@211 395 end
adamc@9 396 in
adamc@9 397 {renameC = #renameC env,
adamc@9 398 relC = #relC env,
adamc@9 399 namedC = #namedC env,
adamc@9 400
adamc@157 401 datatypes = #datatypes env,
adamc@171 402 constructors = #constructors env,
adamc@157 403
adamc@211 404 classes = classes,
adamc@211 405
adamc@9 406 renameE = SM.insert (renameE, x, Rel' (0, t)),
adamc@9 407 relE = (x, t) :: #relE env,
adamc@31 408 namedE = #namedE env,
adamc@31 409
adamc@31 410 renameSgn = #renameSgn env,
adamc@31 411 sgn = #sgn env,
adamc@31 412
adamc@31 413 renameStr = #renameStr env,
adamc@31 414 str = #str env}
adamc@9 415 end
adamc@9 416
adamc@9 417 fun lookupERel (env : env) n =
adamc@9 418 (List.nth (#relE env, n))
adamc@9 419 handle Subscript => raise UnboundRel n
adamc@9 420
adamc@9 421 fun pushENamedAs (env : env) x n t =
adamc@211 422 let
adamc@211 423 val classes = #classes env
adamc@211 424 val classes = case class_pair_in t of
adamc@211 425 NONE => classes
adamc@211 426 | SOME (f, x) =>
adamc@211 427 let
adamc@211 428 val class = Option.getOpt (CM.find (classes, f), empty_class)
adamc@211 429 val class = {
adamc@211 430 ground = KM.insert (#ground class, x, (ENamed n, #2 t))
adamc@211 431 }
adamc@211 432 in
adamc@211 433 CM.insert (classes, f, class)
adamc@211 434 end
adamc@211 435 in
adamc@211 436 {renameC = #renameC env,
adamc@211 437 relC = #relC env,
adamc@211 438 namedC = #namedC env,
adamc@9 439
adamc@211 440 datatypes = #datatypes env,
adamc@211 441 constructors = #constructors env,
adamc@157 442
adamc@211 443 classes = classes,
adamc@31 444
adamc@211 445 renameE = SM.insert (#renameE env, x, Named' (n, t)),
adamc@211 446 relE = #relE env,
adamc@211 447 namedE = IM.insert (#namedE env, n, (x, t)),
adamc@211 448
adamc@211 449 renameSgn = #renameSgn env,
adamc@211 450 sgn = #sgn env,
adamc@211 451
adamc@211 452 renameStr = #renameStr env,
adamc@211 453 str = #str env}
adamc@211 454 end
adamc@9 455
adamc@9 456 fun pushENamed env x t =
adamc@9 457 let
adamc@9 458 val n = !namedCounter
adamc@9 459 in
adamc@9 460 namedCounter := n + 1;
adamc@9 461 (pushENamedAs env x n t, n)
adamc@9 462 end
adamc@9 463
adamc@9 464 fun lookupENamed (env : env) n =
adamc@9 465 case IM.find (#namedE env, n) of
adamc@9 466 NONE => raise UnboundNamed n
adamc@9 467 | SOME x => x
adamc@9 468
adamc@9 469 fun lookupE (env : env) x =
adamc@9 470 case SM.find (#renameE env, x) of
adamc@9 471 NONE => NotBound
adamc@9 472 | SOME (Rel' x) => Rel x
adamc@9 473 | SOME (Named' x) => Named x
adamc@2 474
adamc@31 475 fun pushSgnNamedAs (env : env) x n sgis =
adamc@31 476 {renameC = #renameC env,
adamc@31 477 relC = #relC env,
adamc@31 478 namedC = #namedC env,
adamc@31 479
adamc@157 480 datatypes = #datatypes env,
adamc@171 481 constructors = #constructors env,
adamc@157 482
adamc@211 483 classes = #classes env,
adamc@211 484
adamc@31 485 renameE = #renameE env,
adamc@31 486 relE = #relE env,
adamc@31 487 namedE = #namedE env,
adamc@31 488
adamc@31 489 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
adamc@31 490 sgn = IM.insert (#sgn env, n, (x, sgis)),
adamc@31 491
adamc@31 492 renameStr = #renameStr env,
adamc@31 493 str = #str env}
adamc@31 494
adamc@31 495 fun pushSgnNamed env x sgis =
adamc@31 496 let
adamc@31 497 val n = !namedCounter
adamc@31 498 in
adamc@31 499 namedCounter := n + 1;
adamc@31 500 (pushSgnNamedAs env x n sgis, n)
adamc@31 501 end
adamc@31 502
adamc@31 503 fun lookupSgnNamed (env : env) n =
adamc@31 504 case IM.find (#sgn env, n) of
adamc@31 505 NONE => raise UnboundNamed n
adamc@31 506 | SOME x => x
adamc@31 507
adamc@31 508 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
adamc@31 509
adamc@31 510 fun lookupStrNamed (env : env) n =
adamc@31 511 case IM.find (#str env, n) of
adamc@31 512 NONE => raise UnboundNamed n
adamc@31 513 | SOME x => x
adamc@31 514
adamc@31 515 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
adamc@31 516
adamc@203 517
adamc@34 518 fun sgnSeek f sgis =
adamc@34 519 let
adamc@59 520 fun seek (sgis, sgns, strs, cons) =
adamc@34 521 case sgis of
adamc@34 522 [] => NONE
adamc@34 523 | (sgi, _) :: sgis =>
adamc@34 524 case f sgi of
adamc@158 525 SOME v =>
adamc@158 526 let
adamc@158 527 val cons =
adamc@158 528 case sgi of
adamc@191 529 SgiDatatype (x, n, _, _) => IM.insert (cons, n, x)
adamc@191 530 | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
adamc@158 531 | _ => cons
adamc@158 532 in
adamc@158 533 SOME (v, (sgns, strs, cons))
adamc@158 534 end
adamc@88 535 | NONE =>
adamc@88 536 case sgi of
adamc@88 537 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
adamc@88 538 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
adamc@191 539 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
adamc@191 540 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
adamc@88 541 | SgiVal _ => seek (sgis, sgns, strs, cons)
adamc@88 542 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
adamc@88 543 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
adamc@88 544 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
adamc@203 545 | SgiTable _ => seek (sgis, sgns, strs, cons)
adamc@211 546 | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
adamc@211 547 | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
adamc@34 548 in
adamc@59 549 seek (sgis, IM.empty, IM.empty, IM.empty)
adamc@34 550 end
adamc@34 551
adamc@34 552 fun id x = x
adamc@34 553
adamc@34 554 fun unravelStr (str, _) =
adamc@34 555 case str of
adamc@34 556 StrVar x => (x, [])
adamc@34 557 | StrProj (str, m) =>
adamc@34 558 let
adamc@34 559 val (x, ms) = unravelStr str
adamc@34 560 in
adamc@34 561 (x, ms @ [m])
adamc@34 562 end
adamc@34 563 | _ => raise Fail "unravelStr"
adamc@34 564
adamc@59 565 fun sgnS_con (str, (sgns, strs, cons)) c =
adamc@34 566 case c of
adamc@34 567 CModProj (m1, ms, x) =>
adamc@34 568 (case IM.find (strs, m1) of
adamc@34 569 NONE => c
adamc@34 570 | SOME m1x =>
adamc@34 571 let
adamc@34 572 val (m1, ms') = unravelStr str
adamc@34 573 in
adamc@34 574 CModProj (m1, ms' @ m1x :: ms, x)
adamc@34 575 end)
adamc@34 576 | CNamed n =>
adamc@34 577 (case IM.find (cons, n) of
adamc@34 578 NONE => c
adamc@34 579 | SOME nx =>
adamc@34 580 let
adamc@34 581 val (m1, ms) = unravelStr str
adamc@34 582 in
adamc@34 583 CModProj (m1, ms, nx)
adamc@34 584 end)
adamc@34 585 | _ => c
adamc@34 586
adamc@59 587 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
adamc@59 588 case sgn of
adamc@59 589 SgnProj (m1, ms, x) =>
adamc@59 590 (case IM.find (strs, m1) of
adamc@59 591 NONE => sgn
adamc@59 592 | SOME m1x =>
adamc@59 593 let
adamc@59 594 val (m1, ms') = unravelStr str
adamc@59 595 in
adamc@59 596 SgnProj (m1, ms' @ m1x :: ms, x)
adamc@59 597 end)
adamc@59 598 | SgnVar n =>
adamc@59 599 (case IM.find (sgns, n) of
adamc@59 600 NONE => sgn
adamc@59 601 | SOME nx =>
adamc@59 602 let
adamc@59 603 val (m1, ms) = unravelStr str
adamc@59 604 in
adamc@59 605 SgnProj (m1, ms, nx)
adamc@59 606 end)
adamc@59 607 | _ => sgn
adamc@59 608
adamc@59 609 fun sgnSubSgn x =
adamc@34 610 ElabUtil.Sgn.map {kind = id,
adamc@59 611 con = sgnS_con x,
adamc@34 612 sgn_item = id,
adamc@59 613 sgn = sgnS_sgn x}
adamc@34 614
adamc@211 615
adamc@211 616
adamc@211 617 and projectSgn env {sgn, str, field} =
adamc@211 618 case #1 (hnormSgn env sgn) of
adamc@211 619 SgnConst sgis =>
adamc@211 620 (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
adamc@211 621 NONE => NONE
adamc@211 622 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
adamc@211 623 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
adamc@211 624 | _ => NONE
adamc@211 625
adamc@211 626 and hnormSgn env (all as (sgn, loc)) =
adamc@34 627 case sgn of
adamc@42 628 SgnError => all
adamc@42 629 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
adamc@42 630 | SgnConst _ => all
adamc@42 631 | SgnFun _ => all
adamc@59 632 | SgnProj (m, ms, x) =>
adamc@59 633 let
adamc@59 634 val (_, sgn) = lookupStrNamed env m
adamc@59 635 in
adamc@59 636 case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms,
adamc@59 637 sgn = sgn,
adamc@59 638 field = x} of
adamc@59 639 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
adamc@59 640 | SOME sgn => sgn
adamc@59 641 end
adamc@42 642 | SgnWhere (sgn, x, c) =>
adamc@42 643 case #1 (hnormSgn env sgn) of
adamc@42 644 SgnError => (SgnError, loc)
adamc@42 645 | SgnConst sgis =>
adamc@42 646 let
adamc@42 647 fun traverse (pre, post) =
adamc@42 648 case post of
adamc@42 649 [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
adamc@42 650 | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
adamc@42 651 if x = x' then
adamc@42 652 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
adamc@42 653 else
adamc@42 654 traverse (sgi :: pre, rest)
adamc@42 655 | sgi :: rest => traverse (sgi :: pre, rest)
adamc@42 656
adamc@42 657 val sgis = traverse ([], sgis)
adamc@42 658 in
adamc@42 659 (SgnConst sgis, loc)
adamc@42 660 end
adamc@42 661 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
adamc@42 662
adamc@211 663 fun enrichClasses env classes (m1, ms) sgn =
adamc@59 664 case #1 (hnormSgn env sgn) of
adamc@59 665 SgnConst sgis =>
adamc@211 666 let
adamc@211 667 val (classes, _) =
adamc@211 668 foldl (fn (sgi, (classes, newClasses)) =>
adamc@211 669 let
adamc@211 670 fun found (x, n) =
adamc@211 671 (CM.insert (classes,
adamc@211 672 ClProj (m1, ms, x),
adamc@211 673 empty_class),
adamc@211 674 IS.add (newClasses, n))
adamc@211 675 in
adamc@211 676 case #1 sgi of
adamc@211 677 SgiClassAbs xn => found xn
adamc@211 678 | SgiClass (x, n, _) => found (x, n)
adamc@211 679 | _ => (classes, newClasses)
adamc@211 680 end)
adamc@211 681 (classes, IS.empty) sgis
adamc@211 682 in
adamc@211 683 classes
adamc@211 684 end
adamc@211 685 | _ => classes
adamc@211 686
adamc@211 687 fun pushStrNamedAs (env : env) x n sgn =
adamc@211 688 {renameC = #renameC env,
adamc@211 689 relC = #relC env,
adamc@211 690 namedC = #namedC env,
adamc@211 691
adamc@211 692 datatypes = #datatypes env,
adamc@211 693 constructors = #constructors env,
adamc@211 694
adamc@211 695 classes = enrichClasses env (#classes env) (n, []) sgn,
adamc@211 696
adamc@211 697 renameE = #renameE env,
adamc@211 698 relE = #relE env,
adamc@211 699 namedE = #namedE env,
adamc@211 700
adamc@211 701 renameSgn = #renameSgn env,
adamc@211 702 sgn = #sgn env,
adamc@211 703
adamc@211 704 renameStr = SM.insert (#renameStr env, x, (n, sgn)),
adamc@211 705 str = IM.insert (#str env, n, (x, sgn))}
adamc@211 706
adamc@211 707 fun pushStrNamed env x sgn =
adamc@211 708 let
adamc@211 709 val n = !namedCounter
adamc@211 710 in
adamc@211 711 namedCounter := n + 1;
adamc@211 712 (pushStrNamedAs env x n sgn, n)
adamc@211 713 end
adamc@211 714
adamc@211 715 fun sgiBinds env (sgi, loc) =
adamc@211 716 case sgi of
adamc@211 717 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
adamc@211 718 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@211 719 | SgiDatatype (x, n, xs, xncs) =>
adamc@211 720 let
adamc@211 721 val env = pushCNamedAs env x n (KType, loc) NONE
adamc@211 722 in
adamc@211 723 foldl (fn ((x', n', to), env) =>
adamc@211 724 let
adamc@211 725 val t =
adamc@211 726 case to of
adamc@211 727 NONE => (CNamed n, loc)
adamc@211 728 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@211 729
adamc@211 730 val k = (KType, loc)
adamc@211 731 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
adamc@211 732 in
adamc@211 733 pushENamedAs env x' n' t
adamc@211 734 end)
adamc@211 735 env xncs
adamc@211 736 end
adamc@211 737 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@211 738 let
adamc@211 739 val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
adamc@211 740 in
adamc@211 741 foldl (fn ((x', n', to), env) =>
adamc@211 742 let
adamc@211 743 val t =
adamc@211 744 case to of
adamc@211 745 NONE => (CNamed n, loc)
adamc@211 746 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@211 747
adamc@211 748 val k = (KType, loc)
adamc@211 749 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
adamc@211 750 in
adamc@211 751 pushENamedAs env x' n' t
adamc@211 752 end)
adamc@211 753 env xncs
adamc@211 754 end
adamc@211 755 | SgiVal (x, n, t) => pushENamedAs env x n t
adamc@211 756 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
adamc@211 757 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
adamc@211 758 | SgiConstraint _ => env
adamc@211 759
adamc@211 760 | SgiTable (tn, x, n, c) =>
adamc@211 761 let
adamc@211 762 val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
adamc@211 763 in
adamc@211 764 pushENamedAs env x n t
adamc@211 765 end
adamc@211 766
adamc@211 767 | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE
adamc@211 768 | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c)
adamc@211 769
adamc@211 770
adamc@211 771 fun sgnSubCon x =
adamc@211 772 ElabUtil.Con.map {kind = id,
adamc@211 773 con = sgnS_con x}
adamc@59 774
adamc@59 775 fun projectStr env {sgn, str, field} =
adamc@59 776 case #1 (hnormSgn env sgn) of
adamc@59 777 SgnConst sgis =>
adamc@59 778 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
adamc@59 779 NONE => NONE
adamc@59 780 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
adamc@59 781 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
adamc@59 782 | _ => NONE
adamc@59 783
adamc@158 784 fun chaseMpath env (n, ms) =
adamc@158 785 let
adamc@158 786 val (_, sgn) = lookupStrNamed env n
adamc@158 787 in
adamc@158 788 foldl (fn (m, (str, sgn)) =>
adamc@158 789 case projectStr env {sgn = sgn, str = str, field = m} of
adamc@158 790 NONE => raise Fail "kindof: Unknown substructure"
adamc@158 791 | SOME sgn => ((StrProj (str, m), #2 sgn), sgn))
adamc@158 792 ((StrVar n, #2 sgn), sgn) ms
adamc@158 793 end
adamc@158 794
adamc@42 795 fun projectCon env {sgn, str, field} =
adamc@42 796 case #1 (hnormSgn env sgn) of
adamc@34 797 SgnConst sgis =>
adamc@34 798 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
adamc@34 799 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
adamc@191 800 | SgiDatatype (x, _, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
adamc@191 801 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
adamc@158 802 if x = field then
adamc@158 803 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn))
adamc@158 804 else
adamc@158 805 NONE
adamc@34 806 | _ => NONE) sgis of
adamc@34 807 NONE => NONE
adamc@34 808 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
adamc@34 809 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
adamc@42 810 | _ => NONE
adamc@34 811
adamc@157 812 fun projectDatatype env {sgn, str, field} =
adamc@157 813 case #1 (hnormSgn env sgn) of
adamc@157 814 SgnConst sgis =>
adamc@191 815 (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
adamc@191 816 | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
adamc@157 817 | _ => NONE) sgis of
adamc@157 818 NONE => NONE
adamc@191 819 | SOME ((xs, xncs), subs) => SOME (xs,
adamc@191 820 map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
adamc@157 821 | _ => NONE
adamc@157 822
adamc@174 823 fun projectConstructor env {sgn, str, field} =
adamc@174 824 case #1 (hnormSgn env sgn) of
adamc@174 825 SgnConst sgis =>
adamc@174 826 let
adamc@191 827 fun consider (n, xs, xncs) =
adamc@174 828 ListUtil.search (fn (x, n', to) =>
adamc@174 829 if x <> field then
adamc@174 830 NONE
adamc@174 831 else
adamc@191 832 SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
adamc@174 833 in
adamc@191 834 case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs)
adamc@191 835 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
adamc@174 836 | _ => NONE) sgis of
adamc@174 837 NONE => NONE
adamc@191 838 | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to,
adamc@191 839 sgnSubCon (str, subs) t)
adamc@174 840 end
adamc@174 841 | _ => NONE
adamc@174 842
adamc@42 843 fun projectVal env {sgn, str, field} =
adamc@42 844 case #1 (hnormSgn env sgn) of
adamc@34 845 SgnConst sgis =>
adamc@162 846 let
adamc@191 847 fun seek (n, xs, xncs) =
adamc@162 848 ListUtil.search (fn (x, _, to) =>
adamc@162 849 if x = field then
adamc@191 850 SOME (let
adamc@191 851 val t =
adamc@191 852 case to of
adamc@191 853 NONE => (CNamed n, #2 sgn)
adamc@191 854 | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn)
adamc@191 855 val k = (KType, #2 sgn)
adamc@191 856 in
adamc@191 857 foldr (fn (x, t) => (TCFun (Explicit, x, k, t), #2 sgn))
adamc@191 858 t xs
adamc@191 859 end)
adamc@162 860 else
adamc@162 861 NONE) xncs
adamc@162 862 in
adamc@162 863 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
adamc@191 864 | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs)
adamc@191 865 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
adamc@162 866 | _ => NONE) sgis of
adamc@162 867 NONE => NONE
adamc@162 868 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
adamc@162 869 end
adamc@34 870 | SgnError => SOME (CError, ErrorMsg.dummySpan)
adamc@42 871 | _ => NONE
adamc@34 872
adamc@88 873 fun sgnSeekConstraints (str, sgis) =
adamc@88 874 let
adamc@88 875 fun seek (sgis, sgns, strs, cons, acc) =
adamc@88 876 case sgis of
adamc@88 877 [] => acc
adamc@88 878 | (sgi, _) :: sgis =>
adamc@88 879 case sgi of
adamc@88 880 SgiConstraint (c1, c2) =>
adamc@88 881 let
adamc@88 882 val sub = sgnSubCon (str, (sgns, strs, cons))
adamc@88 883 in
adamc@88 884 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
adamc@88 885 end
adamc@88 886 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 887 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@191 888 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@191 889 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 890 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
adamc@88 891 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
adamc@88 892 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
adamc@203 893 | SgiTable _ => seek (sgis, sgns, strs, cons, acc)
adamc@211 894 | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@211 895 | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 896 in
adamc@88 897 seek (sgis, IM.empty, IM.empty, IM.empty, [])
adamc@88 898 end
adamc@88 899
adamc@88 900 fun projectConstraints env {sgn, str} =
adamc@88 901 case #1 (hnormSgn env sgn) of
adamc@88 902 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
adamc@88 903 | SgnError => SOME []
adamc@88 904 | _ => NONE
adamc@34 905
adamc@157 906 fun declBinds env (d, loc) =
adamc@157 907 case d of
adamc@157 908 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@191 909 | DDatatype (x, n, xs, xncs) =>
adamc@157 910 let
adamc@157 911 val env = pushCNamedAs env x n (KType, loc) NONE
adamc@191 912 val env = pushDatatype env n xs xncs
adamc@157 913 in
adamc@191 914 foldl (fn ((x', n', to), env) =>
adamc@191 915 let
adamc@191 916 val t =
adamc@191 917 case to of
adamc@191 918 NONE => (CNamed n, loc)
adamc@191 919 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 920 val k = (KType, loc)
adamc@191 921 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
adamc@191 922 in
adamc@191 923 pushENamedAs env x' n' t
adamc@191 924 end)
adamc@191 925 env xncs
adamc@157 926 end
adamc@191 927 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
adamc@157 928 let
adamc@157 929 val t = (CModProj (m, ms, x'), loc)
adamc@157 930 val env = pushCNamedAs env x n (KType, loc) (SOME t)
adamc@191 931 val env = pushDatatype env n xs xncs
adamc@157 932
adamc@157 933 val t = (CNamed n, loc)
adamc@157 934 in
adamc@191 935 foldl (fn ((x', n', to), env) =>
adamc@191 936 let
adamc@191 937 val t =
adamc@191 938 case to of
adamc@191 939 NONE => (CNamed n, loc)
adamc@191 940 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@191 941 val k = (KType, loc)
adamc@191 942 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
adamc@191 943 in
adamc@191 944 pushENamedAs env x' n' t
adamc@191 945 end)
adamc@191 946 env xncs
adamc@157 947 end
adamc@157 948 | DVal (x, n, t, _) => pushENamedAs env x n t
adamc@157 949 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
adamc@157 950 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
adamc@157 951 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
adamc@157 952 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
adamc@157 953 | DConstraint _ => env
adamc@157 954 | DExport _ => env
adamc@205 955 | DTable (tn, x, n, c) =>
adamc@205 956 let
adamc@205 957 val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
adamc@205 958 in
adamc@205 959 pushENamedAs env x n t
adamc@205 960 end
adamc@213 961 | DClass (x, n, c) =>
adamc@213 962 let
adamc@213 963 val k = (KArrow ((KType, loc), (KType, loc)), loc)
adamc@213 964 val env = pushCNamedAs env x n k (SOME c)
adamc@213 965 in
adamc@213 966 pushClass env n
adamc@213 967 end
adamc@157 968
adamc@2 969 end