Skip to content

Commit

Permalink
Fixes #1169
Browse files Browse the repository at this point in the history
  • Loading branch information
yav committed Apr 20, 2021
1 parent ad6b125 commit 51e47ff
Show file tree
Hide file tree
Showing 21 changed files with 91 additions and 12 deletions.
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 $
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
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:846:11--846: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
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

0 comments on commit 51e47ff

Please sign in to comment.