Mercurial > urweb

annotate src/elab_env.sml @ 1591:20f898c29525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweaks to choices of source positions to use in error messages, including for subSgn
author Adam Chlipala <adam@chlipala.net>
date Sat, 05 Nov 2011 13:12:07 -0400
parents 287604b4a08d
children 6c00d8af6239
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);
adam@1575 548 if length xcs1 <> length xcs2 then
adam@1575 549 raise Unify
adam@1575 550 else
adam@1575 551 List.app (fn (x1, c1) =>
adam@1575 552 if List.exists (fn (x2, c2) => (eqCons (x1, x2); eqCons (c1, c2); true) handle Unify => false) xcs2 then
adam@1575 553 ()
adam@1575 554 else
adam@1575 555 raise Unify) xcs1)
adamc@904 556 | (CConcat (f1, x1), CConcat (f2, x2)) => (eqCons (f1, f2); eqCons (x1, x2))
adamc@904 557 | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
adamc@904 558
adamc@904 559 | (CUnit, CUnit) => ()
adamc@904 560
adamc@904 561 | (CTuple cs1, CTuple cs2) => (ListPair.appEq (eqCons) (cs1, cs2)
adamc@904 562 handle ListPair.UnequalLengths => raise Unify)
adamc@904 563 | (CProj (c1, n1), CProj (c2, n2)) => (eqCons (c1, c2);
adamc@904 564 if n1 = n2 then () else raise Unify)
adamc@904 565
adamc@904 566 | _ => raise Unify
adamc@904 567
adam@1325 568 fun unifyCons (hnorm : con -> con) rs =
adamc@674 569 let
adamc@711 570 fun unify d (c1, c2) =
adam@1325 571 case (#1 (hnorm c1), #1 (hnorm c2)) of
adam@1303 572 (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2)
adam@1303 573 | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2)
adamc@711 574
adamc@750 575 | (CUnif _, _) => ()
adamc@750 576
adamc@711 577 | (c1', CRel n2) =>
adamc@711 578 if n2 < d then
adamc@711 579 case c1' of
adamc@711 580 CRel n1 => if n1 = n2 then () else raise Unify
adamc@711 581 | _ => raise Unify
adamc@711 582 else if n2 - d >= length rs then
adamc@711 583 case c1' of
adamc@711 584 CRel n1 => if n1 = n2 - length rs then () else raise Unify
adamc@711 585 | _ => raise Unify
adamc@711 586 else
adamc@711 587 let
adamc@711 588 val r = List.nth (rs, n2 - d)
adamc@711 589 in
adamc@711 590 case !r of
adamc@711 591 NONE => r := SOME c1
adamc@904 592 | SOME c2 => eqCons (c1, c2)
adamc@711 593 end
adamc@711 594
adamc@711 595 | (TFun (d1, r1), TFun (d2, r2)) => (unify d (d1, d2); unify d (r1, r2))
adamc@711 596 | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (d + 1) (r1, r2))
adamc@711 597 | (TRecord c1, TRecord c2) => unify d (c1, c2)
adamc@711 598 | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) =>
adamc@711 599 (unify d (a1, a2); unify d (b1, b2); unify d (c1, c2))
adamc@711 600
adamc@711 601 | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify
adamc@711 602 | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) =>
adamc@711 603 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify
adamc@711 604 | (CApp (f1, x1), CApp (f2, x2)) => (unify d (f1, f2); unify d (x1, x2))
adamc@711 605 | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (d + 1) (b1, b2))
adamc@711 606
adamc@711 607 | (CKAbs (_, b1), CKAbs (_, b2)) => unify d (b1, b2)
adamc@711 608 | (CKApp (c1, k1), CKApp (c2, k2)) => (unify d (c1, c2); unifyKinds (k1, k2))
adamc@711 609 | (TKFun (_, c1), TKFun (_, c2)) => unify d (c1, c2)
adamc@711 610
adamc@711 611 | (CName s1, CName s2) => if s1 = s2 then () else raise Unify
adamc@711 612
adamc@711 613 | (CRecord (k1, xcs1), CRecord (k2, xcs2)) =>
adamc@711 614 (unifyKinds (k1, k2);
adam@1575 615 if length xcs1 <> length xcs2 then
adam@1575 616 raise Unify
adam@1575 617 else
adam@1575 618 app (fn (x1, c1) =>
adam@1575 619 if List.exists (fn (x2, c2) => (unify d (x1, x2); unify d (c1, c2); true) handle Unify => false) xcs2 then
adam@1575 620 ()
adam@1575 621 else
adam@1575 622 raise Unify) xcs1)
adamc@711 623 | (CConcat (f1, x1), CConcat (f2, x2)) => (unify d (f1, f2); unify d (x1, x2))
adamc@711 624 | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2))
adamc@711 625
adamc@711 626 | (CUnit, CUnit) => ()
adamc@711 627
adamc@711 628 | (CTuple cs1, CTuple cs2) => (ListPair.appEq (unify d) (cs1, cs2)
adamc@711 629 handle ListPair.UnequalLengths => raise Unify)
adamc@711 630 | (CProj (c1, n1), CProj (c2, n2)) => (unify d (c1, c2);
adamc@711 631 if n1 = n2 then () else raise Unify)
adamc@711 632
adamc@711 633 | _ => raise Unify
adamc@674 634 in
adamc@711 635 unify
adamc@674 636 end
adamc@674 637
adam@1325 638 fun tryUnify hnorm nRs (c1, c2) =
adamc@674 639 let
adamc@711 640 val rs = List.tabulate (nRs, fn _ => ref NONE)
adamc@674 641 in
adam@1325 642 (unifyCons hnorm rs 0 (c1, c2);
adamc@711 643 SOME (map (fn r => case !r of
adamc@711 644 NONE => raise Unify
adamc@711 645 | SOME c => c) rs))
adamc@711 646 handle Unify => NONE
adamc@674 647 end
adamc@674 648
adamc@711 649 fun unifySubst (rs : con list) =
adamc@711 650 U.Con.mapB {kind = fn _ => fn k => k,
adamc@711 651 con = fn d => fn c =>
adamc@711 652 case c of
adamc@711 653 CRel n =>
adamc@711 654 if n < d then
adamc@711 655 c
adamc@711 656 else
adamc@711 657 #1 (List.nth (rs, n - d))
adamc@711 658 | _ => c,
adamc@711 659 bind = fn (d, U.Con.RelC _) => d + 1
adamc@711 660 | (d, _) => d}
adamc@711 661 0
adamc@711 662
adamc@753 663 exception Bad of con * con
adamc@750 664
adamc@754 665 val hasUnif = U.Con.exists {kind = fn _ => false,
adam@1303 666 con = fn CUnif (_, _, _, _, ref NONE) => true
adamc@754 667 | _ => false}
adamc@754 668
adamc@754 669 fun startsWithUnif c =
adamc@754 670 let
adamc@754 671 fun firstArg (c, acc) =
adamc@754 672 case #1 c of
adamc@754 673 CApp (f, x) => firstArg (f, SOME x)
adamc@754 674 | _ => acc
adamc@754 675 in
adamc@754 676 case firstArg (c, NONE) of
adamc@754 677 NONE => false
adamc@754 678 | SOME x => hasUnif x
adamc@754 679 end
adamc@754 680
adamc@753 681 fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
adamc@674 682 let
adamc@711 683 fun resolve c =
adamc@711 684 let
adamc@711 685 fun doHead f =
adamc@711 686 case CM.find (#classes env, f) of
adamc@711 687 NONE => NONE
adamc@711 688 | SOME class =>
adamc@711 689 let
adamc@711 690 val loc = #2 c
adamc@675 691
adamc@753 692 fun generalize (c as (_, loc)) =
adamc@753 693 case #1 c of
adamc@753 694 CApp (f, x) =>
adamc@753 695 let
adamc@753 696 val (f, equate) = generalize f
adamc@753 697
adamc@753 698 fun isRecord () =
adamc@753 699 let
adamc@753 700 val rk = ref NONE
adamc@753 701 val k = (KUnif (loc, "k", rk), loc)
adamc@753 702 val r = ref NONE
adam@1303 703 val rc = (CUnif (0, loc, k, "x", r), loc)
adamc@753 704 in
adamc@753 705 ((CApp (f, rc), loc),
adamc@753 706 fn () => (if consEq (rc, x) then
adamc@753 707 true
adamc@753 708 else
adamc@753 709 (raise Bad (rc, x);
adamc@753 710 false))
adamc@753 711 andalso equate ())
adamc@753 712 end
adamc@753 713 in
adamc@753 714 case #1 x of
adamc@753 715 CConcat _ => isRecord ()
adamc@753 716 | CRecord _ => isRecord ()
adamc@753 717 | _ => ((CApp (f, x), loc), equate)
adamc@753 718 end
adamc@753 719 | _ => (c, fn () => true)
adamc@753 720
adamc@753 721 val (c, equate) = generalize c
adamc@753 722
adamc@711 723 fun tryRules rules =
adamc@711 724 case rules of
adamc@675 725 [] => NONE
adamc@711 726 | (nRs, cs, c', e) :: rules' =>
adam@1325 727 case tryUnify hnorm nRs (c, c') of
adamc@711 728 NONE => tryRules rules'
adamc@711 729 | SOME rs =>
adamc@675 730 let
adamc@711 731 val eos = map (resolve o unifySubst rs) cs
adamc@675 732 in
adamc@750 733 if List.exists (not o Option.isSome) eos
adamc@753 734 orelse not (equate ())
adamc@753 735 orelse not (consEq (c, unifySubst rs c')) then
adamc@711 736 tryRules rules'
adamc@711 737 else
adamc@711 738 let
adamc@711 739 val es = List.mapPartial (fn x => x) eos
adamc@711 740
adamc@711 741 val e = foldr (fn (c, e) => (ECApp (e, c), loc)) e rs
adamc@711 742 val e = foldl (fn (e', e) => (EApp (e, e'), loc)) e es
adamc@711 743 in
adamc@711 744 SOME e
adamc@711 745 end
adamc@675 746 end
adamc@711 747
adamc@711 748 fun rules () = tryRules (#rules class)
adamc@711 749
adamc@711 750 fun tryGrounds ces =
adamc@711 751 case ces of
adamc@711 752 [] => rules ()
adamc@711 753 | (c', e) :: ces' =>
adam@1325 754 case tryUnify hnorm 0 (c, c') of
adamc@711 755 NONE => tryGrounds ces'
adamc@711 756 | SOME _ => SOME e
adamc@675 757 in
adamc@711 758 tryGrounds (#ground class)
adamc@675 759 end
adamc@711 760 in
adamc@754 761 if startsWithUnif c then
adamc@754 762 NONE
adamc@754 763 else
adamc@754 764 case #1 c of
adamc@754 765 TRecord c =>
adamc@754 766 (case #1 (hnorm c) of
adamc@754 767 CRecord (_, xts) =>
adamc@754 768 let
adamc@754 769 fun resolver (xts, acc) =
adamc@754 770 case xts of
adamc@754 771 [] => SOME (ERecord acc, #2 c)
adamc@754 772 | (x, t) :: xts =>
adamc@754 773 let
adamc@754 774 val t = hnorm t
adamc@750 775
adamc@754 776 val t = case t of
adamc@754 777 (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc)
adamc@754 778 | _ => t
adamc@754 779 in
adamc@754 780 case resolve t of
adamc@754 781 NONE => NONE
adamc@754 782 | SOME e => resolver (xts, (x, e, t) :: acc)
adamc@754 783 end
adamc@754 784 in
adamc@754 785 resolver (xts, [])
adamc@754 786 end
adamc@754 787 | _ => NONE)
adamc@754 788 | _ =>
adamc@754 789 case class_head_in c of
adamc@754 790 SOME f => doHead f
adamc@754 791 | _ => NONE
adamc@711 792 end
adamc@674 793 in
adamc@711 794 resolve
adamc@674 795 end
adamc@211 796
adamc@9 797 fun pushERel (env : env) x t =
adamc@9 798 let
adamc@9 799 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
adamc@9 800 | x => x) (#renameE env)
adamc@211 801
adamc@675 802 val classes = CM.map (fn class =>
adamc@711 803 {ground = map (fn (c, e) => (c, liftExp e)) (#ground class),
adamc@711 804 rules = #rules class}) (#classes env)
adamc@711 805 val classes = case class_head_in t of
adamc@211 806 NONE => classes
adamc@711 807 | SOME f =>
adamc@403 808 case CM.find (classes, f) of
adamc@403 809 NONE => classes
adamc@403 810 | SOME class =>
adamc@403 811 let
adamc@711 812 val class = {ground = (t, (ERel 0, #2 t)) :: #ground class,
adamc@711 813 rules = #rules class}
adamc@403 814 in
adamc@403 815 CM.insert (classes, f, class)
adamc@403 816 end
adamc@9 817 in
adamc@623 818 {renameK = #renameK env,
adamc@623 819 relK = #relK env,
adamc@623 820
adamc@623 821 renameC = #renameC env,
adamc@9 822 relC = #relC env,
adamc@9 823 namedC = #namedC env,
adamc@9 824
adamc@157 825 datatypes = #datatypes env,
adamc@171 826 constructors = #constructors env,
adamc@157 827
adamc@211 828 classes = classes,
adamc@211 829
adamc@9 830 renameE = SM.insert (renameE, x, Rel' (0, t)),
adamc@9 831 relE = (x, t) :: #relE env,
adamc@31 832 namedE = #namedE env,
adamc@31 833
adamc@31 834 renameSgn = #renameSgn env,
adamc@31 835 sgn = #sgn env,
adamc@31 836
adamc@31 837 renameStr = #renameStr env,
adamc@31 838 str = #str env}
adamc@9 839 end
adamc@9 840
adamc@9 841 fun lookupERel (env : env) n =
adamc@9 842 (List.nth (#relE env, n))
adamc@9 843 handle Subscript => raise UnboundRel n
adamc@9 844
adamc@674 845 fun rule_in c =
adamc@674 846 let
adamc@674 847 fun quantifiers (c, nvars) =
adamc@674 848 case #1 c of
adamc@674 849 TCFun (_, _, _, c) => quantifiers (c, nvars + 1)
adamc@674 850 | _ =>
adamc@674 851 let
adamc@674 852 fun clauses (c, hyps) =
adamc@674 853 case #1 c of
adamc@674 854 TFun (hyp, c) =>
adamc@711 855 (case class_head_in hyp of
adamc@711 856 SOME _ => clauses (c, hyp :: hyps)
adamc@711 857 | NONE => NONE)
adamc@674 858 | _ =>
adamc@711 859 case class_head_in c of
adamc@674 860 NONE => NONE
adamc@711 861 | SOME f => SOME (f, nvars, rev hyps, c)
adamc@674 862 in
adamc@674 863 clauses (c, [])
adamc@674 864 end
adamc@674 865 in
adamc@711 866 quantifiers (c, 0)
adamc@677 867 end
adamc@677 868
adamc@9 869 fun pushENamedAs (env : env) x n t =
adamc@211 870 let
adamc@211 871 val classes = #classes env
adamc@674 872 val classes = case rule_in t of
adamc@211 873 NONE => classes
adamc@711 874 | SOME (f, nvs, cs, c) =>
adamc@403 875 case CM.find (classes, f) of
adamc@403 876 NONE => classes
adamc@403 877 | SOME class =>
adamc@403 878 let
adamc@675 879 val e = (ENamed n, #2 t)
adamc@675 880
adamc@675 881 val class =
adamc@711 882 {ground = #ground class,
adamc@711 883 rules = (nvs, cs, c, e) :: #rules class}
adamc@403 884 in
adamc@403 885 CM.insert (classes, f, class)
adamc@403 886 end
adamc@211 887 in
adamc@623 888 {renameK = #renameK env,
adamc@623 889 relK = #relK env,
adamc@623 890
adamc@623 891 renameC = #renameC env,
adamc@211 892 relC = #relC env,
adamc@211 893 namedC = #namedC env,
adamc@9 894
adamc@211 895 datatypes = #datatypes env,
adamc@211 896 constructors = #constructors env,
adamc@157 897
adamc@211 898 classes = classes,
adamc@31 899
adamc@211 900 renameE = SM.insert (#renameE env, x, Named' (n, t)),
adamc@211 901 relE = #relE env,
adamc@211 902 namedE = IM.insert (#namedE env, n, (x, t)),
adamc@211 903
adamc@211 904 renameSgn = #renameSgn env,
adamc@211 905 sgn = #sgn env,
adamc@211 906
adamc@211 907 renameStr = #renameStr env,
adamc@211 908 str = #str env}
adamc@211 909 end
adamc@9 910
adamc@9 911 fun pushENamed env x t =
adamc@9 912 let
adamc@9 913 val n = !namedCounter
adamc@9 914 in
adamc@9 915 namedCounter := n + 1;
adamc@9 916 (pushENamedAs env x n t, n)
adamc@9 917 end
adamc@9 918
adamc@9 919 fun lookupENamed (env : env) n =
adamc@9 920 case IM.find (#namedE env, n) of
adamc@9 921 NONE => raise UnboundNamed n
adamc@9 922 | SOME x => x
adamc@9 923
adamc@471 924 fun checkENamed (env : env) n =
adamc@471 925 Option.isSome (IM.find (#namedE env, n))
adamc@471 926
adamc@9 927 fun lookupE (env : env) x =
adamc@9 928 case SM.find (#renameE env, x) of
adamc@9 929 NONE => NotBound
adamc@9 930 | SOME (Rel' x) => Rel x
adamc@9 931 | SOME (Named' x) => Named x
adamc@2 932
adamc@31 933 fun pushSgnNamedAs (env : env) x n sgis =
adamc@623 934 {renameK = #renameK env,
adamc@623 935 relK = #relK env,
adamc@623 936
adamc@623 937 renameC = #renameC env,
adamc@31 938 relC = #relC env,
adamc@31 939 namedC = #namedC env,
adamc@31 940
adamc@157 941 datatypes = #datatypes env,
adamc@171 942 constructors = #constructors env,
adamc@157 943
adamc@211 944 classes = #classes env,
adamc@211 945
adamc@31 946 renameE = #renameE env,
adamc@31 947 relE = #relE env,
adamc@31 948 namedE = #namedE env,
adamc@31 949
adamc@31 950 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
adamc@31 951 sgn = IM.insert (#sgn env, n, (x, sgis)),
adamc@31 952
adamc@31 953 renameStr = #renameStr env,
adamc@31 954 str = #str env}
adamc@31 955
adamc@31 956 fun pushSgnNamed env x sgis =
adamc@31 957 let
adamc@31 958 val n = !namedCounter
adamc@31 959 in
adamc@31 960 namedCounter := n + 1;
adamc@31 961 (pushSgnNamedAs env x n sgis, n)
adamc@31 962 end
adamc@31 963
adamc@31 964 fun lookupSgnNamed (env : env) n =
adamc@31 965 case IM.find (#sgn env, n) of
adamc@31 966 NONE => raise UnboundNamed n
adamc@31 967 | SOME x => x
adamc@31 968
adamc@31 969 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
adamc@31 970
adamc@31 971 fun lookupStrNamed (env : env) n =
adamc@31 972 case IM.find (#str env, n) of
adamc@31 973 NONE => raise UnboundNamed n
adamc@31 974 | SOME x => x
adamc@31 975
adamc@31 976 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
adamc@31 977
adamc@203 978
adamc@216 979 fun sgiSeek (sgi, (sgns, strs, cons)) =
adamc@216 980 case sgi of
adamc@216 981 SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@216 982 | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@805 983 | SgiDatatype dts => (sgns, strs, foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts)
adamc@216 984 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@216 985 | SgiVal _ => (sgns, strs, cons)
adamc@216 986 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
adamc@216 987 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
adamc@216 988 | SgiConstraint _ => (sgns, strs, cons)
adamc@563 989 | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@563 990 | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
adamc@216 991
adamc@34 992 fun sgnSeek f sgis =
adamc@34 993 let
adamc@59 994 fun seek (sgis, sgns, strs, cons) =
adamc@34 995 case sgis of
adamc@34 996 [] => NONE
adamc@34 997 | (sgi, _) :: sgis =>
adamc@34 998 case f sgi of
adamc@158 999 SOME v =>
adamc@158 1000 let
adamc@158 1001 val cons =
adamc@158 1002 case sgi of
adamc@805 1003 SgiDatatype dts => foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts
adamc@191 1004 | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
adamc@158 1005 | _ => cons
adamc@158 1006 in
adamc@158 1007 SOME (v, (sgns, strs, cons))
adamc@158 1008 end
adamc@88 1009 | NONE =>
adamc@216 1010 let
adamc@216 1011 val (sgns, strs, cons) = sgiSeek (sgi, (sgns, strs, cons))
adamc@216 1012 in
adamc@216 1013 seek (sgis, sgns, strs, cons)
adamc@216 1014 end
adamc@34 1015 in
adamc@59 1016 seek (sgis, IM.empty, IM.empty, IM.empty)
adamc@34 1017 end
adamc@34 1018
adamc@34 1019 fun id x = x
adamc@34 1020
adamc@34 1021 fun unravelStr (str, _) =
adamc@34 1022 case str of
adamc@34 1023 StrVar x => (x, [])
adamc@34 1024 | StrProj (str, m) =>
adamc@34 1025 let
adamc@34 1026 val (x, ms) = unravelStr str
adamc@34 1027 in
adamc@34 1028 (x, ms @ [m])
adamc@34 1029 end
adamc@34 1030 | _ => raise Fail "unravelStr"
adamc@34 1031
adamc@59 1032 fun sgnS_con (str, (sgns, strs, cons)) c =
adamc@34 1033 case c of
adamc@34 1034 CModProj (m1, ms, x) =>
adamc@34 1035 (case IM.find (strs, m1) of
adamc@34 1036 NONE => c
adamc@34 1037 | SOME m1x =>
adamc@34 1038 let
adamc@34 1039 val (m1, ms') = unravelStr str
adamc@34 1040 in
adamc@34 1041 CModProj (m1, ms' @ m1x :: ms, x)
adamc@34 1042 end)
adamc@34 1043 | CNamed n =>
adamc@34 1044 (case IM.find (cons, n) of
adamc@34 1045 NONE => c
adamc@34 1046 | SOME nx =>
adamc@34 1047 let
adamc@34 1048 val (m1, ms) = unravelStr str
adamc@34 1049 in
adamc@34 1050 CModProj (m1, ms, nx)
adamc@34 1051 end)
adamc@34 1052 | _ => c
adamc@34 1053
adamc@721 1054 fun sgnS_con' (m1, ms', (sgns, strs, cons)) =
adamc@721 1055 U.Con.map {kind = fn x => x,
adamc@721 1056 con = fn c =>
adamc@721 1057 case c of
kkallio@1454 1058 CModProj (m1', ms, x) =>
kkallio@1454 1059 (case IM.find (strs, m1') of
adamc@721 1060 NONE => c
adamc@721 1061 | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x))
adamc@721 1062 | CNamed n =>
adamc@721 1063 (case IM.find (cons, n) of
adamc@721 1064 NONE => c
adamc@721 1065 | SOME nx => CModProj (m1, ms', nx))
adamc@721 1066 | _ => c}
adamc@216 1067
adamc@59 1068 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
adamc@59 1069 case sgn of
adamc@59 1070 SgnProj (m1, ms, x) =>
adamc@59 1071 (case IM.find (strs, m1) of
adamc@59 1072 NONE => sgn
adamc@59 1073 | SOME m1x =>
adamc@59 1074 let
adamc@59 1075 val (m1, ms') = unravelStr str
adamc@59 1076 in
adamc@59 1077 SgnProj (m1, ms' @ m1x :: ms, x)
adamc@59 1078 end)
adamc@59 1079 | SgnVar n =>
adamc@59 1080 (case IM.find (sgns, n) of
adamc@59 1081 NONE => sgn
adamc@59 1082 | SOME nx =>
adamc@59 1083 let
adamc@59 1084 val (m1, ms) = unravelStr str
adamc@59 1085 in
adamc@59 1086 SgnProj (m1, ms, nx)
adamc@59 1087 end)
adamc@59 1088 | _ => sgn
adamc@59 1089
adamc@59 1090 fun sgnSubSgn x =
adamc@34 1091 ElabUtil.Sgn.map {kind = id,
adamc@59 1092 con = sgnS_con x,
adamc@34 1093 sgn_item = id,
adamc@59 1094 sgn = sgnS_sgn x}
adamc@34 1095
adamc@211 1096
adamc@211 1097
adamc@211 1098 and projectSgn env {sgn, str, field} =
adamc@211 1099 case #1 (hnormSgn env sgn) of
adamc@211 1100 SgnConst sgis =>
adamc@211 1101 (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
adamc@211 1102 NONE => NONE
adamc@211 1103 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
adamc@211 1104 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
adamc@211 1105 | _ => NONE
adamc@211 1106
adamc@211 1107 and hnormSgn env (all as (sgn, loc)) =
adamc@34 1108 case sgn of
adamc@42 1109 SgnError => all
adamc@42 1110 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
adamc@42 1111 | SgnConst _ => all
adamc@42 1112 | SgnFun _ => all
adamc@59 1113 | SgnProj (m, ms, x) =>
adamc@59 1114 let
adamc@59 1115 val (_, sgn) = lookupStrNamed env m
adamc@59 1116 in
adamc@59 1117 case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms,
adamc@59 1118 sgn = sgn,
adamc@59 1119 field = x} of
adamc@59 1120 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
adamc@1058 1121 | SOME sgn => hnormSgn env sgn
adamc@59 1122 end
adamc@42 1123 | SgnWhere (sgn, x, c) =>
adamc@42 1124 case #1 (hnormSgn env sgn) of
adamc@42 1125 SgnError => (SgnError, loc)
adamc@42 1126 | SgnConst sgis =>
adamc@42 1127 let
adamc@42 1128 fun traverse (pre, post) =
adamc@42 1129 case post of
adamc@42 1130 [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
adamc@42 1131 | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
adamc@42 1132 if x = x' then
adamc@42 1133 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
adamc@42 1134 else
adamc@42 1135 traverse (sgi :: pre, rest)
adamc@42 1136 | sgi :: rest => traverse (sgi :: pre, rest)
adamc@42 1137
adamc@42 1138 val sgis = traverse ([], sgis)
adamc@42 1139 in
adamc@42 1140 (SgnConst sgis, loc)
adamc@42 1141 end
adamc@42 1142 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
adamc@42 1143
adamc@849 1144 fun manifest (m, ms, loc) =
adamc@849 1145 foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms
adamc@849 1146
adamc@211 1147 fun enrichClasses env classes (m1, ms) sgn =
adamc@59 1148 case #1 (hnormSgn env sgn) of
adamc@59 1149 SgnConst sgis =>
adamc@211 1150 let
adamc@218 1151 val (classes, _, _, _) =
adamc@218 1152 foldl (fn (sgi, (classes, newClasses, fmap, env)) =>
adamc@211 1153 let
adamc@211 1154 fun found (x, n) =
adamc@211 1155 (CM.insert (classes,
adamc@211 1156 ClProj (m1, ms, x),
adamc@211 1157 empty_class),
adamc@216 1158 IM.insert (newClasses, n, x),
adamc@218 1159 sgiSeek (#1 sgi, fmap),
adamc@218 1160 env)
adamc@216 1161
adamc@218 1162 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env)
adamc@211 1163 in
adamc@211 1164 case #1 sgi of
adamc@217 1165 SgiStr (x, _, sgn) =>
adamc@849 1166 let
adamc@849 1167 val str = manifest (m1, ms, #2 sgi)
adamc@849 1168 val sgn' = sgnSubSgn (str, fmap) sgn
adamc@849 1169 in
adamc@849 1170 (enrichClasses env classes (m1, ms @ [x]) sgn',
adamc@849 1171 newClasses,
adamc@849 1172 sgiSeek (#1 sgi, fmap),
adamc@849 1173 env)
adamc@849 1174 end
adamc@218 1175 | SgiSgn (x, n, sgn) =>
adamc@218 1176 (classes,
adamc@218 1177 newClasses,
adamc@218 1178 fmap,
adamc@218 1179 pushSgnNamedAs env x n sgn)
adamc@218 1180
adamc@563 1181 | SgiClassAbs (x, n, _) => found (x, n)
adamc@563 1182 | SgiClass (x, n, _, _) => found (x, n)
adamc@674 1183 | SgiVal (x, n, c) =>
adamc@674 1184 (case rule_in c of
adamc@674 1185 NONE => default ()
adamc@711 1186 | SOME (cn, nvs, cs, c) =>
adamc@674 1187 let
adamc@711 1188 val loc = #2 c
adamc@721 1189 val globalize = sgnS_con' (m1, ms, fmap)
adamc@674 1190
adamc@674 1191 val nc =
adamc@674 1192 case cn of
adamc@674 1193 ClNamed f => IM.find (newClasses, f)
adamc@674 1194 | _ => NONE
adamc@674 1195 in
adamc@674 1196 case nc of
adamc@674 1197 NONE =>
adamc@419 1198 let
adamc@419 1199 val classes =
adamc@419 1200 case CM.find (classes, cn) of
adamc@419 1201 NONE => classes
adamc@419 1202 | SOME class =>
adamc@419 1203 let
adamc@711 1204 val e = (EModProj (m1, ms, x), #2 sgn)
adamc@675 1205
adamc@675 1206 val class =
adamc@711 1207 {ground = #ground class,
adamc@711 1208 rules = (nvs,
adamc@711 1209 map globalize cs,
adamc@711 1210 globalize c,
adamc@711 1211 e) :: #rules class}
adamc@419 1212 in
adamc@419 1213 CM.insert (classes, cn, class)
adamc@419 1214 end
adamc@419 1215 in
adamc@419 1216 (classes,
adamc@419 1217 newClasses,
adamc@419 1218 fmap,
adamc@419 1219 env)
adamc@419 1220 end
adamc@674 1221 | SOME fx =>
adamc@674 1222 let
adamc@674 1223 val cn = ClProj (m1, ms, fx)
adamc@419 1224
adamc@674 1225 val classes =
adamc@674 1226 case CM.find (classes, cn) of
adamc@674 1227 NONE => classes
adamc@674 1228 | SOME class =>
adamc@674 1229 let
adamc@675 1230 val e = (EModProj (m1, ms, x), #2 sgn)
adamc@675 1231
adamc@675 1232 val class =
adamc@711 1233 {ground = #ground class,
adamc@711 1234 rules = (nvs,
adamc@711 1235 map globalize cs,
adamc@711 1236 globalize c,
adamc@711 1237 e) :: #rules class}
adamc@674 1238 in
adamc@674 1239 CM.insert (classes, cn, class)
adamc@674 1240 end
adamc@674 1241 in
adamc@674 1242 (classes,
adamc@674 1243 newClasses,
adamc@674 1244 fmap,
adamc@674 1245 env)
adamc@674 1246 end
adamc@674 1247 end)
adamc@216 1248 | _ => default ()
adamc@211 1249 end)
adamc@218 1250 (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis
adamc@211 1251 in
adamc@211 1252 classes
adamc@211 1253 end
adamc@211 1254 | _ => classes
adamc@211 1255
adamc@211 1256 fun pushStrNamedAs (env : env) x n sgn =
adamc@623 1257 {renameK = #renameK env,
adamc@623 1258 relK = #relK env,
adamc@623 1259
adamc@623 1260 renameC = #renameC env,
adamc@211 1261 relC = #relC env,
adamc@211 1262 namedC = #namedC env,
adamc@211 1263
adamc@211 1264 datatypes = #datatypes env,
adamc@211 1265 constructors = #constructors env,
adamc@211 1266
adamc@211 1267 classes = enrichClasses env (#classes env) (n, []) sgn,
adamc@211 1268
adamc@211 1269 renameE = #renameE env,
adamc@211 1270 relE = #relE env,
adamc@211 1271 namedE = #namedE env,
adamc@211 1272
adamc@211 1273 renameSgn = #renameSgn env,
adamc@211 1274 sgn = #sgn env,
adamc@211 1275
adamc@211 1276 renameStr = SM.insert (#renameStr env, x, (n, sgn)),
adamc@211 1277 str = IM.insert (#str env, n, (x, sgn))}
adamc@211 1278
adamc@211 1279 fun pushStrNamed env x sgn =
adamc@211 1280 let
adamc@211 1281 val n = !namedCounter
adamc@211 1282 in
adamc@211 1283 namedCounter := n + 1;
adamc@211 1284 (pushStrNamedAs env x n sgn, n)
adamc@211 1285 end
adamc@211 1286
adamc@211 1287 fun sgiBinds env (sgi, loc) =
adamc@211 1288 case sgi of
adamc@211 1289 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
adamc@211 1290 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@805 1291 | SgiDatatype dts =>
adamc@211 1292 let
adamc@805 1293 fun doOne ((x, n, xs, xncs), env) =
adamc@805 1294 let
adamc@805 1295 val k = (KType, loc)
adamc@805 1296 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@341 1297
adamc@805 1298 val env = pushCNamedAs env x n k' NONE
adamc@805 1299 in
adamc@805 1300 foldl (fn ((x', n', to), env) =>
adamc@805 1301 let
adamc@805 1302 val t =
adamc@805 1303 case to of
adamc@805 1304 NONE => (CNamed n, loc)
adamc@805 1305 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@805 1306
adamc@805 1307 val k = (KType, loc)
adamc@805 1308 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
adamc@805 1309 in
adamc@805 1310 pushENamedAs env x' n' t
adamc@805 1311 end)
adamc@805 1312 env xncs
adamc@805 1313 end
adamc@211 1314 in
adamc@805 1315 foldl doOne env dts
adamc@211 1316 end
adamc@211 1317 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@211 1318 let
adamc@341 1319 val k = (KType, loc)
adamc@341 1320 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@341 1321
adamc@341 1322 val env = pushCNamedAs env x n k' (SOME (CModProj (m1, ms, x'), loc))
adamc@211 1323 in
adamc@211 1324 foldl (fn ((x', n', to), env) =>
adamc@211 1325 let
adamc@211 1326 val t =
adamc@211 1327 case to of
adamc@211 1328 NONE => (CNamed n, loc)
adamc@211 1329 | SOME t => (TFun (t, (CNamed n, loc)), loc)
adamc@211 1330
adamc@211 1331 val k = (KType, loc)
adamc@211 1332 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
adamc@211 1333 in
adamc@211 1334 pushENamedAs env x' n' t
adamc@211 1335 end)
adamc@211 1336 env xncs
adamc@211 1337 end
adamc@211 1338 | SgiVal (x, n, t) => pushENamedAs env x n t
adamc@211 1339 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
adamc@211 1340 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
adamc@211 1341 | SgiConstraint _ => env
adamc@211 1342
adamc@711 1343 | SgiClassAbs (x, n, k) => pushCNamedAs env x n k NONE
adamc@711 1344 | SgiClass (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@459 1345
adamc@211 1346 fun sgnSubCon x =
adamc@211 1347 ElabUtil.Con.map {kind = id,
adamc@211 1348 con = sgnS_con x}
adamc@59 1349
adamc@59 1350 fun projectStr env {sgn, str, field} =
adamc@59 1351 case #1 (hnormSgn env sgn) of
adamc@59 1352 SgnConst sgis =>
adamc@59 1353 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
adamc@59 1354 NONE => NONE
adamc@59 1355 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
adamc@59 1356 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
adamc@59 1357 | _ => NONE
adamc@59 1358
adamc@158 1359 fun chaseMpath env (n, ms) =
adamc@158 1360 let
adamc@158 1361 val (_, sgn) = lookupStrNamed env n
adamc@158 1362 in
adamc@158 1363 foldl (fn (m, (str, sgn)) =>
adamc@158 1364 case projectStr env {sgn = sgn, str = str, field = m} of
adamc@158 1365 NONE => raise Fail "kindof: Unknown substructure"
adamc@158 1366 | SOME sgn => ((StrProj (str, m), #2 sgn), sgn))
adamc@158 1367 ((StrVar n, #2 sgn), sgn) ms
adamc@158 1368 end
adamc@158 1369
adamc@42 1370 fun projectCon env {sgn, str, field} =
adamc@42 1371 case #1 (hnormSgn env sgn) of
adamc@34 1372 SgnConst sgis =>
adamc@34 1373 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
adamc@34 1374 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
adamc@805 1375 | SgiDatatype dts =>
adamc@805 1376 (case List.find (fn (x, _, xs, _) => x = field) dts of
adamc@805 1377 SOME (_, _, xs, _) =>
adamc@805 1378 let
adamc@805 1379 val k = (KType, #2 sgn)
adamc@805 1380 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
adamc@805 1381 in
adamc@805 1382 SOME (k', NONE)
adamc@805 1383 end
adamc@805 1384 | NONE => NONE)
adamc@341 1385 | SgiDatatypeImp (x, _, m1, ms, x', xs, _) =>
adamc@341 1386 if x = field then
adamc@341 1387 let
adamc@341 1388 val k = (KType, #2 sgn)
adamc@341 1389 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
adamc@341 1390 in
adamc@341 1391 SOME (k', SOME (CModProj (m1, ms, x'), #2 sgn))
adamc@341 1392 end
adamc@158 1393 else
adamc@158 1394 NONE
adamc@563 1395 | SgiClassAbs (x, _, k) => if x = field then
kkallio@1453 1396 SOME (k, NONE)
adamc@563 1397 else
adamc@563 1398 NONE
adamc@563 1399 | SgiClass (x, _, k, c) => if x = field then
kkallio@1453 1400 SOME (k, SOME c)
adamc@563 1401 else
adamc@563 1402 NONE
adamc@34 1403 | _ => NONE) sgis of
adamc@34 1404 NONE => NONE
adamc@34 1405 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
adamc@34 1406 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
adamc@42 1407 | _ => NONE
adamc@34 1408
adamc@157 1409 fun projectDatatype env {sgn, str, field} =
adamc@157 1410 case #1 (hnormSgn env sgn) of
adamc@157 1411 SgnConst sgis =>
adamc@805 1412 (case sgnSeek (fn SgiDatatype dts =>
adamc@805 1413 (case List.find (fn (x, _, _, _) => x = field) dts of
adamc@805 1414 SOME (_, _, xs, xncs) => SOME (xs, xncs)
adamc@805 1415 | NONE => NONE)
adamc@191 1416 | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
adamc@157 1417 | _ => NONE) sgis of
adamc@157 1418 NONE => NONE
adamc@191 1419 | SOME ((xs, xncs), subs) => SOME (xs,
adamc@191 1420 map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
adamc@157 1421 | _ => NONE
adamc@157 1422
adamc@174 1423 fun projectConstructor env {sgn, str, field} =
adamc@174 1424 case #1 (hnormSgn env sgn) of
adamc@174 1425 SgnConst sgis =>
adamc@174 1426 let
adamc@191 1427 fun consider (n, xs, xncs) =
adamc@174 1428 ListUtil.search (fn (x, n', to) =>
adamc@174 1429 if x <> field then
adamc@174 1430 NONE
adamc@174 1431 else
adamc@191 1432 SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
adamc@174 1433 in
adamc@805 1434 case sgnSeek (fn SgiDatatype dts =>
adamc@805 1435 let
adamc@805 1436 fun search dts =
adamc@805 1437 case dts of
adamc@805 1438 [] => NONE
adamc@805 1439 | (_, n, xs, xncs) :: dts =>
adamc@805 1440 case consider (n, xs, xncs) of
adamc@805 1441 NONE => search dts
adamc@805 1442 | v => v
adamc@805 1443 in
adamc@805 1444 search dts
adamc@805 1445 end
adamc@191 1446 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
adamc@174 1447 | _ => NONE) sgis of
adamc@174 1448 NONE => NONE
adamc@191 1449 | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to,
adamc@191 1450 sgnSubCon (str, subs) t)
adamc@174 1451 end
adamc@174 1452 | _ => NONE
adamc@174 1453
adamc@42 1454 fun projectVal env {sgn, str, field} =
adamc@42 1455 case #1 (hnormSgn env sgn) of
adamc@34 1456 SgnConst sgis =>
adamc@162 1457 let
adamc@191 1458 fun seek (n, xs, xncs) =
adamc@162 1459 ListUtil.search (fn (x, _, to) =>
adamc@162 1460 if x = field then
adamc@191 1461 SOME (let
adamc@467 1462 val base = (CNamed n, #2 sgn)
adamc@467 1463 val nxs = length xs
adamc@467 1464 val base = ListUtil.foldli (fn (i, _, base) =>
adamc@467 1465 (CApp (base,
adamc@467 1466 (CRel (nxs - i - 1), #2 sgn)),
adamc@467 1467 #2 sgn))
adamc@467 1468 base xs
adamc@467 1469
adamc@191 1470 val t =
adamc@191 1471 case to of
adamc@467 1472 NONE => base
adamc@467 1473 | SOME t => (TFun (t, base), #2 sgn)
adamc@191 1474 val k = (KType, #2 sgn)
adamc@191 1475 in
adamc@467 1476 foldr (fn (x, t) => (TCFun (Implicit, x, k, t), #2 sgn))
adamc@191 1477 t xs
adamc@191 1478 end)
adamc@162 1479 else
adamc@162 1480 NONE) xncs
adamc@162 1481 in
adamc@162 1482 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
adamc@805 1483 | SgiDatatype dts =>
adamc@805 1484 let
adamc@805 1485 fun search dts =
adamc@805 1486 case dts of
adamc@805 1487 [] => NONE
adamc@805 1488 | (_, n, xs, xncs) :: dts =>
adamc@805 1489 case seek (n, xs, xncs) of
adamc@805 1490 NONE => search dts
adamc@805 1491 | v => v
adamc@805 1492 in
adamc@805 1493 search dts
adamc@805 1494 end
adamc@191 1495 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
adamc@162 1496 | _ => NONE) sgis of
adamc@162 1497 NONE => NONE
adamc@162 1498 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
adamc@162 1499 end
adamc@34 1500 | SgnError => SOME (CError, ErrorMsg.dummySpan)
adamc@42 1501 | _ => NONE
adamc@34 1502
adamc@88 1503 fun sgnSeekConstraints (str, sgis) =
adamc@88 1504 let
adamc@88 1505 fun seek (sgis, sgns, strs, cons, acc) =
adamc@88 1506 case sgis of
adamc@88 1507 [] => acc
adamc@88 1508 | (sgi, _) :: sgis =>
adamc@88 1509 case sgi of
adamc@88 1510 SgiConstraint (c1, c2) =>
adamc@88 1511 let
adamc@88 1512 val sub = sgnSubCon (str, (sgns, strs, cons))
adamc@88 1513 in
adamc@88 1514 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
adamc@88 1515 end
adamc@88 1516 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 1517 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@805 1518 | SgiDatatype dts => seek (sgis, sgns, strs,
adamc@805 1519 foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts, acc)
adamc@191 1520 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 1521 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
adamc@88 1522 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
adamc@88 1523 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
adamc@563 1524 | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@563 1525 | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 1526 in
adamc@88 1527 seek (sgis, IM.empty, IM.empty, IM.empty, [])
adamc@88 1528 end
adamc@88 1529
adamc@88 1530 fun projectConstraints env {sgn, str} =
adamc@88 1531 case #1 (hnormSgn env sgn) of
adamc@88 1532 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
adamc@88 1533 | SgnError => SOME []
adamc@88 1534 | _ => NONE
adamc@34 1535
adamc@825 1536 fun patBinds env (p, loc) =
adamc@825 1537 case p of
adamc@825 1538 PWild => env
adamc@825 1539 | PVar (x, t) => pushERel env x t
adamc@825 1540 | PPrim _ => env
adamc@825 1541 | PCon (_, _, _, NONE) => env
adamc@825 1542 | PCon (_, _, _, SOME p) => patBinds env p
adamc@825 1543 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
adamc@825 1544
adamc@1272 1545 fun patBindsN (p, _) =
adamc@1272 1546 case p of
adamc@1272 1547 PWild => 0
adamc@1272 1548 | PVar _ => 1
adamc@1272 1549 | PPrim _ => 0
adamc@1272 1550 | PCon (_, _, _, NONE) => 0
adamc@1272 1551 | PCon (_, _, _, SOME p) => patBindsN p
adamc@1272 1552 | PRecord xps => foldl (fn ((_, p, _), n) => patBindsN p + n) 0 xps
adamc@1272 1553
adamc@447 1554 fun edeclBinds env (d, loc) =
adamc@447 1555 case d of
adamc@825 1556 EDVal (p, _, _) => patBinds env p
adamc@447 1557 | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
adamc@447 1558
adamc@157 1559 fun declBinds env (d, loc) =
adamc@157 1560 case d of
adamc@157 1561 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@805 1562 | DDatatype dts =>
adamc@157 1563 let
adamc@805 1564 fun doOne ((x, n, xs, xncs), env) =
adamc@805 1565 let
adamc@805 1566 val k = (KType, loc)
adamc@805 1567 val nxs = length xs
adamc@805 1568 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
adamc@805 1569 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
adamc@805 1570 (KArrow (k, kb), loc)))
adamc@805 1571 ((CNamed n, loc), k) xs
adamc@805 1572
adamc@805 1573 val env = pushCNamedAs env x n kb NONE
adamc@805 1574 val env = pushDatatype env n xs xncs
adamc@805 1575 in
adamc@805 1576 foldl (fn ((x', n', to), env) =>
adamc@805 1577 let
adamc@805 1578 val t =
adamc@805 1579 case to of
adamc@805 1580 NONE => tb
adamc@805 1581 | SOME t => (TFun (t, tb), loc)
adamc@805 1582 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
adamc@805 1583 in
adamc@805 1584 pushENamedAs env x' n' t
adamc@805 1585 end)
adamc@805 1586 env xncs
adamc@805 1587 end
adamc@157 1588 in
adamc@805 1589 foldl doOne env dts
adamc@157 1590 end
adamc@191 1591 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
adamc@157 1592 let
adamc@157 1593 val t = (CModProj (m, ms, x'), loc)
adamc@297 1594 val k = (KType, loc)
adamc@297 1595 val nxs = length xs
adamc@297 1596 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
adamc@297 1597 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
adamc@297 1598 (KArrow (k, kb), loc)))
adamc@297 1599 ((CNamed n, loc), k) xs
adamc@297 1600
adamc@341 1601 val env = pushCNamedAs env x n kb (SOME t)
adamc@191 1602 val env = pushDatatype env n xs xncs
adamc@157 1603 in
adamc@191 1604 foldl (fn ((x', n', to), env) =>
adamc@191 1605 let
adamc@191 1606 val t =
adamc@191 1607 case to of
adamc@297 1608 NONE => tb
adamc@297 1609 | SOME t => (TFun (t, tb), loc)
adamc@297 1610 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
adamc@191 1611 in
adamc@191 1612 pushENamedAs env x' n' t
adamc@191 1613 end)
adamc@191 1614 env xncs
adamc@157 1615 end
adamc@157 1616 | DVal (x, n, t, _) => pushENamedAs env x n t
adamc@157 1617 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
adamc@157 1618 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
adamc@157 1619 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
adamc@157 1620 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
adamc@157 1621 | DConstraint _ => env
adamc@157 1622 | DExport _ => env
adamc@707 1623 | DTable (tn, x, n, c, _, pc, _, cc) =>
adamc@205 1624 let
adamc@705 1625 val ct = (CModProj (tn, [], "sql_table"), loc)
adamc@705 1626 val ct = (CApp (ct, c), loc)
adamc@707 1627 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@338 1628 in
adamc@705 1629 pushENamedAs env x n ct
adamc@338 1630 end
adamc@338 1631 | DSequence (tn, x, n) =>
adamc@338 1632 let
adamc@338 1633 val t = (CModProj (tn, [], "sql_sequence"), loc)
adamc@205 1634 in
adamc@205 1635 pushENamedAs env x n t
adamc@205 1636 end
adamc@754 1637 | DView (tn, x, n, _, c) =>
adamc@754 1638 let
adamc@754 1639 val ct = (CModProj (tn, [], "sql_view"), loc)
adamc@754 1640 val ct = (CApp (ct, c), loc)
adamc@754 1641 in
adamc@754 1642 pushENamedAs env x n ct
adamc@754 1643 end
adamc@563 1644 | DClass (x, n, k, c) =>
adamc@213 1645 let
adamc@563 1646 val k = (KArrow (k, (KType, loc)), loc)
adamc@213 1647 val env = pushCNamedAs env x n k (SOME c)
adamc@213 1648 in
adamc@213 1649 pushClass env n
adamc@213 1650 end
adamc@271 1651 | DDatabase _ => env
adamc@459 1652 | DCookie (tn, x, n, c) =>
adamc@459 1653 let
adamc@459 1654 val t = (CApp ((CModProj (tn, [], "cookie"), loc), c), loc)
adamc@459 1655 in
adamc@459 1656 pushENamedAs env x n t
adamc@459 1657 end
adamc@720 1658 | DStyle (tn, x, n) =>
adamc@718 1659 let
adamc@720 1660 val t = (CModProj (tn, [], "css_class"), loc)
adamc@718 1661 in
adamc@718 1662 pushENamedAs env x n t
adamc@718 1663 end
adamc@1075 1664 | DTask _ => env
adamc@1199 1665 | DPolicy _ => env
adam@1294 1666 | DOnError _ => env
adamc@157 1667
adamc@2 1668 end