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/elaborate.sml | 83 ++++++++++++++++++++++++++++++++++-------------------- src/expl.sml | 2 ++ src/expl_env.sml | 1 + src/expl_print.sml | 18 ++++++++++++ src/expl_util.sig | 1 + src/expl_util.sml | 10 ++++++- src/explify.sml | 4 +-- tests/strdupe.lac | 8 +++--- 8 files changed, 90 insertions(+), 37 deletions(-) diff --git a/src/elaborate.sml b/src/elaborate.sml index 64613703..d2d468db 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1580,37 +1580,60 @@ and elabStr env (str, loc) = 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)) diff --git a/src/expl.sml b/src/expl.sml index 49633d27..8e9bdfed 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -74,6 +74,7 @@ datatype sgn_item' = 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 @@ and sgn' = | 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 diff --git a/src/expl_env.sml b/src/expl_env.sml index b1bea90b..ad4ec00b 100644 --- a/src/expl_env.sml +++ b/src/expl_env.sml @@ -249,6 +249,7 @@ fun sgiBinds env (sgi, _) = 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 diff --git a/src/expl_print.sml b/src/expl_print.sml index 900a4063..aca89834 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -277,6 +277,13 @@ fun p_sgn_item env (sgi, _) = 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 @@ and p_sgn env (sgn, _) = 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 diff --git a/src/expl_util.sig b/src/expl_util.sig index 40ede9a4..2a6c7abe 100644 --- a/src/expl_util.sig +++ b/src/expl_util.sig @@ -82,6 +82,7 @@ structure Sgn : sig 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, 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 diff --git a/src/explify.sml b/src/explify.sml index 03744dba..0c3f5f1f 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -87,7 +87,7 @@ fun explifySgi (sgi, loc) = | 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 @@ and explifySgn (sgn, loc) = | 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) = diff --git a/tests/strdupe.lac b/tests/strdupe.lac index 834a48af..2a11aa51 100644 --- a/tests/strdupe.lac +++ b/tests/strdupe.lac @@ -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 -- cgit v1.2.3