diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-14 13:20:29 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-14 13:20:29 -0400 |
| commit | 25658a4755c86ffbda946fb8b97f882f3ce7a724 (patch) | |
| tree | 4ef4c28ab7483566127b841e2396bcc05d98e23d /src/elab_util.sml | |
| parent | 4a22e79410139a25a9615275c3b9adcd165a5988 (diff) | |
Parsing and elaborating 'table'
Diffstat (limited to 'src/elab_util.sml')
| -rw-r--r-- | src/elab_util.sml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml index 5fa0fa27..8cd02549 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -436,6 +436,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = S.map2 (con ctx c2, fn c2' => (SgiConstraint (c1', c2'), loc))) + | SgiTable (x, n, c) => + S.map2 (con ctx c, + fn c' => + (SgiTable (x, n, c'), loc)) and sg ctx s acc = S.bindP (sg' ctx s acc, sgn ctx) @@ -458,7 +462,8 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = bind (ctx, Str (x, sgn)) | SgiSgn (x, _, sgn) => bind (ctx, Sgn (x, sgn)) - | SgiConstraint _ => ctx, + | SgiConstraint _ => ctx + | SgiTable _ => ctx, sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -594,7 +599,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f | DFfiStr (x, _, sgn) => bind (ctx, Str (x, sgn)) | DConstraint _ => ctx - | DExport _ => ctx, + | DExport _ => ctx + | DTable _ => ctx, mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -682,6 +688,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f fn str' => (DExport (en, sgn', str'), loc))) + | DTable (x, n, c) => + S.map2 (mfc ctx c, + fn c' => + (DTable (x, n, c'), loc)) + and mfvi ctx (x, n, c, e) = S.bind2 (mfc ctx c, fn c' => |