Mercurial > urweb

annotate src/elab_env.sml @ 1327:1cc67fdac4d3

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