Mercurial > urweb
changeset 64:d609820c5834
Proper hiding of shadowed bindings in principal signatures
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 26 Jun 2008 08:54:49 -0400 |
| parents | c5a503ad0d8c |
| children | 2adb20eebee3 |
| files | src/elaborate.sml src/expl.sml src/expl_env.sml src/expl_print.sml src/expl_util.sig src/expl_util.sml src/explify.sml tests/strdupe.lac |
| diffstat | 8 files changed, 90 insertions(+), 37 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Sun Jun 22 20:11:59 2008 -0400 +++ b/src/elaborate.sml Thu Jun 26 08:54:49 2008 -0400 @@ -1580,37 +1580,60 @@ val sgis = map sgiOfDecl ds' val (sgis, _, _, _, _) = - foldr (fn (sgall as (sgi, loc), (sgis, cons, vals, sgns, strs)) => + foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) => case sgi of - L'.SgiConAbs (x, _, _) => - (if SS.member (cons, x) then - sgnError env (DuplicateCon (loc, x)) - else - (); - (sgall :: sgis, SS.add (cons, x), vals, sgns, strs)) - | L'.SgiCon (x, _, _, _) => - (if SS.member (cons, x) then - sgnError env (DuplicateCon (loc, x)) - else - (); - (sgall :: sgis, SS.add (cons, x), vals, sgns, strs)) - | L'.SgiVal (x, _, _) => - if SS.member (vals, x) then - (sgis, cons, vals, sgns, strs) - else - (sgall :: sgis, cons, SS.add (vals, x), sgns, strs) - | L'.SgiSgn (x, _, _) => - (if SS.member (sgns, x) then - sgnError env (DuplicateSgn (loc, x)) - else - (); - (sgall :: sgis, cons, vals, SS.add (sgns, x), strs)) - | L'.SgiStr (x, _, _) => - (if SS.member (strs, x) then - sgnError env (DuplicateStr (loc, x)) - else - (); - (sgall :: sgis, cons, vals, sgns, SS.add (strs, x)))) + L'.SgiConAbs (x, n, k) => + let + val (cons, x) = + if SS.member (cons, x) then + (cons, "?" ^ x) + else + (SS.add (cons, x), x) + in + ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs) + end + | L'.SgiCon (x, n, k, c) => + let + val (cons, x) = + if SS.member (cons, x) then + (cons, "?" ^ x) + else + (SS.add (cons, x), x) + in + ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) + end + | L'.SgiVal (x, n, c) => + let + val (vals, x) = + if SS.member (vals, x) then + (vals, "?" ^ x) + else + (SS.add (vals, x), x) + in + ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs) + end + | L'.SgiSgn (x, n, sgn) => + let + val (sgns, x) = + if SS.member (sgns, x) then + (sgns, "?" ^ x) + else + (SS.add (sgns, x), x) + in + ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) + end + + | L'.SgiStr (x, n, sgn) => + let + val (strs, x) = + if SS.member (strs, x) then + (strs, "?" ^ x) + else + (SS.add (strs, x), x) + in + ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) + end) + ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis in ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc))
--- a/src/expl.sml Sun Jun 22 20:11:59 2008 -0400 +++ b/src/expl.sml Thu Jun 26 08:54:49 2008 -0400 @@ -74,6 +74,7 @@ SgiConAbs of string * int * kind | SgiCon of string * int * kind * con | SgiVal of string * int * con + | SgiSgn of string * int * sgn | SgiStr of string * int * sgn and sgn' = @@ -81,6 +82,7 @@ | SgnVar of int | SgnFun of string * int * sgn * sgn | SgnWhere of sgn * string * con + | SgnProj of int * string list * string withtype sgn_item = sgn_item' located and sgn = sgn' located
--- a/src/expl_env.sml Sun Jun 22 20:11:59 2008 -0400 +++ b/src/expl_env.sml Thu Jun 26 08:54:49 2008 -0400 @@ -249,6 +249,7 @@ SgiConAbs (x, n, k) => pushCNamed env x n k NONE | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) | SgiVal (x, n, t) => pushENamed env x n t + | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn | SgiStr (x, n, sgn) => pushStrNamed env x n sgn end
--- a/src/expl_print.sml Sun Jun 22 20:11:59 2008 -0400 +++ b/src/expl_print.sml Thu Jun 26 08:54:49 2008 -0400 @@ -277,6 +277,13 @@ string ":", space, p_sgn env sgn] + | SgiSgn (x, n, sgn) => box [string "signature", + space, + p_named x n, + space, + string "=", + space, + p_sgn env sgn] and p_sgn env (sgn, _) = case sgn of @@ -317,6 +324,17 @@ string "=", space, p_con env c] + | SgnProj (m1, ms, x) => + let + val (m1x, sgn) = E.lookupStrNamed env m1 + + val m1s = if !debug then + m1x ^ "__" ^ Int.toString m1 + else + m1x + in + p_list_sep (string ".") string (m1x :: ms @ [x]) + end fun p_decl env ((d, _) : decl) = case d of
--- a/src/expl_util.sig Sun Jun 22 20:11:59 2008 -0400 +++ b/src/expl_util.sig Thu Jun 26 08:54:49 2008 -0400 @@ -82,6 +82,7 @@ datatype binder = RelC of string * Expl.kind | NamedC of string * Expl.kind + | Sgn of string * Expl.sgn | Str of string * Expl.sgn val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
--- a/src/expl_util.sml Sun Jun 22 20:11:59 2008 -0400 +++ b/src/expl_util.sml Thu Jun 26 08:54:49 2008 -0400 @@ -294,6 +294,7 @@ 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 @@ 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 @@ 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 @@ S.map2 (con ctx c, fn c' => (SgnWhere (sgn', x, c'), loc))) + | SgnProj _ => S.return2 sAll in sg end
--- a/src/explify.sml Sun Jun 22 20:11:59 2008 -0400 +++ b/src/explify.sml Thu Jun 26 08:54:49 2008 -0400 @@ -87,7 +87,7 @@ | L.SgiCon (x, n, k, c) => (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) | L.SgiVal (x, n, c) => (L'.SgiVal (x, n, explifyCon c), loc) | L.SgiStr (x, n, sgn) => (L'.SgiStr (x, n, explifySgn sgn), loc) - | L.SgiSgn _ => raise Fail "Explify SgiSgn" + | L.SgiSgn (x, n, sgn) => (L'.SgiSgn (x, n, explifySgn sgn), loc) and explifySgn (sgn, loc) = case sgn of @@ -95,7 +95,7 @@ | L.SgnVar n => (L'.SgnVar n, loc) | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc) | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc) - | L.SgnProj _ => raise Fail "Explify SgnProj" + | L.SgnProj x => (L'.SgnProj x, loc) | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) fun explifyDecl (d, loc : EM.span) =
--- a/tests/strdupe.lac Sun Jun 22 20:11:59 2008 -0400 +++ b/tests/strdupe.lac Thu Jun 26 08:54:49 2008 -0400 @@ -1,11 +1,11 @@ val x = 0 -val x = 1 +val x = x type t = int -(*type t = int*) +type t = { A : t } signature S = sig end -(*signature S = sig end*) +signature S = sig type t structure M : S end structure S = struct end -(*structure S = struct end*) +structure S : S = struct type t = int structure M = S end