Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

T1169 #1171

Merged
merged 15 commits into from
Apr 23, 2021
Merged

T1169 #1171

Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions src/Cryptol/ModuleSystem/NamingEnv.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.ModuleSystem.NamingEnv where

import Data.List (nub)
Expand Down Expand Up @@ -106,6 +107,11 @@ merge :: [Name] -> [Name] -> [Name]
merge xs ys | xs == ys = xs
| otherwise = nub (xs ++ ys)

instance PP NamingEnv where
ppPrec _ (NamingEnv mps) = vcat $ map ppNS $ Map.toList mps
where ppNS (ns,xs) = pp ns $$ nest 2 (vcat (map ppNm (Map.toList xs)))
ppNm (x,as) = pp x <+> "->" <+> hsep (punctuate comma (map pp as))

-- | Generate a mapping from 'PrimIdent' to 'Name' for a
-- given naming environment.
toPrimMap :: NamingEnv -> PrimMap
Expand Down
4 changes: 3 additions & 1 deletion src/Cryptol/ModuleSystem/Renamer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -161,8 +161,10 @@ renameModule' thisNested env mpath m =
allImps = openLoop allNested env openDs imps

(inScope,decls') <-
shadowNames allImps $
robdockins marked this conversation as resolved.
Show resolved Hide resolved
shadowNames' CheckNone allImps $
shadowNames' CheckOverlap env $
-- maybe we should allow for a warning
-- if a local name shadows an imported one?
do inScope <- getNamingEnv
ds <- renameTopDecls' (allNested,mpath) (mDecls m)
pure (inScope, ds)
Expand Down
10 changes: 8 additions & 2 deletions src/Cryptol/ModuleSystem/Renamer/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -250,10 +250,16 @@ checkEnv check (NamingEnv lenv) r rw0

where
newEnv = NamingEnv newMap
(rwFin,newMap) = Map.mapAccumWithKey doNS rw0 lenv
(rwFin,newMap) = Map.mapAccumWithKey doNS rw0 lenv -- lenv 1 ns at a time
doNS rw ns = Map.mapAccumWithKey (step ns) rw

step ns acc k xs = (acc', [head xs])
-- namespace, current state, k : parse name, xs : possible entities for k
robdockins marked this conversation as resolved.
Show resolved Hide resolved
step ns acc k xs = (acc', case check of
CheckNone -> xs
_ -> [head xs]
-- we've already reported an overlap error,
-- so resolve arbitrarily to the first entry
)
where
acc' = acc
{ rwWarnings =
Expand Down
1 change: 1 addition & 0 deletions tests/modsys/T15.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
:module T15::B
4 changes: 4 additions & 0 deletions tests/modsys/T15.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Loading module Cryptol
Loading module Cryptol
Loading module T15::A
Loading module T15::B
5 changes: 5 additions & 0 deletions tests/modsys/T15/A.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module T15::A where

update = 0x02


3 changes: 3 additions & 0 deletions tests/modsys/T15/B.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module T15::B where

import T15::A
1 change: 1 addition & 0 deletions tests/modsys/T16.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
:module T16::B
9 changes: 9 additions & 0 deletions tests/modsys/T16.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Loading module Cryptol
Loading module Cryptol
Loading module T16::A
Loading module T16::B

[error] at ./T16/B.cry:5:5--5:11
Multiple definitions for symbol: update
(at Cryptol:844:11--844:17, update)
(at ./T16/A.cry:3:1--3:7, T16::A::update)
5 changes: 5 additions & 0 deletions tests/modsys/T16/A.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module T16::A where

update = 0x02


5 changes: 5 additions & 0 deletions tests/modsys/T16/B.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module T16::B where

import T16::A

f = update
1 change: 1 addition & 0 deletions tests/modsys/T17.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
:module T17::B
5 changes: 5 additions & 0 deletions tests/modsys/T17.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Loading module Cryptol
Loading module Cryptol
Loading module T17::A
Loading module T17::A1
Loading module T17::B
5 changes: 5 additions & 0 deletions tests/modsys/T17/A.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module T17::A where

u = 0x02


5 changes: 5 additions & 0 deletions tests/modsys/T17/A1.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module T17::A1 where

u = 0x03


4 changes: 4 additions & 0 deletions tests/modsys/T17/B.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module T17::B where

import T17::A
import T17::A1
1 change: 1 addition & 0 deletions tests/modsys/T18.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
:module T18::B
10 changes: 10 additions & 0 deletions tests/modsys/T18.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
Loading module Cryptol
Loading module Cryptol
Loading module T18::A
Loading module T18::A1
Loading module T18::B

[error] at ./T18/B.cry:6:5--6:6
Multiple definitions for symbol: u
(at ./T18/A.cry:3:1--3:2, T18::A::u)
(at ./T18/A1.cry:3:1--3:2, T18::A1::u)
5 changes: 5 additions & 0 deletions tests/modsys/T18/A.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module T18::A where

u = 0x02


5 changes: 5 additions & 0 deletions tests/modsys/T18/A1.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module T18::A1 where

u = 0x03


6 changes: 6 additions & 0 deletions tests/modsys/T18/B.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
module T18::B where

import T18::A
import T18::A1

f = u
9 changes: 0 additions & 9 deletions tests/modsys/nested/T15.icry.stdout
Original file line number Diff line number Diff line change
@@ -1,15 +1,6 @@
Loading module Cryptol
Loading module Cryptol
Loading module T15
[warning] at T15.cry:5:13--5:14
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure how I feel about losing these warnings. What do you think?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wondered about that too. More generally, I wonder if we should issue a warning when a local name shadows an imported name. This is what the comment on line 166 of Renamer.hs is about.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I feel like it probably makes sense to do that, controlled by the warnShadowing option.

This binding for `A` shadows the existing binding at
T15.cry:3:11--3:12
[warning] at T15.cry:7:15--7:16
This binding for `A` shadows the existing binding at
T15.cry:5:13--5:14
[warning] at T15.cry:7:15--7:16
This binding for `A::A` shadows the existing binding at
T15.cry:5:13--5:14
Showing a specific instance of polymorphic result:
* Using 'Integer' for 1st type argument of 'T15::A::A::y'
2