Mercurial > urweb

annotate src/elab_env.sml @ 674:fab5998b840e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Type class reductions, but no inclusions yet
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Mar 2009 14:37:31 -0400
parents 588b9d16b00a
children 43430b7190f4
rev   line source
adamc@674 1 (* Copyright (c) 2008-2009, 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@2 34 structure IM = IntBinaryMap
adamc@2 35 structure SM = BinaryMapFn(struct
adamc@2 36 type ord_key = string
adamc@2 37 val compare = String.compare
adamc@2 38 end)
adamc@2 39
adamc@2 40 exception UnboundRel of int
adamc@2 41 exception UnboundNamed of int
adamc@2 42
adamc@13 43
adamc@13 44 (* AST utility functions *)
adamc@13 45
adamc@13 46 exception SynUnif
adamc@13 47
adamc@623 48 val liftKindInKind =
adamc@623 49 U.Kind.mapB {kind = fn bound => fn k =>
adamc@623 50 case k of
adamc@623 51 KRel xn =>
adamc@623 52 if xn < bound then
adamc@623 53 k
adamc@623 54 else
adamc@623 55 KRel (xn + 1)
adamc@623 56 | _ => k,
adamc@623 57 bind = fn (bound, _) => bound + 1}
adamc@623 58
adamc@623 59 val liftKindInCon =
adamc@623 60 U.Con.mapB {kind = fn bound => fn k =>
adamc@623 61 case k of
adamc@623 62 KRel xn =>
adamc@623 63 if xn < bound then
adamc@623 64 k
adamc@623 65 else
adamc@623 66 KRel (xn + 1)
adamc@623 67 | _ => k,
adamc@623 68 con = fn _ => fn c => c,
adamc@623 69 bind = fn (bound, U.Con.RelK _) => bound + 1
adamc@623 70 | (bound, _) => bound}
adamc@623 71
adamc@13 72 val liftConInCon =
adamc@623 73 U.Con.mapB {kind = fn _ => fn k => k,
adamc@13 74 con = fn bound => fn c =>
adamc@13 75 case c of
adamc@16 76 CRel xn =>
adamc@13 77 if xn < bound then
adamc@13 78 c
adamc@13 79 else
adamc@16 80 CRel (xn + 1)
adamc@17 81 (*| CUnif _ => raise SynUnif*)
adamc@13 82 | _ => c,
adamc@623 83 bind = fn (bound, U.Con.RelC _) => bound + 1
adamc@13 84 | (bound, _) => bound}
adamc@13 85
adamc@13 86 val lift = liftConInCon 0
adamc@13 87
adamc@623 88 val liftKindInExp =
adamc@623 89 U.Exp.mapB {kind = fn bound => fn k =>
adamc@623 90 case k of
adamc@623 91 KRel xn =>
adamc@623 92 if xn < bound then
adamc@623 93 k
adamc@623 94 else
adamc@623 95 KRel (xn + 1)
adamc@623 96 | _ => k,
adamc@623 97 con = fn _ => fn c => c,
adamc@623 98 exp = fn _ => fn e => e,
adamc@623 99 bind = fn (bound, U.Exp.RelK _) => bound + 1
adamc@623 100 | (bound, _) => bound}
adamc@623 101
adamc@448 102 val liftConInExp =
adamc@623 103 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@448 104 con = fn bound => fn c =>
adamc@448 105 case c of
adamc@448 106 CRel xn =>
adamc@448 107 if xn < bound then
adamc@448 108 c
adamc@448 109 else
adamc@448 110 CRel (xn + 1)
adamc@448 111 | _ => c,
adamc@448 112 exp = fn _ => fn e => e,
adamc@448 113 bind = fn (bound, U.Exp.RelC _) => bound + 1
adamc@448 114 | (bound, _) => bound}
adamc@448 115
adamc@211 116 val liftExpInExp =
adamc@623 117 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@211 118 con = fn _ => fn c => c,
adamc@211 119 exp = fn bound => fn e =>
adamc@211 120 case e of
adamc@211 121 ERel xn =>
adamc@211 122 if xn < bound then
adamc@211 123 e
adamc@211 124 else
adamc@211 125 ERel (xn + 1)
adamc@211 126 | _ => e,
adamc@211 127 bind = fn (bound, U.Exp.RelE _) => bound + 1
adamc@211 128 | (bound, _) => bound}
adamc@211 129
adamc@211 130
adamc@211 131 val liftExp = liftExpInExp 0
adamc@13 132
adamc@448 133 val subExpInExp =
adamc@623 134 U.Exp.mapB {kind = fn _ => fn k => k,
adamc@448 135 con = fn _ => fn c => c,
adamc@448 136 exp = fn (xn, rep) => fn e =>
adamc@448 137 case e of
adamc@448 138 ERel xn' =>
adamc@448 139 (case Int.compare (xn', xn) of
adamc@448 140 EQUAL => #1 rep
adamc@448 141 | GREATER=> ERel (xn' - 1)
adamc@448 142 | LESS => e)
adamc@448 143 | _ => e,
adamc@448 144 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
adamc@448 145 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
adamc@448 146 | (ctx, _) => ctx}
adamc@448 147
adamc@13 148 (* Back to environments *)
adamc@13 149
adamc@9 150 datatype 'a var' =
adamc@9 151 Rel' of int * 'a
adamc@9 152 | Named' of int * 'a
adamc@2 153
adamc@9 154 datatype 'a var =
adamc@9 155 NotBound
adamc@9 156 | Rel of int * 'a
adamc@9 157 | Named of int * 'a
adamc@2 158
adamc@191 159 type datatyp = string list * (string * con option) IM.map
adamc@157 160
adamc@211 161 datatype class_name =
adamc@211 162 ClNamed of int
adamc@211 163 | ClProj of int * string list * string
adamc@211 164
adamc@216 165 fun cn2s cn =
adamc@216 166 case cn of
adamc@216 167 ClNamed n => "Named(" ^ Int.toString n ^ ")"
adamc@216 168 | ClProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
adamc@216 169
adamc@211 170 structure CK = struct
adamc@211 171 type ord_key = class_name
adamc@211 172 open Order
adamc@211 173 fun compare x =
adamc@211 174 case x of
adamc@211 175 (ClNamed n1, ClNamed n2) => Int.compare (n1, n2)
adamc@211 176 | (ClNamed _, _) => LESS
adamc@211 177 | (_, ClNamed _) => GREATER
adamc@211 178
adamc@211 179 | (ClProj (m1, ms1, x1), ClProj (m2, ms2, x2)) =>
adamc@211 180 join (Int.compare (m1, m2),
adamc@211 181 fn () => join (joinL String.compare (ms1, ms2),
adamc@211 182 fn () => String.compare (x1, x2)))
adamc@211 183 end
adamc@211 184
adamc@211 185 structure CM = BinaryMapFn(CK)
adamc@211 186
adamc@211 187 datatype class_key =
adamc@211 188 CkNamed of int
adamc@211 189 | CkRel of int
adamc@211 190 | CkProj of int * string list * string
adamc@467 191 | CkApp of class_key * class_key
adamc@211 192
adamc@216 193 fun ck2s ck =
adamc@216 194 case ck of
adamc@216 195 CkNamed n => "Named(" ^ Int.toString n ^ ")"
adamc@216 196 | CkRel n => "Rel(" ^ Int.toString n ^ ")"
adamc@216 197 | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")"
adamc@467 198 | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")"
adamc@216 199
adamc@674 200 type class_key_n = class_key * int
adamc@674 201
adamc@674 202 fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]"
adamc@674 203
adamc@216 204 fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")"
adamc@216 205
adamc@211 206 structure KK = struct
adamc@674 207 type ord_key = class_key_n
adamc@211 208 open Order
adamc@674 209 fun compare' x =
adamc@211 210 case x of
adamc@211 211 (CkNamed n1, CkNamed n2) => Int.compare (n1, n2)
adamc@211 212 | (CkNamed _, _) => LESS
adamc@211 213 | (_, CkNamed _) => GREATER
adamc@211 214
adamc@211 215 | (CkRel n1, CkRel n2) => Int.compare (n1, n2)
adamc@211 216 | (CkRel _, _) => LESS
adamc@211 217 | (_, CkRel _) => GREATER
adamc@211 218
adamc@211 219 | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) =>
adamc@211 220 join (Int.compare (m1, m2),
adamc@211 221 fn () => join (joinL String.compare (ms1, ms2),
adamc@211 222 fn () => String.compare (x1, x2)))
adamc@467 223 | (CkProj _, _) => LESS
adamc@467 224 | (_, CkProj _) => GREATER
adamc@467 225
adamc@467 226 | (CkApp (f1, x1), CkApp (f2, x2)) =>
adamc@674 227 join (compare' (f1, f2),
adamc@674 228 fn () => compare' (x1, x2))
adamc@674 229 fun compare ((k1, n1), (k2, n2)) =
adamc@674 230 join (Int.compare (n1, n2),
adamc@674 231 fn () => compare' (k1, k2))
adamc@211 232 end
adamc@211 233
adamc@211 234 structure KM = BinaryMapFn(KK)
adamc@211 235
adamc@674 236 type class = ((class_name * class_key) list * exp) KM.map
adamc@674 237 val empty_class = KM.empty
adamc@211 238
adamc@419 239 fun printClasses cs = (print "Classes:\n";
adamc@674 240 CM.appi (fn (cn, km) =>
adamc@419 241 (print (cn2s cn ^ ":");
adamc@674 242 KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km;
adamc@419 243 print "\n")) cs)
adamc@216 244
adamc@2 245 type env = {
adamc@623 246 renameK : int SM.map,
adamc@623 247 relK : string list,
adamc@623 248
adamc@9 249 renameC : kind var' SM.map,
adamc@2 250 relC : (string * kind) list,
adamc@11 251 namedC : (string * kind * con option) IM.map,
adamc@9 252
adamc@157 253 datatypes : datatyp IM.map,
adamc@191 254 constructors : (datatype_kind * int * string list * con option * int) SM.map,
adamc@157 255
adamc@211 256 classes : class CM.map,
adamc@211 257
adamc@9 258 renameE : con var' SM.map,
adamc@9 259 relE : (string * con) list,
adamc@31 260 namedE : (string * con) IM.map,
adamc@31 261
adamc@31 262 renameSgn : (int * sgn) SM.map,
adamc@31 263 sgn : (string * sgn) IM.map,
adamc@31 264
adamc@31 265 renameStr : (int * sgn) SM.map,
adamc@31 266 str : (string * sgn) IM.map
adamc@2 267 }
adamc@2 268
adamc@2 269 val namedCounter = ref 0
adamc@2 270
adamc@109 271 fun newNamed () =
adamc@109 272 let
adamc@109 273 val r = !namedCounter
adamc@109 274 in
adamc@109 275 namedCounter := r + 1;
adamc@109 276 r
adamc@109 277 end
adamc@109 278
adamc@2 279 val empty = {
adamc@623 280 renameK = SM.empty,
adamc@623 281 relK = [],
adamc@623 282
adamc@2 283 renameC = SM.empty,
adamc@2 284 relC = [],
adamc@9 285 namedC = IM.empty,
adamc@9 286
adamc@157 287 datatypes = IM.empty,
adamc@171 288 constructors = SM.empty,
adamc@157 289
adamc@211 290 classes = CM.empty,
adamc@211 291
adamc@9 292 renameE = SM.empty,
adamc@9 293 relE = [],
adamc@31 294 namedE = IM.empty,
adamc@31 295
adamc@31 296 renameSgn = SM.empty,
adamc@31 297 sgn = IM.empty,
adamc@31 298
adamc@31 299 renameStr = SM.empty,
adamc@31 300 str = IM.empty
adamc@2 301 }
adamc@2 302
adamc@674 303 fun liftClassKey' ck =
adamc@211 304 case ck of
adamc@211 305 CkNamed _ => ck
adamc@211 306 | CkRel n => CkRel (n + 1)
adamc@211 307 | CkProj _ => ck
adamc@674 308 | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2)
adamc@674 309
adamc@674 310 fun liftClassKey (ck, n) = (liftClassKey' ck, n)
adamc@211 311
adamc@623 312 fun pushKRel (env : env) x =
adamc@623 313 let
adamc@623 314 val renameK = SM.map (fn n => n+1) (#renameK env)
adamc@623 315 in
adamc@623 316 {renameK = SM.insert (renameK, x, 0),
adamc@623 317 relK = x :: #relK env,
adamc@623 318
adamc@623 319 renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k)
adamc@623 320 | x => x) (#renameC env),
adamc@623 321 relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
adamc@623 322 namedC = #namedC env,
adamc@623 323
adamc@623 324 datatypes = #datatypes env,
adamc@623 325 constructors = #constructors env,
adamc@623 326
adamc@623 327 classes = #classes env,
adamc@623 328
adamc@623 329 renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
adamc@623 330 | Named' (n, c) => Named' (n, c)) (#renameE env),
adamc@623 331 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
adamc@623 332 namedE = #namedE env,
adamc@623 333
adamc@623 334 renameSgn = #renameSgn env,
adamc@623 335 sgn = #sgn env,
adamc@623 336
adamc@623 337 renameStr = #renameStr env,
adamc@623 338 str = #str env
adamc@623 339 }
adamc@623 340 end
adamc@623 341
adamc@623 342 fun lookupKRel (env : env) n =
adamc@623 343 (List.nth (#relK env, n))
adamc@623 344 handle Subscript => raise UnboundRel n
adamc@623 345
adamc@623 346 fun lookupK (env : env) x = SM.find (#renameK env, x)
adamc@623 347
adamc@2 348 fun pushCRel (env : env) x k =
adamc@2 349 let
adamc@9 350 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
adamc@2 351 | x => x) (#renameC env)
adamc@2 352 in
adamc@623 353 {renameK = #renameK env,
adamc@623 354 relK = #relK env,
adamc@623 355
adamc@623 356 renameC = SM.insert (renameC, x, Rel' (0, k)),
adamc@2 357 relC = (x, k) :: #relC env,
adamc@514 358 namedC = #namedC env,
adamc@9 359
adamc@157 360 datatypes = #datatypes env,
adamc@171 361 constructors = #constructors env,
adamc@157 362
adamc@674 363 classes = CM.map (fn class =>
adamc@674 364 KM.foldli (fn (ck, e, km) =>
adamc@674 365 KM.insert (km, liftClassKey ck, e))
adamc@674 366 KM.empty class)
adamc@211 367 (#classes env),
adamc@211 368
adamc@328 369 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
adamc@517 370 | Named' (n, c) => Named' (n, c)) (#renameE env),
adamc@13 371 relE = map (fn (x, c) => (x, lift c)) (#relE env),
adamc@514 372 namedE = #namedE env,
adamc@31 373
adamc@31 374 renameSgn = #renameSgn env,
adamc@31 375 sgn = #sgn env,
adamc@31 376
adamc@31 377 renameStr = #renameStr env,
adamc@31 378 str = #str env
adamc@31 379 }
adamc@2 380 end
adamc@2 381
adamc@2 382 fun lookupCRel (env : env) n =
adamc@2 383 (List.nth (#relC env, n))
adamc@2 384 handle Subscript => raise UnboundRel n
adamc@2 385
adamc@11 386 fun pushCNamedAs (env : env) x n k co =
adamc@623 387 {renameK = #renameK env,
adamc@623 388 relK = #relK env,
adamc@623 389
adamc@623 390 renameC = SM.insert (#renameC env, x, Named' (n, k)),
adamc@5 391 relC = #relC env,
adamc@11 392 namedC = IM.insert (#namedC env, n, (x, k, co)),
adamc@9 393
adamc@157 394 datatypes = #datatypes env,
adamc@171 395 constructors = #constructors env,
adamc@157 396
adamc@211 397 classes = #classes env,
adamc@211 398
adamc@9 399 renameE = #renameE env,
adamc@9 400 relE = #relE env,
adamc@31 401 namedE = #namedE env,
adamc@31 402
adamc@31 403 renameSgn = #renameSgn env,
adamc@31 404 sgn = #sgn env,
adamc@31 405
adamc@31 406 renameStr = #renameStr env,
adamc@31 407 str = #str env}
adamc@5 408
adamc@11 409 fun pushCNamed env x k co =
adamc@2 410 let
adamc@2 411 val n = !namedCounter
adamc@2 412 in
adamc@2 413 namedCounter := n + 1;
adamc@11 414 (pushCNamedAs env x n k co, n)
adamc@2 415 end
adamc@2 416
adamc@2 417 fun lookupCNamed (env : env) n =
adamc@2 418 case IM.find (#namedC env, n) of
adamc@2 419 NONE => raise UnboundNamed n
adamc@2 420 | SOME x => x
adamc@2 421
adamc@2 422 fun lookupC (env : env) x =
adamc@2 423 case SM.find (#renameC env, x) of
adamc@9 424 NONE => NotBound
adamc@9 425 | SOME (Rel' x) => Rel x
adamc@9 426 | SOME (Named' x) => Named x
adamc@9 427
adamc@191 428 fun pushDatatype (env : env) n xs xncs =
adamc@188 429 let
adamc@188 430 val dk = U.classifyDatatype xncs
adamc@188 431 in
adamc@623 432 {renameK = #renameK env,
adamc@623 433 relK = #relK env,
adamc@623 434
adamc@623 435 renameC = #renameC env,
adamc@188 436 relC = #relC env,
adamc@188 437 namedC = #namedC env,
adamc@157 438
adamc@188 439 datatypes = IM.insert (#datatypes env, n,
adamc@191 440 (xs, foldl (fn ((x, n, to), cons) =>
adamc@191 441 IM.insert (cons, n, (x, to))) IM.empty xncs)),
adamc@188 442 constructors = foldl (fn ((x, n', to), cmap) =>
adamc@191 443 SM.insert (cmap, x, (dk, n', xs, to, n)))
adamc@188 444 (#constructors env) xncs,
adamc@157 445
adamc@211 446 classes = #classes env,
adamc@211 447
adamc@188 448 renameE = #renameE env,
adamc@188 449 relE = #relE env,
adamc@188 450 namedE = #namedE env,
adamc@157 451
adamc@188 452 renameSgn = #renameSgn env,
adamc@188 453 sgn = #sgn env,
adamc@157 454
adamc@188 455 renameStr = #renameStr env,
adamc@188 456 str = #str env}
adamc@188 457 end
adamc@157 458
adamc@157 459 fun lookupDatatype (env : env) n =
adamc@157 460 case IM.find (#datatypes env, n) of
adamc@157 461 NONE => raise UnboundNamed n
adamc@157 462 | SOME x => x
adamc@157 463
adamc@191 464 fun lookupDatatypeConstructor (_, dt) n =
adamc@157 465 case IM.find (dt, n) of
adamc@157 466 NONE => raise UnboundNamed n
adamc@157 467 | SOME x => x
adamc@157 468
adamc@171 469 fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
adamc@171 470
adamc@191 471 fun datatypeArgs (xs, _) = xs
adamc@191 472 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
adamc@157 473
adamc@211 474 fun pushClass (env : env) n =
adamc@623 475 {renameK = #renameK env,
adamc@623 476 relK = #relK env,
adamc@623 477
adamc@623 478 renameC = #renameC env,
adamc@211 479 relC = #relC env,
adamc@211 480 namedC = #namedC env,
adamc@211 481
adamc@211 482 datatypes = #datatypes env,
adamc@211 483 constructors = #constructors env,
adamc@211 484
adamc@674 485 classes = CM.insert (#classes env, ClNamed n, KM.empty),
adamc@211 486
adamc@211 487 renameE = #renameE env,
adamc@211 488 relE = #relE env,
adamc@211 489 namedE = #namedE env,
adamc@211 490
adamc@211 491 renameSgn = #renameSgn env,
adamc@211 492 sgn = #sgn env,
adamc@211 493
adamc@211 494 renameStr = #renameStr env,
adamc@403 495 str = #str env}
adamc@211 496
adamc@211 497 fun class_name_in (c, _) =
adamc@211 498 case c of
adamc@211 499 CNamed n => SOME (ClNamed n)
adamc@211 500 | CModProj x => SOME (ClProj x)
adamc@228 501 | CUnif (_, _, _, ref (SOME c)) => class_name_in c
adamc@211 502 | _ => NONE
adamc@211 503
adamc@403 504 fun isClass (env : env) c =
adamc@403 505 let
adamc@403 506 fun find NONE = false
adamc@403 507 | find (SOME c) = Option.isSome (CM.find (#classes env, c))
adamc@403 508 in
adamc@403 509 find (class_name_in c)
adamc@403 510 end
adamc@403 511
adamc@211 512 fun class_key_in (c, _) =
adamc@211 513 case c of
adamc@211 514 CRel n => SOME (CkRel n)
adamc@211 515 | CNamed n => SOME (CkNamed n)
adamc@211 516 | CModProj x => SOME (CkProj x)
adamc@228 517 | CUnif (_, _, _, ref (SOME c)) => class_key_in c
adamc@467 518 | CApp (c1, c2) =>
adamc@467 519 (case (class_key_in c1, class_key_in c2) of
adamc@467 520 (SOME k1, SOME k2) => SOME (CkApp (k1, k2))
adamc@467 521 | _ => NONE)
adamc@211 522 | _ => NONE
adamc@211 523
adamc@674 524 fun class_key_out loc =
adamc@674 525 let
adamc@674 526 fun cko k =
adamc@674 527 case k of
adamc@674 528 CkRel n => (CRel n, loc)
adamc@674 529 | CkNamed n => (CNamed n, loc)
adamc@674 530 | CkProj x => (CModProj x, loc)
adamc@674 531 | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc)
adamc@674 532 in
adamc@674 533 cko
adamc@674 534 end
adamc@674 535
adamc@211 536 fun class_pair_in (c, _) =
adamc@211 537 case c of
adamc@211 538 CApp (f, x) =>
adamc@211 539 (case (class_name_in f, class_key_in x) of
adamc@211 540 (SOME f, SOME x) => SOME (f, x)
adamc@211 541 | _ => NONE)
adamc@452 542 | CUnif (_, _, _, ref (SOME c)) => class_pair_in c
adamc@211 543 | _ => NONE
adamc@211 544
adamc@674 545 fun sub_class_key (n, c) =
adamc@674 546 let
adamc@674 547 fun csk k =
adamc@674 548 case k of
adamc@674 549 CkRel n' => if n' = n then
adamc@674 550 c
adamc@674 551 else
adamc@674 552 k
adamc@674 553 | CkNamed _ => k
adamc@674 554 | CkProj _ => k
adamc@674 555 | CkApp (k1, k2) => CkApp (csk k1, csk k2)
adamc@674 556 in
adamc@674 557 csk
adamc@674 558 end
adamc@674 559
adamc@211 560 fun resolveClass (env : env) c =
adamc@674 561 let
adamc@674 562 fun doPair (f, x) =
adamc@674 563 case CM.find (#classes env, f) of
adamc@674 564 NONE => NONE
adamc@674 565 | SOME class =>
adamc@674 566 let
adamc@674 567 val loc = #2 c
adamc@674 568
adamc@674 569 fun tryRules (k, args) =
adamc@674 570 let
adamc@674 571 val len = length args
adamc@674 572 in
adamc@674 573 case KM.find (class, (k, length args)) of
adamc@674 574 SOME (cs, e) =>
adamc@674 575 let
adamc@674 576 val es = map (fn (cn, ck) =>
adamc@674 577 let
adamc@674 578 val ck = ListUtil.foldli (fn (i, arg, ck) =>
adamc@674 579 sub_class_key (len - i - 1,
adamc@674 580 arg)
adamc@674 581 ck)
adamc@674 582 ck args
adamc@674 583 in
adamc@674 584 doPair (cn, ck)
adamc@674 585 end) cs
adamc@674 586 in
adamc@674 587 if List.exists (not o Option.isSome) es then
adamc@674 588 NONE
adamc@674 589 else
adamc@674 590 let
adamc@674 591 val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc))
adamc@674 592 e args
adamc@674 593 val e = foldr (fn (pf, e) => (EApp (e, pf), loc))
adamc@674 594 e (List.mapPartial (fn x => x) es)
adamc@674 595 in
adamc@674 596 SOME e
adamc@674 597 end
adamc@674 598 end
adamc@674 599 | NONE =>
adamc@674 600 case k of
adamc@674 601 CkApp (k1, k2) => tryRules (k1, k2 :: args)
adamc@674 602 | _ => NONE
adamc@674 603 end
adamc@674 604 in
adamc@674 605 tryRules (x, [])
adamc@674 606 end
adamc@674 607 in
adamc@674 608 case class_pair_in c of
adamc@674 609 SOME p => doPair p
adamc@674 610 | _ => NONE
adamc@674 611 end
adamc@211 612
adamc@9 613 fun pushERel (env : env) x t =
adamc@9 614 let
adamc@9 615 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
adamc@9 616 | x => x) (#renameE env)
adamc@211 617
adamc@674 618 val classes = CM.map (KM.map (fn (ps, e) => (ps, liftExp e))) (#classes env)
adamc@211 619 val classes = case class_pair_in t of
adamc@211 620 NONE => classes
adamc@211 621 | SOME (f, x) =>
adamc@403 622 case CM.find (classes, f) of
adamc@403 623 NONE => classes
adamc@403 624 | SOME class =>
adamc@403 625 let
adamc@674 626 val class = KM.insert (class, (x, 0), ([], (ERel 0, #2 t)))
adamc@403 627 in
adamc@403 628 CM.insert (classes, f, class)
adamc@403 629 end
adamc@9 630 in
adamc@623 631 {renameK = #renameK env,
adamc@623 632 relK = #relK env,
adamc@623 633
adamc@623 634 renameC = #renameC env,
adamc@9 635 relC = #relC env,
adamc@9 636 namedC = #namedC env,
adamc@9 637
adamc@157 638 datatypes = #datatypes env,
adamc@171 639 constructors = #constructors env,
adamc@157 640
adamc@211 641 classes = classes,
adamc@211 642
adamc@9 643 renameE = SM.insert (renameE, x, Rel' (0, t)),
adamc@9 644 relE = (x, t) :: #relE env,
adamc@31 645 namedE = #namedE env,
adamc@31 646
adamc@31 647 renameSgn = #renameSgn env,
adamc@31 648 sgn = #sgn env,
adamc@31 649
adamc@31 650 renameStr = #renameStr env,
adamc@31 651 str = #str env}
adamc@9 652 end
adamc@9 653
adamc@9 654 fun lookupERel (env : env) n =
adamc@9 655 (List.nth (#relE env, n))
adamc@9 656 handle Subscript => raise UnboundRel n
adamc@9 657
adamc@674 658 fun rule_in c =
adamc@674 659 let
adamc@674 660 fun quantifiers (c, nvars) =
adamc@674 661 case #1 c of
adamc@674 662 TCFun (_, _, _, c) => quantifiers (c, nvars + 1)
adamc@674 663 | _ =>
adamc@674 664 let
adamc@674 665 fun clauses (c, hyps) =
adamc@674 666 case #1 c of
adamc@674 667 TFun (hyp, c) =>
adamc@674 668 (case class_pair_in hyp of
adamc@674 669 NONE => NONE
adamc@674 670 | SOME p => clauses (c, p :: hyps))
adamc@674 671 | _ =>
adamc@674 672 case class_pair_in c of
adamc@674 673 NONE => NONE
adamc@674 674 | SOME (cn, ck) =>
adamc@674 675 let
adamc@674 676 fun dearg (ck, i) =
adamc@674 677 if i >= nvars then
adamc@674 678 SOME (nvars, hyps, (cn, ck))
adamc@674 679 else case ck of
adamc@674 680 CkApp (ck, CkRel i') =>
adamc@674 681 if i' = i then
adamc@674 682 dearg (ck, i + 1)
adamc@674 683 else
adamc@674 684 NONE
adamc@674 685 | _ => NONE
adamc@674 686 in
adamc@674 687 dearg (ck, 0)
adamc@674 688 end
adamc@674 689 in
adamc@674 690 clauses (c, [])
adamc@674 691 end
adamc@674 692 in
adamc@674 693 quantifiers (c, 0)
adamc@674 694 end
adamc@674 695
adamc@9 696 fun pushENamedAs (env : env) x n t =
adamc@211 697 let
adamc@211 698 val classes = #classes env
adamc@674 699 val classes = case rule_in t of
adamc@211 700 NONE => classes
adamc@674 701 | SOME (nvars, hyps, (f, x)) =>
adamc@403 702 case CM.find (classes, f) of
adamc@403 703 NONE => classes
adamc@403 704 | SOME class =>
adamc@403 705 let
adamc@674 706 val class = KM.insert (class, (x, nvars), (hyps, (ENamed n, #2 t)))
adamc@403 707 in
adamc@403 708 CM.insert (classes, f, class)
adamc@403 709 end
adamc@211 710 in
adamc@623 711 {renameK = #renameK env,
adamc@623 712 relK = #relK env,
adamc@623 713
adamc@623 714 renameC = #renameC env,
adamc@211 715 relC = #relC env,
adamc@211 716 namedC = #namedC env,
adamc@9 717
adamc@211 718 datatypes = #datatypes env,
adamc@211 719 constructors = #constructors env,
adamc@157 720
adamc@211 721 classes = classes,
adamc@31 722
adamc@211 723 renameE = SM.insert (#renameE env, x, Named' (n, t)),
adamc@211 724 relE = #relE env,
adamc@211 725 namedE = IM.insert (#namedE env, n, (x, t)),
adamc@211 726
adamc@211 727 renameSgn = #renameSgn env,
adamc@211 728 sgn = #sgn env,
adamc@211 729
adamc@211 730 renameStr = #renameStr env,
adamc@211 731 str = #str env}
adamc@211 732 end
adamc@9 733
adamc@9 734 fun pushENamed env x t =
adamc@9 735 let
adamc@9 736 val n = !namedCounter
adamc@9 737 in
adamc@9 738 namedCounter := n + 1;
adamc@9 739 (pushENamedAs env x n t, n)
adamc@9 740 end
adamc@9 741
adamc@9 742 fun lookupENamed (env : env) n =
adamc@9 743 case IM.find (#namedE env, n) of
adamc@9 744 NONE => raise UnboundNamed n
adamc@9 745 | SOME x => x
adamc@9 746
adamc@471 747 fun checkENamed (env : env) n =
adamc@471 748 Option.isSome (IM.find (#namedE env, n))
adamc@471 749
adamc@9 750 fun lookupE (env : env) x =
adamc@9 751 case SM.find (#renameE env, x) of
adamc@9 752 NONE => NotBound
adamc@9 753 | SOME (Rel' x) => Rel x
adamc@9 754 | SOME (Named' x) => Named x
adamc@2 755
adamc@31 756 fun pushSgnNamedAs (env : env) x n sgis =
adamc@623 757 {renameK = #renameK env,
adamc@623 758 relK = #relK env,
adamc@623 759
adamc@623 760 renameC = #renameC env,
adamc@31 761 relC = #relC env,
adamc@31 762 namedC = #namedC env,
adamc@31 763
adamc@157 764 datatypes = #datatypes env,
adamc@171 765 constructors = #constructors env,
adamc@157 766
adamc@211 767 classes = #classes env,
adamc@211 768
adamc@31 769 renameE = #renameE env,
adamc@31 770 relE = #relE env,
adamc@31 771 namedE = #namedE env,
adamc@31 772
adamc@31 773 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
adamc@31 774 sgn = IM.insert (#sgn env, n, (x, sgis)),
adamc@31 775
adamc@31 776 renameStr = #renameStr env,
adamc@31 777 str = #str env}
adamc@31 778
adamc@31 779 fun pushSgnNamed env x sgis =
adamc@31 780 let
adamc@31 781 val n = !namedCounter
adamc@31 782 in
adamc@31 783 namedCounter := n + 1;
adamc@31 784 (pushSgnNamedAs env x n sgis, n)
adamc@31 785 end
adamc@31 786
adamc@31 787 fun lookupSgnNamed (env : env) n =
adamc@31 788 case IM.find (#sgn env, n) of
adamc@31 789 NONE => raise UnboundNamed n
adamc@31 790 | SOME x => x
adamc@31 791
adamc@31 792 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
adamc@31 793
adamc@31 794 fun lookupStrNamed (env : env) n =
adamc@31 795 case IM.find (#str env, n) of
adamc@31 796 NONE => raise UnboundNamed n
adamc@31 797 | SOME x => x
adamc@31 798
adamc@31 799 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
adamc@31 800
adamc@203 801
adamc@216 802 fun sgiSeek (sgi, (sgns, strs, cons)) =
adamc@216 803 case sgi of
adamc@216 804 SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@216 805 | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@216 806 | SgiDatatype (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@216 807 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@216 808 | SgiVal _ => (sgns, strs, cons)
adamc@216 809 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
adamc@216 810 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
adamc@216 811 | SgiConstraint _ => (sgns, strs, cons)
adamc@563 812 | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@563 813 | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@216 814
adamc@34 815 fun sgnSeek f sgis =
adamc@34 816 let
adamc@59 817 fun seek (sgis, sgns, strs, cons) =
adamc@34 818 case sgis of
adamc@34 819 [] => NONE
adamc@34 820 | (sgi, _) :: sgis =>
adamc@34 821 case f sgi of
adamc@158 822 SOME v =>
adamc@158 823 let
adamc@158 824 val cons =
adamc@158 825 case sgi of
adamc@191 826 SgiDatatype (x, n, _, _) => IM.insert (cons, n, x)
adamc@191 827 | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
adamc@158 828 | _ => cons
adamc@158 829 in
adamc@158 830 SOME (v, (sgns, strs, cons))
adamc@158 831 end
adamc@88 832 | NONE =>
adamc@216 833 let
adamc@216 834 val (sgns, strs, cons) = sgiSeek (sgi, (sgns, strs, cons))
adamc@216 835 in
adamc@216 836 seek (sgis, sgns, strs, cons)
adamc@216 837 end
adamc@34 838 in
adamc@59 839 seek (sgis, IM.empty, IM.empty, IM.empty)
adamc@34 840 end
adamc@34 841
adamc@34 842 fun id x = x
adamc@34 843
adamc@34 844 fun unravelStr (str, _) =
adamc@34 845 case str of
adamc@34 846 StrVar x => (x, [])
adamc@34 847 | StrProj (str, m) =>
adamc@34 848 let
adamc@34 849 val (x, ms) = unravelStr str
adamc@34 850 in
adamc@34 851 (x, ms @ [m])
adamc@34 852 end
adamc@34 853 | _ => raise Fail "unravelStr"
adamc@34 854
adamc@59 855 fun sgnS_con (str, (sgns, strs, cons)) c =
adamc@34 856 case c of
adamc@34 857 CModProj (m1, ms, x) =>
adamc@34 858 (case IM.find (strs, m1) of
adamc@34 859 NONE => c
adamc@34 860 | SOME m1x =>
adamc@34 861 let
adamc@34 862 val (m1, ms') = unravelStr str
adamc@34 863 in
adamc@34 864 CModProj (m1, ms' @ m1x :: ms, x)
adamc@34 865 end)
adamc@34 866 | CNamed n =>
adamc@34 867 (case IM.find (cons, n) of
adamc@34 868 NONE => c
adamc@34 869 | SOME nx =>
adamc@34 870 let
adamc@34 871 val (m1, ms) = unravelStr str
adamc@34 872 in
adamc@34 873 CModProj (m1, ms, nx)
adamc@34 874 end)
adamc@34 875 | _ => c
adamc@34 876
adamc@467 877 fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c =
adamc@216 878 case c of
adamc@216 879 CModProj (m1, ms, x) =>
adamc@216 880 (case IM.find (strs, m1) of
adamc@216 881 NONE => c
adamc@216 882 | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x))
adamc@216 883 | CNamed n =>
adamc@216 884 (case IM.find (cons, n) of
adamc@216 885 NONE => c
adamc@216 886 | SOME nx => CModProj (m1, ms', nx))
adamc@467 887 | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1),
adamc@467 888 (sgnS_con' arg (#1 c2), #2 c2))
adamc@216 889 | _ => c
adamc@216 890
adamc@674 891 fun sgnS_class_name (arg as (m1, ms', (sgns, strs, cons))) nm =
adamc@674 892 case nm of
adamc@674 893 ClProj (m1, ms, x) =>
adamc@674 894 (case IM.find (strs, m1) of
adamc@674 895 NONE => nm
adamc@674 896 | SOME m1x => ClProj (m1, ms' @ m1x :: ms, x))
adamc@674 897 | ClNamed n =>
adamc@674 898 (case IM.find (cons, n) of
adamc@674 899 NONE => nm
adamc@674 900 | SOME nx => ClProj (m1, ms', nx))
adamc@674 901
adamc@674 902 fun sgnS_class_key (arg as (m1, ms', (sgns, strs, cons))) k =
adamc@674 903 case k of
adamc@674 904 CkProj (m1, ms, x) =>
adamc@674 905 (case IM.find (strs, m1) of
adamc@674 906 NONE => k
adamc@674 907 | SOME m1x => CkProj (m1, ms' @ m1x :: ms, x))
adamc@674 908 | CkNamed n =>
adamc@674 909 (case IM.find (cons, n) of
adamc@674 910 NONE => k
adamc@674 911 | SOME nx => CkProj (m1, ms', nx))
adamc@674 912 | CkApp (k1, k2) => CkApp (sgnS_class_key arg k1,
adamc@674 913 sgnS_class_key arg k2)
adamc@674 914 | _ => k
adamc@674 915
adamc@59 916 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
adamc@59 917 case sgn of
adamc@59 918 SgnProj (m1, ms, x) =>
adamc@59 919 (case IM.find (strs, m1) of
adamc@59 920 NONE => sgn
adamc@59 921 | SOME m1x =>
adamc@59 922 let
adamc@59 923 val (m1, ms') = unravelStr str
adamc@59 924 in
adamc@59 925 SgnProj (m1, ms' @ m1x :: ms, x)
adamc@59 926 end)
adamc@59 927 | SgnVar n =>
adamc@59 928 (case IM.find (sgns, n) of
adamc@59 929 NONE => sgn
adamc@59 930 | SOME nx =>
adamc@59 931 let
adamc@59 932 val (m1, ms) = unravelStr str
adamc@59 933 in
adamc@59 934 SgnProj (m1, ms, nx)
adamc@59 935 end)
adamc@59 936 | _ => sgn
adamc@59 937
adamc@59 938 fun sgnSubSgn x =
adamc@34 939 ElabUtil.Sgn.map {kind = id,
adamc@59 940 con = sgnS_con x,
adamc@34 941 sgn_item = id,
adamc@59 942 sgn = sgnS_sgn x}
adamc@34 943
adamc@211 944
adamc@211 945
adamc@211 946 and projectSgn env {sgn, str, field} =
adamc@211 947 case #1 (hnormSgn env sgn) of
adamc@211 948 SgnConst sgis =>
adamc@211 949 (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
adamc@211 950 NONE => NONE
adamc@211 951 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
adamc@211 952 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
adamc@211 953 | _ => NONE
adamc@211 954
adamc@211 955 and hnormSgn env (all as (sgn, loc)) =
adamc@34 956 case sgn of
adamc@42 957 SgnError => all
adamc@42 958 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
adamc@42 959 | SgnConst _ => all
adamc@42 960 | SgnFun _ => all
adamc@59 961 | SgnProj (m, ms, x) =>
adamc@59 962 let
adamc@59 963 val (_, sgn) = lookupStrNamed env m
adamc@59 964 in
adamc@59 965 case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms,
adamc@59 966 sgn = sgn,
adamc@59 967 field = x} of
adamc@59 968 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
adamc@59 969 | SOME sgn => sgn
adamc@59 970 end
adamc@42 971 | SgnWhere (sgn, x, c) =>
adamc@42 972 case #1 (hnormSgn env sgn) of
adamc@42 973 SgnError => (SgnError, loc)
adamc@42 974 | SgnConst sgis =>
adamc@42 975 let
adamc@42 976 fun traverse (pre, post) =
adamc@42 977 case post of
adamc@42 978 [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
adamc@42 979 | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
adamc@42 980 if x = x' then
adamc@42 981 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
adamc@42 982 else
adamc@42 983 traverse (sgi :: pre, rest)
adamc@42 984 | sgi :: rest => traverse (sgi :: pre, rest)
adamc@42 985
adamc@42 986 val sgis = traverse ([], sgis)
adamc@42 987 in
adamc@42 988 (SgnConst sgis, loc)
adamc@42 989 end
adamc@42 990 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
adamc@42 991
adamc@211 992 fun enrichClasses env classes (m1, ms) sgn =
adamc@59 993 case #1 (hnormSgn env sgn) of
adamc@59 994 SgnConst sgis =>
adamc@211 995 let
adamc@218 996 val (classes, _, _, _) =
adamc@218 997 foldl (fn (sgi, (classes, newClasses, fmap, env)) =>
adamc@211 998 let
adamc@211 999 fun found (x, n) =
adamc@211 1000 (CM.insert (classes,
adamc@211 1001 ClProj (m1, ms, x),
adamc@211 1002 empty_class),
adamc@216 1003 IM.insert (newClasses, n, x),
adamc@218 1004 sgiSeek (#1 sgi, fmap),
adamc@218 1005 env)
adamc@216 1006
adamc@218 1007 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env)
adamc@211 1008 in
adamc@211 1009 case #1 sgi of
adamc@217 1010 SgiStr (x, _, sgn) =>
adamc@217 1011 (enrichClasses env classes (m1, ms @ [x]) sgn,
adamc@217 1012 newClasses,
adamc@218 1013 sgiSeek (#1 sgi, fmap),
adamc@218 1014 env)
adamc@218 1015 | SgiSgn (x, n, sgn) =>
adamc@218 1016 (classes,
adamc@218 1017 newClasses,
adamc@218 1018 fmap,
adamc@218 1019 pushSgnNamedAs env x n sgn)
adamc@218 1020
adamc@563 1021 | SgiClassAbs (x, n, _) => found (x, n)
adamc@563 1022 | SgiClass (x, n, _, _) => found (x, n)
adamc@674 1023 | SgiVal (x, n, c) =>
adamc@674 1024 (case rule_in c of
adamc@674 1025 NONE => default ()
adamc@674 1026 | SOME (nvars, hyps, (cn, a)) =>
adamc@674 1027 let
adamc@674 1028 val globalize = sgnS_class_key (m1, ms, fmap)
adamc@674 1029 val ck = globalize a
adamc@674 1030 val hyps = map (fn (n, k) => (sgnS_class_name (m1, ms, fmap) n,
adamc@674 1031 globalize k)) hyps
adamc@216 1032
adamc@674 1033 fun unravel c =
adamc@674 1034 case c of
adamc@674 1035 ClNamed n =>
adamc@674 1036 ((case lookupCNamed env n of
adamc@674 1037 (_, _, SOME c') =>
adamc@674 1038 (case class_name_in c' of
adamc@674 1039 NONE => c
adamc@674 1040 | SOME k => unravel k)
adamc@674 1041 | _ => c)
adamc@674 1042 handle UnboundNamed _ => c)
adamc@674 1043 | _ => c
adamc@674 1044
adamc@674 1045 val nc =
adamc@674 1046 case cn of
adamc@674 1047 ClNamed f => IM.find (newClasses, f)
adamc@674 1048 | _ => NONE
adamc@674 1049 in
adamc@674 1050 case nc of
adamc@674 1051 NONE =>
adamc@419 1052 let
adamc@419 1053 val classes =
adamc@419 1054 case CM.find (classes, cn) of
adamc@419 1055 NONE => classes
adamc@419 1056 | SOME class =>
adamc@419 1057 let
adamc@674 1058 val class = KM.insert (class, (ck, nvars),
adamc@674 1059 (hyps,
adamc@674 1060 (EModProj (m1, ms, x),
adamc@674 1061 #2 sgn)))
adamc@419 1062 in
adamc@419 1063 CM.insert (classes, cn, class)
adamc@419 1064 end
adamc@419 1065 in
adamc@419 1066 (classes,
adamc@419 1067 newClasses,
adamc@419 1068 fmap,
adamc@419 1069 env)
adamc@419 1070 end
adamc@674 1071 | SOME fx =>
adamc@674 1072 let
adamc@674 1073 val cn = ClProj (m1, ms, fx)
adamc@419 1074
adamc@674 1075 val classes =
adamc@674 1076 case CM.find (classes, cn) of
adamc@674 1077 NONE => classes
adamc@674 1078 | SOME class =>
adamc@674 1079 let
adamc@674 1080 val class = KM.insert (class, (ck, nvars),
adamc@674 1081 (hyps,
adamc@674 1082 (EModProj (m1, ms, x), #2 sgn)))
adamc@674 1083 in
adamc@674 1084 CM.insert (classes, cn, class)
adamc@674 1085 end
adamc@674 1086 in
adamc@674 1087 (classes,
adamc@674 1088 newClasses,
adamc@674 1089 fmap,
adamc@674 1090 env)
adamc@674 1091 end
adamc@674 1092 end)
adamc@216 1093 | _ => default ()
adamc@211 1094 end)
adamc@218 1095 (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis
adamc@211 1096 in
adamc@211 1097 classes
adamc@211 1098 end
adamc@211 1099 | _ => classes
adamc@211 1100
adamc@211 1101 fun pushStrNamedAs (env : env) x n sgn =
adamc@623 1102 {renameK = #renameK env,
adamc@623 1103 relK = #relK env,
adamc@623 1104
adamc@623 1105 renameC = #renameC env,
adamc@211 1106 relC = #relC env,
adamc@211 1107 namedC = #namedC env,
adamc@211 1108
adamc@211 1109 datatypes = #datatypes env,
adamc@211 1110 constructors = #constructors env,
adamc@211 1111
adamc@211 1112 classes = enrichClasses env (#classes env) (n, []) sgn,
adamc@211 1113
adamc@211 1114 renameE = #renameE env,
adamc@211 1115 relE = #relE env,
adamc@211 1116 namedE = #namedE env,
adamc@211 1117
adamc@211 1118 renameSgn = #renameSgn env,
adamc@211 1119 sgn = #sgn env,
adamc@211 1120
adamc@211 1121 renameStr = SM.insert (#renameStr env, x, (n, sgn)),
adamc@211 1122 str = IM.insert (#str env, n, (x, sgn))}
adamc@211 1123
adamc@211 1124 fun pushStrNamed env x sgn =
adamc@211 1125 let
adamc@211 1126 val n = !namedCounter
adamc@211 1127 in
adamc@211 1128 namedCounter := n + 1;
adamc@211 1129 (pushStrNamedAs env x n sgn, n)
adamc@211 1130 end
adamc@211 1131
adamc@211 1132 fun sgiBinds env (sgi, loc) =
adamc@211 1133 case sgi of
adamc@211 1134 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
adamc@211 1135 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@211 1136 | SgiDatatype (x, n, xs, xncs) =>
adamc@211 1137 let
adamc@341 1138 val k = (KType, loc)
adamc@341 1139 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@341 1140
adamc@341 1141 val env = pushCNamedAs env x n k' NONE
adamc@211 1142 in
adamc@211 1143 foldl (fn ((x', n', to), env) =>
adamc@211 1144 let
adamc@211 1145 val t =
adamc@211 1146 case to of
adamc@211 1147 NONE => (CNamed n, loc)
adamc@211 1148 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@211 1149
adamc@211 1150 val k = (KType, loc)
adamc@211 1151 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
adamc@211 1152 in
adamc@211 1153 pushENamedAs env x' n' t
adamc@211 1154 end)
adamc@211 1155 env xncs
adamc@211 1156 end
adamc@211 1157 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@211 1158 let
adamc@341 1159 val k = (KType, loc)
adamc@341 1160 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@341 1161
adamc@341 1162 val env = pushCNamedAs env x n k' (SOME (CModProj (m1, ms, x'), loc))
adamc@211 1163 in
adamc@211 1164 foldl (fn ((x', n', to), env) =>
adamc@211 1165 let
adamc@211 1166 val t =
adamc@211 1167 case to of
adamc@211 1168 NONE => (CNamed n, loc)
adamc@211 1169 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@211 1170
adamc@211 1171 val k = (KType, loc)
adamc@211 1172 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
adamc@211 1173 in
adamc@211 1174 pushENamedAs env x' n' t
adamc@211 1175 end)
adamc@211 1176 env xncs
adamc@211 1177 end
adamc@211 1178 | SgiVal (x, n, t) => pushENamedAs env x n t
adamc@211 1179 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
adamc@211 1180 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
adamc@211 1181 | SgiConstraint _ => env
adamc@211 1182
adamc@563 1183 | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE
adamc@563 1184 | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c)
adamc@459 1185
adamc@211 1186 fun sgnSubCon x =
adamc@211 1187 ElabUtil.Con.map {kind = id,
adamc@211 1188 con = sgnS_con x}
adamc@59 1189
adamc@59 1190 fun projectStr env {sgn, str, field} =
adamc@59 1191 case #1 (hnormSgn env sgn) of
adamc@59 1192 SgnConst sgis =>
adamc@59 1193 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
adamc@59 1194 NONE => NONE
adamc@59 1195 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
adamc@59 1196 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
adamc@59 1197 | _ => NONE
adamc@59 1198
adamc@158 1199 fun chaseMpath env (n, ms) =
adamc@158 1200 let
adamc@158 1201 val (_, sgn) = lookupStrNamed env n
adamc@158 1202 in
adamc@158 1203 foldl (fn (m, (str, sgn)) =>
adamc@158 1204 case projectStr env {sgn = sgn, str = str, field = m} of
adamc@158 1205 NONE => raise Fail "kindof: Unknown substructure"
adamc@158 1206 | SOME sgn => ((StrProj (str, m), #2 sgn), sgn))
adamc@158 1207 ((StrVar n, #2 sgn), sgn) ms
adamc@158 1208 end
adamc@158 1209
adamc@42 1210 fun projectCon env {sgn, str, field} =
adamc@42 1211 case #1 (hnormSgn env sgn) of
adamc@34 1212 SgnConst sgis =>
adamc@34 1213 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
adamc@34 1214 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
adamc@341 1215 | SgiDatatype (x, _, xs, _) =>
adamc@158 1216 if x = field then
adamc@341 1217 let
adamc@341 1218 val k = (KType, #2 sgn)
adamc@341 1219 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
adamc@341 1220 in
adamc@341 1221 SOME (k', NONE)
adamc@341 1222 end
adamc@341 1223 else
adamc@341 1224 NONE
adamc@341 1225 | SgiDatatypeImp (x, _, m1, ms, x', xs, _) =>
adamc@341 1226 if x = field then
adamc@341 1227 let
adamc@341 1228 val k = (KType, #2 sgn)
adamc@341 1229 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
adamc@341 1230 in
adamc@341 1231 SOME (k', SOME (CModProj (m1, ms, x'), #2 sgn))
adamc@341 1232 end
adamc@158 1233 else
adamc@158 1234 NONE
adamc@563 1235 | SgiClassAbs (x, _, k) => if x = field then
adamc@563 1236 SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), NONE)
adamc@563 1237 else
adamc@563 1238 NONE
adamc@563 1239 | SgiClass (x, _, k, c) => if x = field then
adamc@563 1240 SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), SOME c)
adamc@563 1241 else
adamc@563 1242 NONE
adamc@34 1243 | _ => NONE) sgis of
adamc@34 1244 NONE => NONE
adamc@34 1245 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
adamc@34 1246 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
adamc@42 1247 | _ => NONE
adamc@34 1248
adamc@157 1249 fun projectDatatype env {sgn, str, field} =
adamc@157 1250 case #1 (hnormSgn env sgn) of
adamc@157 1251 SgnConst sgis =>
adamc@191 1252 (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
adamc@191 1253 | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
adamc@157 1254 | _ => NONE) sgis of
adamc@157 1255 NONE => NONE
adamc@191 1256 | SOME ((xs, xncs), subs) => SOME (xs,
adamc@191 1257 map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
adamc@157 1258 | _ => NONE
adamc@157 1259
adamc@174 1260 fun projectConstructor env {sgn, str, field} =
adamc@174 1261 case #1 (hnormSgn env sgn) of
adamc@174 1262 SgnConst sgis =>
adamc@174 1263 let
adamc@191 1264 fun consider (n, xs, xncs) =
adamc@174 1265 ListUtil.search (fn (x, n', to) =>
adamc@174 1266 if x <> field then
adamc@174 1267 NONE
adamc@174 1268 else
adamc@191 1269 SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
adamc@174 1270 in
adamc@191 1271 case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs)
adamc@191 1272 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
adamc@174 1273 | _ => NONE) sgis of
adamc@174 1274 NONE => NONE
adamc@191 1275 | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to,
adamc@191 1276 sgnSubCon (str, subs) t)
adamc@174 1277 end
adamc@174 1278 | _ => NONE
adamc@174 1279
adamc@42 1280 fun projectVal env {sgn, str, field} =
adamc@42 1281 case #1 (hnormSgn env sgn) of
adamc@34 1282 SgnConst sgis =>
adamc@162 1283 let
adamc@191 1284 fun seek (n, xs, xncs) =
adamc@162 1285 ListUtil.search (fn (x, _, to) =>
adamc@162 1286 if x = field then
adamc@191 1287 SOME (let
adamc@467 1288 val base = (CNamed n, #2 sgn)
adamc@467 1289 val nxs = length xs
adamc@467 1290 val base = ListUtil.foldli (fn (i, _, base) =>
adamc@467 1291 (CApp (base,
adamc@467 1292 (CRel (nxs - i - 1), #2 sgn)),
adamc@467 1293 #2 sgn))
adamc@467 1294 base xs
adamc@467 1295
adamc@191 1296 val t =
adamc@191 1297 case to of
adamc@467 1298 NONE => base
adamc@467 1299 | SOME t => (TFun (t, base), #2 sgn)
adamc@191 1300 val k = (KType, #2 sgn)
adamc@191 1301 in
adamc@467 1302 foldr (fn (x, t) => (TCFun (Implicit, x, k, t), #2 sgn))
adamc@191 1303 t xs
adamc@191 1304 end)
adamc@162 1305 else
adamc@162 1306 NONE) xncs
adamc@162 1307 in
adamc@162 1308 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
adamc@191 1309 | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs)
adamc@191 1310 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
adamc@162 1311 | _ => NONE) sgis of
adamc@162 1312 NONE => NONE
adamc@162 1313 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
adamc@162 1314 end
adamc@34 1315 | SgnError => SOME (CError, ErrorMsg.dummySpan)
adamc@42 1316 | _ => NONE
adamc@34 1317
adamc@88 1318 fun sgnSeekConstraints (str, sgis) =
adamc@88 1319 let
adamc@88 1320 fun seek (sgis, sgns, strs, cons, acc) =
adamc@88 1321 case sgis of
adamc@88 1322 [] => acc
adamc@88 1323 | (sgi, _) :: sgis =>
adamc@88 1324 case sgi of
adamc@88 1325 SgiConstraint (c1, c2) =>
adamc@88 1326 let
adamc@88 1327 val sub = sgnSubCon (str, (sgns, strs, cons))
adamc@88 1328 in
adamc@88 1329 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
adamc@88 1330 end
adamc@88 1331 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 1332 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@191 1333 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@191 1334 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 1335 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
adamc@88 1336 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
adamc@88 1337 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
adamc@563 1338 | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@563 1339 | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 1340 in
adamc@88 1341 seek (sgis, IM.empty, IM.empty, IM.empty, [])
adamc@88 1342 end
adamc@88 1343
adamc@88 1344 fun projectConstraints env {sgn, str} =
adamc@88 1345 case #1 (hnormSgn env sgn) of
adamc@88 1346 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
adamc@88 1347 | SgnError => SOME []
adamc@88 1348 | _ => NONE
adamc@34 1349
adamc@447 1350 fun edeclBinds env (d, loc) =
adamc@447 1351 case d of
adamc@447 1352 EDVal (x, t, _) => pushERel env x t
adamc@447 1353 | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
adamc@447 1354
adamc@157 1355 fun declBinds env (d, loc) =
adamc@157 1356 case d of
adamc@157 1357 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@191 1358 | DDatatype (x, n, xs, xncs) =>
adamc@157 1359 let
adamc@297 1360 val k = (KType, loc)
adamc@297 1361 val nxs = length xs
adamc@297 1362 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
adamc@297 1363 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
adamc@297 1364 (KArrow (k, kb), loc)))
adamc@297 1365 ((CNamed n, loc), k) xs
adamc@297 1366
adamc@297 1367 val env = pushCNamedAs env x n kb NONE
adamc@191 1368 val env = pushDatatype env n xs xncs
adamc@157 1369 in
adamc@191 1370 foldl (fn ((x', n', to), env) =>
adamc@191 1371 let
adamc@191 1372 val t =
adamc@191 1373 case to of
adamc@297 1374 NONE => tb
adamc@297 1375 | SOME t => (TFun (t, tb), loc)
adamc@297 1376 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
adamc@191 1377 in
adamc@191 1378 pushENamedAs env x' n' t
adamc@191 1379 end)
adamc@191 1380 env xncs
adamc@157 1381 end
adamc@191 1382 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
adamc@157 1383 let
adamc@157 1384 val t = (CModProj (m, ms, x'), loc)
adamc@297 1385 val k = (KType, loc)
adamc@297 1386 val nxs = length xs
adamc@297 1387 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
adamc@297 1388 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
adamc@297 1389 (KArrow (k, kb), loc)))
adamc@297 1390 ((CNamed n, loc), k) xs
adamc@297 1391
adamc@341 1392 val env = pushCNamedAs env x n kb (SOME t)
adamc@191 1393 val env = pushDatatype env n xs xncs
adamc@157 1394 in
adamc@191 1395 foldl (fn ((x', n', to), env) =>
adamc@191 1396 let
adamc@191 1397 val t =
adamc@191 1398 case to of
adamc@297 1399 NONE => tb
adamc@297 1400 | SOME t => (TFun (t, tb), loc)
adamc@297 1401 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
adamc@191 1402 in
adamc@191 1403 pushENamedAs env x' n' t
adamc@191 1404 end)
adamc@191 1405 env xncs
adamc@157 1406 end
adamc@157 1407 | DVal (x, n, t, _) => pushENamedAs env x n t
adamc@157 1408 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
adamc@157 1409 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
adamc@157 1410 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
adamc@157 1411 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
adamc@157 1412 | DConstraint _ => env
adamc@157 1413 | DExport _ => env
adamc@205 1414 | DTable (tn, x, n, c) =>
adamc@205 1415 let
adamc@338 1416 val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
adamc@338 1417 in
adamc@338 1418 pushENamedAs env x n t
adamc@338 1419 end
adamc@338 1420 | DSequence (tn, x, n) =>
adamc@338 1421 let
adamc@338 1422 val t = (CModProj (tn, [], "sql_sequence"), loc)
adamc@205 1423 in
adamc@205 1424 pushENamedAs env x n t
adamc@205 1425 end
adamc@563 1426 | DClass (x, n, k, c) =>
adamc@213 1427 let
adamc@563 1428 val k = (KArrow (k, (KType, loc)), loc)
adamc@213 1429 val env = pushCNamedAs env x n k (SOME c)
adamc@213 1430 in
adamc@213 1431 pushClass env n
adamc@213 1432 end
adamc@271 1433 | DDatabase _ => env
adamc@459 1434 | DCookie (tn, x, n, c) =>
adamc@459 1435 let
adamc@459 1436 val t = (CApp ((CModProj (tn, [], "cookie"), loc), c), loc)
adamc@459 1437 in
adamc@459 1438 pushENamedAs env x n t
adamc@459 1439 end
adamc@157 1440
adamc@243 1441 fun patBinds env (p, loc) =
adamc@243 1442 case p of
adamc@243 1443 PWild => env
adamc@243 1444 | PVar (x, t) => pushERel env x t
adamc@243 1445 | PPrim _ => env
adamc@243 1446 | PCon (_, _, _, NONE) => env
adamc@243 1447 | PCon (_, _, _, SOME p) => patBinds env p
adamc@243 1448 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
adamc@243 1449
adamc@2 1450 end