summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-22 19:10:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-22 19:10:38 -0400
commite4a1bf8af62cb275bf5f5ae2f83b7197b1b58461 (patch)
treef3be22e5bbf731f7e45263b40f58a3cf5be686ea /src/elab_util.sml
parent5eee5f4a3b11c467c853f8397c7f679e5d5acc7a (diff)
Subsignatures
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml10
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' =>