From aabe8dd88a80467442826e460e6b01f0dad2fb4d Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 26 Jun 2008 08:54:49 -0400 Subject: Proper hiding of shadowed bindings in principal signatures --- src/expl_util.sml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'src/expl_util.sml') diff --git a/src/expl_util.sml b/src/expl_util.sml index ebdd22d2..23329f3e 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -294,6 +294,7 @@ datatype binder = RelC of string * Expl.kind | NamedC of string * Expl.kind | Str of string * Expl.sgn + | Sgn of string * Expl.sgn fun mapfoldB {kind, con, sgn_item, sgn, bind} = let @@ -332,6 +333,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) @@ -347,7 +352,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)) @@ -366,6 +373,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = S.map2 (con ctx c, fn c' => (SgnWhere (sgn', x, c'), loc))) + | SgnProj _ => S.return2 sAll in sg end -- cgit v1.2.3