Mercurial > urweb
comparison src/elab_env.sml @ 88:7bab29834cd6
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 |