diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-06-22 19:10:38 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-06-22 19:10:38 -0400 |
| commit | e4a1bf8af62cb275bf5f5ae2f83b7197b1b58461 (patch) | |
| tree | f3be22e5bbf731f7e45263b40f58a3cf5be686ea /src/elab_util.sml | |
| parent | 5eee5f4a3b11c467c853f8397c7f679e5d5acc7a (diff) | |
Subsignatures
Diffstat (limited to 'src/elab_util.sml')
| -rw-r--r-- | src/elab_util.sml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml index e112a180..2d075fb4 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -305,6 +305,7 @@ datatype binder = RelC of string * Elab.kind | NamedC of string * Elab.kind | Str of string * Elab.sgn + | Sgn of string * Elab.sgn fun mapfoldB {kind, con, sgn_item, sgn, bind} = let @@ -343,6 +344,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = S.map2 (sg ctx s, fn s' => (SgiStr (x, n, s'), loc)) + | SgiSgn (x, n, s) => + S.map2 (sg ctx s, + fn s' => + (SgiSgn (x, n, s'), loc)) and sg ctx s acc = S.bindP (sg' ctx s acc, sgn ctx) @@ -358,7 +363,9 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = bind (ctx, NamedC (x, k)) | SgiVal _ => ctx | SgiStr (x, _, sgn) => - bind (ctx, Str (x, sgn)), + bind (ctx, Str (x, sgn)) + | SgiSgn (x, _, sgn) => + bind (ctx, Sgn (x, sgn)), sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -370,6 +377,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = S.map2 (sg (bind (ctx, Str (m, s1'))) s2, fn s2' => (SgnFun (m, n, s1', s2'), loc))) + | SgnProj _ => S.return2 sAll | SgnWhere (sgn, x, c) => S.bind2 (sg ctx sgn, fn sgn' => |