This commit is contained in:
Iavor Diatchki 2021-04-20 13:52:09 -07:00
parent 3df9273041
commit 6818969db6
21 changed files with 91 additions and 12 deletions

View File

@ -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)

View File

@ -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 =

1
tests/modsys/T15.icry Normal file
View File

@ -0,0 +1 @@
:module T15::B

View File

@ -0,0 +1,4 @@
Loading module Cryptol
Loading module Cryptol
Loading module T15::A
Loading module T15::B

5
tests/modsys/T15/A.cry Normal file
View File

@ -0,0 +1,5 @@
module T15::A where
update = 0x02

3
tests/modsys/T15/B.cry Normal file
View File

@ -0,0 +1,3 @@
module T15::B where
import T15::A

1
tests/modsys/T16.icry Normal file
View File

@ -0,0 +1 @@
:module T16::B

View File

@ -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
tests/modsys/T16/A.cry Normal file
View File

@ -0,0 +1,5 @@
module T16::A where
update = 0x02

5
tests/modsys/T16/B.cry Normal file
View File

@ -0,0 +1,5 @@
module T16::B where
import T16::A
f = update

1
tests/modsys/T17.icry Normal file
View File

@ -0,0 +1 @@
:module T17::B

View File

@ -0,0 +1,5 @@
Loading module Cryptol
Loading module Cryptol
Loading module T17::A
Loading module T17::A1
Loading module T17::B

5
tests/modsys/T17/A.cry Normal file
View File

@ -0,0 +1,5 @@
module T17::A where
u = 0x02

5
tests/modsys/T17/A1.cry Normal file
View File

@ -0,0 +1,5 @@
module T17::A1 where
u = 0x03

4
tests/modsys/T17/B.cry Normal file
View File

@ -0,0 +1,4 @@
module T17::B where
import T17::A
import T17::A1

1
tests/modsys/T18.icry Normal file
View File

@ -0,0 +1 @@
:module T18::B

View File

@ -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
tests/modsys/T18/A.cry Normal file
View File

@ -0,0 +1,5 @@
module T18::A where
u = 0x02

5
tests/modsys/T18/A1.cry Normal file
View File

@ -0,0 +1,5 @@
module T18::A1 where
u = 0x03

6
tests/modsys/T18/B.cry Normal file
View File

@ -0,0 +1,6 @@
module T18::B where
import T18::A
import T18::A1
f = u

View File

@ -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