Skip to content

Commit

Permalink
Things that depend on newtype constructors should depend on the newtypes
Browse files Browse the repository at this point in the history
Fixes #1511
  • Loading branch information
yav committed Mar 29, 2023
1 parent cb551e4 commit 05412e9
Show file tree
Hide file tree
Showing 4 changed files with 43 additions and 18 deletions.
44 changes: 26 additions & 18 deletions src/Cryptol/ModuleSystem/Renamer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -453,8 +453,16 @@ renameTopDecls' ds =


(noNameDs,nameDs) = partitionEithers (map topDeclName ds1)
ctrs = [ nm | (_,nm@(ConstratintAt {})) <- nameDs ]

ctrs = [ nm | (_,nm@(ConstratintAt {}),_) <- nameDs ]
indirect = Map.fromList [ (y,x)
| (_,x,ys) <- nameDs, y <- ys ]
mkDepName x = case Map.lookup x fromParams of
Just dn -> dn
Nothing -> NamedThing x
depsFor x =
[ Map.findWithDefault (mkDepName y) (NamedThing y) indirect
| y <- Set.toList (Map.findWithDefault Set.empty x deps)
]

{- See [NOTE: Dependencies on Top Level Constraints] -}
addCtr nm ctr =
Expand Down Expand Up @@ -493,15 +501,9 @@ renameTopDecls' ds =
Nothing -> []
_ -> []

mkDepName x = case Map.lookup x fromParams of
Just dn -> dn
Nothing -> NamedThing x

toNode (d,x) = ((d,x),x, addCtrs (d,x) ++
addModParams d ++
map mkDepName
( Set.toList
( Map.findWithDefault Set.empty x deps) ))
toNode (d,x,_) = ((d,x),x, addCtrs (d,x) ++
addModParams d ++
depsFor x)

ordered = stronglyConnComp (map toNode nameDs)
fromSCC x =
Expand Down Expand Up @@ -588,28 +590,32 @@ declName decl =
where
bad x = panic "declName" [x]

topDeclName :: TopDecl Name -> Either (TopDecl Name) (TopDecl Name, DepName)
topDeclName ::
TopDecl Name ->
Either (TopDecl Name) (TopDecl Name, DepName, [DepName])
topDeclName topDecl =
case topDecl of
Decl d -> hasName (declName (tlValue d))
DPrimType d -> hasName (thing (primTName (tlValue d)))
TDNewtype d -> hasName (thing (nName (tlValue d)))
TDNewtype d -> hasName' (thing (nName (tlValue d)))
[ nConName (tlValue d) ]
DModule d -> hasName (thing (mName m))
where NestedModule m = tlValue d

DInterfaceConstraint _ ds -> Right (topDecl, ConstratintAt (srcRange ds))
DInterfaceConstraint _ ds -> special (ConstratintAt (srcRange ds))

DImport {} -> noName

DModParam m -> Right ( topDecl
, ModParamName (srcRange (mpSignature m))
(mpName m))
DModParam m -> special (ModParamName (srcRange (mpSignature m))
(mpName m))

Include {} -> bad "Include"
DParamDecl {} -> bad "DParamDecl"
where
noName = Left topDecl
hasName n = Right (topDecl, NamedThing n)
hasName n = hasName' n []
hasName' n ms = Right (topDecl, NamedThing n, map NamedThing ms)
special x = Right (topDecl, x, [])
bad x = panic "topDeclName" [x]


Expand Down Expand Up @@ -877,6 +883,8 @@ instance Rename Newtype where
do nameT <- rnLocated (renameType NameBind) (nName n)
nameC <- renameVar NameBind (nConName n)

depsOf (NamedThing nameC) (addDep (thing nameT))

depsOf (NamedThing (thing nameT)) $
do ps' <- traverse rename (nParams n)
body' <- traverse (traverse rename) (nBody n)
Expand Down
11 changes: 11 additions & 0 deletions tests/issues/issue1511.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
module M where

v: [1]
v = MOOD.SAD.value

newtype MOOD_t = { value: [1] }

MOOD = { HAPPY = MOOD_t { value = 0b1 }
, SAD = MOOD_t { value = 0b0 }
}

2 changes: 2 additions & 0 deletions tests/issues/issue1511.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
:load issue1511.cry
v
4 changes: 4 additions & 0 deletions tests/issues/issue1511.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Loading module Cryptol
Loading module Cryptol
Loading module M
0x0

0 comments on commit 05412e9

Please sign in to comment.