From cdc1211c43e9073a4d03472ffb549c67df281cea Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 1 Jul 2008 15:58:02 -0400 Subject: Constraints in modules --- src/elab_util.sml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) (limited to 'src/elab_util.sml') diff --git a/src/elab_util.sml b/src/elab_util.sml index 65906c72..9879a9f9 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -379,6 +379,12 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = | 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f | 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 -- cgit v1.2.3