Mercurial > urweb

annotate src/elab_env.sml @ 1244:1eedc9086e6c

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