mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Change naming convention for module parameters
Also: * Remove unused Renamer errors * Do not repeat the same error many times * Check that all module parameters have different names
This commit is contained in:
parent
6262568a12
commit
94dd15f91a
@ -46,7 +46,7 @@ import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.Utils.Ident (ModName)
|
||||
import Cryptol.Utils.Ident (ModName,Ident)
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.Fixity(Fixity)
|
||||
import Cryptol.Parser.AST(Pragma)
|
||||
@ -112,7 +112,7 @@ isEmptyIfaceParams IfaceParams { .. } =
|
||||
|
||||
|
||||
data IfaceModParam = IfaceModParam
|
||||
{ ifModParamName :: Maybe ModName
|
||||
{ ifModParamName :: Ident
|
||||
, ifModParamRange :: Range
|
||||
, ifModParamSig :: Name
|
||||
, ifModParamInstance :: Map Name Name -- ^ Maps param names to names in sig.
|
||||
|
@ -32,7 +32,8 @@ import Prelude.Compat
|
||||
|
||||
import Data.Either(partitionEithers)
|
||||
import Data.Maybe(fromJust)
|
||||
import Data.List(find,foldl')
|
||||
import Data.List(find,foldl',groupBy,sortBy)
|
||||
import Data.Function(on)
|
||||
import Data.Foldable(toList)
|
||||
import Data.Map.Strict(Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
@ -200,6 +201,16 @@ renameModule' info@Extra { extraModPath = mpath } env m =
|
||||
shadowNames' CheckNone env $ -- the actual check will happen below
|
||||
unzip <$> mapM (doModParam allNested) (mModParams m)
|
||||
|
||||
let repeated = groupBy ((==) `on` ifModParamName)
|
||||
$ sortBy (compare `on` ifModParamName) params
|
||||
|
||||
forM_ repeated \ps ->
|
||||
case ps of
|
||||
[_] -> pure ()
|
||||
~(p : _) -> recordError
|
||||
(MultipleModParams (ifModParamName p)
|
||||
(map ifModParamRange ps))
|
||||
|
||||
shadowNames' CheckOverlap (mconcat (env : envs))
|
||||
-- here is the check
|
||||
do inScope <- getNamingEnv
|
||||
@ -394,7 +405,7 @@ topDeclName topDecl =
|
||||
|
||||
DModParam m -> Right ( topDecl
|
||||
, ModParamName (srcRange (mpSignature m))
|
||||
(mpAs m))
|
||||
(mpName m))
|
||||
|
||||
Include {} -> bad "Include"
|
||||
where
|
||||
@ -447,16 +458,21 @@ doModParam owned mp =
|
||||
Just q -> qualify q newEnv'
|
||||
pure ( newEnv
|
||||
, IfaceModParam
|
||||
{ ifModParamName = mpAs mp
|
||||
{ ifModParamName = mpName mp
|
||||
, ifModParamRange = loc
|
||||
, ifModParamSig = nm
|
||||
, ifModParamInstance = nameMap
|
||||
}
|
||||
)
|
||||
|
||||
|
||||
Nothing -> panic "doModParam"
|
||||
[ "Missing signature", show sigName ]
|
||||
-- This can happen if the interface was undefined (i.e., error)
|
||||
Nothing -> pure
|
||||
(mempty, IfaceModParam { ifModParamName = mpName mp
|
||||
, ifModParamRange = loc
|
||||
, ifModParamSig = nm
|
||||
, ifModParamInstance = mempty
|
||||
})
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Compute names coming through `import submodule` statements.
|
||||
@ -537,7 +553,7 @@ data Extra = Extra
|
||||
, extraModPath :: ModPath
|
||||
-- ^ Path to the current location (for nested modules)
|
||||
|
||||
, extraModParams :: !(Map (Maybe ModName) IfaceModParam)
|
||||
, extraModParams :: !(Map Ident IfaceModParam)
|
||||
-- ^ Module parameters for the current module
|
||||
|
||||
, extraFromModParam :: !(Map Name DepName)
|
||||
@ -591,11 +607,11 @@ instance Rename (WithExtra TopDecl) where
|
||||
|
||||
instance Rename (WithExtra ModParam) where
|
||||
rename (WithExtra info mp) =
|
||||
depsOf (ModParamName (srcRange (mpSignature mp)) (mpAs mp))
|
||||
depsOf (ModParamName (srcRange (mpSignature mp)) (mpName mp))
|
||||
do x <- rnLocated (resolveName NameUse NSSignature) (mpSignature mp)
|
||||
pure (WithExtra info mp { mpSignature = x, mpRenaming = ren })
|
||||
where
|
||||
ren = case Map.lookup (mpAs mp) (extraModParams info) of
|
||||
ren = case Map.lookup (mpName mp) (extraModParams info) of
|
||||
Just r -> ifModParamInstance r
|
||||
Nothing -> panic "rename@ModParam"
|
||||
[ "Missing module parameter", show (mpAs mp) ]
|
||||
|
@ -41,25 +41,18 @@ data RenamerError
|
||||
| FixityError (Located Name) Fixity (Located Name) Fixity
|
||||
-- ^ When the fixity of two operators conflict
|
||||
|
||||
| InvalidConstraint (Type PName)
|
||||
-- ^ When it's not possible to produce a Prop from a Type.
|
||||
|
||||
| MalformedBuiltin (Type PName) PName
|
||||
-- ^ When a builtin type/type-function is used incorrectly.
|
||||
|
||||
| BoundReservedType PName (Maybe Range) Doc
|
||||
-- ^ When a builtin type is named in a binder.
|
||||
|
||||
| OverlappingRecordUpdate (Located [Selector]) (Located [Selector])
|
||||
-- ^ When record updates overlap (e.g., @{ r | x = e1, x.y = e2 }@)
|
||||
|
||||
| InvalidDependency [DepName]
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
| MultipleModParams Ident [Range]
|
||||
deriving (Show, Generic, NFData, Eq, Ord)
|
||||
|
||||
|
||||
-- We use this because parameter constrstaints have no names
|
||||
data DepName = NamedThing Name
|
||||
| ModParamName Range (Maybe ModName)
|
||||
| ModParamName Range Ident
|
||||
{- ^ Note that the range is important not just for error
|
||||
reporting but to distinguish module parameters with
|
||||
the same name (e.g., in nested functors) -}
|
||||
@ -125,19 +118,6 @@ instance PP RenamerError where
|
||||
, text "are not compatible."
|
||||
, text "You may use explicit parentheses to disambiguate." ])
|
||||
|
||||
InvalidConstraint ty ->
|
||||
hang (hsep $ [text "[error]"] ++ maybe [] (\r -> [text "at" <+> pp r]) (getLoc ty))
|
||||
4 (fsep [ pp ty, text "is not a valid constraint" ])
|
||||
|
||||
MalformedBuiltin ty pn ->
|
||||
hang (hsep $ [text "[error]"] ++ maybe [] (\r -> [text "at" <+> pp r]) (getLoc ty))
|
||||
4 (fsep [ text "invalid use of built-in type", pp pn
|
||||
, text "in type", pp ty ])
|
||||
|
||||
BoundReservedType n loc src ->
|
||||
hang (hsep $ [text "[error]"] ++ maybe [] (\r -> [text "at" <+> pp r]) loc)
|
||||
4 (fsep [ text "built-in type", quotes (pp n), text "shadowed in", src ])
|
||||
|
||||
OverlappingRecordUpdate xs ys ->
|
||||
hang "[error] Overlapping record updates:"
|
||||
4 (vcat [ ppLab xs, ppLab ys ])
|
||||
@ -150,6 +130,10 @@ instance PP RenamerError where
|
||||
| x <- ds ])
|
||||
where ppR r = pp (from r) <.> "--" <.> pp (to r)
|
||||
|
||||
MultipleModParams x rs ->
|
||||
hang ("[error] Multiple parameters with name" <+> backticks (pp x))
|
||||
4 (vcat [ "•" <+> pp r | r <- rs ])
|
||||
|
||||
instance PP DepName where
|
||||
ppPrec _ d =
|
||||
case d of
|
||||
@ -160,10 +144,7 @@ instance PP DepName where
|
||||
NSType -> "type" <+> pp n
|
||||
NSValue -> pp n
|
||||
NSSignature -> "signature" <+> pp n
|
||||
ModParamName r x ->
|
||||
case x of
|
||||
Nothing -> "module parameter at" <+> pp r
|
||||
Just m -> "module parameter" <+> pp m
|
||||
ModParamName _r i -> "module parameter" <+> pp i
|
||||
|
||||
|
||||
|
||||
|
@ -14,10 +14,8 @@ module Cryptol.ModuleSystem.Renamer.Monad where
|
||||
import Data.List(sort)
|
||||
import Data.Set(Set)
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Foldable as F
|
||||
import Data.Map.Strict ( Map )
|
||||
import qualified Data.Map.Strict as Map
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Data.Semigroup as S
|
||||
import MonadLib hiding (mapM, mapM_)
|
||||
|
||||
@ -57,7 +55,7 @@ data RO = RO
|
||||
|
||||
data RW = RW
|
||||
{ rwWarnings :: ![RenamerWarning]
|
||||
, rwErrors :: !(Seq.Seq RenamerError)
|
||||
, rwErrors :: !(Set RenamerError)
|
||||
, rwSupply :: !Supply
|
||||
, rwNameUseCount :: !(Map Name Int)
|
||||
-- ^ How many times did we refer to each name.
|
||||
@ -125,7 +123,7 @@ runRenamer info m = (res, warns)
|
||||
warns = sort (rwWarnings rw ++ warnUnused (renContext info) (renEnv info) rw)
|
||||
|
||||
(a,rw) = runM (unRenameM m) ro
|
||||
RW { rwErrors = Seq.empty
|
||||
RW { rwErrors = Set.empty
|
||||
, rwWarnings = []
|
||||
, rwSupply = renSupply info
|
||||
, rwNameUseCount = Map.empty
|
||||
@ -141,8 +139,8 @@ runRenamer info m = (res, warns)
|
||||
, roNestedMods = Map.empty
|
||||
}
|
||||
|
||||
res | Seq.null (rwErrors rw) = Right (a,rwSupply rw)
|
||||
| otherwise = Left (F.toList (rwErrors rw))
|
||||
res | Set.null (rwErrors rw) = Right (a,rwSupply rw)
|
||||
| otherwise = Left (Set.toList (rwErrors rw))
|
||||
|
||||
|
||||
setCurMod :: ModPath -> RenameM a -> RenameM a
|
||||
@ -168,7 +166,7 @@ nestedModuleOrig x = RenameM (asks (Map.lookup x . roNestedMods))
|
||||
recordError :: RenamerError -> RenameM ()
|
||||
recordError f = RenameM $
|
||||
do RW { .. } <- get
|
||||
set RW { rwErrors = rwErrors Seq.|> f, .. }
|
||||
set RW { rwErrors = Set.insert f rwErrors, .. }
|
||||
|
||||
recordWarning :: RenamerWarning -> RenameM ()
|
||||
recordWarning w =
|
||||
|
@ -272,6 +272,7 @@ mod_param_decl :: { ModParam PName }
|
||||
'import' 'signature'
|
||||
name mbAs { ModParam { mpSignature = $4
|
||||
, mpAs = fmap thing $5
|
||||
, mpName = mkModParamName $4 $5
|
||||
, mpDoc = $1
|
||||
, mpRenaming = mempty } }
|
||||
|
||||
|
@ -255,17 +255,29 @@ data Signature name = Signature
|
||||
} deriving (Eq,Show,Generic,NFData)
|
||||
|
||||
{- | A module parameter declaration.
|
||||
A functor may have either 1 unnamed parameter or multiple named parameters
|
||||
For the time being, unnamed parameters introduce the names from the
|
||||
signature unqualified, while the named version adds them qualified. -}
|
||||
|
||||
> import signature A
|
||||
> import signature A as B
|
||||
|
||||
The name of the parameter is derived from the `as` clause. If there
|
||||
is no `as` clause then it is derived from the name of the signature.
|
||||
|
||||
If there is no `as` clause, then the type/value parameters are unqualified,
|
||||
and otherwise they are qualified.
|
||||
-}
|
||||
data ModParam name = ModParam
|
||||
{ mpSignature :: Located name -- ^ Signature for parameter
|
||||
, mpAs :: Maybe ModName -- ^ Qualifier and parameter name
|
||||
, mpAs :: Maybe ModName -- ^ Qualified for actual params
|
||||
, mpName :: !Ident
|
||||
{- ^ Parameter name (for inst.)
|
||||
Note that this is not resolved in the rename, and is only used
|
||||
when instantiating a functor. -}
|
||||
|
||||
, mpDoc :: Maybe (Located Text) -- ^ Optional documentation
|
||||
, mpRenaming :: !(Map name name)
|
||||
-- ^ Filled in by the renamer.
|
||||
-- Maps the actual parameter names of the componenets to
|
||||
-- the names in the signature.
|
||||
{- ^ Filled in by the renamer.
|
||||
Maps the actual (value/type) parameter names to the names in the
|
||||
signature. -}
|
||||
} deriving (Eq,Show,Generic,NFData)
|
||||
|
||||
|
||||
@ -1132,6 +1144,7 @@ instance NoPos (Signature name) where
|
||||
instance NoPos (ModParam name) where
|
||||
noPos mp = ModParam { mpSignature = noPos (mpSignature mp)
|
||||
, mpAs = mpAs mp
|
||||
, mpName = mpName mp
|
||||
, mpDoc = noPos <$> mpDoc mp
|
||||
, mpRenaming = mpRenaming mp
|
||||
}
|
||||
|
@ -192,6 +192,18 @@ expected x = P $ \cfg _ s ->
|
||||
mkModName :: [Text] -> ModName
|
||||
mkModName = packModName
|
||||
|
||||
-- | This is how we derive the name of a module parameter from the
|
||||
-- @import source@ declaration.
|
||||
mkModParamName :: Located PName -> Maybe (Located ModName) -> Ident
|
||||
mkModParamName lsig qual =
|
||||
case qual of
|
||||
Nothing ->
|
||||
case thing lsig of
|
||||
UnQual i -> i
|
||||
Qual _ i -> i
|
||||
NewName {} -> panic "mkModParamName" ["Unexpected NewName",show lsig]
|
||||
Just m -> packIdent (last (modNameChunks (thing m)))
|
||||
|
||||
-- Note that type variables are not resolved at this point: they are tcons.
|
||||
mkSchema :: [TParam PName] -> [Prop PName] -> Type PName -> Schema PName
|
||||
mkSchema xs ps t = Forall xs ps t Nothing
|
||||
|
@ -23,10 +23,10 @@ import Control.DeepSeq
|
||||
|
||||
-- | Information about associativity.
|
||||
data Assoc = LeftAssoc | RightAssoc | NonAssoc
|
||||
deriving (Show, Eq, Generic, NFData)
|
||||
deriving (Show, Eq, Ord, Generic, NFData)
|
||||
|
||||
data Fixity = Fixity { fAssoc :: !Assoc, fLevel :: !Int }
|
||||
deriving (Eq, Generic, NFData, Show)
|
||||
deriving (Eq, Ord, Generic, NFData, Show)
|
||||
|
||||
data FixityCmp = FCError
|
||||
| FCLeft
|
||||
|
Loading…
Reference in New Issue
Block a user