Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- a/src/elab_util.sml Tue Jul 01 13:23:46 2008 -0400 +++ b/src/elab_util.sml Tue Jul 01 15:58:02 2008 -0400 @@ -379,6 +379,12 @@ S.map2 (sg ctx s, fn s' => (SgiSgn (x, n, s'), loc)) + | SgiConstraint (c1, c2) => + S.bind2 (con ctx c1, + fn c1' => + S.map2 (con ctx c2, + fn c2' => + (SgiConstraint (c1', c2'), loc))) and sg ctx s acc = S.bindP (sg' ctx s acc, sgn ctx) @@ -396,7 +402,8 @@ | SgiStr (x, _, sgn) => bind (ctx, Str (x, sgn)) | SgiSgn (x, _, sgn) => - bind (ctx, Sgn (x, sgn)), + bind (ctx, Sgn (x, sgn)) + | SgiConstraint _ => ctx, sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -502,7 +509,8 @@ | DStr (x, _, sgn, _) => bind (ctx, Str (x, sgn)) | DFfiStr (x, _, sgn) => - bind (ctx, Str (x, sgn)), + bind (ctx, Str (x, sgn)) + | DConstraint _ => ctx, mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -557,6 +565,12 @@ S.map2 (mfsg ctx sgn, fn sgn' => (DFfiStr (x, n, sgn'), loc)) + | DConstraint (c1, c2) => + S.bind2 (mfc ctx c1, + fn c1' => + S.map2 (mfc ctx c2, + fn c2' => + (DConstraint (c1', c2'), loc))) in mfd end