Mercurial > urweb

annotate src/elab_env.sml @ 709:0406e9cccb72

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