Mercurial > urweb

annotate src/elab_env.sml @ 109:813e5a52063d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove closure conversion in favor of zany fun with modules, which also replaces 'page'
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Jul 2008 10:17:06 -0400
parents f0f59e918cac
children e3041657d653
rev   line source
adamc@2 1 (* Copyright (c) 2008, 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@13 48 val liftConInCon =
adamc@13 49 U.Con.mapB {kind = fn k => k,
adamc@13 50 con = fn bound => fn c =>
adamc@13 51 case c of
adamc@16 52 CRel xn =>
adamc@13 53 if xn < bound then
adamc@13 54 c
adamc@13 55 else
adamc@16 56 CRel (xn + 1)
adamc@17 57 (*| CUnif _ => raise SynUnif*)
adamc@13 58 | _ => c,
adamc@13 59 bind = fn (bound, U.Con.Rel _) => bound + 1
adamc@13 60 | (bound, _) => bound}
adamc@13 61
adamc@13 62 val lift = liftConInCon 0
adamc@13 63
adamc@13 64
adamc@13 65 (* Back to environments *)
adamc@13 66
adamc@9 67 datatype 'a var' =
adamc@9 68 Rel' of int * 'a
adamc@9 69 | Named' of int * 'a
adamc@2 70
adamc@9 71 datatype 'a var =
adamc@9 72 NotBound
adamc@9 73 | Rel of int * 'a
adamc@9 74 | Named of int * 'a
adamc@2 75
adamc@2 76 type env = {
adamc@9 77 renameC : kind var' SM.map,
adamc@2 78 relC : (string * kind) list,
adamc@11 79 namedC : (string * kind * con option) IM.map,
adamc@9 80
adamc@9 81 renameE : con var' SM.map,
adamc@9 82 relE : (string * con) list,
adamc@31 83 namedE : (string * con) IM.map,
adamc@31 84
adamc@31 85 renameSgn : (int * sgn) SM.map,
adamc@31 86 sgn : (string * sgn) IM.map,
adamc@31 87
adamc@31 88 renameStr : (int * sgn) SM.map,
adamc@31 89 str : (string * sgn) IM.map
adamc@2 90 }
adamc@2 91
adamc@2 92 val namedCounter = ref 0
adamc@2 93
adamc@109 94 fun newNamed () =
adamc@109 95 let
adamc@109 96 val r = !namedCounter
adamc@109 97 in
adamc@109 98 namedCounter := r + 1;
adamc@109 99 r
adamc@109 100 end
adamc@109 101
adamc@2 102 val empty = {
adamc@2 103 renameC = SM.empty,
adamc@2 104 relC = [],
adamc@9 105 namedC = IM.empty,
adamc@9 106
adamc@9 107 renameE = SM.empty,
adamc@9 108 relE = [],
adamc@31 109 namedE = IM.empty,
adamc@31 110
adamc@31 111 renameSgn = SM.empty,
adamc@31 112 sgn = IM.empty,
adamc@31 113
adamc@31 114 renameStr = SM.empty,
adamc@31 115 str = IM.empty
adamc@2 116 }
adamc@2 117
adamc@2 118 fun pushCRel (env : env) x k =
adamc@2 119 let
adamc@9 120 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
adamc@2 121 | x => x) (#renameC env)
adamc@2 122 in
adamc@9 123 {renameC = SM.insert (renameC, x, Rel' (0, k)),
adamc@2 124 relC = (x, k) :: #relC env,
adamc@13 125 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
adamc@9 126
adamc@9 127 renameE = #renameE env,
adamc@13 128 relE = map (fn (x, c) => (x, lift c)) (#relE env),
adamc@31 129 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
adamc@31 130
adamc@31 131 renameSgn = #renameSgn env,
adamc@31 132 sgn = #sgn env,
adamc@31 133
adamc@31 134 renameStr = #renameStr env,
adamc@31 135 str = #str env
adamc@31 136 }
adamc@2 137 end
adamc@2 138
adamc@2 139 fun lookupCRel (env : env) n =
adamc@2 140 (List.nth (#relC env, n))
adamc@2 141 handle Subscript => raise UnboundRel n
adamc@2 142
adamc@11 143 fun pushCNamedAs (env : env) x n k co =
adamc@9 144 {renameC = SM.insert (#renameC env, x, Named' (n, k)),
adamc@5 145 relC = #relC env,
adamc@11 146 namedC = IM.insert (#namedC env, n, (x, k, co)),
adamc@9 147
adamc@9 148 renameE = #renameE env,
adamc@9 149 relE = #relE env,
adamc@31 150 namedE = #namedE env,
adamc@31 151
adamc@31 152 renameSgn = #renameSgn env,
adamc@31 153 sgn = #sgn env,
adamc@31 154
adamc@31 155 renameStr = #renameStr env,
adamc@31 156 str = #str env}
adamc@5 157
adamc@11 158 fun pushCNamed env x k co =
adamc@2 159 let
adamc@2 160 val n = !namedCounter
adamc@2 161 in
adamc@2 162 namedCounter := n + 1;
adamc@11 163 (pushCNamedAs env x n k co, n)
adamc@2 164 end
adamc@2 165
adamc@2 166 fun lookupCNamed (env : env) n =
adamc@2 167 case IM.find (#namedC env, n) of
adamc@2 168 NONE => raise UnboundNamed n
adamc@2 169 | SOME x => x
adamc@2 170
adamc@2 171 fun lookupC (env : env) x =
adamc@2 172 case SM.find (#renameC env, x) of
adamc@9 173 NONE => NotBound
adamc@9 174 | SOME (Rel' x) => Rel x
adamc@9 175 | SOME (Named' x) => Named x
adamc@9 176
adamc@9 177 fun pushERel (env : env) x t =
adamc@9 178 let
adamc@9 179 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
adamc@9 180 | x => x) (#renameE env)
adamc@9 181 in
adamc@9 182 {renameC = #renameC env,
adamc@9 183 relC = #relC env,
adamc@9 184 namedC = #namedC env,
adamc@9 185
adamc@9 186 renameE = SM.insert (renameE, x, Rel' (0, t)),
adamc@9 187 relE = (x, t) :: #relE env,
adamc@31 188 namedE = #namedE env,
adamc@31 189
adamc@31 190 renameSgn = #renameSgn env,
adamc@31 191 sgn = #sgn env,
adamc@31 192
adamc@31 193 renameStr = #renameStr env,
adamc@31 194 str = #str env}
adamc@9 195 end
adamc@9 196
adamc@9 197 fun lookupERel (env : env) n =
adamc@9 198 (List.nth (#relE env, n))
adamc@9 199 handle Subscript => raise UnboundRel n
adamc@9 200
adamc@9 201 fun pushENamedAs (env : env) x n t =
adamc@9 202 {renameC = #renameC env,
adamc@9 203 relC = #relC env,
adamc@9 204 namedC = #namedC env,
adamc@9 205
adamc@9 206 renameE = SM.insert (#renameE env, x, Named' (n, t)),
adamc@9 207 relE = #relE env,
adamc@31 208 namedE = IM.insert (#namedE env, n, (x, t)),
adamc@31 209
adamc@31 210 renameSgn = #renameSgn env,
adamc@31 211 sgn = #sgn env,
adamc@31 212
adamc@31 213 renameStr = #renameStr env,
adamc@31 214 str = #str env}
adamc@9 215
adamc@9 216 fun pushENamed env x t =
adamc@9 217 let
adamc@9 218 val n = !namedCounter
adamc@9 219 in
adamc@9 220 namedCounter := n + 1;
adamc@9 221 (pushENamedAs env x n t, n)
adamc@9 222 end
adamc@9 223
adamc@9 224 fun lookupENamed (env : env) n =
adamc@9 225 case IM.find (#namedE env, n) of
adamc@9 226 NONE => raise UnboundNamed n
adamc@9 227 | SOME x => x
adamc@9 228
adamc@9 229 fun lookupE (env : env) x =
adamc@9 230 case SM.find (#renameE env, x) of
adamc@9 231 NONE => NotBound
adamc@9 232 | SOME (Rel' x) => Rel x
adamc@9 233 | SOME (Named' x) => Named x
adamc@2 234
adamc@31 235 fun pushSgnNamedAs (env : env) x n sgis =
adamc@31 236 {renameC = #renameC env,
adamc@31 237 relC = #relC env,
adamc@31 238 namedC = #namedC env,
adamc@31 239
adamc@31 240 renameE = #renameE env,
adamc@31 241 relE = #relE env,
adamc@31 242 namedE = #namedE env,
adamc@31 243
adamc@31 244 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
adamc@31 245 sgn = IM.insert (#sgn env, n, (x, sgis)),
adamc@31 246
adamc@31 247 renameStr = #renameStr env,
adamc@31 248 str = #str env}
adamc@31 249
adamc@31 250 fun pushSgnNamed env x sgis =
adamc@31 251 let
adamc@31 252 val n = !namedCounter
adamc@31 253 in
adamc@31 254 namedCounter := n + 1;
adamc@31 255 (pushSgnNamedAs env x n sgis, n)
adamc@31 256 end
adamc@31 257
adamc@31 258 fun lookupSgnNamed (env : env) n =
adamc@31 259 case IM.find (#sgn env, n) of
adamc@31 260 NONE => raise UnboundNamed n
adamc@31 261 | SOME x => x
adamc@31 262
adamc@31 263 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
adamc@31 264
adamc@31 265 fun pushStrNamedAs (env : env) x n sgis =
adamc@31 266 {renameC = #renameC env,
adamc@31 267 relC = #relC env,
adamc@31 268 namedC = #namedC env,
adamc@31 269
adamc@31 270 renameE = #renameE env,
adamc@31 271 relE = #relE env,
adamc@31 272 namedE = #namedE env,
adamc@31 273
adamc@31 274 renameSgn = #renameSgn env,
adamc@31 275 sgn = #sgn env,
adamc@31 276
adamc@31 277 renameStr = SM.insert (#renameStr env, x, (n, sgis)),
adamc@31 278 str = IM.insert (#str env, n, (x, sgis))}
adamc@31 279
adamc@31 280 fun pushStrNamed env x sgis =
adamc@31 281 let
adamc@31 282 val n = !namedCounter
adamc@31 283 in
adamc@31 284 namedCounter := n + 1;
adamc@31 285 (pushStrNamedAs env x n sgis, n)
adamc@31 286 end
adamc@31 287
adamc@31 288 fun lookupStrNamed (env : env) n =
adamc@31 289 case IM.find (#str env, n) of
adamc@31 290 NONE => raise UnboundNamed n
adamc@31 291 | SOME x => x
adamc@31 292
adamc@31 293 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
adamc@31 294
adamc@13 295 fun declBinds env (d, _) =
adamc@13 296 case d of
adamc@13 297 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@13 298 | DVal (x, n, t, _) => pushENamedAs env x n t
adamc@31 299 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
adamc@31 300 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
adamc@48 301 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
adamc@88 302 | DConstraint _ => env
adamc@109 303 | DExport _ => env
adamc@31 304
adamc@31 305 fun sgiBinds env (sgi, _) =
adamc@31 306 case sgi of
adamc@31 307 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
adamc@31 308 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
adamc@31 309 | SgiVal (x, n, t) => pushENamedAs env x n t
adamc@31 310 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
adamc@59 311 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
adamc@88 312 | SgiConstraint _ => env
adamc@31 313
adamc@34 314 fun sgnSeek f sgis =
adamc@34 315 let
adamc@59 316 fun seek (sgis, sgns, strs, cons) =
adamc@34 317 case sgis of
adamc@34 318 [] => NONE
adamc@34 319 | (sgi, _) :: sgis =>
adamc@34 320 case f sgi of
adamc@59 321 SOME v => SOME (v, (sgns, strs, cons))
adamc@88 322 | NONE =>
adamc@88 323 case sgi of
adamc@88 324 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
adamc@88 325 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
adamc@88 326 | SgiVal _ => seek (sgis, sgns, strs, cons)
adamc@88 327 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
adamc@88 328 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
adamc@88 329 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
adamc@34 330 in
adamc@59 331 seek (sgis, IM.empty, IM.empty, IM.empty)
adamc@34 332 end
adamc@34 333
adamc@34 334 fun id x = x
adamc@34 335
adamc@34 336 fun unravelStr (str, _) =
adamc@34 337 case str of
adamc@34 338 StrVar x => (x, [])
adamc@34 339 | StrProj (str, m) =>
adamc@34 340 let
adamc@34 341 val (x, ms) = unravelStr str
adamc@34 342 in
adamc@34 343 (x, ms @ [m])
adamc@34 344 end
adamc@34 345 | _ => raise Fail "unravelStr"
adamc@34 346
adamc@59 347 fun sgnS_con (str, (sgns, strs, cons)) c =
adamc@34 348 case c of
adamc@34 349 CModProj (m1, ms, x) =>
adamc@34 350 (case IM.find (strs, m1) of
adamc@34 351 NONE => c
adamc@34 352 | SOME m1x =>
adamc@34 353 let
adamc@34 354 val (m1, ms') = unravelStr str
adamc@34 355 in
adamc@34 356 CModProj (m1, ms' @ m1x :: ms, x)
adamc@34 357 end)
adamc@34 358 | CNamed n =>
adamc@34 359 (case IM.find (cons, n) of
adamc@34 360 NONE => c
adamc@34 361 | SOME nx =>
adamc@34 362 let
adamc@34 363 val (m1, ms) = unravelStr str
adamc@34 364 in
adamc@34 365 CModProj (m1, ms, nx)
adamc@34 366 end)
adamc@34 367 | _ => c
adamc@34 368
adamc@59 369 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
adamc@59 370 case sgn of
adamc@59 371 SgnProj (m1, ms, x) =>
adamc@59 372 (case IM.find (strs, m1) of
adamc@59 373 NONE => sgn
adamc@59 374 | SOME m1x =>
adamc@59 375 let
adamc@59 376 val (m1, ms') = unravelStr str
adamc@59 377 in
adamc@59 378 SgnProj (m1, ms' @ m1x :: ms, x)
adamc@59 379 end)
adamc@59 380 | SgnVar n =>
adamc@59 381 (case IM.find (sgns, n) of
adamc@59 382 NONE => sgn
adamc@59 383 | SOME nx =>
adamc@59 384 let
adamc@59 385 val (m1, ms) = unravelStr str
adamc@59 386 in
adamc@59 387 SgnProj (m1, ms, nx)
adamc@59 388 end)
adamc@59 389 | _ => sgn
adamc@59 390
adamc@59 391 fun sgnSubCon x =
adamc@34 392 ElabUtil.Con.map {kind = id,
adamc@59 393 con = sgnS_con x}
adamc@34 394
adamc@59 395 fun sgnSubSgn x =
adamc@34 396 ElabUtil.Sgn.map {kind = id,
adamc@59 397 con = sgnS_con x,
adamc@34 398 sgn_item = id,
adamc@59 399 sgn = sgnS_sgn x}
adamc@34 400
adamc@42 401 fun hnormSgn env (all as (sgn, loc)) =
adamc@34 402 case sgn of
adamc@42 403 SgnError => all
adamc@42 404 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
adamc@42 405 | SgnConst _ => all
adamc@42 406 | SgnFun _ => all
adamc@59 407 | SgnProj (m, ms, x) =>
adamc@59 408 let
adamc@59 409 val (_, sgn) = lookupStrNamed env m
adamc@59 410 in
adamc@59 411 case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms,
adamc@59 412 sgn = sgn,
adamc@59 413 field = x} of
adamc@59 414 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
adamc@59 415 | SOME sgn => sgn
adamc@59 416 end
adamc@42 417 | SgnWhere (sgn, x, c) =>
adamc@42 418 case #1 (hnormSgn env sgn) of
adamc@42 419 SgnError => (SgnError, loc)
adamc@42 420 | SgnConst sgis =>
adamc@42 421 let
adamc@42 422 fun traverse (pre, post) =
adamc@42 423 case post of
adamc@42 424 [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
adamc@42 425 | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
adamc@42 426 if x = x' then
adamc@42 427 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
adamc@42 428 else
adamc@42 429 traverse (sgi :: pre, rest)
adamc@42 430 | sgi :: rest => traverse (sgi :: pre, rest)
adamc@42 431
adamc@42 432 val sgis = traverse ([], sgis)
adamc@42 433 in
adamc@42 434 (SgnConst sgis, loc)
adamc@42 435 end
adamc@42 436 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
adamc@42 437
adamc@59 438 and projectSgn env {sgn, str, field} =
adamc@59 439 case #1 (hnormSgn env sgn) of
adamc@59 440 SgnConst sgis =>
adamc@59 441 (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
adamc@59 442 NONE => NONE
adamc@59 443 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
adamc@59 444 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
adamc@59 445 | _ => NONE
adamc@59 446
adamc@59 447 fun projectStr env {sgn, str, field} =
adamc@59 448 case #1 (hnormSgn env sgn) of
adamc@59 449 SgnConst sgis =>
adamc@59 450 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
adamc@59 451 NONE => NONE
adamc@59 452 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
adamc@59 453 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
adamc@59 454 | _ => NONE
adamc@59 455
adamc@42 456 fun projectCon env {sgn, str, field} =
adamc@42 457 case #1 (hnormSgn env sgn) of
adamc@34 458 SgnConst sgis =>
adamc@34 459 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
adamc@34 460 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
adamc@34 461 | _ => NONE) sgis of
adamc@34 462 NONE => NONE
adamc@34 463 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
adamc@34 464 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
adamc@42 465 | _ => NONE
adamc@34 466
adamc@42 467 fun projectVal env {sgn, str, field} =
adamc@42 468 case #1 (hnormSgn env sgn) of
adamc@34 469 SgnConst sgis =>
adamc@34 470 (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of
adamc@34 471 NONE => NONE
adamc@34 472 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
adamc@34 473 | SgnError => SOME (CError, ErrorMsg.dummySpan)
adamc@42 474 | _ => NONE
adamc@34 475
adamc@88 476 fun sgnSeekConstraints (str, sgis) =
adamc@88 477 let
adamc@88 478 fun seek (sgis, sgns, strs, cons, acc) =
adamc@88 479 case sgis of
adamc@88 480 [] => acc
adamc@88 481 | (sgi, _) :: sgis =>
adamc@88 482 case sgi of
adamc@88 483 SgiConstraint (c1, c2) =>
adamc@88 484 let
adamc@88 485 val sub = sgnSubCon (str, (sgns, strs, cons))
adamc@88 486 in
adamc@88 487 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
adamc@88 488 end
adamc@88 489 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 490 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
adamc@88 491 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
adamc@88 492 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
adamc@88 493 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
adamc@88 494 in
adamc@88 495 seek (sgis, IM.empty, IM.empty, IM.empty, [])
adamc@88 496 end
adamc@88 497
adamc@88 498 fun projectConstraints env {sgn, str} =
adamc@88 499 case #1 (hnormSgn env sgn) of
adamc@88 500 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
adamc@88 501 | SgnError => SOME []
adamc@88 502 | _ => NONE
adamc@34 503
adamc@2 504 end