Mercurial > urweb

comparison src/elab_env.sml @ 88:7bab29834cd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Constraints in modules
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 15:58:02 -0400
parents abb2b32c19fb
children f0f59e918cac
comparison
equal deleted inserted replaced
87:275aaeb73f1f 88:7bab29834cd6
289 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 289 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
290 | DVal (x, n, t, _) => pushENamedAs env x n t 290 | DVal (x, n, t, _) => pushENamedAs env x n t
291 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 291 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
292 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn 292 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
293 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn 293 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
294 | DConstraint _ => env
294 295
295 fun sgiBinds env (sgi, _) = 296 fun sgiBinds env (sgi, _) =
296 case sgi of 297 case sgi of
297 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE 298 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
298 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 299 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
299 | SgiVal (x, n, t) => pushENamedAs env x n t 300 | SgiVal (x, n, t) => pushENamedAs env x n t
300 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 301 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
301 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 302 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
303 | SgiConstraint _ => env
302 304
303 fun sgnSeek f sgis = 305 fun sgnSeek f sgis =
304 let 306 let
305 fun seek (sgis, sgns, strs, cons) = 307 fun seek (sgis, sgns, strs, cons) =
306 case sgis of 308 case sgis of
307 [] => NONE 309 [] => NONE
308 | (sgi, _) :: sgis => 310 | (sgi, _) :: sgis =>
309 case f sgi of 311 case f sgi of
310 SOME v => SOME (v, (sgns, strs, cons)) 312 SOME v => SOME (v, (sgns, strs, cons))
311 | NONE => 313 | NONE =>
312 case sgi of 314 case sgi of
313 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 315 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
314 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 316 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
315 | SgiVal _ => seek (sgis, sgns, strs, cons) 317 | SgiVal _ => seek (sgis, sgns, strs, cons)
316 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) 318 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
317 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) 319 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
320 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
318 in 321 in
319 seek (sgis, IM.empty, IM.empty, IM.empty) 322 seek (sgis, IM.empty, IM.empty, IM.empty)
320 end 323 end
321 324
322 fun id x = x 325 fun id x = x
459 NONE => NONE 462 NONE => NONE
460 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)) 463 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
461 | SgnError => SOME (CError, ErrorMsg.dummySpan) 464 | SgnError => SOME (CError, ErrorMsg.dummySpan)
462 | _ => NONE 465 | _ => NONE
463 466
467 fun sgnSeekConstraints (str, sgis) =
468 let
469 fun seek (sgis, sgns, strs, cons, acc) =
470 case sgis of
471 [] => acc
472 | (sgi, _) :: sgis =>
473 case sgi of
474 SgiConstraint (c1, c2) =>
475 let
476 val sub = sgnSubCon (str, (sgns, strs, cons))
477 in
478 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
479 end
480 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
481 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
482 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
483 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
484 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
485 in
486 seek (sgis, IM.empty, IM.empty, IM.empty, [])
487 end
488
489 fun projectConstraints env {sgn, str} =
490 case #1 (hnormSgn env sgn) of
491 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
492 | SgnError => SOME []
493 | _ => NONE
464 494
465 end 495 end