Skip to content

Commit

Permalink
Merge pull request #1171 from GaloisInc/T1169
Browse files Browse the repository at this point in the history
T1169
  • Loading branch information
yav authored Apr 23, 2021
2 parents 9995513 + 5478037 commit 74c5f4e
Show file tree
Hide file tree
Showing 31 changed files with 126 additions and 21 deletions.
5 changes: 1 addition & 4 deletions .github/ci.sh
Original file line number Diff line number Diff line change
Expand Up @@ -134,10 +134,7 @@ install_system_deps() {
test_dist() {
setup_dist_bins
setup_external_tools
if $IS_WIN; then
echo "Warning: janky hacky workaround to #764"
sed -i 's!/!\\!g' tests/modsys/T14.icry.stdout
fi
echo "test-runner version: $($BIN/test-runner --version)"
$BIN/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol tests
}

Expand Down
2 changes: 1 addition & 1 deletion cabal.GHC-8.10.2.config
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ constraints: any.Cabal ==3.2.0.0,
any.test-framework ==0.8.2.0,
any.test-framework-hunit ==0.3.0.2,
test-framework-hunit -base3 +base4,
any.test-lib ==0.2.2,
any.test-lib ==0.3,
any.text ==1.2.4.1,
any.text-short ==0.1.3,
text-short -asserts,
Expand Down
2 changes: 1 addition & 1 deletion cabal.GHC-8.10.3.config
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,7 @@ constraints: any.Cabal ==3.2.1.0,
any.test-framework ==0.8.2.0,
any.test-framework-hunit ==0.3.0.2,
test-framework-hunit -base3 +base4,
any.test-lib ==0.2.2,
any.test-lib ==0.3,
any.text ==1.2.4.1,
any.text-short ==0.1.3,
text-short -asserts,
Expand Down
2 changes: 1 addition & 1 deletion cabal.GHC-8.6.5.config
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ constraints: any.Cabal ==2.4.0.1,
any.test-framework ==0.8.2.0,
any.test-framework-hunit ==0.3.0.2,
test-framework-hunit -base3 +base4,
any.test-lib ==0.2.1,
any.test-lib ==0.3,
any.text ==1.2.4.0,
any.tf-random ==0.5,
any.th-abstraction ==0.3.2.0,
Expand Down
2 changes: 1 addition & 1 deletion cabal.GHC-8.8.4.config
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ constraints: any.Cabal ==3.0.1.0,
any.test-framework ==0.8.2.0,
any.test-framework-hunit ==0.3.0.2,
test-framework-hunit -base3 +base4,
any.test-lib ==0.2.1,
any.test-lib ==0.3,
any.text ==1.2.4.0,
any.tf-random ==0.5,
any.th-abstraction ==0.3.2.0,
Expand Down
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 $
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
2 changes: 1 addition & 1 deletion tests/cryptol-test-runner.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ flag static

executable cryptol-test-runner
Main-is: Main.hs
build-depends: base,filepath,test-lib
build-depends: base,filepath,test-lib >= 0.3
GHC-options: -Wall -O2
Default-language: Haskell2010

Expand Down
4 changes: 4 additions & 0 deletions tests/modsys/T14.icry.stdout.mingw32
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Loading module Cryptol

Parse error at .\T14\Main.cry:3:9,
unexpected: MalformedUtf8
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)
9 changes: 9 additions & 0 deletions tests/modsys/T16.icry.stdout.mingw32
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)
10 changes: 10 additions & 0 deletions tests/modsys/T18.icry.stdout.mingw32
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 74c5f4e

Please sign in to comment.