module Cryptol.ModuleSystem.Renamer (
NamingEnv(), shadowing
, BindsNames(..), InModule(..), namingEnv'
, checkNamingEnv
, shadowNames
, Rename(..), runRenamer, RenameM()
, RenamerError(..)
, RenamerWarning(..)
, renameVar
, renameType
, renameModule
) where
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.NamingEnv
import Cryptol.Prims.Syntax
import Cryptol.Parser.AST
import Cryptol.Parser.Position
import Cryptol.Utils.Ident (packIdent,packInfix)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
import MonadLib hiding (mapM)
import qualified Data.Map as Map
import GHC.Generics (Generic)
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
data RenamerError
= MultipleSyms (Located PName) [Name] NameDisp
| UnboundExpr (Located PName) NameDisp
| UnboundType (Located PName) NameDisp
| OverlappingSyms [Name] NameDisp
| ExpectedValue (Located PName) NameDisp
| ExpectedType (Located PName) NameDisp
| FixityError (Located Name) (Located Name) NameDisp
| InvalidConstraint (Type PName) NameDisp
| MalformedConstraint (Located (Type PName)) NameDisp
deriving (Show,Generic)
instance NFData RenamerError where rnf = genericRnf
instance PP RenamerError where
ppPrec _ e = case e of
MultipleSyms lqn qns disp -> fixNameDisp disp $
hang (text "[error] at" <+> pp (srcRange lqn))
4 $ (text "Multiple definitions for symbol:" <+> pp (thing lqn))
$$ vcat (map ppLocName qns)
UnboundExpr lqn disp -> fixNameDisp disp $
hang (text "[error] at" <+> pp (srcRange lqn))
4 (text "Value not in scope:" <+> pp (thing lqn))
UnboundType lqn disp -> fixNameDisp disp $
hang (text "[error] at" <+> pp (srcRange lqn))
4 (text "Type not in scope:" <+> pp (thing lqn))
OverlappingSyms qns disp -> fixNameDisp disp $
hang (text "[error]")
4 $ text "Overlapping symbols defined:"
$$ vcat (map ppLocName qns)
ExpectedValue lqn disp -> fixNameDisp disp $
hang (text "[error] at" <+> pp (srcRange lqn))
4 (fsep [ text "Expected a value named", quotes (pp (thing lqn))
, text "but found a type instead"
, text "Did you mean `(" <> pp (thing lqn) <> text")?" ])
ExpectedType lqn disp -> fixNameDisp disp $
hang (text "[error] at" <+> pp (srcRange lqn))
4 (fsep [ text "Expected a type named", quotes (pp (thing lqn))
, text "but found a value instead" ])
FixityError o1 o2 disp -> fixNameDisp disp $
hang (text "[error]")
4 (fsep [ text "The fixities of", pp o1, text "and", pp o2
, text "are not compatible. "
, text "You may use explicit parenthesis to disambiguate" ])
InvalidConstraint ty disp -> fixNameDisp disp $
hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty))
4 (fsep [ pp ty, text "is not a valid constraint" ])
MalformedConstraint t disp -> fixNameDisp disp $
hang (text "[error] at" <+> pp (srcRange t))
4 (sep [ quotes (pp (thing t))
, text "is not a valid argument to a constraint" ])
data RenamerWarning
= SymbolShadowed Name [Name] NameDisp
deriving (Show,Generic)
instance NFData RenamerWarning where rnf = genericRnf
instance PP RenamerWarning where
ppPrec _ (SymbolShadowed new originals disp) = fixNameDisp disp $
hang (text "[warning] at" <+> loc)
4 $ fsep [ text "This binding for" <+> sym
, (text "shadows the existing binding" <> plural) <+> text "from" ]
$$ vcat (map ppLocName originals)
where
plural | length originals > 1 = char 's'
| otherwise = empty
loc = pp (nameLoc new)
sym = pp new
data RO = RO
{ roLoc :: Range
, roMod :: !ModName
, roNames :: NamingEnv
, roDisp :: !NameDisp
}
data Out = Out
{ oWarnings :: [RenamerWarning]
, oErrors :: [RenamerError]
} deriving (Show)
instance Monoid Out where
mempty = Out [] []
mappend l r = Out (oWarnings l `mappend` oWarnings r)
(oErrors l `mappend` oErrors r)
newtype RenameM a = RenameM
{ unRenameM :: ReaderT RO (WriterT Out SupplyM) a }
instance Monoid a => Monoid (RenameM a) where
mempty = return mempty
mappend a b =
do x <- a
y <- b
return (mappend x y)
instance Functor RenameM where
fmap f m = RenameM (fmap f (unRenameM m))
instance Applicative RenameM where
pure x = RenameM (pure x)
l <*> r = RenameM (unRenameM l <*> unRenameM r)
instance Monad RenameM where
return x = RenameM (return x)
m >>= k = RenameM (unRenameM m >>= unRenameM . k)
runRenamer :: Supply -> ModName -> NamingEnv -> RenameM a
-> (Either [RenamerError] (a,Supply),[RenamerWarning])
runRenamer s ns env m = (res,oWarnings out)
where
((a,out),s') = runM (unRenameM m) RO { roLoc = emptyRange
, roNames = env
, roMod = ns
, roDisp = neverQualifyMod ns
`mappend` toNameDisp env
} s
res | null (oErrors out) = Right (a,s')
| otherwise = Left (oErrors out)
record :: (NameDisp -> RenamerError) -> RenameM ()
record f = RenameM $
do RO { .. } <- ask
put mempty { oErrors = [f roDisp] }
curLoc :: RenameM Range
curLoc = RenameM (roLoc `fmap` ask)
located :: a -> RenameM (Located a)
located thing =
do srcRange <- curLoc
return Located { .. }
withLoc :: HasLoc loc => loc -> RenameM a -> RenameM a
withLoc loc m = RenameM $ case getLoc loc of
Just range -> do
ro <- ask
local ro { roLoc = range } (unRenameM m)
Nothing -> unRenameM m
getNS :: RenameM ModName
getNS = RenameM (roMod `fmap` ask)
shadowNames :: BindsNames env => env -> RenameM a -> RenameM a
shadowNames = shadowNames' CheckAll
data EnvCheck = CheckAll
| CheckOverlap
| CheckNone
deriving (Eq,Show)
shadowNames' :: BindsNames env => EnvCheck -> env -> RenameM a -> RenameM a
shadowNames' check names m = RenameM $ do
env <- inBase (namingEnv names)
ro <- ask
put (checkEnv (roDisp ro) check env (roNames ro))
let ro' = ro { roNames = env `shadowing` roNames ro }
local ro' (unRenameM m)
shadowNamesNS :: BindsNames (InModule env) => env -> RenameM a -> RenameM a
shadowNamesNS names m =
do ns <- getNS
shadowNames (InModule ns names) m
checkEnv :: NameDisp -> EnvCheck -> NamingEnv -> NamingEnv -> Out
checkEnv _ CheckNone _ _ = mempty
checkEnv disp check l r = Map.foldlWithKey (step neExprs) mempty (neExprs l)
`mappend` Map.foldlWithKey (step neTypes) mempty (neTypes l)
where
step prj acc k ns = acc `mappend` mempty
{ oWarnings =
if check == CheckAll
then case Map.lookup k (prj r) of
Nothing -> []
Just os -> [SymbolShadowed (head ns) os disp]
else []
, oErrors = containsOverlap disp ns
}
containsOverlap :: NameDisp -> [Name] -> [RenamerError]
containsOverlap _ [_] = []
containsOverlap _ [] = panic "Renamer" ["Invalid naming environment"]
containsOverlap disp ns = [OverlappingSyms ns disp]
checkNamingEnv :: NamingEnv -> ([RenamerError],[RenamerWarning])
checkNamingEnv env = (out, [])
where
out = Map.foldr check outTys (neExprs env)
outTys = Map.foldr check mempty (neTypes env)
disp = toNameDisp env
check ns acc = containsOverlap disp ns ++ acc
supply :: SupplyM a -> RenameM a
supply m = RenameM (inBase m)
class Rename f where
rename :: f PName -> RenameM (f Name)
renameModule :: Module PName -> RenameM (NamingEnv,Module Name)
renameModule m =
do env <- supply (namingEnv m)
decls' <- shadowNames' CheckOverlap env (traverse rename (mDecls m))
return (env,m { mDecls = decls' })
instance Rename TopDecl where
rename td = case td of
Decl d -> Decl <$> traverse rename d
TDNewtype n -> TDNewtype <$> traverse rename n
Include n -> return (Include n)
rnLocated :: (a -> RenameM b) -> Located a -> RenameM (Located b)
rnLocated f loc = withLoc loc $
do a' <- f (thing loc)
return loc { thing = a' }
instance Rename Decl where
rename d = case d of
DSignature ns sig -> DSignature <$> traverse (rnLocated renameVar) ns
<*> rename sig
DPragma ns p -> DPragma <$> traverse (rnLocated renameVar) ns
<*> pure p
DBind b -> DBind <$> rename b
DPatBind pat e -> do (pe,[pat']) <- renamePats [pat]
shadowNames pe (DPatBind pat' <$> rename e)
DType syn -> DType <$> rename syn
DLocated d' r -> withLoc r
$ DLocated <$> rename d' <*> pure r
DFixity{} -> panic "Renamer" ["Unexpected fixity declaration"
, show d]
instance Rename Newtype where
rename n = do
name' <- rnLocated renameType (nName n)
shadowNames (nParams n) $
do ps' <- traverse rename (nParams n)
body' <- traverse (rnNamed rename) (nBody n)
return Newtype { nName = name'
, nParams = ps'
, nBody = body' }
renameVar :: PName -> RenameM Name
renameVar qn = do
ro <- RenameM ask
case Map.lookup qn (neExprs (roNames ro)) of
Just [n] -> return n
Just [] -> panic "Renamer" ["Invalid expression renaming environment"]
Just syms ->
do n <- located qn
record (MultipleSyms n syms)
return (head syms)
Nothing ->
do n <- located qn
case Map.lookup qn (neTypes (roNames ro)) of
Just _ -> record (ExpectedValue n)
Nothing -> record (UnboundExpr n)
mkFakeName qn
typeExists :: PName -> RenameM (Maybe Name)
typeExists pn =
do ro <- RenameM ask
case Map.lookup pn (neTypes (roNames ro)) of
Just [n] -> return (Just n)
Just [] -> panic "Renamer" ["Invalid type renaming environment"]
Just syms -> do n <- located pn
record (MultipleSyms n syms)
return (Just (head syms))
Nothing -> return Nothing
renameType :: PName -> RenameM Name
renameType pn =
do mb <- typeExists pn
case mb of
Just n -> return n
Nothing ->
do ro <- RenameM ask
let n = Located { srcRange = roLoc ro, thing = pn }
case Map.lookup pn (neExprs (roNames ro)) of
Just _ -> record (ExpectedType n)
Nothing -> record (UnboundType n)
mkFakeName pn
mkFakeName :: PName -> RenameM Name
mkFakeName pn = RenameM $
do ro <- ask
inBase (liftSupply (mkParameter (getIdent pn) (roLoc ro)))
instance Rename Schema where
rename s = snd `fmap` renameSchema s
renameSchema :: Schema PName -> RenameM (NamingEnv,Schema Name)
renameSchema (Forall ps p ty loc) =
do env <- supply (namingEnv ps)
s' <- shadowNames env $ Forall <$> traverse rename ps
<*> traverse rename p
<*> rename ty
<*> pure loc
return (env,s')
instance Rename TParam where
rename TParam { .. } =
do n <- renameType tpName
return TParam { tpName = n, .. }
instance Rename Prop where
rename p = case p of
CFin t -> CFin <$> rename t
CEqual l r -> CEqual <$> rename l <*> rename r
CGeq l r -> CGeq <$> rename l <*> rename r
CArith t -> CArith <$> rename t
CCmp t -> CCmp <$> rename t
CLocated p' r -> withLoc r
$ CLocated <$> rename p' <*> pure r
CType t -> translateProp =<< resolveTypeFixity t
translateProp :: Type PName -> RenameM (Prop Name)
translateProp ty = go ty
where
go t = case t of
TLocated t' r -> (`CLocated` r) <$> go t'
TUser n [l,r]
| i == packIdent "==" -> CEqual <$> rename l <*> rename r
| i == packIdent ">=" -> CGeq <$> rename l <*> rename r
| i == packIdent "<=" -> CGeq <$> rename r <*> rename l
where
i = getIdent n
_ ->
do record (InvalidConstraint ty)
CType <$> rename t
instance Rename Type where
rename ty0 = go =<< resolveTypeFixity ty0
where
go :: Type PName -> RenameM (Type Name)
go (TFun a b) = TFun <$> go a <*> go b
go (TSeq n a) = TSeq <$> go n <*> go a
go TBit = return TBit
go (TNum c) = return (TNum c)
go (TChar c) = return (TChar c)
go TInf = return TInf
go (TUser pn ps)
| i == packIdent "inf", null ps = return TInf
| i == packIdent "Bit", null ps = return TBit
| i == packIdent "min" = TApp TCMin <$> traverse go ps
| i == packIdent "max" = TApp TCMax <$> traverse go ps
| i == packIdent "lengthFromThen" = TApp TCLenFromThen <$> traverse go ps
| i == packIdent "lengthFromThenTo" = TApp TCLenFromThenTo <$> traverse go ps
| i == packIdent "width" = TApp TCWidth <$> traverse go ps
where
i = getIdent pn
go (TUser qn ps) = TUser <$> renameType qn <*> traverse go ps
go (TApp f xs) = TApp f <$> traverse go xs
go (TRecord fs) = TRecord <$> traverse (rnNamed go) fs
go (TTuple fs) = TTuple <$> traverse go fs
go TWild = return TWild
go (TLocated t' r) = withLoc r (TLocated <$> go t' <*> pure r)
go (TParens t') = TParens <$> go t'
go (TInfix a o f b) = TInfix <$> rename a
<*> rnLocated renameType o
<*> pure f
<*> rename b
resolveTypeFixity :: Type PName -> RenameM (Type PName)
resolveTypeFixity = go
where
go t = case t of
TFun a b -> TFun <$> go a <*> go b
TSeq n a -> TSeq <$> go n <*> go a
TUser pn ps -> TUser pn <$> traverse go ps
TApp f xs -> TApp f <$> traverse go xs
TRecord fs -> TRecord <$> traverse (traverse go) fs
TTuple fs -> TTuple <$> traverse go fs
TLocated t' r-> withLoc r (TLocated <$> go t' <*> pure r)
TParens t' -> TParens <$> go t'
TInfix a o _ b ->
do let op = lookupFixity o
a' <- go a
b' <- go b
mkTInfix a' op b'
TBit -> return t
TNum _ -> return t
TChar _ -> return t
TInf -> return t
TWild -> return t
type TOp = Type PName -> Type PName -> Type PName
infixProps :: [PName]
infixProps = map (mkUnqual . packInfix) [ "==", ">=", "<=" ]
mkTInfix :: Type PName -> (TOp,Fixity) -> Type PName -> RenameM (Type PName)
mkTInfix t@(TUser o1 [x,y]) op@(o2,f2) z
| o1 `elem` infixProps =
do let f1 = Fixity NonAssoc 0
case compareFixity f1 f2 of
FCLeft -> return (o2 t z)
FCRight -> do r <- mkTInfix y op z
return (TUser o1 [x,r])
FCError -> return (o2 t z)
mkTInfix t@(TApp o1 [x,y]) op@(o2,f2) z
| Just (a1,p1) <- Map.lookup o1 tBinOpPrec =
case compareFixity (Fixity a1 p1) f2 of
FCLeft -> return (o2 t z)
FCRight -> do r <- mkTInfix y op z
return (TApp o1 [x,r])
FCError -> panic "Renamer" [ "fixity problem for type operators"
, show (o2 t z) ]
mkTInfix (TLocated t _) op z =
mkTInfix t op z
mkTInfix t (op,_) z =
return (op t z)
lookupFixity :: Located PName -> (TOp,Fixity)
lookupFixity op =
case lkp of
Just (p,f) -> (\x y -> TApp p [x,y], f)
Nothing -> (\x y -> TUser sym [x,y], Fixity NonAssoc 0)
where
sym = thing op
lkp = do n <- Map.lookup (thing op) tfunNames
(fAssoc,fLevel) <- Map.lookup n tBinOpPrec
return (n,Fixity { .. })
instance Rename Bind where
rename b = do
n' <- rnLocated renameVar (bName b)
mbSig <- traverse renameSchema (bSignature b)
shadowNames (fst `fmap` mbSig) $
do (patEnv,pats') <- renamePats (bParams b)
e' <- shadowNames' CheckNone patEnv (rnLocated rename (bDef b))
return b { bName = n'
, bParams = pats'
, bDef = e'
, bSignature = snd `fmap` mbSig
, bPragmas = bPragmas b
}
instance Rename BindDef where
rename DPrim = return DPrim
rename (DExpr e) = DExpr <$> rename e
instance Rename Pattern where
rename p = case p of
PVar lv -> PVar <$> rnLocated renameVar lv
PWild -> pure PWild
PTuple ps -> PTuple <$> traverse rename ps
PRecord nps -> PRecord <$> traverse (rnNamed rename) nps
PList elems -> PList <$> traverse rename elems
PTyped p' t -> PTyped <$> rename p' <*> rename t
PSplit l r -> PSplit <$> rename l <*> rename r
PLocated p' loc -> withLoc loc
$ PLocated <$> rename p' <*> pure loc
instance Rename Expr where
rename e = case e of
EVar n -> EVar <$> renameVar n
ELit l -> return (ELit l)
ETuple es -> ETuple <$> traverse rename es
ERecord fs -> ERecord <$> traverse (rnNamed rename) fs
ESel e' s -> ESel <$> rename e' <*> pure s
EList es -> EList <$> traverse rename es
EFromTo s n e'-> EFromTo <$> rename s
<*> traverse rename n
<*> traverse rename e'
EInfFrom a b -> EInfFrom<$> rename a <*> traverse rename b
EComp e' bs -> do arms' <- traverse renameArm bs
let (envs,bs') = unzip arms'
shadowNames envs (EComp <$> rename e' <*> pure bs')
EApp f x -> EApp <$> rename f <*> rename x
EAppT f ti -> EAppT <$> rename f <*> traverse rename ti
EIf b t f -> EIf <$> rename b <*> rename t <*> rename f
EWhere e' ds -> do ns <- getNS
shadowNames (map (InModule ns) ds) $
EWhere <$> rename e' <*> traverse rename ds
ETyped e' ty -> ETyped <$> rename e' <*> rename ty
ETypeVal ty -> ETypeVal<$> rename ty
EFun ps e' -> do (env,ps') <- renamePats ps
shadowNames' CheckNone env (EFun ps' <$> rename e')
ELocated e' r -> withLoc r
$ ELocated <$> rename e' <*> pure r
EParens p -> EParens <$> rename p
EInfix x y _ z-> do op <- renameOp y
x' <- rename x
z' <- rename z
mkEInfix x' op z'
mkEInfix :: Expr Name
-> (Located Name,Fixity)
-> Expr Name
-> RenameM (Expr Name)
mkEInfix e@(EInfix x o1 f1 y) op@(o2,f2) z =
case compareFixity f1 f2 of
FCLeft -> return (EInfix e o2 f2 z)
FCRight -> do r <- mkEInfix y op z
return (EInfix x o1 f1 r)
FCError -> do record (FixityError o1 o2)
return (EInfix e o2 f2 z)
mkEInfix (ELocated e' _) op z =
mkEInfix e' op z
mkEInfix e (o,f) z =
return (EInfix e o f z)
renameOp :: Located PName -> RenameM (Located Name,Fixity)
renameOp ln = withLoc ln $
do n <- renameVar (thing ln)
ro <- RenameM ask
case Map.lookup n (neFixity (roNames ro)) of
Just fixity -> return (ln { thing = n },fixity)
Nothing -> return (ln { thing = n },defaultFixity)
instance Rename TypeInst where
rename ti = case ti of
NamedInst nty -> NamedInst <$> traverse rename nty
PosInst ty -> PosInst <$> rename ty
renameArm :: [Match PName] -> RenameM (NamingEnv,[Match Name])
renameArm (m:ms) =
do (me,m') <- renameMatch m
shadowNames me $
do (env,rest) <- renameArm ms
return (env `shadowing` me, m':rest)
renameArm [] =
return (mempty,[])
renameMatch :: Match PName -> RenameM (NamingEnv,Match Name)
renameMatch (Match p e) =
do (pe,[p']) <- renamePats [p]
e' <- rename e
return (pe,Match p' e')
renameMatch (MatchLet b) =
do ns <- getNS
be <- supply (namingEnv (InModule ns b))
b' <- shadowNames be (rename b)
return (be,MatchLet b')
renamePats :: [Pattern PName] -> RenameM (NamingEnv,[Pattern Name])
renamePats = loop
where
loop ps = case ps of
p:rest -> do
pe <- patternEnv p
shadowNames pe $
do p' <- rename p
(env',rest') <- loop rest
return (pe `mappend` env', p':rest')
[] -> return (mempty, [])
patternEnv :: Pattern PName -> RenameM NamingEnv
patternEnv p0 = go p0
where
go (PVar Located { .. }) =
do n <- supply (liftSupply (mkParameter (getIdent thing) srcRange))
return (singletonE thing n)
go PWild = return mempty
go (PTuple ps) = foldMap go ps
go (PRecord fs) = foldMap (foldMap go) fs
go (PList ps) = foldMap go ps
go (PTyped p ty) = go p `mappend` typeEnv ty
go (PSplit a b) = go a `mappend` go b
go (PLocated p loc) = withLoc loc (go p)
typeEnv (TFun a b) = typeEnv a `mappend` typeEnv b
typeEnv (TSeq a b) = typeEnv a `mappend` typeEnv b
typeEnv TBit = return mempty
typeEnv TNum{} = return mempty
typeEnv TChar{} = return mempty
typeEnv TInf = return mempty
typeEnv (TUser pn ps) =
do mb <- typeExists pn
case mb of
Just _ -> foldMap typeEnv ps
Nothing
| null ps ->
do loc <- curLoc
n <- supply (liftSupply (mkParameter (getIdent pn) loc))
return (singletonT pn n)
| otherwise ->
do loc <- curLoc
record (UnboundType (Located loc pn))
n <- supply (liftSupply (mkParameter (getIdent pn) loc))
return (singletonT pn n)
typeEnv (TApp _ ts) = foldMap typeEnv ts
typeEnv (TRecord fs) = foldMap (foldMap typeEnv) fs
typeEnv (TTuple ts) = foldMap typeEnv ts
typeEnv TWild = return mempty
typeEnv (TLocated ty loc) = withLoc loc (typeEnv ty)
typeEnv (TParens ty) = typeEnv ty
typeEnv (TInfix a _ _ b) = typeEnv a `mappend` typeEnv b
instance Rename Match where
rename m = case m of
Match p e -> Match <$> rename p <*> rename e
MatchLet b -> shadowNamesNS b (MatchLet <$> rename b)
instance Rename TySyn where
rename (TySyn n ps ty) =
shadowNames ps $ TySyn <$> rnLocated renameType n
<*> traverse rename ps
<*> rename ty
rnNamed :: (a -> RenameM b) -> Named a -> RenameM (Named b)
rnNamed = traverse