Mercurial > urweb
comparison src/elab_util.sml @ 88:7bab29834cd6
Constraints in modules
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jul 2008 15:58:02 -0400 |
parents | 1f85890c9846 |
children | f0f59e918cac |
comparison
equal
deleted
inserted
replaced
87:275aaeb73f1f | 88:7bab29834cd6 |
---|---|
377 (SgiStr (x, n, s'), loc)) | 377 (SgiStr (x, n, s'), loc)) |
378 | SgiSgn (x, n, s) => | 378 | SgiSgn (x, n, s) => |
379 S.map2 (sg ctx s, | 379 S.map2 (sg ctx s, |
380 fn s' => | 380 fn s' => |
381 (SgiSgn (x, n, s'), loc)) | 381 (SgiSgn (x, n, s'), loc)) |
382 | SgiConstraint (c1, c2) => | |
383 S.bind2 (con ctx c1, | |
384 fn c1' => | |
385 S.map2 (con ctx c2, | |
386 fn c2' => | |
387 (SgiConstraint (c1', c2'), loc))) | |
382 | 388 |
383 and sg ctx s acc = | 389 and sg ctx s acc = |
384 S.bindP (sg' ctx s acc, sgn ctx) | 390 S.bindP (sg' ctx s acc, sgn ctx) |
385 | 391 |
386 and sg' ctx (sAll as (s, loc)) = | 392 and sg' ctx (sAll as (s, loc)) = |
394 bind (ctx, NamedC (x, k)) | 400 bind (ctx, NamedC (x, k)) |
395 | SgiVal _ => ctx | 401 | SgiVal _ => ctx |
396 | SgiStr (x, _, sgn) => | 402 | SgiStr (x, _, sgn) => |
397 bind (ctx, Str (x, sgn)) | 403 bind (ctx, Str (x, sgn)) |
398 | SgiSgn (x, _, sgn) => | 404 | SgiSgn (x, _, sgn) => |
399 bind (ctx, Sgn (x, sgn)), | 405 bind (ctx, Sgn (x, sgn)) |
406 | SgiConstraint _ => ctx, | |
400 sgi ctx si)) ctx sgis, | 407 sgi ctx si)) ctx sgis, |
401 fn sgis' => | 408 fn sgis' => |
402 (SgnConst sgis', loc)) | 409 (SgnConst sgis', loc)) |
403 | 410 |
404 | SgnVar _ => S.return2 sAll | 411 | SgnVar _ => S.return2 sAll |
500 | DSgn (x, _, sgn) => | 507 | DSgn (x, _, sgn) => |
501 bind (ctx, Sgn (x, sgn)) | 508 bind (ctx, Sgn (x, sgn)) |
502 | DStr (x, _, sgn, _) => | 509 | DStr (x, _, sgn, _) => |
503 bind (ctx, Str (x, sgn)) | 510 bind (ctx, Str (x, sgn)) |
504 | DFfiStr (x, _, sgn) => | 511 | DFfiStr (x, _, sgn) => |
505 bind (ctx, Str (x, sgn)), | 512 bind (ctx, Str (x, sgn)) |
513 | DConstraint _ => ctx, | |
506 mfd ctx d)) ctx ds, | 514 mfd ctx d)) ctx ds, |
507 fn ds' => (StrConst ds', loc)) | 515 fn ds' => (StrConst ds', loc)) |
508 | StrVar _ => S.return2 strAll | 516 | StrVar _ => S.return2 strAll |
509 | StrProj (str, x) => | 517 | StrProj (str, x) => |
510 S.map2 (mfst ctx str, | 518 S.map2 (mfst ctx str, |
555 (DStr (x, n, sgn', str'), loc))) | 563 (DStr (x, n, sgn', str'), loc))) |
556 | DFfiStr (x, n, sgn) => | 564 | DFfiStr (x, n, sgn) => |
557 S.map2 (mfsg ctx sgn, | 565 S.map2 (mfsg ctx sgn, |
558 fn sgn' => | 566 fn sgn' => |
559 (DFfiStr (x, n, sgn'), loc)) | 567 (DFfiStr (x, n, sgn'), loc)) |
568 | DConstraint (c1, c2) => | |
569 S.bind2 (mfc ctx c1, | |
570 fn c1' => | |
571 S.map2 (mfc ctx c2, | |
572 fn c2' => | |
573 (DConstraint (c1', c2'), loc))) | |
560 in | 574 in |
561 mfd | 575 mfd |
562 end | 576 end |
563 | 577 |
564 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} = | 578 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} = |