Mercurial > urweb

comparison src/elab_util.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 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} =