diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index dc49f7464..6e3054550 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -37,7 +37,8 @@ import Cryptol.Eval.Concrete (Value) import Cryptol.Eval.Type (TValue(..), tValTy) import Cryptol.Eval.Value (GenValue(..), asWordVal, enumerateSeqMap) import Cryptol.Parser -import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type) +import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type, + ExportType(..)) import Cryptol.Parser.Position (Located(..), emptyRange) import Cryptol.Parser.Selector import Cryptol.Utils.Ident @@ -319,7 +320,17 @@ getCryptolExpr (Let binds body) = mkBind (LetBinding x rhs) = DBind . (\bindBody -> - Bind (fakeLoc (UnQual (mkIdent x))) [] bindBody Nothing False Nothing [] True Nothing) . + Bind { bName = fakeLoc (UnQual (mkIdent x)) + , bParams = [] + , bDef = bindBody + , bSignature = Nothing + , bInfix = False + , bFixity = Nothing + , bPragmas = [] + , bMono = True + , bDoc = Nothing + , bExport = Public + }) . fakeLoc . DExpr <$> getCryptolExpr rhs diff --git a/cryptol-remote-api/src/CryptolServer/Names.hs b/cryptol-remote-api/src/CryptolServer/Names.hs index 85b3aefec..1552d8c31 100644 --- a/cryptol-remote-api/src/CryptolServer/Names.hs +++ b/cryptol-remote-api/src/CryptolServer/Names.hs @@ -17,9 +17,11 @@ import Cryptol.Parser.Name (PName(..)) import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), focusedEnv) import Cryptol.ModuleSystem.Interface (IfaceDecl(..), IfaceDecls(..)) import Cryptol.ModuleSystem.Name (Name) -import Cryptol.ModuleSystem.NamingEnv (NamingEnv(..), lookupValNames, shadowing) +import Cryptol.ModuleSystem.NamingEnv + (NamingEnv, namespaceMap, lookupValNames, shadowing) import Cryptol.TypeCheck.Type (Schema(..)) import Cryptol.Utils.PP (pp) +import Cryptol.Utils.Ident(Namespace(..)) import CryptolServer import CryptolServer.Data.Type @@ -41,7 +43,7 @@ visibleNames _ = do me <- getModuleEnv let DEnv { deNames = dyNames } = meDynEnv me let ModContext { mctxDecls = fDecls, mctxNames = fNames} = focusedEnv me - let inScope = Map.keys (neExprs $ dyNames `shadowing` fNames) + let inScope = Map.keys (namespaceMap NSValue $ dyNames `shadowing` fNames) return $ concatMap (getInfo fNames (ifDecls fDecls)) inScope getInfo :: NamingEnv -> Map Name IfaceDecl -> PName -> [NameInfo] diff --git a/cryptol.cabal b/cryptol.cabal index f721e782d..5fafd8841 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -111,9 +111,11 @@ library Cryptol.ModuleSystem.Monad, Cryptol.ModuleSystem.Name, Cryptol.ModuleSystem.NamingEnv, - Cryptol.ModuleSystem.Renamer, Cryptol.ModuleSystem.Exports, Cryptol.ModuleSystem.InstantiateModule, + Cryptol.ModuleSystem.Renamer, + Cryptol.ModuleSystem.Renamer.Monad, + Cryptol.ModuleSystem.Renamer.Error, Cryptol.TypeCheck, Cryptol.TypeCheck.Type, @@ -126,12 +128,12 @@ library Cryptol.TypeCheck.Infer, Cryptol.TypeCheck.CheckModuleInstance, Cryptol.TypeCheck.InferTypes, + Cryptol.TypeCheck.Interface, Cryptol.TypeCheck.Error, Cryptol.TypeCheck.Kind, Cryptol.TypeCheck.Subst, Cryptol.TypeCheck.Instantiate, Cryptol.TypeCheck.Unify, - Cryptol.TypeCheck.Depends, Cryptol.TypeCheck.PP, Cryptol.TypeCheck.Solve, Cryptol.TypeCheck.Default, @@ -189,6 +191,7 @@ library Cryptol.Symbolic.What4, Cryptol.REPL.Command, + Cryptol.REPL.Browse, Cryptol.REPL.Monad, Cryptol.REPL.Trie diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index 8c011c315..36f6d76f5 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -29,7 +29,7 @@ module Cryptol.ModuleSystem ( , renameType -- * Interfaces - , Iface(..), IfaceParams(..), IfaceDecls(..), genIface + , Iface, IfaceG(..), IfaceParams(..), IfaceDecls(..), T.genIface , IfaceTySyn, IfaceDecl(..) ) where @@ -44,6 +44,7 @@ import qualified Cryptol.Parser.AST as P import Cryptol.Parser.Name (PName) import Cryptol.Parser.NoPat (RemovePatterns) import qualified Cryptol.TypeCheck.AST as T +import qualified Cryptol.TypeCheck.Interface as T import qualified Cryptol.Utils.Ident as M -- Public Interface ------------------------------------------------------------ @@ -105,10 +106,14 @@ evalDecls dgs env = runModuleM env (interactive (Base.evalDecls dgs)) noPat :: RemovePatterns a => a -> ModuleCmd a noPat a env = runModuleM env (interactive (Base.noPat a)) +-- | Rename a *use* of a value name. The distinction between uses and +-- binding is used to keep track of dependencies. renameVar :: R.NamingEnv -> PName -> ModuleCmd Name renameVar names n env = runModuleM env $ interactive $ - Base.rename M.interactiveName names (R.renameVar n) + Base.rename M.interactiveName names (R.renameVar R.NameUse n) +-- | Rename a *use* of a type name. The distinction between uses and +-- binding is used to keep track of dependencies. renameType :: R.NamingEnv -> PName -> ModuleCmd Name renameType names n env = runModuleM env $ interactive $ - Base.rename M.interactiveName names (R.renameType n) + Base.rename M.interactiveName names (R.renameType R.NameUse n) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 46f5d033d..1c8961399 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -12,14 +12,38 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} module Cryptol.ModuleSystem.Base where +import qualified Control.Exception as X +import Control.Monad (unless,when) +import Data.Maybe (fromMaybe) +import Data.Monoid ((<>)) +import Data.Text.Encoding (decodeUtf8') +import Data.IORef(newIORef,readIORef) +import System.Directory (doesFileExist, canonicalizePath) +import System.FilePath ( addExtension + , isAbsolute + , joinPath + , () + , normalise + , takeDirectory + , takeFileName + ) +import qualified System.IO.Error as IOE +import qualified Data.Map as Map + +import Prelude () +import Prelude.Compat hiding ( (<>) ) + + + import Cryptol.ModuleSystem.Env (DynamicEnv(..)) import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Monad -import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap) +import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..)) import Cryptol.ModuleSystem.Env (lookupModule , LoadedModule(..) , meCoreLint, CoreLint(..) @@ -53,33 +77,21 @@ import Cryptol.Prelude ( preludeContents, floatContents, arrayContents , suiteBContents, primeECContents, preludeReferenceContents ) import Cryptol.Transform.MonoValues (rewModule) -import qualified Control.Exception as X -import Control.Monad (unless,when) -import Data.Maybe (fromMaybe) -import Data.Monoid ((<>)) -import Data.Text.Encoding (decodeUtf8') -import System.Directory (doesFileExist, canonicalizePath) -import System.FilePath ( addExtension - , isAbsolute - , joinPath - , () - , normalise - , takeDirectory - , takeFileName - ) -import qualified System.IO.Error as IOE -import qualified Data.Map as Map - -import Prelude () -import Prelude.Compat hiding ( (<>) ) - -- Renaming -------------------------------------------------------------------- rename :: ModName -> R.NamingEnv -> R.RenameM a -> ModuleM a rename modName env m = do + ifaces <- getIfaces (res,ws) <- liftSupply $ \ supply -> - case R.runRenamer supply modName env m of + let info = R.RenamerInfo + { renSupply = supply + , renContext = TopModule modName + , renEnv = env + , renIfaces = ifaces + } + in + case R.runRenamer info m of (Right (a,supply'),ws) -> ((Right a,ws),supply') (Left errs,ws) -> ((Left errs,ws),supply) @@ -89,12 +101,8 @@ rename modName env m = do Left errs -> renamerErrors errs -- | Rename a module in the context of its imported modules. -renameModule :: P.Module PName - -> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name) -renameModule m = do - (decls,menv) <- importIfaces (map thing (P.mImports m)) - (declsEnv,rm) <- rename (thing (mName m)) menv (R.renameModule m) - return (decls,declsEnv,rm) +renameModule :: P.Module PName -> ModuleM R.RenamedModule +renameModule m = rename (thing (mName m)) mempty (R.renameModule m) -- NoPat ----------------------------------------------------------------------- @@ -200,7 +208,10 @@ doLoadModule quiet isrc path fp pm0 = unless quiet $ withLogger logPutStrLn ("Loading module " ++ pretty (P.thing (P.mName pm))) - tcm <- optionalInstantiate =<< checkModule isrc path pm + + + (nameEnv,tcmod) <- checkModule isrc path pm + tcm <- optionalInstantiate tcmod -- extend the eval env, unless a functor. tbl <- Concrete.primTable <$> getEvalOptsAction @@ -208,7 +219,7 @@ doLoadModule quiet isrc path fp pm0 = callStacks <- getCallStacks let ?callStacks = callStacks unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm) - loadedModule path fp tcm + loadedModule path fp nameEnv tcm return tcm where @@ -231,17 +242,6 @@ doLoadModule quiet isrc path fp pm0 = fullyQualified :: P.Import -> P.Import fullyQualified i = i { iAs = Just (iModule i) } --- | Find the interface referenced by an import, and generate the naming --- environment that it describes. -importIface :: P.Import -> ModuleM (IfaceDecls,R.NamingEnv) -importIface imp = - do Iface { .. } <- getIface (T.iModule imp) - return (ifPublic, R.interpImport imp ifPublic) - --- | Load a series of interfaces, merging their public interfaces. -importIfaces :: [P.Import] -> ModuleM (IfaceDecls,R.NamingEnv) -importIfaces is = mconcat `fmap` mapM importIface is - moduleFile :: ModName -> String -> FilePath moduleFile n = addExtension (joinPath (modNameChunks n)) @@ -299,13 +299,13 @@ addPrelude :: P.Module PName -> P.Module PName addPrelude m | preludeName == P.thing (P.mName m) = m | preludeName `elem` importedMods = m - | otherwise = m { mImports = importPrelude : mImports m } + | otherwise = m { mDecls = importPrelude : mDecls m } where importedMods = map (P.iModule . P.thing) (P.mImports m) - importPrelude = P.Located + importPrelude = P.DImport P.Located { P.srcRange = emptyRange , P.thing = P.Import - { iModule = preludeName + { iModule = P.ImpTop preludeName , iAs = Nothing , iSpec = Nothing } @@ -360,11 +360,8 @@ checkDecls ds = do decls = mctxDecls fe names = mctxNames fe - -- introduce names for the declarations before renaming them - declsEnv <- liftSupply (R.namingEnv' (map (R.InModule interactiveName) ds)) - rds <- rename interactiveName (declsEnv `R.shadowing` names) - (traverse R.rename ds) - + (declsEnv,rds) <- rename interactiveName names + $ R.renameTopDecls interactiveName ds prims <- getPrimMap let act = TCAction { tcAction = T.tcDecls, tcLinter = declsLinter , tcPrims = prims } @@ -390,12 +387,23 @@ getPrimMap = [ "Unable to find the prelude" ] -- | Load a module, be it a normal module or a functor instantiation. -checkModule :: ImportSource -> ModulePath -> P.Module PName -> ModuleM T.Module +checkModule :: + ImportSource -> ModulePath -> P.Module PName -> + ModuleM (R.NamingEnv, T.Module) checkModule isrc path m = case P.mInstance m of Nothing -> checkSingleModule T.tcModule isrc path m - Just fmName -> do tf <- getLoaded (thing fmName) - checkSingleModule (T.tcModuleInst tf) isrc path m + Just fmName -> + do mbtf <- getLoadedMaybe (thing fmName) + case mbtf of + Just tf -> + do renThis <- io $ newIORef (lmNamingEnv tf) + let how = T.tcModuleInst renThis (lmModule tf) + (_,m') <- checkSingleModule how isrc path m + newEnv <- io $ readIORef renThis + pure (newEnv,m') + Nothing -> panic "checkModule" + [ "Functor of module instantiation not loaded" ] -- | Typecheck a single module. If the module is an instantiation @@ -406,7 +414,7 @@ checkSingleModule :: ImportSource {- ^ why are we loading this -} -> ModulePath {- path -} -> P.Module PName {- ^ module to check -} -> - ModuleM T.Module + ModuleM (R.NamingEnv,T.Module) checkSingleModule how isrc path m = do -- check that the name of the module matches expectations @@ -432,13 +440,13 @@ checkSingleModule how isrc path m = do npm <- noPat nim -- rename everything - (tcEnv,declsEnv,scm) <- renameModule npm + renMod <- renameModule npm -- when generating the prim map for the typechecker, if we're checking the -- prelude, we have to generate the map from the renaming environment, as we -- don't have the interface yet. prims <- if thing (mName m) == preludeName - then return (R.toPrimMap declsEnv) + then return (R.toPrimMap (R.rmDefines renMod)) else getPrimMap -- typecheck @@ -447,11 +455,12 @@ checkSingleModule how isrc path m = do , tcPrims = prims } - tcm0 <- typecheck act scm noIfaceParams tcEnv + tcm0 <- typecheck act (R.rmModule renMod) noIfaceParams (R.rmImported renMod) let tcm = tcm0 -- fromMaybe tcm0 (addModParams tcm0) - liftSupply (`rewModule` tcm) + rewMod <- liftSupply (`rewModule` tcm) + pure (R.rmInScope renMod,rewMod) data TCLinter o = TCLinter { lintCheck :: @@ -529,7 +538,7 @@ typecheck act i params env = do -- | Generate input for the typechecker. genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM T.InferInput -genInferInput r prims params env = do +genInferInput r prims params env' = do seeds <- getNameSeeds monoBinds <- getMonoBinds solver <- getTCSolver @@ -538,6 +547,8 @@ genInferInput r prims params env = do callStacks <- getCallStacks -- TODO: include the environment needed by the module + let env = flatPublicDecls env' + -- XXX: we should really just pass this directly return T.InferInput { T.inpRange = r , T.inpVars = Map.map ifDeclSig (ifDecls env) diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index da3678c56..ae2c55f95 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -11,6 +11,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} module Cryptol.ModuleSystem.Env where #ifndef RELOCATABLE @@ -24,6 +25,7 @@ import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply) import qualified Cryptol.ModuleSystem.NamingEnv as R import Cryptol.Parser.AST import qualified Cryptol.TypeCheck as T +import qualified Cryptol.TypeCheck.Interface as T import qualified Cryptol.TypeCheck.AST as T import Cryptol.Utils.PP (PP(..),text,parens,NameDisp) @@ -31,6 +33,7 @@ import Data.ByteString(ByteString) import Control.Monad (guard,mplus) import qualified Control.Exception as X import Data.Function (on) +import Data.Set(Set) import Data.Map (Map) import qualified Data.Map as Map import Data.Semigroup @@ -185,21 +188,65 @@ allDeclGroups = concatMap T.mDecls . loadedNonParamModules -- or type check new expressions. data ModContext = ModContext { mctxParams :: IfaceParams + , mctxExported :: Set Name , mctxDecls :: IfaceDecls + -- ^ Should contain at least names in NamingEnv, but may have more , mctxNames :: R.NamingEnv + -- ^ What's in scope inside the module , mctxNameDisp :: NameDisp - , mctxTypeProvenace :: Map Name DeclProvenance - , mctxValueProvenance :: Map Name DeclProvenance } --- | Specifies how a declared name came to be in scope. -data DeclProvenance = - NameIsImportedFrom ModName - | NameIsLocalPublic - | NameIsLocalPrivate - | NameIsParameter - | NameIsDynamicDecl - deriving (Eq,Ord) +-- This instance is a bit bogus. It is mostly used to add the dynamic +-- environemnt to an existing module, and it makes sense for that use case. +instance Semigroup ModContext where + x <> y = ModContext { mctxParams = jnParams (mctxParams x) (mctxParams y) + , mctxExported = mctxExported x <> mctxExported y + , mctxDecls = mctxDecls x <> mctxDecls y + , mctxNames = names + , mctxNameDisp = R.toNameDisp names + } + + where + names = mctxNames x `R.shadowing` mctxNames y + jnParams a b + | isEmptyIfaceParams a = b + | isEmptyIfaceParams b = a + | otherwise = + panic "ModContext" [ "Cannot combined 2 parameterized contexts" ] + +instance Monoid ModContext where + mempty = ModContext { mctxParams = noIfaceParams + , mctxDecls = mempty + , mctxExported = mempty + , mctxNames = mempty + , mctxNameDisp = R.toNameDisp mempty + } + + + +modContextOf :: ModName -> ModuleEnv -> Maybe ModContext +modContextOf mname me = + do lm <- lookupModule mname me + let localIface = lmInterface lm + localNames = lmNamingEnv lm + loadedDecls = map (ifPublic . lmInterface) + $ getLoadedModules (meLoadedModules me) + pure ModContext + { mctxParams = ifParams localIface + , mctxExported = ifaceDeclsNames (ifPublic localIface) + , mctxDecls = mconcat (ifPrivate localIface : loadedDecls) + , mctxNames = localNames + , mctxNameDisp = R.toNameDisp localNames + } + +dynModContext :: ModuleEnv -> ModContext +dynModContext me = mempty { mctxNames = dynNames + , mctxNameDisp = R.toNameDisp dynNames + , mctxDecls = deIfaceDecls (meDynEnv me) + } + where dynNames = deNames (meDynEnv me) + + -- | Given the state of the environment, compute information about what's @@ -207,69 +254,13 @@ data DeclProvenance = -- additional definitions from the REPL (e.g., let bound names, and @it@). focusedEnv :: ModuleEnv -> ModContext focusedEnv me = - ModContext - { mctxParams = parameters - , mctxDecls = mconcat (dynDecls : localDecls : importedDecls) - , mctxNames = namingEnv - , mctxNameDisp = R.toNameDisp namingEnv - , mctxTypeProvenace = fst provenance - , mctxValueProvenance = snd provenance - } - - where - (importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports) - localDecls = publicDecls `mappend` privateDecls - localNames = R.unqualifiedEnv localDecls `mappend` - R.modParamsNamingEnv parameters - dynDecls = deIfaceDecls (meDynEnv me) - dynNames = deNames (meDynEnv me) - - namingEnv = dynNames `R.shadowing` - localNames `R.shadowing` - mconcat importedNames - - provenance = shadowProvs - $ declsProv NameIsDynamicDecl dynDecls - : declsProv NameIsLocalPublic publicDecls - : declsProv NameIsLocalPrivate privateDecls - : paramProv parameters - : importedProvs - - (imports, parameters, publicDecls, privateDecls) = - case meFocusedModule me of - Nothing -> (mempty, noIfaceParams, mempty, mempty) - Just fm -> - case lookupModule fm me of - Just lm -> - let Iface { .. } = lmInterface lm - in (T.mImports (lmModule lm), ifParams, ifPublic, ifPrivate) - Nothing -> panic "focusedEnv" ["Focused module is not loaded."] - - loadImport imp = - case lookupModule (iModule imp) me of - Just lm -> - let decls = ifPublic (lmInterface lm) - in ( R.interpImport imp decls - , decls - , declsProv (NameIsImportedFrom (iModule imp)) decls - ) - Nothing -> panic "focusedEnv" - [ "Missing imported module: " ++ show (pp (iModule imp)) ] - - - -- earlier ones shadow - shadowProvs ps = let (tss,vss) = unzip ps - in (Map.unions tss, Map.unions vss) - - paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns) - where doMap mp = const NameIsParameter <$> mp - - declsProv prov IfaceDecls { .. } = - ( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ] - , doMap ifDecls - ) - where doMap mp = const prov <$> mp - + case meFocusedModule me of + Nothing -> dynModContext me + Just fm -> case modContextOf fm me of + Just c -> dynModContext me <> c + Nothing -> panic "focusedEnv" + [ "Focused modules not loaded: " ++ show (pp fm) ] + -- Loaded Modules -------------------------------------------------------------- @@ -341,9 +332,11 @@ data LoadedModule = LoadedModule -- For files we just use the cononical path, for in memory things we -- use their label. + , lmNamingEnv :: !R.NamingEnv + -- ^ What's in scope in this module + , lmInterface :: Iface - -- ^ The module's interface. This is for convenient. At the moment - -- we have the whole module in 'lmModule', so this could be computer. + -- ^ The module's interface. , lmModule :: T.Module -- ^ The actual type-checked module @@ -369,8 +362,9 @@ lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules -- | Add a freshly loaded module. If it was previously loaded, then -- the new version is ignored. addLoadedModule :: - ModulePath -> String -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules -addLoadedModule path ident fp tm lm + ModulePath -> String -> Fingerprint -> R.NamingEnv -> T.Module -> + LoadedModules -> LoadedModules +addLoadedModule path ident fp nameEnv tm lm | isLoaded (T.mName tm) lm = lm | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded : lmLoadedParamModules lm } @@ -381,7 +375,8 @@ addLoadedModule path ident fp tm lm { lmName = T.mName tm , lmFilePath = path , lmModuleId = ident - , lmInterface = genIface tm + , lmNamingEnv = nameEnv + , lmInterface = T.genIface tm , lmModule = tm , lmFingerprint = fp } @@ -435,7 +430,8 @@ deIfaceDecls DEnv { deDecls = dgs } = , ifNewtypes = Map.empty , ifAbstractTypes = Map.empty , ifDecls = Map.singleton (ifDeclName ifd) ifd + , ifModules = Map.empty } | decl <- concatMap T.groupDecls dgs - , let ifd = mkIfaceDecl decl + , let ifd = T.mkIfaceDecl decl ] diff --git a/src/Cryptol/ModuleSystem/Exports.hs b/src/Cryptol/ModuleSystem/Exports.hs index a37ce5f39..f510e1cbf 100644 --- a/src/Cryptol/ModuleSystem/Exports.hs +++ b/src/Cryptol/ModuleSystem/Exports.hs @@ -3,14 +3,17 @@ module Cryptol.ModuleSystem.Exports where import Data.Set(Set) import qualified Data.Set as Set +import Data.Map(Map) +import qualified Data.Map as Map import Data.Foldable(fold) import Control.DeepSeq(NFData) import GHC.Generics (Generic) import Cryptol.Parser.AST -import Cryptol.Parser.Names +import Cryptol.Parser.Names(namesD,tnamesD,tnamesNT) +import Cryptol.ModuleSystem.Name -modExports :: Ord name => Module name -> ExportSpec name +modExports :: Ord name => ModuleG mname name -> ExportSpec name modExports m = fold (concat [ exportedNames d | d <- mDecls m ]) where names by td = [ td { tlValue = thing n } | n <- fst (by (tlValue td)) ] @@ -20,46 +23,61 @@ modExports m = fold (concat [ exportedNames d | d <- mDecls m ]) exportedNames (DPrimType t) = [ exportType (thing . primTName <$> t) ] exportedNames (TDNewtype nt) = map exportType (names tnamesNT nt) exportedNames (Include {}) = [] + exportedNames (DImport {}) = [] exportedNames (DParameterFun {}) = [] exportedNames (DParameterType {}) = [] exportedNames (DParameterConstraint {}) = [] + exportedNames (DModule nested) = + case tlValue nested of + NestedModule x -> + [exportName NSModule nested { tlValue = thing (mName x) }] -data ExportSpec name = ExportSpec { eTypes :: Set name - , eBinds :: Set name - } deriving (Show, Generic) +newtype ExportSpec name = ExportSpec (Map Namespace (Set name)) + deriving (Show, Generic) instance NFData name => NFData (ExportSpec name) instance Ord name => Semigroup (ExportSpec name) where - l <> r = ExportSpec { eTypes = eTypes l <> eTypes r - , eBinds = eBinds l <> eBinds r - } + ExportSpec l <> ExportSpec r = ExportSpec (Map.unionWith Set.union l r) instance Ord name => Monoid (ExportSpec name) where - mempty = ExportSpec { eTypes = mempty, eBinds = mempty } - mappend = (<>) + mempty = ExportSpec Map.empty + +exportName :: Ord name => Namespace -> TopLevel name -> ExportSpec name +exportName ns n + | tlExport n == Public = ExportSpec + $ Map.singleton ns + $ Set.singleton (tlValue n) + | otherwise = mempty + +exported :: Namespace -> ExportSpec name -> Set name +exported ns (ExportSpec mp) = Map.findWithDefault Set.empty ns mp -- | Add a binding name to the export list, if it should be exported. exportBind :: Ord name => TopLevel name -> ExportSpec name -exportBind n - | tlExport n == Public = mempty { eBinds = Set.singleton (tlValue n) } - | otherwise = mempty +exportBind = exportName NSValue -- | Add a type synonym name to the export list, if it should be exported. exportType :: Ord name => TopLevel name -> ExportSpec name -exportType n - | tlExport n == Public = mempty { eTypes = Set.singleton (tlValue n) } - | otherwise = mempty +exportType = exportName NSType + + + +isExported :: Ord name => Namespace -> name -> ExportSpec name -> Bool +isExported ns x (ExportSpec s) = + case Map.lookup ns s of + Nothing -> False + Just mp -> Set.member x mp -- | Check to see if a binding is exported. isExportedBind :: Ord name => name -> ExportSpec name -> Bool -isExportedBind n = Set.member n . eBinds +isExportedBind = isExported NSValue -- | Check to see if a type synonym is exported. isExportedType :: Ord name => name -> ExportSpec name -> Bool -isExportedType n = Set.member n . eTypes +isExportedType = isExported NSType diff --git a/src/Cryptol/ModuleSystem/InstantiateModule.hs b/src/Cryptol/ModuleSystem/InstantiateModule.hs index 749edd1cf..9d6b46729 100644 --- a/src/Cryptol/ModuleSystem/InstantiateModule.hs +++ b/src/Cryptol/ModuleSystem/InstantiateModule.hs @@ -1,4 +1,5 @@ {-# Language FlexibleInstances, PatternGuards #-} +{-# Language BlockArguments #-} -- | Assumes that local names do not shadow top level names. module Cryptol.ModuleSystem.InstantiateModule ( instantiateModule @@ -10,12 +11,13 @@ import Data.Map (Map) import qualified Data.Map as Map import MonadLib(ReaderT,runReaderT,ask) +import Cryptol.Utils.Panic(panic) +import Cryptol.Utils.Ident(ModName,modParamIdent) import Cryptol.Parser.Position(Located(..)) import Cryptol.ModuleSystem.Name import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst(listParamSubst, apSubst) import Cryptol.TypeCheck.SimpType(tRebuild) -import Cryptol.Utils.Ident(ModName,modParamIdent) {- XXX: Should we simplify constraints in the instantiated modules? @@ -33,15 +35,23 @@ instantiateModule :: FreshM m => ModName {- ^ Name of the new module -} -> Map TParam Type {- ^ Type params -} -> Map Name Expr {- ^ Value parameters -} -> - m ([Located Prop], Module) - -- ^ Instantiated constraints, fresh module, new supply -instantiateModule func newName tpMap vpMap = - runReaderT newName $ + m (Name -> Name, [Located Prop], Module) + -- ^ Renaming, instantiated constraints, fresh module, new supply +instantiateModule func newName tpMap vpMap + | not (null (mSubModules func)) = + panic "instantiateModule" + [ "XXX: we don't support functors with nested moduels yet." ] + | otherwise = + runReaderT (TopModule newName) $ do let oldVpNames = Map.keys vpMap newVpNames <- mapM freshParamName (Map.keys vpMap) let vpNames = Map.fromList (zip oldVpNames newVpNames) env <- computeEnv func tpMap vpNames + let ren x = case nameNamespace x of + NSValue -> Map.findWithDefault x x (funNameMap env) + NSType -> Map.findWithDefault x x (tyNameMap env) + NSModule -> x let rnMp :: Inst a => (a -> Name) -> Map Name a -> Map Name a rnMp f m = Map.fromList [ (f x, x) | a <- Map.elems m @@ -60,7 +70,8 @@ instantiateModule func newName tpMap vpMap = let renamedDecls = inst env (mDecls func) paramDecls = map (mkParamDecl su vpNames) (Map.toList vpMap) - return ( goals + return ( ren + , goals , Module { mName = newName , mExports = renamedExports @@ -72,6 +83,9 @@ instantiateModule func newName tpMap vpMap = , mParamConstraints = [] , mParamFuns = Map.empty , mDecls = paramDecls ++ renamedDecls + + , mSubModules = mempty + , mFunctors = mempty } ) where @@ -110,7 +124,7 @@ instance Defines DeclGroup where -------------------------------------------------------------------------------- -type InstM = ReaderT ModName +type InstM = ReaderT ModPath -- | Generate a new instance of a declared name. freshenName :: FreshM m => Name -> InstM m Name @@ -119,13 +133,15 @@ freshenName x = let sys = case nameInfo x of Declared _ s -> s _ -> UserName - liftSupply (mkDeclared m sys (nameIdent x) (nameFixity x) (nameLoc x)) + liftSupply (mkDeclared (nameNamespace x) + m sys (nameIdent x) (nameFixity x) (nameLoc x)) freshParamName :: FreshM m => Name -> InstM m Name freshParamName x = do m <- ask let newName = modParamIdent (nameIdent x) - liftSupply (mkDeclared m UserName newName (nameFixity x) (nameLoc x)) + liftSupply (mkDeclared (nameNamespace x) + m UserName newName (nameFixity x) (nameLoc x)) @@ -263,11 +279,14 @@ instance Inst UserTC where where y = Map.findWithDefault x x (tyNameMap env) instance Inst (ExportSpec Name) where - inst env es = ExportSpec { eTypes = Set.map instT (eTypes es) - , eBinds = Set.map instV (eBinds es) - } - where instT x = Map.findWithDefault x x (tyNameMap env) - instV x = Map.findWithDefault x x (funNameMap env) + inst env (ExportSpec spec) = ExportSpec (Map.mapWithKey doNS spec) + where + doNS ns = + case ns of + NSType -> Set.map \x -> Map.findWithDefault x x (tyNameMap env) + NSValue -> Set.map \x -> Map.findWithDefault x x (funNameMap env) + NSModule -> id + instance Inst TySyn where inst env ts = TySyn { tsName = instTyName env x diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs index 2e2d084ea..d8e2ad11f 100644 --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -12,24 +12,27 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-} module Cryptol.ModuleSystem.Interface ( - Iface(..) + Iface + , IfaceG(..) , IfaceDecls(..) , IfaceTySyn, ifTySynName , IfaceNewtype - , IfaceDecl(..), mkIfaceDecl + , IfaceDecl(..) , IfaceParams(..) - , genIface + , emptyIface , ifacePrimMap , noIfaceParams + , isEmptyIfaceParams + , ifaceIsFunctor + , flatPublicIface + , flatPublicDecls + , filterIfaceDecls + , ifaceDeclsNames ) where -import Cryptol.ModuleSystem.Name -import Cryptol.TypeCheck.AST -import Cryptol.Utils.Ident (ModName) -import Cryptol.Utils.Panic(panic) -import Cryptol.Parser.Position(Located) - +import Data.Set(Set) +import qualified Data.Set as Set import qualified Data.Map as Map import Data.Semigroup import Data.Text (Text) @@ -40,15 +43,52 @@ import Control.DeepSeq import Prelude () import Prelude.Compat +import Cryptol.ModuleSystem.Name +import Cryptol.Utils.Ident (ModName) +import Cryptol.Utils.Panic(panic) +import Cryptol.Utils.Fixity(Fixity) +import Cryptol.Parser.AST(Pragma) +import Cryptol.Parser.Position(Located) +import Cryptol.TypeCheck.Type + -- | The resulting interface generated by a module that has been typechecked. -data Iface = Iface - { ifModName :: !ModName -- ^ Module name +data IfaceG mname = Iface + { ifModName :: !mname -- ^ Module name , ifPublic :: IfaceDecls -- ^ Exported definitions , ifPrivate :: IfaceDecls -- ^ Private defintiions , ifParams :: IfaceParams -- ^ Uninterpreted constants (aka module params) } deriving (Show, Generic, NFData) +ifaceIsFunctor :: IfaceG mname -> Bool +ifaceIsFunctor = not . isEmptyIfaceParams . ifParams + +-- | The public declarations in all modules, including nested +-- The modules field contains public functors +-- Assumes that we are not a functor. +flatPublicIface :: IfaceG mname -> IfaceDecls +flatPublicIface iface = flatPublicDecls (ifPublic iface) + + +flatPublicDecls :: IfaceDecls -> IfaceDecls +flatPublicDecls ifs = mconcat ( ifs { ifModules = fun } + : map flatPublicIface (Map.elems nofun) + ) + + where + (fun,nofun) = Map.partition ifaceIsFunctor (ifModules ifs) + + +type Iface = IfaceG ModName + +emptyIface :: mname -> IfaceG mname +emptyIface nm = Iface + { ifModName = nm + , ifPublic = mempty + , ifPrivate = mempty + , ifParams = noIfaceParams + } + data IfaceParams = IfaceParams { ifParamTypes :: Map.Map Name ModTParam , ifParamConstraints :: [Located Prop] -- ^ Constraints on param. types @@ -62,29 +102,57 @@ noIfaceParams = IfaceParams , ifParamFuns = Map.empty } +isEmptyIfaceParams :: IfaceParams -> Bool +isEmptyIfaceParams IfaceParams { .. } = + Map.null ifParamTypes && null ifParamConstraints && Map.null ifParamFuns + data IfaceDecls = IfaceDecls { ifTySyns :: Map.Map Name IfaceTySyn , ifNewtypes :: Map.Map Name IfaceNewtype , ifAbstractTypes :: Map.Map Name IfaceAbstractType , ifDecls :: Map.Map Name IfaceDecl + , ifModules :: !(Map.Map Name (IfaceG Name)) } deriving (Show, Generic, NFData) +filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls +filterIfaceDecls p ifs = IfaceDecls + { ifTySyns = filterMap (ifTySyns ifs) + , ifNewtypes = filterMap (ifNewtypes ifs) + , ifAbstractTypes = filterMap (ifAbstractTypes ifs) + , ifDecls = filterMap (ifDecls ifs) + , ifModules = filterMap (ifModules ifs) + } + where + filterMap :: Map.Map Name a -> Map.Map Name a + filterMap = Map.filterWithKey (\k _ -> p k) + +ifaceDeclsNames :: IfaceDecls -> Set Name +ifaceDeclsNames i = Set.unions [ Map.keysSet (ifTySyns i) + , Map.keysSet (ifNewtypes i) + , Map.keysSet (ifAbstractTypes i) + , Map.keysSet (ifDecls i) + , Map.keysSet (ifModules i) + ] + + instance Semigroup IfaceDecls where l <> r = IfaceDecls { ifTySyns = Map.union (ifTySyns l) (ifTySyns r) , ifNewtypes = Map.union (ifNewtypes l) (ifNewtypes r) , ifAbstractTypes = Map.union (ifAbstractTypes l) (ifAbstractTypes r) , ifDecls = Map.union (ifDecls l) (ifDecls r) + , ifModules = Map.union (ifModules l) (ifModules r) } instance Monoid IfaceDecls where - mempty = IfaceDecls Map.empty Map.empty Map.empty Map.empty + mempty = IfaceDecls Map.empty Map.empty Map.empty Map.empty Map.empty mappend l r = l <> r mconcat ds = IfaceDecls { ifTySyns = Map.unions (map ifTySyns ds) , ifNewtypes = Map.unions (map ifNewtypes ds) , ifAbstractTypes = Map.unions (map ifAbstractTypes ds) , ifDecls = Map.unions (map ifDecls ds) + , ifModules = Map.unions (map ifModules ds) } type IfaceTySyn = TySyn @@ -104,61 +172,6 @@ data IfaceDecl = IfaceDecl , ifDeclDoc :: Maybe Text -- ^ Documentation } deriving (Show, Generic, NFData) -mkIfaceDecl :: Decl -> IfaceDecl -mkIfaceDecl d = IfaceDecl - { ifDeclName = dName d - , ifDeclSig = dSignature d - , ifDeclPragmas = dPragmas d - , ifDeclInfix = dInfix d - , ifDeclFixity = dFixity d - , ifDeclDoc = dDoc d - } - --- | Generate an Iface from a typechecked module. -genIface :: Module -> Iface -genIface m = Iface - { ifModName = mName m - - , ifPublic = IfaceDecls - { ifTySyns = tsPub - , ifNewtypes = ntPub - , ifAbstractTypes = atPub - , ifDecls = dPub - } - - , ifPrivate = IfaceDecls - { ifTySyns = tsPriv - , ifNewtypes = ntPriv - , ifAbstractTypes = atPriv - , ifDecls = dPriv - } - - , ifParams = IfaceParams - { ifParamTypes = mParamTypes m - , ifParamConstraints = mParamConstraints m - , ifParamFuns = mParamFuns m - } - } - where - - (tsPub,tsPriv) = - Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m ) - (mTySyns m) - (ntPub,ntPriv) = - Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m ) - (mNewtypes m) - - (atPub,atPriv) = - Map.partitionWithKey (\qn _ -> qn `isExportedType` mExports m) - (mPrimTypes m) - - (dPub,dPriv) = - Map.partitionWithKey (\ qn _ -> qn `isExportedBind` mExports m) - $ Map.fromList [ (qn,mkIfaceDecl d) | dg <- mDecls m - , d <- groupDecls dg - , let qn = dName d - ] - -- | Produce a PrimMap from an interface. -- diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index 304b72c40..7a478603f 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -21,6 +21,7 @@ import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Name (FreshM(..),Supply) import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning()) +import Cryptol.ModuleSystem.NamingEnv(NamingEnv) import qualified Cryptol.Parser as Parser import qualified Cryptol.Parser.AST as P import Cryptol.Parser.Position (Located) @@ -463,11 +464,15 @@ getImportSource = ModuleT $ do _ -> return (FromModule noModuleName) getIface :: P.ModName -> ModuleM Iface -getIface mn = - do env <- ModuleT get - case lookupModule mn env of - Just lm -> return (lmInterface lm) - Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)] +getIface mn = ($ mn) <$> getIfaces + +getIfaces :: ModuleM (P.ModName -> Iface) +getIfaces = doLookup <$> ModuleT get + where + doLookup env mn = + case lookupModule mn env of + Just lm -> lmInterface lm + Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)] getLoaded :: P.ModName -> ModuleM T.Module getLoaded mn = ModuleT $ @@ -505,14 +510,16 @@ unloadModule rm = ModuleT $ do env <- get set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) } -loadedModule :: ModulePath -> Fingerprint -> T.Module -> ModuleM () -loadedModule path fp m = ModuleT $ do +loadedModule :: + ModulePath -> Fingerprint -> NamingEnv -> T.Module -> ModuleM () +loadedModule path fp nameEnv m = ModuleT $ do env <- get ident <- case path of InFile p -> unModuleT $ io (canonicalizePath p) InMem l _ -> pure l - set $! env { meLoadedModules = addLoadedModule path ident fp m (meLoadedModules env) } + set $! env { meLoadedModules = addLoadedModule path ident fp nameEnv m + (meLoadedModules env) } modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM () modifyEvalEnv f = ModuleT $ do diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index 7570ebd5d..2dcc9e1d9 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -14,6 +14,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} -- for the instances of RunM and BaseM {-# LANGUAGE UndecidableInstances #-} @@ -26,10 +27,13 @@ module Cryptol.ModuleSystem.Name ( , nameInfo , nameLoc , nameFixity + , nameNamespace , asPrim - , cmpNameLexical - , cmpNameDisplay + , asOrigName , ppLocName + , Namespace(..) + , ModPath(..) + , cmpNameDisplay -- ** Creation , mkDeclared @@ -49,33 +53,35 @@ module Cryptol.ModuleSystem.Name ( , lookupPrimType ) where -import Cryptol.Parser.Position (Range,Located(..),emptyRange) -import Cryptol.Utils.Fixity -import Cryptol.Utils.Ident -import Cryptol.Utils.Panic -import Cryptol.Utils.PP - - import Control.DeepSeq import qualified Data.Map as Map import qualified Data.Monoid as M -import Data.Ord (comparing) -import qualified Data.Text as Text -import Data.Char(isAlpha,toUpper) import GHC.Generics (Generic) import MonadLib import Prelude () import Prelude.Compat +import qualified Data.Text as Text +import Data.Char(isAlpha,toUpper) + + + +import Cryptol.Parser.Position (Range,Located(..),emptyRange) +import Cryptol.Utils.Fixity +import Cryptol.Utils.Ident +import Cryptol.Utils.Panic +import Cryptol.Utils.PP + -- Names ----------------------------------------------------------------------- -- | Information about the binding site of the name. -data NameInfo = Declared !ModName !NameSource +data NameInfo = Declared !ModPath !NameSource -- ^ This name refers to a declaration from this module | Parameter -- ^ This name is a parameter (function or type) deriving (Eq, Show, Generic, NFData) + data Name = Name { nUnique :: {-# UNPACK #-} !Int -- ^ INVARIANT: this field uniquely identifies a name for one -- session with the Cryptol library. Names are unique to @@ -84,6 +90,8 @@ data Name = Name { nUnique :: {-# UNPACK #-} !Int , nInfo :: !NameInfo -- ^ Information about the origin of this name. + , nNamespace :: !Namespace + , nIdent :: !Ident -- ^ The name of the identifier @@ -100,6 +108,7 @@ data Name = Name { nUnique :: {-# UNPACK #-} !Int data NameSource = SystemName | UserName deriving (Generic, NFData, Show, Eq) + instance Eq Name where a == b = compare a b == EQ a /= b = compare a b /= EQ @@ -107,54 +116,41 @@ instance Eq Name where instance Ord Name where compare a b = compare (nUnique a) (nUnique b) --- | Compare two names lexically. -cmpNameLexical :: Name -> Name -> Ordering -cmpNameLexical l r = - case (nameInfo l, nameInfo r) of - - (Declared nsl _,Declared nsr _) -> - case compare nsl nsr of - EQ -> comparing nameIdent l r - cmp -> cmp - - (Parameter,Parameter) -> comparing nameIdent l r - - (Declared nsl _,Parameter) -> compare (modNameToText nsl) - (identText (nameIdent r)) - (Parameter,Declared nsr _) -> compare (identText (nameIdent l)) - (modNameToText nsr) -- | Compare two names by the way they would be displayed. +-- This is used to order names nicely when showing what's in scope cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering cmpNameDisplay disp l r = - case (nameInfo l, nameInfo r) of + case (asOrigName l, asOrigName r) of - (Declared nsl _, Declared nsr _) -> -- XXX: uses system name info? - let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp) - pfxr = fmtModName nsr (getNameFormat nsr (nameIdent r) disp) - in case cmpText pfxl pfxr of - EQ -> cmpName l r - cmp -> cmp + (Just ogl, Just ogr) -> -- XXX: uses system name info? + case cmpText (fmtPref ogl) (fmtPref ogr) of + EQ -> cmpName l r + cmp -> cmp - (Parameter,Parameter) -> cmpName l r + (Nothing,Nothing) -> cmpName l r - (Declared nsl _,Parameter) -> - let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp) - in case cmpText pfxl (identText (nameIdent r)) of - EQ -> GT - cmp -> cmp + (Just ogl,Nothing) -> + case cmpText (fmtPref ogl) (identText (nameIdent r)) of + EQ -> GT + cmp -> cmp - (Parameter,Declared nsr _) -> - let pfxr = fmtModName nsr (getNameFormat nsr (nameIdent r) disp) - in case cmpText (identText (nameIdent l)) pfxr of - EQ -> LT - cmp -> cmp + (Nothing,Just ogr) -> + case cmpText (identText (nameIdent l)) (fmtPref ogr) of + EQ -> LT + cmp -> cmp where cmpName xs ys = cmpIdent (nameIdent xs) (nameIdent ys) cmpIdent xs ys = cmpText (identText xs) (identText ys) + --- let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp) + fmtPref og = case getNameFormat og disp of + UnQualified -> "" + Qualified q -> modNameToText q + NotInScope -> Text.pack $ show $ pp (ogModule og) + -- Note that this assumes that `xs` is `l` and `ys` is `r` cmpText xs ys = case (Text.null xs, Text.null ys) of @@ -169,22 +165,17 @@ cmpNameDisplay disp l r = | a == '_' = 1 | otherwise = 0 + + -- | Figure out how the name should be displayed, by referencing the display -- function in the environment. NOTE: this function doesn't take into account -- the need for parentheses. ppName :: Name -> Doc -ppName Name { .. } = - case nInfo of - - Declared m _ -> withNameDisp $ \disp -> - case getNameFormat m nIdent disp of - Qualified m' -> ppQual m' <.> pp nIdent - UnQualified -> pp nIdent - NotInScope -> ppQual m <.> pp nIdent -- XXX: only when not in scope? - where - ppQual mo = if mo == exprModName then empty else pp mo <.> text "::" +ppName nm = + case asOrigName nm of + Just og -> pp og + Nothing -> pp (nameIdent nm) - Parameter -> pp nIdent instance PP Name where ppPrec _ = ppPrefixName @@ -199,6 +190,7 @@ instance PPName Name where ppPrefixName n @ Name { .. } = optParens (isInfixIdent nIdent) (ppName n) + -- | Pretty-print a name with its source location information. ppLocName :: Name -> Doc ppLocName n = pp Located { srcRange = nameLoc n, thing = n } @@ -209,6 +201,9 @@ nameUnique = nUnique nameIdent :: Name -> Ident nameIdent = nIdent +nameNamespace :: Name -> Namespace +nameNamespace = nNamespace + nameInfo :: Name -> NameInfo nameInfo = nInfo @@ -218,22 +213,32 @@ nameLoc = nLoc nameFixity :: Name -> Maybe Fixity nameFixity = nFixity - +-- | Primtiives must be in a top level module, at least for now. asPrim :: Name -> Maybe PrimIdent asPrim Name { .. } = case nInfo of - Declared p _ -> Just $ PrimIdent p $ identText nIdent - _ -> Nothing + Declared (TopModule m) _ -> Just $ PrimIdent m $ identText nIdent + _ -> Nothing toParamInstName :: Name -> Name toParamInstName n = case nInfo n of - Declared m s -> n { nInfo = Declared (paramInstModName m) s } + Declared m s -> n { nInfo = Declared (apPathRoot paramInstModName m) s } Parameter -> n asParamName :: Name -> Name asParamName n = n { nInfo = Parameter } +asOrigName :: Name -> Maybe OrigName +asOrigName nm = + case nInfo nm of + Declared p _ -> + Just OrigName { ogModule = apPathRoot notParamInstModName p + , ogNamespace = nNamespace nm + , ogName = nIdent nm + } + Parameter -> Nothing + -- Name Supply ----------------------------------------------------------------- @@ -321,15 +326,17 @@ nextUnique (Supply n) = s' `seq` (n,s') -- Name Construction ----------------------------------------------------------- -- | Make a new name for a declaration. -mkDeclared :: ModName -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name,Supply) -mkDeclared m sys nIdent nFixity nLoc s = +mkDeclared :: + Namespace -> ModPath -> NameSource -> Ident -> Maybe Fixity -> Range -> + Supply -> (Name,Supply) +mkDeclared nNamespace m sys nIdent nFixity nLoc s = let (nUnique,s') = nextUnique s nInfo = Declared m sys in (Name { .. }, s') -- | Make a new parameter name. -mkParameter :: Ident -> Range -> Supply -> (Name,Supply) -mkParameter nIdent nLoc s = +mkParameter :: Namespace -> Ident -> Range -> Supply -> (Name,Supply) +mkParameter nNamespace nIdent nLoc s = let (nUnique,s') = nextUnique s nFixity = Nothing in (Name { nInfo = Parameter, .. }, s') @@ -340,6 +347,7 @@ paramModRecParam = Name { nInfo = Parameter , nIdent = packIdent "$modParams" , nLoc = emptyRange , nUnique = 0x01 + , nNamespace = NSValue } -- Prim Maps ------------------------------------------------------------------- diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index 92b550288..4426dac4e 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -15,23 +15,17 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE BlockArguments #-} module Cryptol.ModuleSystem.NamingEnv where -import Cryptol.ModuleSystem.Interface -import Cryptol.ModuleSystem.Name -import Cryptol.Parser.AST -import Cryptol.Parser.Name(isGeneratedName) -import Cryptol.Parser.Position -import qualified Cryptol.TypeCheck.AST as T -import Cryptol.Utils.PP -import Cryptol.Utils.Panic (panic) - import Data.List (nub) -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe,mapMaybe,maybeToList) +import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map +import Data.Set (Set) import qualified Data.Set as Set import Data.Semigroup -import MonadLib (runId,Id) +import MonadLib (runId,Id,StateT,runStateT,lift,sets_,forM_) import GHC.Generics (Generic) import Control.DeepSeq @@ -39,46 +33,71 @@ import Control.DeepSeq import Prelude () import Prelude.Compat +import Cryptol.Utils.PP +import Cryptol.Utils.Panic (panic) +import Cryptol.Parser.AST +import Cryptol.Parser.Name(isGeneratedName) +import Cryptol.Parser.Position +import qualified Cryptol.TypeCheck.AST as T +import Cryptol.ModuleSystem.Interface +import Cryptol.ModuleSystem.Name + -- Naming Environment ---------------------------------------------------------- -- | The 'NamingEnv' is used by the renamer to determine what -- identifiers refer to. -data NamingEnv = NamingEnv { neExprs :: !(Map.Map PName [Name]) - -- ^ Expr renaming environment - , neTypes :: !(Map.Map PName [Name]) - -- ^ Type renaming environment - } deriving (Show, Generic, NFData) +newtype NamingEnv = NamingEnv (Map Namespace (Map PName [Name])) + deriving (Show,Generic,NFData) + +-- | All names mentioned in the environment +namingEnvNames :: NamingEnv -> Set Name +namingEnvNames (NamingEnv xs) = + Set.fromList $ concatMap (concat . Map.elems) $ Map.elems xs + + +-- | Get the names in a given namespace +namespaceMap :: Namespace -> NamingEnv -> Map PName [Name] +namespaceMap ns (NamingEnv env) = Map.findWithDefault Map.empty ns env + +-- | Resolve a name in the given namespace. +lookupNS :: Namespace -> PName -> NamingEnv -> [Name] +lookupNS ns x = Map.findWithDefault [] x . namespaceMap ns -- | Return a list of value-level names to which this parsed name may refer. lookupValNames :: PName -> NamingEnv -> [Name] -lookupValNames qn ro = Map.findWithDefault [] qn (neExprs ro) +lookupValNames = lookupNS NSValue -- | Return a list of type-level names to which this parsed name may refer. lookupTypeNames :: PName -> NamingEnv -> [Name] -lookupTypeNames qn ro = Map.findWithDefault [] qn (neTypes ro) +lookupTypeNames = lookupNS NSType +-- | Singleton renaming environment for the given namespace. +singletonNS :: Namespace -> PName -> Name -> NamingEnv +singletonNS ns pn n = NamingEnv (Map.singleton ns (Map.singleton pn [n])) +-- | Singleton expression renaming environment. +singletonE :: PName -> Name -> NamingEnv +singletonE = singletonNS NSValue -instance Semigroup NamingEnv where - l <> r = - NamingEnv { neExprs = Map.unionWith merge (neExprs l) (neExprs r) - , neTypes = Map.unionWith merge (neTypes l) (neTypes r) } +-- | Singleton type renaming environment. +singletonT :: PName -> Name -> NamingEnv +singletonT = singletonNS NSType -instance Monoid NamingEnv where - mempty = - NamingEnv { neExprs = Map.empty - , neTypes = Map.empty } - mappend l r = l <> r +namingEnvRename :: (Name -> Name) -> NamingEnv -> NamingEnv +namingEnvRename f (NamingEnv mp) = NamingEnv (ren <$> mp) + where + ren nsm = map f <$> nsm + - mconcat envs = - NamingEnv { neExprs = Map.unionsWith merge (map neExprs envs) - , neTypes = Map.unionsWith merge (map neTypes envs) } +instance Semigroup NamingEnv where + NamingEnv l <> NamingEnv r = + NamingEnv (Map.unionWith (Map.unionWith merge) l r) +instance Monoid NamingEnv where + mempty = NamingEnv Map.empty {-# INLINE mempty #-} - {-# INLINE mappend #-} - {-# INLINE mconcat #-} -- | Merge two name maps, collapsing cases where the entries are the same, and @@ -90,59 +109,53 @@ merge xs ys | xs == ys = xs -- | Generate a mapping from 'PrimIdent' to 'Name' for a -- given naming environment. toPrimMap :: NamingEnv -> PrimMap -toPrimMap NamingEnv { .. } = PrimMap { .. } +toPrimMap env = + PrimMap + { primDecls = fromNS NSValue + , primTypes = fromNS NSType + } where + fromNS ns = Map.fromList + [ entry x | xs <- Map.elems (namespaceMap ns env), x <- xs ] + entry n = case asPrim n of Just p -> (p,n) Nothing -> panic "toPrimMap" [ "Not a declared name?" , show n ] - primDecls = Map.fromList [ entry n | ns <- Map.elems neExprs, n <- ns ] - primTypes = Map.fromList [ entry n | ns <- Map.elems neTypes, n <- ns ] -- | Generate a display format based on a naming environment. toNameDisp :: NamingEnv -> NameDisp -toNameDisp NamingEnv { .. } = NameDisp display +toNameDisp env = NameDisp (`Map.lookup` names) where - display mn ident = Map.lookup (mn,ident) names - - -- only format declared names, as parameters don't need any special - -- formatting. names = Map.fromList - $ [ mkEntry (mn, nameIdent n) pn | (pn,ns) <- Map.toList neExprs - , n <- ns - , Declared mn _ <- [nameInfo n] ] - - ++ [ mkEntry (mn, nameIdent n) pn | (pn,ns) <- Map.toList neTypes - , n <- ns - , Declared mn _ <- [nameInfo n] ] - - mkEntry key pn = (key,fmt) - where fmt = case getModName pn of - Just ns -> Qualified ns - Nothing -> UnQualified + [ (og, qn) + | ns <- [ NSValue, NSType, NSModule ] + , (pn,xs) <- Map.toList (namespaceMap ns env) + , x <- xs + , og <- maybeToList (asOrigName x) + , let qn = case getModName pn of + Just q -> Qualified q + Nothing -> UnQualified + ] -- | Produce sets of visible names for types and declarations. -- --- NOTE: if entries in the NamingEnv would have produced a name clash, they will --- be omitted from the resulting sets. -visibleNames :: NamingEnv -> ({- types -} Set.Set Name - ,{- decls -} Set.Set Name) - -visibleNames NamingEnv { .. } = (types,decls) +-- NOTE: if entries in the NamingEnv would have produced a name clash, +-- they will be omitted from the resulting sets. +visibleNames :: NamingEnv -> Map Namespace (Set Name) +visibleNames (NamingEnv env) = Set.fromList . mapMaybe check . Map.elems <$> env where - types = Set.fromList [ n | [n] <- Map.elems neTypes ] - decls = Set.fromList [ n | [n] <- Map.elems neExprs ] + check names = + case names of + [name] -> Just name + _ -> Nothing -- | Qualify all symbols in a 'NamingEnv' with the given prefix. qualify :: ModName -> NamingEnv -> NamingEnv -qualify pfx NamingEnv { .. } = - NamingEnv { neExprs = Map.mapKeys toQual neExprs - , neTypes = Map.mapKeys toQual neTypes - } - +qualify pfx (NamingEnv env) = NamingEnv (Map.mapKeys toQual <$> env) where -- XXX we don't currently qualify fresh names toQual (Qual _ n) = Qual pfx n @@ -150,53 +163,84 @@ qualify pfx NamingEnv { .. } = toQual n@NewName{} = n filterNames :: (PName -> Bool) -> NamingEnv -> NamingEnv -filterNames p NamingEnv { .. } = - NamingEnv { neExprs = Map.filterWithKey check neExprs - , neTypes = Map.filterWithKey check neTypes - } - where - check :: PName -> a -> Bool - check n _ = p n +filterNames p (NamingEnv env) = NamingEnv (Map.filterWithKey check <$> env) + where check n _ = p n --- | Singleton type renaming environment. -singletonT :: PName -> Name -> NamingEnv -singletonT qn tn = mempty { neTypes = Map.singleton qn [tn] } - --- | Singleton expression renaming environment. -singletonE :: PName -> Name -> NamingEnv -singletonE qn en = mempty { neExprs = Map.singleton qn [en] } - -- | Like mappend, but when merging, prefer values on the lhs. shadowing :: NamingEnv -> NamingEnv -> NamingEnv -shadowing l r = NamingEnv - { neExprs = Map.union (neExprs l) (neExprs r) - , neTypes = Map.union (neTypes l) (neTypes r) } +shadowing (NamingEnv l) (NamingEnv r) = NamingEnv (Map.unionWith Map.union l r) travNamingEnv :: Applicative f => (Name -> f Name) -> NamingEnv -> f NamingEnv -travNamingEnv f ne = NamingEnv <$> neExprs' <*> neTypes' - where - neExprs' = traverse (traverse f) (neExprs ne) - neTypes' = traverse (traverse f) (neTypes ne) +travNamingEnv f (NamingEnv mp) = + NamingEnv <$> traverse (traverse (traverse f)) mp -data InModule a = InModule !ModName a +{- | Do somethign in context. If `Nothing` than we are working with +a local declaration. Otherwise we are at the top-level of the +given module. -} +data InModule a = InModule (Maybe ModPath) a deriving (Functor,Traversable,Foldable,Show) --- | Generate a 'NamingEnv' using an explicit supply. -namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv,Supply) -namingEnv' a supply = runId (runSupplyT supply (runBuild (namingEnv a))) - -newTop :: FreshM m => ModName -> PName -> Maybe Fixity -> Range -> m Name -newTop ns thing fx rng = liftSupply (mkDeclared ns src (getIdent thing) fx rng) +newTop :: + FreshM m => Namespace -> ModPath -> PName -> Maybe Fixity -> Range -> m Name +newTop ns m thing fx rng = + liftSupply (mkDeclared ns m src (getIdent thing) fx rng) where src = if isGeneratedName thing then SystemName else UserName -newLocal :: FreshM m => PName -> Range -> m Name -newLocal thing rng = liftSupply (mkParameter (getIdent thing) rng) +newLocal :: FreshM m => Namespace -> PName -> Range -> m Name +newLocal ns thing rng = liftSupply (mkParameter ns (getIdent thing) rng) newtype BuildNamingEnv = BuildNamingEnv { runBuild :: SupplyT Id NamingEnv } + +buildNamingEnv :: BuildNamingEnv -> Supply -> (NamingEnv,Supply) +buildNamingEnv b supply = runId $ runSupplyT supply $ runBuild b + +-- | Generate a 'NamingEnv' using an explicit supply. +defsOf :: BindsNames a => a -> Supply -> (NamingEnv,Supply) +defsOf = buildNamingEnv . namingEnv + + +-------------------------------------------------------------------------------- +-- Collect definitions of nested modules + +type NestedMods = Map Name NamingEnv +type CollectM = StateT NestedMods (SupplyT Id) + +collectNestedModules :: + NamingEnv -> Module PName -> Supply -> (NestedMods, Supply) +collectNestedModules env m = + collectNestedModulesDecls env (thing (mName m)) (mDecls m) + +collectNestedModulesDecls :: + NamingEnv -> ModName -> [TopDecl PName] -> Supply -> (NestedMods, Supply) +collectNestedModulesDecls env m ds sup = (mp,newS) + where + s0 = Map.empty + mpath = TopModule m + ((_,mp),newS) = runId $ runSupplyT sup $ runStateT s0 $ + collectNestedModulesDs mpath env ds + +collectNestedModulesDs :: ModPath -> NamingEnv -> [TopDecl PName] -> CollectM () +collectNestedModulesDs mpath env ds = + forM_ [ tlValue nm | DModule nm <- ds ] \(NestedModule nested) -> + do let pname = thing (mName nested) + name = case lookupNS NSModule pname env of + [n] -> n + _ -> panic "collectedNestedModulesDs" + [ "Missing/ambi definition for " ++ show pname ] + newEnv <- lift (runBuild (moduleDefs (Nested mpath (nameIdent name)) nested)) + sets_ (Map.insert name newEnv) + let newMPath = Nested mpath (nameIdent name) + collectNestedModulesDs newMPath newEnv (mDecls nested) + +-------------------------------------------------------------------------------- + + + + instance Semigroup BuildNamingEnv where BuildNamingEnv a <> BuildNamingEnv b = BuildNamingEnv $ do x <- a @@ -212,6 +256,10 @@ instance Monoid BuildNamingEnv where do ns <- sequence (map runBuild bs) return (mconcat ns) +-------------------------------------------------------------------------------- + + + -- | Things that define exported names. class BindsNames a where namingEnv :: a -> BuildNamingEnv @@ -235,12 +283,12 @@ instance BindsNames (Schema PName) where {-# INLINE namingEnv #-} --- | Interpret an import in the context of an interface, to produce a name --- environment for the renamer, and a 'NameDisp' for pretty-printing. -interpImport :: Import {- ^ The import declarations -} -> - IfaceDecls {- ^ Declarations of imported module -} -> + +-- | Adapt the things exported by something to the specific import/open. +interpImportEnv :: ImportG name {- ^ The import declarations -} -> + NamingEnv {- ^ All public things coming in -} -> NamingEnv -interpImport imp publicDecls = qualified +interpImportEnv imp public = qualified where -- optionally qualify names based on the import @@ -257,16 +305,21 @@ interpImport imp publicDecls = qualified | otherwise = public - -- generate the initial environment from the public interface, where no names - -- are qualified - public = unqualifiedEnv publicDecls + + +-- | Interpret an import in the context of an interface, to produce a name +-- environment for the renamer, and a 'NameDisp' for pretty-printing. +interpImportIface :: Import {- ^ The import declarations -} -> + IfaceDecls {- ^ Declarations of imported module -} -> + NamingEnv +interpImportIface imp = interpImportEnv imp . unqualifiedEnv -- | Generate a naming environment from a declaration interface, where none of -- the names are qualified. unqualifiedEnv :: IfaceDecls -> NamingEnv unqualifiedEnv IfaceDecls { .. } = - mconcat [ exprs, tySyns, ntTypes, absTys, ntExprs ] + mconcat [ exprs, tySyns, ntTypes, absTys, ntExprs, mods ] where toPName n = mkUnqual (nameIdent n) @@ -275,16 +328,17 @@ unqualifiedEnv IfaceDecls { .. } = ntTypes = mconcat [ singletonT (toPName n) n | n <- Map.keys ifNewtypes ] absTys = mconcat [ singletonT (toPName n) n | n <- Map.keys ifAbstractTypes ] ntExprs = mconcat [ singletonE (toPName n) n | n <- Map.keys ifNewtypes ] - + mods = mconcat [ singletonNS NSModule (toPName n) n + | n <- Map.keys ifModules ] -- | Compute an unqualified naming environment, containing the various module -- parameters. modParamsNamingEnv :: IfaceParams -> NamingEnv modParamsNamingEnv IfaceParams { .. } = - NamingEnv { neExprs = Map.fromList $ map fromFu $ Map.keys ifParamFuns - , neTypes = Map.fromList $ map fromTy $ Map.elems ifParamTypes - } - + NamingEnv $ Map.fromList + [ (NSValue, Map.fromList $ map fromFu $ Map.keys ifParamFuns) + , (NSType, Map.fromList $ map fromTy $ Map.elems ifParamTypes) + ] where toPName n = mkUnqual (nameIdent n) @@ -301,14 +355,16 @@ data ImportIface = ImportIface Import Iface -- mapping only from unqualified names to qualified ones. instance BindsNames ImportIface where namingEnv (ImportIface imp Iface { .. }) = BuildNamingEnv $ - return (interpImport imp ifPublic) + return (interpImportIface imp ifPublic) {-# INLINE namingEnv #-} -- | Introduce the name instance BindsNames (InModule (Bind PName)) where - namingEnv (InModule ns b) = BuildNamingEnv $ + namingEnv (InModule mb b) = BuildNamingEnv $ do let Located { .. } = bName b - n <- newTop ns thing (bFixity b) srcRange + n <- case mb of + Just m -> newTop NSValue m thing (bFixity b) srcRange + Nothing -> newLocal NSValue thing srcRange -- local fixitiies? return (singletonE thing n) @@ -316,15 +372,18 @@ instance BindsNames (InModule (Bind PName)) where instance BindsNames (TParam PName) where namingEnv TParam { .. } = BuildNamingEnv $ do let range = fromMaybe emptyRange tpRange - n <- newLocal tpName range + n <- newLocal NSType tpName range return (singletonT tpName n) -- | The naming environment for a single module. This is the mapping from -- unqualified names to fully qualified names with uniques. instance BindsNames (Module PName) where - namingEnv Module { .. } = foldMap (namingEnv . InModule ns) mDecls - where - ns = thing mName + namingEnv m = moduleDefs (TopModule (thing (mName m))) m + + +moduleDefs :: ModPath -> ModuleG mname PName -> BuildNamingEnv +moduleDefs m Module { .. } = foldMap (namingEnv . InModule (Just m)) mDecls + instance BindsNames (InModule (TopDecl PName)) where namingEnv (InModule ns td) = @@ -335,60 +394,70 @@ instance BindsNames (InModule (TopDecl PName)) where DParameterType d -> namingEnv (InModule ns d) DParameterConstraint {} -> mempty DParameterFun d -> namingEnv (InModule ns d) - Include _ -> mempty + Include _ -> mempty + DImport {} -> mempty -- see 'openLoop' in the renamer + DModule m -> namingEnv (InModule ns (tlValue m)) + + +instance BindsNames (InModule (NestedModule PName)) where + namingEnv (InModule ~(Just m) (NestedModule mdef)) = BuildNamingEnv $ + do let pnmame = mName mdef + nm <- newTop NSModule m (thing pnmame) Nothing (srcRange pnmame) + pure (singletonNS NSModule (thing pnmame) nm) instance BindsNames (InModule (PrimType PName)) where - namingEnv (InModule ns PrimType { .. }) = + namingEnv (InModule ~(Just m) PrimType { .. }) = BuildNamingEnv $ do let Located { .. } = primTName - nm <- newTop ns thing primTFixity srcRange + nm <- newTop NSType m thing primTFixity srcRange pure (singletonT thing nm) instance BindsNames (InModule (ParameterFun PName)) where - namingEnv (InModule ns ParameterFun { .. }) = BuildNamingEnv $ + namingEnv (InModule ~(Just ns) ParameterFun { .. }) = BuildNamingEnv $ do let Located { .. } = pfName - ntName <- newTop ns thing pfFixity srcRange + ntName <- newTop NSValue ns thing pfFixity srcRange return (singletonE thing ntName) instance BindsNames (InModule (ParameterType PName)) where - namingEnv (InModule ns ParameterType { .. }) = BuildNamingEnv $ + namingEnv (InModule ~(Just ns) ParameterType { .. }) = BuildNamingEnv $ -- XXX: we don't seem to have a fixity environment at the type level do let Located { .. } = ptName - ntName <- newTop ns thing Nothing srcRange + ntName <- newTop NSType ns thing Nothing srcRange return (singletonT thing ntName) -- NOTE: we use the same name at the type and expression level, as there's only -- ever one name introduced in the declaration. The names are only ever used in -- different namespaces, so there's no ambiguity. instance BindsNames (InModule (Newtype PName)) where - namingEnv (InModule ns Newtype { .. }) = BuildNamingEnv $ + namingEnv (InModule ~(Just ns) Newtype { .. }) = BuildNamingEnv $ do let Located { .. } = nName - ntName <- newTop ns thing Nothing srcRange + ntName <- newTop NSType ns thing Nothing srcRange + -- XXX: the name reuse here is sketchy return (singletonT thing ntName `mappend` singletonE thing ntName) -- | The naming environment for a single declaration. instance BindsNames (InModule (Decl PName)) where namingEnv (InModule pfx d) = case d of - DBind b -> BuildNamingEnv $ - do n <- mkName (bName b) (bFixity b) - return (singletonE (thing (bName b)) n) - + DBind b -> namingEnv (InModule pfx b) DSignature ns _sig -> foldMap qualBind ns DPragma ns _p -> foldMap qualBind ns DType syn -> qualType (tsName syn) (tsFixity syn) DProp syn -> qualType (psName syn) (psFixity syn) DLocated d' _ -> namingEnv (InModule pfx d') - DPatBind _pat _e -> panic "ModuleSystem" ["Unexpected pattern binding"] - DFixity{} -> panic "ModuleSystem" ["Unexpected fixity declaration"] + DRec {} -> panic "namingEnv" [ "DRec" ] + DPatBind _pat _e -> panic "namingEnv" ["Unexpected pattern binding"] + DFixity{} -> panic "namingEnv" ["Unexpected fixity declaration"] where - mkName ln fx = newTop pfx (thing ln) fx (srcRange ln) + mkName ns ln fx = case pfx of + Just m -> newTop ns m (thing ln) fx (srcRange ln) + Nothing -> newLocal ns (thing ln) (srcRange ln) qualBind ln = BuildNamingEnv $ - do n <- mkName ln Nothing + do n <- mkName NSValue ln Nothing return (singletonE (thing ln) n) qualType ln f = BuildNamingEnv $ - do n <- mkName ln f + do n <- mkName NSType ln f return (singletonT (thing ln) n) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 30ca109c6..35c61c191 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -6,19 +6,13 @@ -- Stability : provisional -- Portability : portable -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE OverloadedStrings #-} +{-# Language RecordWildCards #-} +{-# Language FlexibleInstances #-} +{-# Language FlexibleContexts #-} +{-# Language BlockArguments #-} module Cryptol.ModuleSystem.Renamer ( NamingEnv(), shadowing - , BindsNames(..), InModule(..), namingEnv' - , checkNamingEnv + , BindsNames(..), InModule(..) , shadowNames , Rename(..), runRenamer, RenameM() , RenamerError(..) @@ -26,428 +20,437 @@ module Cryptol.ModuleSystem.Renamer ( , renameVar , renameType , renameModule + , renameTopDecls + , RenamerInfo(..) + , NameType(..) + , RenamedModule(..) ) where -import Cryptol.ModuleSystem.Name -import Cryptol.ModuleSystem.NamingEnv -import Cryptol.ModuleSystem.Exports -import Cryptol.Parser.AST -import Cryptol.Parser.Position -import Cryptol.Parser.Selector(ppNestedSels,selName) -import Cryptol.Utils.Panic (panic) -import Cryptol.Utils.PP -import Cryptol.Utils.RecordMap +import Prelude () +import Prelude.Compat -import Data.List(find) -import qualified Data.Foldable as F -import Data.Map.Strict ( Map ) +import Data.Either(partitionEithers) +import Data.Maybe(fromJust) +import Data.List(find,foldl') +import Data.Foldable(toList) +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 Data.Set (Set) import qualified Data.Set as Set +import Data.Graph(SCC(..)) +import Data.Graph.SCC(stronglyConnComp) import MonadLib hiding (mapM, mapM_) -import GHC.Generics (Generic) -import Control.DeepSeq - -import Prelude () -import Prelude.Compat - --- Errors ---------------------------------------------------------------------- - -data RenamerError - = MultipleSyms (Located PName) [Name] NameDisp - -- ^ Multiple imported symbols contain this name - - | UnboundExpr (Located PName) NameDisp - -- ^ Expression name is not bound to any definition - - | UnboundType (Located PName) NameDisp - -- ^ Type name is not bound to any definition - - | OverlappingSyms [Name] NameDisp - -- ^ An environment has produced multiple overlapping symbols - - | ExpectedValue (Located PName) NameDisp - -- ^ When a value is expected from the naming environment, but one or more - -- types exist instead. - - | ExpectedType (Located PName) NameDisp - -- ^ When a type is missing from the naming environment, but one or more - -- values exist with the same name. - - | FixityError (Located Name) Fixity (Located Name) Fixity NameDisp - -- ^ When the fixity of two operators conflict - - | InvalidConstraint (Type PName) NameDisp - -- ^ When it's not possible to produce a Prop from a Type. - - | MalformedBuiltin (Type PName) PName NameDisp - -- ^ When a builtin type/type-function is used incorrectly. - - | BoundReservedType PName (Maybe Range) Doc NameDisp - -- ^ When a builtin type is named in a binder. - | OverlappingRecordUpdate (Located [Selector]) (Located [Selector]) NameDisp - -- ^ When record updates overlap (e.g., @{ r | x = e1, x.y = e2 }@) - deriving (Show, Generic, NFData) - -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 f1 o2 f2 disp -> fixNameDisp disp $ - hang (text "[error] at" <+> pp (srcRange o1) <+> text "and" <+> pp (srcRange o2)) - 4 (fsep [ text "The fixities of" - , nest 2 $ vcat - [ "•" <+> pp (thing o1) <+> parens (pp f1) - , "•" <+> pp (thing o2) <+> parens (pp f2) ] - , text "are not compatible." - , text "You may use explicit parentheses 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" ]) - - MalformedBuiltin ty pn disp -> fixNameDisp disp $ - hang (text "[error]" <+> maybe empty (\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 disp -> fixNameDisp disp $ - hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) loc) - 4 (fsep [ text "built-in type", quotes (pp n), text "shadowed in", src ]) - - OverlappingRecordUpdate xs ys disp -> fixNameDisp disp $ - hang "[error] Overlapping record updates:" - 4 (vcat [ ppLab xs, ppLab ys ]) - where - ppLab as = ppNestedSels (thing as) <+> "at" <+> pp (srcRange as) +import Cryptol.ModuleSystem.Name +import Cryptol.ModuleSystem.NamingEnv +import Cryptol.ModuleSystem.Exports +import Cryptol.Parser.Position(getLoc) +import Cryptol.Parser.AST +import Cryptol.Parser.Selector(selName) +import Cryptol.Utils.Panic (panic) +import Cryptol.Utils.RecordMap +import Cryptol.Utils.Ident(allNamespaces,packModName) --- Warnings -------------------------------------------------------------------- +import Cryptol.ModuleSystem.Interface +import Cryptol.ModuleSystem.Renamer.Error +import Cryptol.ModuleSystem.Renamer.Monad -data RenamerWarning - = SymbolShadowed Name [Name] NameDisp - - | UnusedName Name NameDisp - deriving (Show, Generic, NFData) - -instance PP RenamerWarning where - ppPrec _ (SymbolShadowed new originals disp) = fixNameDisp disp $ - hang (text "[warning] at" <+> loc) - 4 $ fsep [ text "This binding for" <+> backticks sym - , text "shadows the existing binding" <.> plural <+> - text "at" ] - $$ vcat (map (pp . nameLoc) originals) - - where - plural | length originals > 1 = char 's' - | otherwise = empty - - loc = pp (nameLoc new) - sym = pp new - - ppPrec _ (UnusedName x disp) = fixNameDisp disp $ - hang (text "[warning] at" <+> pp (nameLoc x)) - 4 (text "Unused name:" <+> pp x) - - -data RenamerWarnings = RenamerWarnings - { renWarnNameDisp :: !NameDisp - , renWarnShadow :: Map Name (Set Name) - , renWarnUnused :: Set Name - } -noRenamerWarnings :: RenamerWarnings -noRenamerWarnings = RenamerWarnings - { renWarnNameDisp = mempty - , renWarnShadow = Map.empty - , renWarnUnused = Set.empty +data RenamedModule = RenamedModule + { rmModule :: Module Name -- ^ The renamed module + , rmDefines :: NamingEnv -- ^ What this module defines + , rmInScope :: NamingEnv -- ^ What's in scope in this module + , rmImported :: IfaceDecls -- ^ Imported declarations } -addRenamerWarning :: RenamerWarning -> RenamerWarnings -> RenamerWarnings -addRenamerWarning w ws = - case w of - SymbolShadowed x xs d -> - ws { renWarnNameDisp = renWarnNameDisp ws <> d - , renWarnShadow = Map.insertWith Set.union x (Set.fromList xs) - (renWarnShadow ws) - } - UnusedName x d -> - ws { renWarnNameDisp = renWarnNameDisp ws <> d - , renWarnUnused = Set.insert x (renWarnUnused ws) - } - -listRenamerWarnings :: RenamerWarnings -> [RenamerWarning] -listRenamerWarnings ws = - [ mk (UnusedName x) | x <- Set.toList (renWarnUnused ws) ] ++ - [ mk (SymbolShadowed x (Set.toList xs)) - | (x,xs) <- Map.toList (renWarnShadow ws) ] +renameModule :: Module PName -> RenameM RenamedModule +renameModule m0 = + do let m = m0 { mDecls = snd (addImplicitNestedImports (mDecls m0)) } + env <- liftSupply (defsOf m) + nested <- liftSupply (collectNestedModules env m) + setNestedModule (nestedModuleNames nested) + do (ifs,(inScope,m1)) <- collectIfaceDeps + $ renameModule' nested env (TopModule (thing (mName m))) m + pure RenamedModule + { rmModule = m1 + , rmDefines = env + , rmInScope = inScope + , rmImported = ifs + -- XXX: maybe we should keep the nested defines too? + } + +renameTopDecls :: + ModName -> [TopDecl PName] -> RenameM (NamingEnv,[TopDecl Name]) +renameTopDecls m ds0 = + do let ds = snd (addImplicitNestedImports ds0) + let mpath = TopModule m + env <- liftSupply (defsOf (map (InModule (Just mpath)) ds)) + nested <- liftSupply (collectNestedModulesDecls env m ds) + + setNestedModule (nestedModuleNames nested) + do ds1 <- shadowNames' CheckOverlap env + (renameTopDecls' (nested,mpath) ds) + pure (env,ds1) + + +-- | Returns declarations with additional imports and the public module names +-- of this module and its children +addImplicitNestedImports :: + [TopDecl PName] -> ([[Ident]], [TopDecl PName]) +addImplicitNestedImports decls = (concat exportedMods, concat newDecls ++ other) where - mk f = f (renWarnNameDisp ws) - - --- Renaming Monad -------------------------------------------------------------- - -data RO = RO - { roLoc :: Range - , roMod :: !ModName - , roNames :: NamingEnv - , roDisp :: !NameDisp - } - -data RW = RW - { rwWarnings :: !RenamerWarnings - , rwErrors :: !(Seq.Seq RenamerError) - , rwSupply :: !Supply - , rwNameUseCount :: !(Map Name Int) - -- ^ How many times did we refer to each name. - -- Used to generate warnings for unused definitions. - } - - - -newtype RenameM a = RenameM - { unRenameM :: ReaderT RO (StateT RW Lift) a } - -instance S.Semigroup a => S.Semigroup (RenameM a) where - {-# INLINE (<>) #-} - a <> b = - do x <- a - y <- b - return (x S.<> y) - -instance (S.Semigroup a, Monoid a) => Monoid (RenameM a) where - {-# INLINE mempty #-} - mempty = return mempty - - {-# INLINE mappend #-} - mappend = (S.<>) - -instance Functor RenameM where - {-# INLINE fmap #-} - fmap f m = RenameM (fmap f (unRenameM m)) - -instance Applicative RenameM where - {-# INLINE pure #-} - pure x = RenameM (pure x) - - {-# INLINE (<*>) #-} - l <*> r = RenameM (unRenameM l <*> unRenameM r) + (mods,other) = foldr classify ([], []) decls + (newDecls,exportedMods) = unzip (map processModule mods) + processModule m = + let NestedModule m1 = tlValue m + (childExs, ds1) = addImplicitNestedImports (mDecls m1) + mname = getIdent (thing (mName m1)) + imps = map (mname :) ([] : childExs) + isToName is = case is of + [i] -> mkUnqual i + _ -> mkQual (isToQual (init is)) (last is) + isToQual is = packModName (map identText is) + mkImp xs = DImport + Located + { srcRange = srcRange (mName m1) + , thing = Import + { iModule = ImpNested (isToName xs) + , iAs = Just (isToQual xs) + , iSpec = Nothing + } + } + in ( DModule m { tlValue = NestedModule m1 { mDecls = ds1 } } + : map mkImp imps + , case tlExport m of + Public -> imps + Private -> [] + ) + + + classify d (ms,ds) = + case d of + DModule tl -> (tl : ms, ds) + _ -> (ms, d : ds) + + +nestedModuleNames :: NestedMods -> Map ModPath Name +nestedModuleNames mp = Map.fromList (map entry (Map.keys mp)) + where + entry n = case nameInfo n of + Declared p _ -> (Nested p (nameIdent n),n) + _ -> panic "nestedModuleName" [ "Not a top-level name" ] -instance Monad RenameM where - {-# INLINE return #-} - return x = RenameM (return x) - {-# INLINE (>>=) #-} - m >>= k = RenameM (unRenameM m >>= unRenameM . k) +class Rename f where + rename :: f PName -> RenameM (f Name) -instance FreshM RenameM where - liftSupply f = RenameM $ sets $ \ RW { .. } -> - let (a,s') = f rwSupply - rw' = RW { rwSupply = s', .. } - in a `seq` rw' `seq` (a, rw') -runRenamer :: Supply -> ModName -> NamingEnv -> RenameM a - -> (Either [RenamerError] (a,Supply),[RenamerWarning]) -runRenamer s ns env m = (res, listRenamerWarnings warns) +-- | Returns: +-- +-- * Interfaces for imported things, +-- * Things defines in the module +-- * Renamed module +renameModule' :: + NestedMods -> NamingEnv -> ModPath -> ModuleG mname PName -> + RenameM (NamingEnv, ModuleG mname Name) +renameModule' thisNested env mpath m = + setCurMod mpath + do (moreNested,imps) <- mconcat <$> mapM doImport (mImports m) + let allNested = Map.union moreNested thisNested + openDs = map thing (mSubmoduleImports m) + allImps = openLoop allNested env openDs imps + + (inScope,decls') <- + shadowNames allImps $ + shadowNames' CheckOverlap env $ + do inScope <- getNamingEnv + ds <- renameTopDecls' (allNested,mpath) (mDecls m) + pure (inScope, ds) + let m1 = m { mDecls = decls' } + exports = modExports m1 + mapM_ recordUse (exported NSType exports) + return (inScope, m1) + + +renameDecls :: [Decl PName] -> RenameM [Decl Name] +renameDecls ds = + do (ds1,deps) <- depGroup (traverse rename ds) + let toNode d = let x = NamedThing (declName d) + in ((d,x), x, map NamedThing + $ Set.toList + $ Map.findWithDefault Set.empty x deps) + ordered = toList (stronglyConnComp (map toNode ds1)) + fromSCC x = + case x of + AcyclicSCC (d,_) -> pure [d] + CyclicSCC ds_xs -> + let (rds,xs) = unzip ds_xs + in case mapM validRecursiveD rds of + Nothing -> do record (InvalidDependency xs) + pure rds + Just bs -> + do checkSameModule xs + pure [DRec bs] + concat <$> mapM fromSCC ordered + + +validRecursiveD :: Decl name -> Maybe (Bind name) +validRecursiveD d = + case d of + DBind b -> Just b + DLocated d' _ -> validRecursiveD d' + _ -> Nothing + +checkSameModule :: [DepName] -> RenameM () +checkSameModule xs = + case ms of + a : as | let bad = [ fst b | b <- as, snd a /= snd b ] + , not (null bad) -> + record $ InvalidDependency $ map NamedThing $ fst a : bad + _ -> pure () where - warns = foldr addRenamerWarning (rwWarnings rw) - (warnUnused ns env ro rw) - - (a,rw) = runM (unRenameM m) ro - RW { rwErrors = Seq.empty - , rwWarnings = noRenamerWarnings - , rwSupply = s - , rwNameUseCount = Map.empty - } - - ro = RO { roLoc = emptyRange - , roNames = env - , roMod = ns - , roDisp = neverQualifyMod ns `mappend` toNameDisp env - } - - res | Seq.null (rwErrors rw) = Right (a,rwSupply rw) - | otherwise = Left (F.toList (rwErrors rw)) - --- | Record an error. XXX: use a better name -record :: (NameDisp -> RenamerError) -> RenameM () -record f = RenameM $ - do RO { .. } <- ask - RW { .. } <- get - set RW { rwErrors = rwErrors Seq.|> f roDisp, .. } - --- | Get the source range for wahtever we are currently renaming. -curLoc :: RenameM Range -curLoc = RenameM (roLoc `fmap` ask) - --- | Annotate something with the current range. -located :: a -> RenameM (Located a) -located thing = - do srcRange <- curLoc - return Located { .. } - --- | Do the given computation using the source code range from `loc` if any. -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 - --- | Retrieve the name of the current module. -getNS :: RenameM ModName -getNS = RenameM (roMod `fmap` ask) - --- | Shadow the current naming environment with some more names. -shadowNames :: BindsNames env => env -> RenameM a -> RenameM a -shadowNames = shadowNames' CheckAll - -data EnvCheck = CheckAll -- ^ Check for overlap and shadowing - | CheckOverlap -- ^ Only check for overlap - | CheckNone -- ^ Don't check the environment - deriving (Eq,Show) - --- | Shadow the current naming environment with some more names. -shadowNames' :: BindsNames env => EnvCheck -> env -> RenameM a -> RenameM a -shadowNames' check names m = do - do env <- liftSupply (namingEnv' names) - RenameM $ - do ro <- ask - env' <- sets (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 - - --- | Generate warnings when the left environment shadows things defined in --- the right. Additionally, generate errors when two names overlap in the --- left environment. -checkEnv :: NameDisp -> EnvCheck -> NamingEnv -> NamingEnv -> RW -> (NamingEnv,RW) -checkEnv disp check l r rw - | check == CheckNone = (l',rw) - | otherwise = (l',rw'') - + ms = [ (x,p) | NamedThing x <- xs, Declared p _ <- [ nameInfo x ] ] + + +renameTopDecls' :: + (NestedMods,ModPath) -> [TopDecl PName] -> RenameM [TopDecl Name] +renameTopDecls' info ds = + do (ds1,deps) <- depGroup (traverse (renameWithMods info) ds) + + + let (noNameDs,nameDs) = partitionEithers (map topDeclName ds1) + ctrs = [ nm | (_,nm@(ConstratintAt {})) <- nameDs ] + toNode (d,x) = ((d,x),x, (if usesCtrs d then ctrs else []) ++ + map NamedThing + ( Set.toList + ( Map.findWithDefault Set.empty x deps) )) + ordered = stronglyConnComp (map toNode nameDs) + fromSCC x = + case x of + AcyclicSCC (d,_) -> pure [d] + CyclicSCC ds_xs -> + let (rds,xs) = unzip ds_xs + in case mapM valid rds of + Nothing -> do record (InvalidDependency xs) + pure rds + Just bs -> + do checkSameModule xs + pure [Decl TopLevel + { tlDoc = Nothing + , tlExport = Public + , tlValue = DRec bs + }] + where + valid d = case d of + Decl tl -> validRecursiveD (tlValue tl) + _ -> Nothing + rds <- mapM fromSCC ordered + pure (concat (noNameDs:rds)) where - - l' = l { neExprs = es, neTypes = ts } - - (rw',es) = Map.mapAccumWithKey (step neExprs) rw (neExprs l) - (rw'',ts) = Map.mapAccumWithKey (step neTypes) rw' (neTypes l) - - step prj acc k ns = (acc', [head ns]) - where - acc' = acc - { rwWarnings = - if check == CheckAll - then case Map.lookup k (prj r) of - Nothing -> rwWarnings acc - Just os -> addRenamerWarning - (SymbolShadowed (head ns) os disp) - (rwWarnings acc) - - else rwWarnings acc - , rwErrors = rwErrors acc Seq.>< containsOverlap disp ns - } - --- | Check the RHS of a single name rewrite for conflicting sources. -containsOverlap :: NameDisp -> [Name] -> Seq.Seq RenamerError -containsOverlap _ [_] = Seq.empty -containsOverlap _ [] = panic "Renamer" ["Invalid naming environment"] -containsOverlap disp ns = Seq.singleton (OverlappingSyms ns disp) - --- | Throw errors for any names that overlap in a rewrite environment. -checkNamingEnv :: NamingEnv -> ([RenamerError],[RenamerWarning]) -checkNamingEnv env = (F.toList out, []) + usesCtrs td = + case td of + Decl tl -> isValDecl (tlValue tl) + DPrimType {} -> False + TDNewtype {} -> False + DParameterType {} -> False + DParameterConstraint {} -> False + DParameterFun {} -> False + DModule tl -> any usesCtrs (mDecls m) + where NestedModule m = tlValue tl + DImport {} -> False + Include {} -> bad "Include" + + isValDecl d = + case d of + DLocated d' _ -> isValDecl d' + DBind {} -> True + DType {} -> False + DProp {} -> False + DRec {} -> True + DSignature {} -> bad "DSignature" + DFixity {} -> bad "DFixity" + DPragma {} -> bad "DPragma" + DPatBind {} -> bad "DPatBind" + + bad msg = panic "renameTopDecls'" [msg] + + +declName :: Decl Name -> Name +declName decl = + case decl of + DLocated d _ -> declName d + DBind b -> thing (bName b) + DType (TySyn x _ _ _) -> thing x + DProp (PropSyn x _ _ _) -> thing x + + DSignature {} -> bad "DSignature" + DFixity {} -> bad "DFixity" + DPragma {} -> bad "DPragma" + DPatBind {} -> bad "DPatBind" + DRec {} -> bad "DRec" where - out = Map.foldr check outTys (neExprs env) - outTys = Map.foldr check mempty (neTypes env) - - disp = toNameDisp env - - check ns acc = containsOverlap disp ns Seq.>< acc - -recordUse :: Name -> RenameM () -recordUse x = RenameM $ sets_ $ \rw -> - rw { rwNameUseCount = Map.insertWith (+) x 1 (rwNameUseCount rw) } - - -warnUnused :: ModName -> NamingEnv -> RO -> RW -> [RenamerWarning] -warnUnused m0 env ro rw = - map warn - $ Map.keys - $ Map.filterWithKey keep - $ rwNameUseCount rw + bad x = panic "declName" [x] + +topDeclName :: TopDecl Name -> Either (TopDecl Name) (TopDecl Name, 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))) + DParameterType d -> hasName (thing (ptName d)) + DParameterFun d -> hasName (thing (pfName d)) + DModule d -> hasName (thing (mName m)) + where NestedModule m = tlValue d + + DParameterConstraint ds -> + case ds of + [] -> noName + _ -> Right (topDecl, ConstratintAt (fromJust (getLoc ds))) + DImport {} -> noName + + Include {} -> bad "Include" where - warn x = UnusedName x (roDisp ro) - keep k n = n == 1 && isLocal k - oldNames = fst (visibleNames env) - isLocal nm = case nameInfo nm of - Declared m sys -> sys == UserName && - m == m0 && nm `Set.notMember` oldNames - Parameter -> True - --- Renaming -------------------------------------------------------------------- - -class Rename f where - rename :: f PName -> RenameM (f Name) - -renameModule :: Module PName -> RenameM (NamingEnv,Module Name) -renameModule m = - do env <- liftSupply (namingEnv' m) - -- NOTE: we explicitly hide shadowing errors here, by using shadowNames' - decls' <- shadowNames' CheckOverlap env (traverse rename (mDecls m)) - let m1 = m { mDecls = decls' } - exports = modExports m1 - mapM_ recordUse (eTypes exports) - return (env,m1) + noName = Left topDecl + hasName n = Right (topDecl, NamedThing n) + bad x = panic "topDeclName" [x] + + +-- | Returns: +-- * The public interface of the imported module +-- * Infromation about nested modules in this module +-- * New names introduced through this import +doImport :: Located Import -> RenameM (NestedMods, NamingEnv) +doImport li = + do let i = thing li + decls <- lookupImport i + let declsOf = unqualifiedEnv . ifPublic + nested = declsOf <$> ifModules decls + pure (nested, interpImportIface i decls) + + + +-------------------------------------------------------------------------------- +-- Compute names coming through `open` statements. + +data OpenLoopState = OpenLoopState + { unresolvedOpen :: [ImportG PName] + , scopeImports :: NamingEnv -- names from open/impot + , scopeDefs :: NamingEnv -- names defined in this module + , scopingRel :: NamingEnv -- defs + imports with shadowing + -- (just a cache) + , openLoopChange :: Bool + } -instance Rename TopDecl where - rename td = case td of - Decl d -> Decl <$> traverse rename d - DPrimType d -> DPrimType <$> traverse rename d - TDNewtype n -> TDNewtype <$> traverse rename n - Include n -> return (Include n) - DParameterFun f -> DParameterFun <$> rename f - DParameterType f -> DParameterType <$> rename f +-- | Processing of a single @open@ declaration +processOpen :: NestedMods -> OpenLoopState -> ImportG PName -> OpenLoopState +processOpen modEnvs s o = + case lookupNS NSModule (iModule o) (scopingRel s) of + [] -> s { unresolvedOpen = o : unresolvedOpen s } + [n] -> + case Map.lookup n modEnvs of + Nothing -> panic "openLoop" [ "Missing defintion for module", show n ] + Just def -> + let new = interpImportEnv o def + newImps = new <> scopeImports s + in s { scopeImports = newImps + , scopingRel = scopeDefs s `shadowing` newImps + , openLoopChange = True + } + _ -> s + {- Notes: + * ambiguity will be reported later when we do the renaming + * assumes scoping only grows, which should be true + * we are not adding the names from *either* of the imports + so this may give rise to undefined names, so we may want to + suppress reporing undefined names if there ambiguities for + module names. Alternatively we could add the defitions from + *all* options, but that might lead to spurious ambiguity errors. + -} + +{- | Complete the set of import using @open@ declarations. +This should terminate because on each iteration either @unresolvedOpen@ +decreases or @openLoopChange@ remians @False@. We don't report errors +here, as they will be reported during renaming anyway. -} +openLoop :: + NestedMods {- ^ Definitions of all known nested modules -} -> + NamingEnv {- ^ Definitions of the module (these shadow) -} -> + [ImportG PName] {- ^ Open declarations -} -> + NamingEnv {- ^ Imported declarations -} -> + NamingEnv {- ^ Completed imports -} +openLoop modEnvs defs os imps = + scopingRel $ loop OpenLoopState + { unresolvedOpen = os + , scopeImports = imps + , scopeDefs = defs + , scopingRel = defs `shadowing` imps + , openLoopChange = True + } + where + loop s + | openLoopChange s = + loop $ foldl' (processOpen modEnvs) + s { unresolvedOpen = [], openLoopChange = False } + (unresolvedOpen s) + | otherwise = s + + +-------------------------------------------------------------------------------- + + +data WithMods f n = WithMods (NestedMods,ModPath) (f n) + +forgetMods :: WithMods f n -> f n +forgetMods (WithMods _ td) = td + +renameWithMods :: + Rename (WithMods f) => (NestedMods,ModPath) -> f PName -> RenameM (f Name) +renameWithMods info m = forgetMods <$> rename (WithMods info m) + + +instance Rename (WithMods TopDecl) where + rename (WithMods info td) = WithMods info <$> + case td of + Decl d -> Decl <$> traverse rename d + DPrimType d -> DPrimType <$> traverse rename d + TDNewtype n -> TDNewtype <$> traverse rename n + Include n -> return (Include n) + DParameterFun f -> DParameterFun <$> rename f + DParameterType f -> DParameterType <$> rename f + + DParameterConstraint ds -> + case ds of + [] -> pure (DParameterConstraint []) + _ -> depsOf (ConstratintAt (fromJust (getLoc ds))) + $ DParameterConstraint <$> mapM renameLocated ds + DModule m -> DModule <$> traverse (renameWithMods info) m + DImport li -> DImport <$> traverse renI li + where + renI i = do m <- rename (iModule i) + pure i { iModule = m } + +instance Rename ImpName where + rename i = + case i of + ImpTop m -> pure (ImpTop m) + ImpNested m -> ImpNested <$> resolveName NameUse NSModule m + +instance Rename (WithMods NestedModule) where + rename (WithMods info (NestedModule m)) = WithMods info <$> + do let (nested,mpath) = info + lnm = mName m + nm = thing lnm + newMPath = Nested mpath (getIdent nm) + n <- resolveName NameBind NSModule nm + depsOf (NamedThing n) + do let env = case Map.lookup n (fst info) of + Just defs -> defs + Nothing -> panic "rename" + [ "Missing environment for nested module", show n ] + -- XXX: we should store in scope somehwere if we want to browse + -- nested modules properly + (_inScope,m1) <- renameModule' nested env newMPath m + pure (NestedModule m1 { mName = lnm { thing = n } }) - DParameterConstraint d -> DParameterConstraint <$> mapM renameLocated d renameLocated :: Rename f => Located (f PName) -> RenameM (Located (f Name)) renameLocated x = @@ -456,21 +459,23 @@ renameLocated x = instance Rename PrimType where rename pt = - do x <- rnLocated renameType (primTName pt) - let (as,ps) = primTCts pt - (_,cts) <- renameQual as ps $ \as' ps' -> pure (as',ps') - pure pt { primTCts = cts, primTName = x } + do x <- rnLocated (renameType NameBind) (primTName pt) + depsOf (NamedThing (thing x)) + do let (as,ps) = primTCts pt + (_,cts) <- renameQual as ps $ \as' ps' -> pure (as',ps') + pure pt { primTCts = cts, primTName = x } instance Rename ParameterType where rename a = - do n' <- rnLocated renameType (ptName a) + do n' <- rnLocated (renameType NameBind) (ptName a) return a { ptName = n' } instance Rename ParameterFun where rename a = - do n' <- rnLocated renameVar (pfName a) - sig' <- renameSchema (pfSchema a) - return a { pfName = n', pfSchema = snd sig' } + do n' <- rnLocated (renameVar NameBind) (pfName a) + depsOf (NamedThing (thing n')) + do sig' <- renameSchema (pfSchema a) + return a { pfName = n', pfSchema = snd sig' } rnLocated :: (a -> RenameM b) -> Located a -> RenameM (Located b) rnLocated f loc = withLoc loc $ @@ -479,101 +484,95 @@ rnLocated f loc = withLoc loc $ 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 - - -- XXX we probably shouldn't see these at this point... - DPatBind pat e -> do (pe,pat') <- renamePat pat - shadowNames pe (DPatBind pat' <$> rename e) + DBind b -> DBind <$> rename b DType syn -> DType <$> rename syn DProp syn -> DProp <$> rename syn DLocated d' r -> withLoc r $ DLocated <$> rename d' <*> pure r - DFixity{} -> panic "Renamer" ["Unexpected fixity declaration" - , show d] + + DFixity{} -> panic "renaem" [ "DFixity" ] + DSignature {} -> panic "rename" [ "DSignature" ] + DPragma {} -> panic "rename" [ "DPragma" ] + DPatBind {} -> panic "rename" [ "DPatBind " ] + DRec {} -> panic "rename" [ "DRec" ] + + instance Rename Newtype where - rename n = do - name' <- rnLocated renameType (nName n) + rename n = shadowNames (nParams n) $ - do ps' <- traverse rename (nParams n) - body' <- traverse (traverse 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) - - -- This is an unbound value. Record an error and invent a bogus real name - -- for it. - Nothing -> - do n <- located qn - - case Map.lookup qn (neTypes (roNames ro)) of - -- types existed with the name of the value expected - Just _ -> record (ExpectedValue n) - - -- the value is just missing - Nothing -> record (UnboundExpr n) - - mkFakeName qn - --- | Produce a name if one exists. Note that this includes situations where --- overlap exists, as it's just a query about anything being in scope. In the --- event that overlap does exist, an error will be recorded. -typeExists :: PName -> RenameM (Maybe Name) -typeExists pn = + do name' <- rnLocated (renameType NameBind) (nName n) + depsOf (NamedThing (thing name')) $ + do ps' <- traverse rename (nParams n) + body' <- traverse (traverse rename) (nBody n) + return Newtype { nName = name' + , nParams = ps' + , nBody = body' } + + + +-- | Try to resolve a name +resolveNameMaybe :: NameType -> Namespace -> PName -> RenameM (Maybe Name) +resolveNameMaybe nt expected qn = do ro <- RenameM ask - case Map.lookup pn (neTypes (roNames ro)) of - Just [n] -> recordUse n >> return (Just n) - Just [] -> panic "Renamer" ["Invalid type renaming environment"] - Just syms -> do n <- located pn - mapM_ recordUse syms - record (MultipleSyms n syms) - return (Just (head syms)) - Nothing -> return Nothing - -renameType :: PName -> RenameM Name -renameType pn = - do mb <- typeExists pn + let lkpIn here = Map.lookup qn (namespaceMap here (roNames ro)) + use = case expected of + NSType -> recordUse + _ -> const (pure ()) + case lkpIn expected of + Just [n] -> + do case nt of + NameBind -> pure () + NameUse -> addDep n + use n -- for warning + return (Just n) + Just [] -> panic "Renamer" ["Invalid expression renaming environment"] + Just syms -> + do mapM_ use syms -- mark as used to avoid unused warnings + n <- located qn + record (MultipleSyms n syms) + return (Just (head syms)) + + Nothing -> pure Nothing + +-- | Resolve a name, and report error on failure +resolveName :: NameType -> Namespace -> PName -> RenameM Name +resolveName nt expected qn = + do mb <- resolveNameMaybe nt expected qn case mb of - Just n -> return n - - -- This is an unbound value. Record an error and invent a bogus real name - -- for it. + Just n -> pure n Nothing -> do ro <- RenameM ask - let n = Located { srcRange = roLoc ro, thing = pn } + let lkpIn here = Map.lookup qn (namespaceMap here (roNames ro)) + others = [ ns | ns <- allNamespaces + , ns /= expected + , Just _ <- [lkpIn ns] ] + nm <- located qn + case others of + -- name exists in a different namespace + actual : _ -> record (WrongNamespace expected actual nm) + + -- the value is just missing + [] -> record (UnboundName expected nm) + + mkFakeName expected qn + - case Map.lookup pn (neExprs (roNames ro)) of +renameVar :: NameType -> PName -> RenameM Name +renameVar nt = resolveName nt NSValue - -- values exist with the same name, so throw a different error - Just _ -> record (ExpectedType n) +renameType :: NameType -> PName -> RenameM Name +renameType nt = resolveName nt NSType - -- no terms with the same name, so the type is just unbound - Nothing -> record (UnboundType n) - mkFakeName pn -- | Assuming an error has been recorded already, construct a fake name that's -- not expected to make it out of the renamer. -mkFakeName :: PName -> RenameM Name -mkFakeName pn = +mkFakeName :: Namespace -> PName -> RenameM Name +mkFakeName ns pn = do ro <- RenameM ask - liftSupply (mkParameter (getIdent pn) (roLoc ro)) + liftSupply (mkParameter ns (getIdent pn) (roLoc ro)) -- | Rename a schema, assuming that none of its type variables are already in -- scope. @@ -593,7 +592,7 @@ renameQual :: [TParam PName] -> [Prop PName] -> ([TParam Name] -> [Prop Name] -> RenameM a) -> RenameM (NamingEnv, a) renameQual as ps k = - do env <- liftSupply (namingEnv' as) + do env <- liftSupply (defsOf as) res <- shadowNames env $ do as' <- traverse rename as ps' <- traverse rename ps k as' ps' @@ -601,7 +600,7 @@ renameQual as ps k = instance Rename TParam where rename TParam { .. } = - do n <- renameType tpName + do n <- renameType NameBind tpName return TParam { tpName = n, .. } instance Rename Prop where @@ -616,7 +615,7 @@ instance Rename Type where TBit -> return TBit TNum c -> return (TNum c) TChar c -> return (TChar c) - TUser qn ps -> TUser <$> renameType qn <*> traverse rename ps + TUser qn ps -> TUser <$> renameType NameUse qn <*> traverse rename ps TTyApp fs -> TTyApp <$> traverse (traverse rename) fs TRecord fs -> TRecord <$> traverse (traverse rename) fs TTuple fs -> TTuple <$> traverse rename fs @@ -628,7 +627,8 @@ instance Rename Type where b' <- rename b mkTInfix a' o' b' -mkTInfix :: Type Name -> (Located Name, Fixity) -> Type Name -> RenameM (Type Name) +mkTInfix :: + Type Name -> (Located Name, Fixity) -> Type Name -> RenameM (Type Name) mkTInfix t@(TInfix x o1 f1 y) op@(o2,f2) z = case compareFixity f1 f2 of @@ -647,20 +647,21 @@ mkTInfix t (o,f) z = -- | Rename a binding. 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) - -- NOTE: renamePats will generate warnings, so we don't need to trigger - -- them again here. - e' <- shadowNames' CheckNone patEnv (rnLocated rename (bDef b)) - return b { bName = n' - , bParams = pats' - , bDef = e' - , bSignature = snd `fmap` mbSig - , bPragmas = bPragmas b - } + rename b = + do n' <- rnLocated (renameVar NameBind) (bName b) + depsOf (NamedThing (thing n')) + do mbSig <- traverse renameSchema (bSignature b) + shadowNames (fst `fmap` mbSig) $ + do (patEnv,pats') <- renamePats (bParams b) + -- NOTE: renamePats will generate warnings, + -- so we don't need to trigger them again here. + 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 @@ -669,7 +670,7 @@ instance Rename BindDef where -- NOTE: this only renames types within the pattern. instance Rename Pattern where rename p = case p of - PVar lv -> PVar <$> rnLocated renameVar lv + PVar lv -> PVar <$> rnLocated (renameVar NameBind) lv PWild -> pure PWild PTuple ps -> PTuple <$> traverse rename ps PRecord nps -> PRecord <$> traverse (traverse rename) nps @@ -702,12 +703,12 @@ instance Rename UpdField where instance Rename FunDesc where rename (FunDesc nm offset) = - do nm' <- traverse renameVar nm + do nm' <- traverse (renameVar NameBind) nm pure (FunDesc nm' offset) instance Rename Expr where rename expr = case expr of - EVar n -> EVar <$> renameVar n + EVar n -> EVar <$> renameVar NameUse n ELit l -> return (ELit l) ENeg e -> ENeg <$> rename e EComplement e -> EComplement @@ -737,9 +738,8 @@ instance Rename Expr where 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 + EWhere e' ds -> shadowNames (map (InModule Nothing) ds) $ + EWhere <$> rename e' <*> renameDecls ds ETyped e' ty -> ETyped <$> rename e' <*> rename ty ETypeVal ty -> ETypeVal<$> rename ty EFun desc ps e' -> do desc' <- rename desc @@ -810,14 +810,14 @@ mkEInfix e (o,f) z = renameOp :: Located PName -> RenameM (Located Name, Fixity) renameOp ln = withLoc ln $ - do n <- renameVar (thing ln) + do n <- renameVar NameUse (thing ln) fixity <- lookupFixity n return (ln { thing = n }, fixity) renameTypeOp :: Located PName -> RenameM (Located Name, Fixity) renameTypeOp ln = withLoc ln $ - do n <- renameType (thing ln) + do n <- renameType NameUse (thing ln) fixity <- lookupFixity n return (ln { thing = n }, fixity) @@ -859,8 +859,7 @@ renameMatch (Match p e) = return (pe,Match p' e') renameMatch (MatchLet b) = - do ns <- getNS - be <- liftSupply (namingEnv' (InModule ns b)) + do be <- liftSupply (defsOf (InModule Nothing b)) b' <- shadowNames be (rename b) return (be,MatchLet b') @@ -892,7 +891,8 @@ patternEnv :: Pattern PName -> RenameM NamingEnv patternEnv = go where go (PVar Located { .. }) = - do n <- liftSupply (mkParameter (getIdent thing) srcRange) + do n <- liftSupply (mkParameter NSValue (getIdent thing) srcRange) + -- XXX: for deps, we should record a use return (singletonE thing n) go PWild = return mempty @@ -919,7 +919,7 @@ patternEnv = go typeEnv TChar{} = return mempty typeEnv (TUser pn ps) = - do mb <- typeExists pn + do mb <- resolveNameMaybe NameUse NSType pn case mb of -- The type is already bound, don't introduce anything. @@ -931,15 +931,15 @@ patternEnv = go -- of the type of the pattern. | null ps -> do loc <- curLoc - n <- liftSupply (mkParameter (getIdent pn) loc) + n <- liftSupply (mkParameter NSType (getIdent pn) loc) return (singletonT pn n) -- This references a type synonym that's not in scope. Record an -- error and continue with a made up name. | otherwise -> do loc <- curLoc - record (UnboundType (Located loc pn)) - n <- liftSupply (mkParameter (getIdent pn) loc) + record (UnboundName NSType (Located loc pn)) + n <- liftSupply (mkParameter NSType (getIdent pn) loc) return (singletonT pn n) typeEnv (TRecord fs) = bindTypes (map snd (recordElements fs)) @@ -961,18 +961,17 @@ patternEnv = go instance Rename Match where rename m = case m of Match p e -> Match <$> rename p <*> rename e - MatchLet b -> shadowNamesNS b (MatchLet <$> rename b) + MatchLet b -> shadowNames (InModule Nothing b) (MatchLet <$> rename b) instance Rename TySyn where rename (TySyn n f ps ty) = - shadowNames ps $ TySyn <$> rnLocated renameType n - <*> pure f - <*> traverse rename ps - <*> rename ty + shadowNames ps + do n' <- rnLocated (renameType NameBind) n + depsOf (NamedThing (thing n')) $ + TySyn n' <$> pure f <*> traverse rename ps <*> rename ty instance Rename PropSyn where rename (PropSyn n f ps cs) = - shadowNames ps $ PropSyn <$> rnLocated renameType n - <*> pure f - <*> traverse rename ps - <*> traverse rename cs + shadowNames ps + do n' <- rnLocated (renameType NameBind) n + PropSyn n' <$> pure f <*> traverse rename ps <*> traverse rename cs diff --git a/src/Cryptol/ModuleSystem/Renamer/Error.hs b/src/Cryptol/ModuleSystem/Renamer/Error.hs new file mode 100644 index 000000000..bfe152e07 --- /dev/null +++ b/src/Cryptol/ModuleSystem/Renamer/Error.hs @@ -0,0 +1,205 @@ +-- | +-- Module : Cryptol.ModuleSystem.Renamer +-- Copyright : (c) 2013-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + +{-# Language DeriveGeneric, DeriveAnyClass #-} +{-# Language OverloadedStrings #-} +module Cryptol.ModuleSystem.Renamer.Error where + +import Cryptol.ModuleSystem.Name +import Cryptol.Parser.AST +import Cryptol.Parser.Position +import Cryptol.Parser.Selector(ppNestedSels) +import Cryptol.Utils.PP + +import GHC.Generics (Generic) +import Control.DeepSeq + +import Prelude () +import Prelude.Compat + +-- Errors ---------------------------------------------------------------------- + +data RenamerError + = MultipleSyms (Located PName) [Name] + -- ^ Multiple imported symbols contain this name + + | UnboundName Namespace (Located PName) + -- ^ Some name not bound to any definition + + | OverlappingSyms [Name] + -- ^ An environment has produced multiple overlapping symbols + + | WrongNamespace Namespace Namespace (Located PName) + -- ^ expected, actual. + -- When a name is missing from the expected namespace, but exists in another + + | 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) + + +-- We use this because parameter constrstaints have no names +data DepName = NamedThing Name + | ConstratintAt Range -- ^ identifed by location in source + deriving (Eq,Ord,Show,Generic,NFData) + +depNameLoc :: DepName -> Range +depNameLoc x = + case x of + NamedThing n -> nameLoc n + ConstratintAt r -> r + + + +instance PP RenamerError where + ppPrec _ e = case e of + + MultipleSyms lqn qns -> + hang (text "[error] at" <+> pp (srcRange lqn)) + 4 $ (text "Multiple definitions for symbol:" <+> pp (thing lqn)) + $$ vcat (map ppLocName qns) + + UnboundName ns lqn -> + hang (text "[error] at" <+> pp (srcRange lqn)) + 4 (something <+> "not in scope:" <+> pp (thing lqn)) + where + something = case ns of + NSValue -> "Value" + NSType -> "Type" + NSModule -> "Module" + + OverlappingSyms qns -> + hang (text "[error]") + 4 $ text "Overlapping symbols defined:" + $$ vcat (map ppLocName qns) + + WrongNamespace expected actual lqn -> + hang ("[error] at" <+> pp (srcRange lqn )) + 4 (fsep + [ "Expected a", sayNS expected, "named", quotes (pp (thing lqn)) + , "but found a", sayNS actual, "instead" + , suggestion + ]) + where + sayNS ns = case ns of + NSValue -> "value" + NSType -> "type" + NSModule -> "module" + suggestion = + case (expected,actual) of + (NSValue,NSType) -> + "Did you mean `(" <.> pp (thing lqn) <.> text")?" + _ -> empty + + FixityError o1 f1 o2 f2 -> + hang (text "[error] at" <+> pp (srcRange o1) <+> text "and" <+> pp (srcRange o2)) + 4 (fsep [ text "The fixities of" + , nest 2 $ vcat + [ "•" <+> pp (thing o1) <+> parens (pp f1) + , "•" <+> pp (thing o2) <+> parens (pp f2) ] + , text "are not compatible." + , text "You may use explicit parentheses to disambiguate." ]) + + InvalidConstraint ty -> + hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty)) + 4 (fsep [ pp ty, text "is not a valid constraint" ]) + + MalformedBuiltin ty pn -> + hang (text "[error]" <+> maybe empty (\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 (text "[error]" <+> maybe empty (\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 ]) + where + ppLab as = ppNestedSels (thing as) <+> "at" <+> pp (srcRange as) + + InvalidDependency ds -> + "[error] Invalid recursive dependency:" + $$ nest 4 (vcat [ "•" <+> pp x <.> ", defined at" <+> ppR (depNameLoc x) + | x <- ds ]) + where ppR r = pp (from r) <.> "--" <.> pp (to r) + +instance PP DepName where + ppPrec _ d = + case d of + ConstratintAt r -> "constraint at" <+> pp r + NamedThing n -> + case nameNamespace n of + NSModule -> "submodule" <+> pp n + NSType -> "type" <+> pp n + NSValue -> pp n + + + +-- Warnings -------------------------------------------------------------------- + +data RenamerWarning + = SymbolShadowed PName Name [Name] + | UnusedName Name + deriving (Show, Generic, NFData) + +instance Eq RenamerWarning where + x == y = compare x y == EQ + +-- used to determine in what order ot show things +instance Ord RenamerWarning where + compare w1 w2 = + case w1 of + SymbolShadowed x y _ -> + case w2 of + SymbolShadowed x' y' _ -> compare (byStart y,x) (byStart y',x') + _ -> LT + UnusedName x -> + case w2 of + UnusedName y -> compare (byStart x) (byStart y) + _ -> GT + + where + byStart = from . nameLoc + + +instance PP RenamerWarning where + ppPrec _ (SymbolShadowed k x os) = + hang (text "[warning] at" <+> loc) + 4 $ fsep [ "This binding for" <+> backticks (pp k) + , "shadows the existing binding" <.> plural + , text "at" ] + $$ vcat (map (pp . nameLoc) os) + + where + plural | length os > 1 = char 's' + | otherwise = empty + + loc = pp (nameLoc x) + + ppPrec _ (UnusedName x) = + hang (text "[warning] at" <+> pp (nameLoc x)) + 4 (text "Unused name:" <+> pp x) + + + diff --git a/src/Cryptol/ModuleSystem/Renamer/Monad.hs b/src/Cryptol/ModuleSystem/Renamer/Monad.hs new file mode 100644 index 000000000..e8bb2ad98 --- /dev/null +++ b/src/Cryptol/ModuleSystem/Renamer/Monad.hs @@ -0,0 +1,336 @@ +-- | +-- Module : Cryptol.ModuleSystem.Renamer +-- Copyright : (c) 2013-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + +{-# Language RecordWildCards #-} +{-# Language FlexibleContexts #-} +{-# Language BlockArguments #-} +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_) + +import Prelude () +import Prelude.Compat + +import Cryptol.ModuleSystem.Name +import Cryptol.ModuleSystem.NamingEnv +import Cryptol.ModuleSystem.Interface +import Cryptol.Parser.AST +import Cryptol.Parser.Position +import Cryptol.Utils.Panic (panic) +import Cryptol.Utils.Ident(modPathCommon) + +import Cryptol.ModuleSystem.Renamer.Error + +-- | Indicates if a name is in a binding poisition or a use site +data NameType = NameBind | NameUse + +-- | Information needed to do some renaming. +data RenamerInfo = RenamerInfo + { renSupply :: Supply -- ^ Use to make new names + , renContext :: ModPath -- ^ We are renaming things in here + , renEnv :: NamingEnv -- ^ This is what's in scope + , renIfaces :: ModName -> Iface + } + +newtype RenameM a = RenameM { unRenameM :: ReaderT RO (StateT RW Lift) a } + +data RO = RO + { roLoc :: Range + , roNames :: NamingEnv + , roIfaces :: ModName -> Iface + , roCurMod :: ModPath -- ^ Current module we are working on + , roNestedMods :: Map ModPath Name + } + +data RW = RW + { rwWarnings :: ![RenamerWarning] + , rwErrors :: !(Seq.Seq RenamerError) + , rwSupply :: !Supply + , rwNameUseCount :: !(Map Name Int) + -- ^ How many times did we refer to each name. + -- Used to generate warnings for unused definitions. + + , rwCurrentDeps :: Set Name + -- ^ keeps track of names *used* by something. + -- see 'depsOf' + + , rwDepGraph :: Map DepName (Set Name) + -- ^ keeps track of the dependencies for things. + -- see 'depsOf' + + , rwExternalDeps :: !IfaceDecls + -- ^ Info about imported things + } + + + +instance S.Semigroup a => S.Semigroup (RenameM a) where + {-# INLINE (<>) #-} + a <> b = + do x <- a + y <- b + return (x S.<> y) + +instance (S.Semigroup a, Monoid a) => Monoid (RenameM a) where + {-# INLINE mempty #-} + mempty = return mempty + + {-# INLINE mappend #-} + mappend = (S.<>) + +instance Functor RenameM where + {-# INLINE fmap #-} + fmap f m = RenameM (fmap f (unRenameM m)) + +instance Applicative RenameM where + {-# INLINE pure #-} + pure x = RenameM (pure x) + + {-# INLINE (<*>) #-} + l <*> r = RenameM (unRenameM l <*> unRenameM r) + +instance Monad RenameM where + {-# INLINE return #-} + return x = RenameM (return x) + + {-# INLINE (>>=) #-} + m >>= k = RenameM (unRenameM m >>= unRenameM . k) + +instance FreshM RenameM where + liftSupply f = RenameM $ sets $ \ RW { .. } -> + let (a,s') = f rwSupply + rw' = RW { rwSupply = s', .. } + in a `seq` rw' `seq` (a, rw') + + +runRenamer :: RenamerInfo -> RenameM a + -> ( Either [RenamerError] (a,Supply) + , [RenamerWarning] + ) +runRenamer info m = (res, warns) + where + warns = sort (rwWarnings rw ++ warnUnused (renContext info) (renEnv info) rw) + + (a,rw) = runM (unRenameM m) ro + RW { rwErrors = Seq.empty + , rwWarnings = [] + , rwSupply = renSupply info + , rwNameUseCount = Map.empty + , rwExternalDeps = mempty + , rwCurrentDeps = Set.empty + , rwDepGraph = Map.empty + } + + ro = RO { roLoc = emptyRange + , roNames = renEnv info + , roIfaces = renIfaces info + , roCurMod = renContext info + , roNestedMods = Map.empty + } + + res | Seq.null (rwErrors rw) = Right (a,rwSupply rw) + | otherwise = Left (F.toList (rwErrors rw)) + + +setCurMod :: ModPath -> RenameM a -> RenameM a +setCurMod mpath (RenameM m) = + RenameM $ mapReader (\ro -> ro { roCurMod = mpath }) m + +getCurMod :: RenameM ModPath +getCurMod = RenameM $ asks roCurMod + +getNamingEnv :: RenameM NamingEnv +getNamingEnv = RenameM (asks roNames) + + +setNestedModule :: Map ModPath Name -> RenameM a -> RenameM a +setNestedModule mp (RenameM m) = + RenameM $ mapReader (\ro -> ro { roNestedMods = mp }) m + +nestedModuleOrig :: ModPath -> RenameM (Maybe Name) +nestedModuleOrig x = RenameM (asks (Map.lookup x . roNestedMods)) + + +-- | Record an error. XXX: use a better name +record :: RenamerError -> RenameM () +record f = RenameM $ + do RW { .. } <- get + set RW { rwErrors = rwErrors Seq.|> f, .. } + +collectIfaceDeps :: RenameM a -> RenameM (IfaceDecls,a) +collectIfaceDeps (RenameM m) = + RenameM + do ds <- sets \s -> (rwExternalDeps s, s { rwExternalDeps = mempty }) + a <- m + ds' <- sets \s -> (rwExternalDeps s, s { rwExternalDeps = ds }) + pure (ds',a) + +-- | Rename something. All name uses in the sub-computation are assumed +-- to be dependenices of the thing. +depsOf :: DepName -> RenameM a -> RenameM a +depsOf x (RenameM m) = RenameM + do ds <- sets \rw -> (rwCurrentDeps rw, rw { rwCurrentDeps = Set.empty }) + a <- m + sets_ \rw -> + rw { rwCurrentDeps = Set.union (rwCurrentDeps rw) ds + , rwDepGraph = Map.insert x (rwCurrentDeps rw) (rwDepGraph rw) + } + pure a + +-- | This is used when renaming a group of things. The result contains +-- dependencies between names defines and the group, and is intended to +-- be used to order the group members in dependency order. +depGroup :: RenameM a -> RenameM (a, Map DepName (Set Name)) +depGroup (RenameM m) = RenameM + do ds <- sets \rw -> (rwDepGraph rw, rw { rwDepGraph = Map.empty }) + a <- m + ds1 <- sets \rw -> (rwDepGraph rw, rw { rwDepGraph = ds }) + pure (a,ds1) + +-- | Get the source range for wahtever we are currently renaming. +curLoc :: RenameM Range +curLoc = RenameM (roLoc `fmap` ask) + +-- | Annotate something with the current range. +located :: a -> RenameM (Located a) +located thing = + do srcRange <- curLoc + return Located { .. } + +-- | Do the given computation using the source code range from `loc` if any. +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 + + +-- | Shadow the current naming environment with some more names. +shadowNames :: BindsNames env => env -> RenameM a -> RenameM a +shadowNames = shadowNames' CheckAll + +data EnvCheck = CheckAll -- ^ Check for overlap and shadowing + | CheckOverlap -- ^ Only check for overlap + | CheckNone -- ^ Don't check the environment + deriving (Eq,Show) + +-- | Shadow the current naming environment with some more names. +shadowNames' :: BindsNames env => EnvCheck -> env -> RenameM a -> RenameM a +shadowNames' check names m = do + do env <- liftSupply (defsOf names) + RenameM $ + do ro <- ask + env' <- sets (checkEnv check env (roNames ro)) + let ro' = ro { roNames = env' `shadowing` roNames ro } + local ro' (unRenameM m) + +-- | Generate warnings when the left environment shadows things defined in +-- the right. Additionally, generate errors when two names overlap in the +-- left environment. +checkEnv :: EnvCheck -> NamingEnv -> NamingEnv -> RW -> (NamingEnv,RW) +checkEnv check (NamingEnv lenv) r rw0 + | check == CheckNone = (newEnv,rw0) + | otherwise = (newEnv,rwFin) + + where + newEnv = NamingEnv newMap + (rwFin,newMap) = Map.mapAccumWithKey doNS rw0 lenv + doNS rw ns = Map.mapAccumWithKey (step ns) rw + + step ns acc k xs = (acc', [head xs]) + where + acc' = acc + { rwWarnings = + if check == CheckAll + then case Map.lookup k (namespaceMap ns r) of + Just os | [x] <- xs + , let os' = filter (/=x) os + , not (null os') -> + SymbolShadowed k x os' : rwWarnings acc + _ -> rwWarnings acc + + else rwWarnings acc + , rwErrors = rwErrors acc Seq.>< containsOverlap xs + } + +-- | Check the RHS of a single name rewrite for conflicting sources. +containsOverlap :: [Name] -> Seq.Seq RenamerError +containsOverlap [_] = Seq.empty +containsOverlap [] = panic "Renamer" ["Invalid naming environment"] +containsOverlap ns = Seq.singleton (OverlappingSyms ns) + + +recordUse :: Name -> RenameM () +recordUse x = RenameM $ sets_ $ \rw -> + rw { rwNameUseCount = Map.insertWith (+) x 1 (rwNameUseCount rw) } + {- NOTE: we don't distinguish between bindings and uses here, because + the situation is complicated by the pattern signatures where the first + "use" site is actually the binding site. Instead we just count them all, and + something is considered unused if it is used only once (i.e, just the + binding site) -} + +-- | Mark something as a dependency. This is similar but different from +-- `recordUse`, in particular: +-- * We only record use sites, not bindings +-- * We record all namespaces, not just types +-- * We only keep track of actual uses mentioned in the code. +-- Otoh, `recordUse` also considers exported entities to be used. +-- * If we depend on a name from a sibling submodule we add a dependency on +-- the module in our common ancestor. Examples: +-- - @A::B::x@ depends on @A::B::C::D::y@, @x@ depends on @A::B::C@ +-- - @A::B::x@ depends on @A::P::Q::y@@, @x@ depends on @A::P@ + +addDep :: Name -> RenameM () +addDep x = + do cur <- getCurMod + deps <- case nameInfo x of + Declared m _ | Just (c,_,i:_) <- modPathCommon cur m -> + do mb <- nestedModuleOrig (Nested c i) + pure case mb of + Just y -> Set.fromList [x,y] + Nothing -> Set.singleton x + _ -> pure (Set.singleton x) + RenameM $ + sets_ \rw -> rw { rwCurrentDeps = Set.union deps (rwCurrentDeps rw) } + + +warnUnused :: ModPath -> NamingEnv -> RW -> [RenamerWarning] +warnUnused m0 env rw = + map warn + $ Map.keys + $ Map.filterWithKey keep + $ rwNameUseCount rw + where + warn x = UnusedName x + keep nm count = count == 1 && isLocal nm + oldNames = Map.findWithDefault Set.empty NSType (visibleNames env) + isLocal nm = case nameInfo nm of + Declared m sys -> sys == UserName && + m == m0 && nm `Set.notMember` oldNames + Parameter -> True + +-- | Get the exported declarations in a module +lookupImport :: Import -> RenameM IfaceDecls +lookupImport imp = RenameM $ + do getIf <- roIfaces <$> ask + let ifs = ifPublic (getIf (iModule imp)) + sets_ \s -> s { rwExternalDeps = ifs <> rwExternalDeps s } + pure ifs + + diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index cedda2032..dfc982931 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -43,7 +43,7 @@ import Cryptol.Utils.RecordMap(RecordMap) import Paths_cryptol } -{- state 196 contains 1 shift/reduce conflicts. +{- state 202 contains 1 shift/reduce conflicts. `_` identifier conflicts with `_` in record update. We have `_` as an identifier for the cases where we parse types as expressions, for example `[ 12 .. _ ]`. @@ -77,6 +77,7 @@ import Paths_cryptol 'type' { Located $$ (Token (KW KW_type ) _)} 'newtype' { Located $$ (Token (KW KW_newtype) _)} 'module' { Located $$ (Token (KW KW_module ) _)} + 'submodule' { Located $$ (Token (KW KW_submodule ) _)} 'where' { Located $$ (Token (KW KW_where ) _)} 'let' { Located $$ (Token (KW KW_let ) _)} 'if' { Located $$ (Token (KW KW_if ) _)} @@ -158,27 +159,27 @@ import Paths_cryptol %% -vmodule :: { Module PName } - : 'module' modName 'where' 'v{' vmod_body 'v}' { mkModule $2 $5 } - | 'module' modName '=' modName 'where' 'v{' vmod_body 'v}' - { mkModuleInstance $2 $4 $7 } - | 'v{' vmod_body 'v}' { mkAnonymousModule $2 } +vmodule :: { Module PName } + : 'module' module_def { $2 } + | 'v{' vmod_body 'v}' { mkAnonymousModule $2 } -vmod_body :: { ([Located Import], [TopDecl PName]) } - : vimports 'v;' vtop_decls { (reverse $1, reverse $3) } - | vimports ';' vtop_decls { (reverse $1, reverse $3) } - | vimports { (reverse $1, []) } - | vtop_decls { ([], reverse $1) } - | {- empty -} { ([], []) } -vimports :: { [Located Import] } - : vimports 'v;' import { $3 : $1 } - | vimports ';' import { $3 : $1 } - | import { [$1] } +module_def :: { Module PName } + + : modName 'where' + 'v{' vmod_body 'v}' { mkModule $1 $4 } + + | modName '=' modName 'where' + 'v{' vmod_body 'v}' { mkModuleInstance $1 $3 $6 } + +vmod_body :: { [TopDecl PName] } + : vtop_decls { reverse $1 } + | {- empty -} { [] } + -- XXX replace rComb with uses of at -import :: { Located Import } - : 'import' modName mbAs mbImportSpec +import :: { Located (ImportG (ImpName PName)) } + : 'import' impName mbAs mbImportSpec { Located { srcRange = rComb $1 $ fromMaybe (srcRange $2) $ msum [ fmap srcRange $4 @@ -191,6 +192,11 @@ import :: { Located Import } } } } +impName :: { Located (ImpName PName) } + : 'submodule' qname { ImpNested `fmap` $2 } + | modName { ImpTop `fmap` $1 } + + mbAs :: { Maybe (Located ModName) } : 'as' modName { Just $2 } | {- empty -} { Nothing } @@ -242,6 +248,9 @@ vtop_decl :: { [TopDecl PName] } | prim_bind { $1 } | private_decls { $1 } | parameter_decls { $1 } + | mbDoc 'submodule' + module_def {% ((:[]) . exportModule $1) `fmap` mkNested $3 } + | import { [DImport $1] } top_decl :: { [TopDecl PName] } : decl { [Decl (TopLevel {tlExport = Public, tlValue = $1 })] } @@ -303,6 +312,7 @@ decl :: { Decl PName } , bInfix = True , bFixity = Nothing , bDoc = Nothing + , bExport = Public } } | 'type' name '=' type {% at ($1,$4) `fmap` mkTySyn $2 [] $4 } diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 715d103fb..7c7e1fbd8 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -37,7 +37,10 @@ module Cryptol.Parser.AST , psFixity -- * Declarations - , Module(..) + , Module + , ModuleG(..) + , mImports + , mSubmoduleImports , Program(..) , TopDecl(..) , Decl(..) @@ -50,11 +53,12 @@ module Cryptol.Parser.AST , Pragma(..) , ExportType(..) , TopLevel(..) - , Import(..), ImportSpec(..) + , Import, ImportG(..), ImportSpec(..), ImpName(..) , Newtype(..) , PrimType(..) , ParameterType(..) , ParameterFun(..) + , NestedModule(..) -- * Interactive , ReplInput(..) @@ -119,14 +123,38 @@ newtype Program name = Program [TopDecl name] deriving (Show) -- | A parsed module. -data Module name = Module - { mName :: Located ModName -- ^ Name of the module +data ModuleG mname name = Module + { mName :: Located mname -- ^ Name of the module , mInstance :: !(Maybe (Located ModName)) -- ^ Functor to instantiate -- (if this is a functor instnaces) - , mImports :: [Located Import] -- ^ Imports for the module + -- , mImports :: [Located Import] -- ^ Imports for the module , mDecls :: [TopDecl name] -- ^ Declartions for the module } deriving (Show, Generic, NFData) +mImports :: ModuleG mname name -> [ Located Import ] +mImports m = + [ li { thing = i { iModule = n } } + | DImport li <- mDecls m + , let i = thing li + , ImpTop n <- [iModule i] + ] + +mSubmoduleImports :: ModuleG mname name -> [ Located (ImportG name) ] +mSubmoduleImports m = + [ li { thing = i { iModule = n } } + | DImport li <- mDecls m + , let i = thing li + , ImpNested n <- [iModule i] + ] + + + +type Module = ModuleG ModName + + +newtype NestedModule name = NestedModule (ModuleG name name) + deriving (Show,Generic,NFData) + modRange :: Module name -> Range modRange m = rCombs $ catMaybes @@ -146,12 +174,21 @@ data TopDecl name = | DParameterConstraint [Located (Prop name)] -- ^ @parameter type constraint (fin T)@ | DParameterFun (ParameterFun name) -- ^ @parameter someVal : [256]@ + | DModule (TopLevel (NestedModule name)) -- ^ Nested module + | DImport (Located (ImportG (ImpName name))) -- ^ An import declaration deriving (Show, Generic, NFData) +data ImpName name = + ImpTop ModName + | ImpNested name + deriving (Show, Generic, NFData) + data Decl name = DSignature [Located name] (Schema name) | DFixity !Fixity [Located name] | DPragma [Located name] Pragma | DBind (Bind name) + | DRec [Bind name] + -- ^ A group of recursive bindings, introduced by the renamer. | DPatBind (Pattern name) (Expr name) | DType (TySyn name) | DProp (PropSyn name) @@ -178,16 +215,15 @@ data ParameterFun name = ParameterFun -- | An import declaration. -data Import = Import { iModule :: !ModName - , iAs :: Maybe ModName - , iSpec :: Maybe ImportSpec - } deriving (Eq, Show, Generic, NFData) +data ImportG mname = Import + { iModule :: !mname + , iAs :: Maybe ModName + , iSpec :: Maybe ImportSpec + } deriving (Eq, Show, Generic, NFData) + +type Import = ImportG ModName -- | The list of names following an import. --- --- INVARIANT: All of the 'Name' entries in the list are expected to be --- unqualified names; the 'QName' or 'NewName' constructors should not be --- present. data ImportSpec = Hiding [Ident] | Only [Ident] deriving (Eq, Show, Generic, NFData) @@ -234,6 +270,7 @@ data Bind name = Bind , bPragmas :: [Pragma] -- ^ Optional pragmas , bMono :: Bool -- ^ Is this a monomorphic binding , bDoc :: Maybe Text -- ^ Optional doc string + , bExport :: !ExportType } deriving (Eq, Generic, NFData, Functor, Show) type LBindDef = Located (BindDef PName) @@ -482,14 +519,17 @@ instance HasLoc a => HasLoc (TopLevel a) where getLoc = getLoc . tlValue instance HasLoc (TopDecl name) where - getLoc td = case td of - Decl tld -> getLoc tld - DPrimType pt -> getLoc pt - TDNewtype n -> getLoc n - Include lfp -> getLoc lfp - DParameterType d -> getLoc d - DParameterFun d -> getLoc d - DParameterConstraint d -> getLoc d + getLoc td = + case td of + Decl tld -> getLoc tld + DPrimType pt -> getLoc pt + TDNewtype n -> getLoc n + Include lfp -> getLoc lfp + DParameterType d -> getLoc d + DParameterFun d -> getLoc d + DParameterConstraint d -> getLoc d + DModule d -> getLoc d + DImport d -> getLoc d instance HasLoc (PrimType name) where getLoc pt = Just (rComb (srcRange (primTName pt)) (srcRange (primTKind pt))) @@ -500,7 +540,7 @@ instance HasLoc (ParameterType name) where instance HasLoc (ParameterFun name) where getLoc a = getLoc (pfName a) -instance HasLoc (Module name) where +instance HasLoc (ModuleG mname name) where getLoc m | null locs = Nothing | otherwise = Just (rCombs locs) @@ -510,6 +550,9 @@ instance HasLoc (Module name) where , getLoc (mDecls m) ] +instance HasLoc (NestedModule name) where + getLoc (NestedModule m) = getLoc m + instance HasLoc (Newtype name) where getLoc n | null locs = Nothing @@ -537,10 +580,24 @@ ppNamed s x = ppL (name x) <+> text s <+> pp (value x) ppNamed' :: PP a => String -> (Ident, (Range, a)) -> Doc ppNamed' s (i,(_,v)) = pp i <+> text s <+> pp v -instance (Show name, PPName name) => PP (Module name) where - ppPrec _ m = text "module" <+> ppL (mName m) <+> text "where" - $$ vcat (map ppL (mImports m)) - $$ vcat (map pp (mDecls m)) + + +instance (Show name, PPName mname, PPName name) => PP (ModuleG mname name) where + ppPrec _ = ppModule 0 + +ppModule :: (Show name, PPName mname, PPName name) => + Int -> ModuleG mname name -> Doc +ppModule n m = + text "module" <+> ppL (mName m) <+> text "where" $$ nest n body + where + body = vcat (map ppL (mImports m)) + $$ vcat (map pp (mDecls m)) + + + +instance (Show name, PPName name) => PP (NestedModule name) where + ppPrec _ (NestedModule m) = ppModule 2 m + instance (Show name, PPName name) => PP (Program name) where ppPrec _ (Program ds) = vcat (map pp ds) @@ -556,10 +613,12 @@ instance (Show name, PPName name) => PP (TopDecl name) where DParameterType d -> pp d DParameterConstraint d -> "parameter" <+> "type" <+> "constraint" <+> prop - where prop = case map pp d of + where prop = case map (pp . thing) d of [x] -> x [] -> "()" xs -> parens (hsep (punctuate comma xs)) + DModule d -> pp d + DImport i -> pp (thing i) instance (Show name, PPName name) => PP (PrimType name) where ppPrec _ pt = @@ -580,6 +639,7 @@ instance (Show name, PPName name) => PP (Decl name) where DSignature xs s -> commaSep (map ppL xs) <+> text ":" <+> pp s DPatBind p e -> pp p <+> text "=" <+> pp e DBind b -> ppPrec n b + DRec bs -> "recursive" $$ nest 2 (vcat (map (ppPrec n) bs)) DFixity f ns -> ppFixity f ns DPragma xs p -> ppPragma xs p DType ts -> ppPrec n ts @@ -596,13 +656,19 @@ instance PPName name => PP (Newtype name) where [ text "newtype", ppL (nName nt), hsep (map pp (nParams nt)), char '=' , braces (commaSep (map (ppNamed' ":") (displayFields (nBody nt)))) ] -instance PP Import where +instance PP mname => PP (ImportG mname) where ppPrec _ d = text "import" <+> sep [ pp (iModule d), mbAs, mbSpec ] where mbAs = maybe empty (\ name -> text "as" <+> pp name ) (iAs d) mbSpec = maybe empty pp (iSpec d) +instance PP name => PP (ImpName name) where + ppPrec _ nm = + case nm of + ImpTop x -> pp x + ImpNested x -> "submodule" <+> pp x + instance PP ImportSpec where ppPrec _ s = case s of Hiding names -> text "hiding" <+> parens (commaSep (map pp names)) @@ -915,13 +981,15 @@ instance (NoPos a, NoPos b) => NoPos (a,b) where instance NoPos (Program name) where noPos (Program x) = Program (noPos x) -instance NoPos (Module name) where +instance NoPos (ModuleG mname name) where noPos m = Module { mName = mName m , mInstance = mInstance m - , mImports = noPos (mImports m) , mDecls = noPos (mDecls m) } +instance NoPos (NestedModule name) where + noPos (NestedModule m) = NestedModule (noPos m) + instance NoPos (TopDecl name) where noPos decl = case decl of @@ -932,6 +1000,9 @@ instance NoPos (TopDecl name) where DParameterFun d -> DParameterFun (noPos d) DParameterType d -> DParameterType (noPos d) DParameterConstraint d -> DParameterConstraint (noPos d) + DModule d -> DModule (noPos d) + DImport d -> DImport (noPos d) + instance NoPos (PrimType name) where noPos x = x @@ -953,6 +1024,7 @@ instance NoPos (Decl name) where DPatBind x y -> DPatBind (noPos x) (noPos y) DFixity f ns -> DFixity f (noPos ns) DBind x -> DBind (noPos x) + DRec bs -> DRec (map noPos bs) DType x -> DType (noPos x) DProp x -> DProp (noPos x) DLocated x _ -> noPos x @@ -973,6 +1045,7 @@ instance NoPos (Bind name) where , bPragmas = noPos (bPragmas x) , bMono = bMono x , bDoc = bDoc x + , bExport = bExport x } instance NoPos Pragma where diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x index 41197cd3c..36eba1275 100644 --- a/src/Cryptol/Parser/Lexer.x +++ b/src/Cryptol/Parser/Lexer.x @@ -100,6 +100,7 @@ $white+ { emit $ White Space } "private" { emit $ KW KW_private } "include" { emit $ KW KW_include } "module" { emit $ KW KW_module } +"submodule" { emit $ KW KW_submodule } "newtype" { emit $ KW KW_newtype } "pragma" { emit $ KW KW_pragma } "property" { emit $ KW KW_property } diff --git a/src/Cryptol/Parser/LexerUtils.hs b/src/Cryptol/Parser/LexerUtils.hs index 4e2a650b0..7b18c515e 100644 --- a/src/Cryptol/Parser/LexerUtils.hs +++ b/src/Cryptol/Parser/LexerUtils.hs @@ -487,6 +487,7 @@ data TokenKW = KW_else | KW_max | KW_min | KW_module + | KW_submodule | KW_newtype | KW_pragma | KW_property diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index 59f2de4ee..d4ffb46be 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -9,7 +9,19 @@ -- This module defines the scoping rules for value- and type-level -- names in Cryptol. -module Cryptol.Parser.Names where +module Cryptol.Parser.Names + ( tnamesNT + , tnamesT + , tnamesC + + , namesD + , tnamesD + , namesB + , namesP + + , boundNames + , boundNamesSet + ) where import Cryptol.Parser.AST import Cryptol.Utils.RecordMap @@ -17,7 +29,6 @@ import Cryptol.Utils.RecordMap import Data.Set (Set) import qualified Data.Set as Set - -- | The names defined by a newtype. tnamesNT :: Newtype name -> ([Located name], ()) tnamesNT x = ([ nName x ], ()) @@ -34,6 +45,8 @@ namesD :: Ord name => Decl name -> ([Located name], Set name) namesD decl = case decl of DBind b -> namesB b + DRec bs -> let (xs,ys) = unzip (map namesB bs) + in (concat xs, Set.unions ys) -- remove binders? DPatBind p e -> (namesP p, namesE e) DSignature {} -> ([],Set.empty) DFixity{} -> ([],Set.empty) @@ -42,25 +55,10 @@ namesD decl = DProp {} -> ([],Set.empty) DLocated d _ -> namesD d --- | The names defined and used by a single declarations in such a way --- that they cannot be duplicated in a file. For example, it is fine --- to use @x@ on the RHS of two bindings, but not on the LHS of two --- type signatures. -allNamesD :: Ord name => Decl name -> [Located name] -allNamesD decl = - case decl of - DBind b -> fst (namesB b) - DPatBind p _ -> namesP p - DSignature ns _ -> ns - DFixity _ ns -> ns - DPragma ns _ -> ns - DType ts -> [tsName ts] - DProp ps -> [psName ps] - DLocated d _ -> allNamesD d - -- | The names defined and used by a single binding. namesB :: Ord name => Bind name -> ([Located name], Set name) -namesB b = ([bName b], boundLNames (namesPs (bParams b)) (namesDef (thing (bDef b)))) +namesB b = + ([bName b], boundLNames (namesPs (bParams b)) (namesDef (thing (bDef b)))) namesDef :: Ord name => BindDef name -> Set name @@ -164,6 +162,7 @@ tnamesD decl = DFixity {} -> ([], Set.empty) DPragma {} -> ([], Set.empty) DBind b -> ([], tnamesB b) + DRec bs -> ([], Set.unions (map tnamesB bs)) DPatBind _ e -> ([], tnamesE e) DLocated d _ -> tnamesD d DType (TySyn n _ ps t) diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs index fbe975a0f..fda369f7c 100644 --- a/src/Cryptol/Parser/NoInclude.hs +++ b/src/Cryptol/Parser/NoInclude.hs @@ -160,7 +160,7 @@ collectErrors f ts = do return rs -- | Remove includes from a module. -noIncludeModule :: Module PName -> NoIncM (Module PName) +noIncludeModule :: ModuleG mname PName -> NoIncM (ModuleG mname PName) noIncludeModule m = update `fmap` collectErrors noIncTopDecl (mDecls m) where update tds = m { mDecls = concat tds } @@ -174,13 +174,19 @@ noIncludeProgram (Program tds) = -- reference. noIncTopDecl :: TopDecl PName -> NoIncM [TopDecl PName] noIncTopDecl td = case td of - Decl _ -> return [td] + Decl _ -> pure [td] DPrimType {} -> pure [td] - TDNewtype _-> return [td] - DParameterType {} -> return [td] - DParameterConstraint {} -> return [td] - DParameterFun {} -> return [td] + TDNewtype _-> pure [td] + DParameterType {} -> pure [td] + DParameterConstraint {} -> pure [td] + DParameterFun {} -> pure [td] Include lf -> resolveInclude lf + DModule tl -> + case tlValue tl of + NestedModule m -> + do m1 <- noIncludeModule m + pure [ DModule tl { tlValue = NestedModule m1 } ] + DImport {} -> pure [td] -- | Resolve the file referenced by a include into a list of top-level -- declarations. diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index 48dc4608c..835a4fa4e 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -44,18 +44,23 @@ instance RemovePatterns (Program PName) where instance RemovePatterns (Expr PName) where removePatterns e = runNoPatM (noPatE e) -instance RemovePatterns (Module PName) where +instance RemovePatterns (ModuleG mname PName) where removePatterns m = runNoPatM (noPatModule m) instance RemovePatterns [Decl PName] where removePatterns ds = runNoPatM (noPatDs ds) +instance RemovePatterns (NestedModule PName) where + removePatterns (NestedModule m) = (NestedModule m1,errs) + where (m1,errs) = removePatterns m + simpleBind :: Located PName -> Expr PName -> Bind PName simpleBind x e = Bind { bName = x, bParams = [] , bDef = at e (Located emptyRange (DExpr e)) , bSignature = Nothing, bPragmas = [] , bMono = True, bInfix = False, bFixity = Nothing , bDoc = Nothing + , bExport = Public } sel :: Pattern PName -> PName -> Selector -> Bind PName @@ -226,6 +231,7 @@ noMatchD decl = DBind b -> do b1 <- noMatchB b return [DBind b1] + DRec {} -> panic "noMatchD" [ "DRec" ] DPatBind p e -> do (p',bs) <- noPat p let (x,ts) = splitSimpleP p' @@ -240,6 +246,7 @@ noMatchD decl = , bInfix = False , bFixity = Nothing , bDoc = Nothing + , bExport = Public } : map DBind bs DType {} -> return [decl] DProp {} -> return [decl] @@ -323,7 +330,7 @@ noPatTopDs tds = noPatProg :: Program PName -> NoPatM (Program PName) noPatProg (Program topDs) = Program <$> noPatTopDs topDs -noPatModule :: Module PName -> NoPatM (Module PName) +noPatModule :: ModuleG mname PName -> NoPatM (ModuleG mname PName) noPatModule m = do ds1 <- noPatTopDs (mDecls m) return m { mDecls = ds1 } @@ -385,6 +392,13 @@ annotTopDs tds = TDNewtype {} -> (d :) <$> annotTopDs ds Include {} -> (d :) <$> annotTopDs ds + DModule m -> + case removePatterns (tlValue m) of + (m1,errs) -> do lift (mapM_ recordError errs) + (DModule m { tlValue = m1 } :) <$> annotTopDs ds + + DImport {} -> (d :) <$> annotTopDs ds + [] -> return [] @@ -403,6 +417,7 @@ annotD :: Decl PName -> ExceptionT () (StateT AnnotMap NoPatM) (Decl PName) annotD decl = case decl of DBind b -> DBind <$> lift (annotB b) + DRec {} -> panic "annotD" [ "DRec" ] DSignature {} -> raise () DFixity{} -> raise () DPragma {} -> raise () @@ -524,6 +539,7 @@ toDocs TopLevel { .. } DSignature ns _ -> [ (thing n, [txt]) | n <- ns ] DFixity _ ns -> [ (thing n, [txt]) | n <- ns ] DBind b -> [ (thing (bName b), [txt]) ] + DRec {} -> panic "toDocs" [ "DRec" ] DLocated d _ -> go txt d DPatBind p _ -> [ (thing n, [txt]) | n <- namesP p ] diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index ca03c2f58..0f1ebda36 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -38,7 +38,7 @@ import Cryptol.Parser.Lexer import Cryptol.Parser.LexerUtils(SelectorType(..)) import Cryptol.Parser.Position import Cryptol.Parser.Utils (translateExprToNumT,widthIdent) -import Cryptol.Utils.Ident(packModName) +import Cryptol.Utils.Ident(packModName,packIdent,modNameChunks) import Cryptol.Utils.PP import Cryptol.Utils.Panic import Cryptol.Utils.RecordMap @@ -433,6 +433,11 @@ exportNewtype e d n = TDNewtype TopLevel { tlExport = e , tlDoc = d , tlValue = n } +exportModule :: Maybe (Located Text) -> NestedModule PName -> TopDecl PName +exportModule mbDoc m = DModule TopLevel { tlExport = Public + , tlDoc = mbDoc + , tlValue = m } + mkParFun :: Maybe (Located Text) -> Located PName -> Schema PName -> @@ -464,7 +469,9 @@ changeExport e = map change change (Decl d) = Decl d { tlExport = e } change (DPrimType t) = DPrimType t { tlExport = e } change (TDNewtype n) = TDNewtype n { tlExport = e } + change (DModule m) = DModule m { tlExport = e } change td@Include{} = td + change td@DImport{} = td change (DParameterType {}) = panic "changeExport" ["private type parameter?"] change (DParameterFun {}) = panic "changeExport" ["private value parameter?"] change (DParameterConstraint {}) = @@ -534,6 +541,7 @@ mkProperty f ps e = DBind Bind { bName = f , bInfix = False , bFixity = Nothing , bDoc = Nothing + , bExport = Public } -- NOTE: The lists of patterns are reversed! @@ -549,6 +557,7 @@ mkIndexedDecl f (ps, ixs) e = , bInfix = False , bFixity = Nothing , bDoc = Nothing + , bExport = Public } where rhs :: Expr PName @@ -588,6 +597,7 @@ mkPrimDecl mbDoc ln sig = , bInfix = isInfixIdent (getIdent (thing ln)) , bFixity = Nothing , bDoc = Nothing + , bExport = Public } , exportDecl Nothing Public $ DSignature [ln] sig @@ -737,18 +747,24 @@ mkProp ty = err = errorMessage r ["Invalid constraint"] -- | Make an ordinary module -mkModule :: Located ModName -> - ([Located Import], [TopDecl PName]) -> - Module PName -mkModule nm (is,ds) = Module { mName = nm - , mInstance = Nothing - , mImports = is - , mDecls = ds - } +mkModule :: Located ModName -> [TopDecl PName] -> Module PName +mkModule nm ds = Module { mName = nm + , mInstance = Nothing + , mDecls = ds + } + +mkNested :: Module PName -> ParseM (NestedModule PName) +mkNested m = + case modNameChunks (thing nm) of + [c] -> pure (NestedModule m { mName = nm { thing = mkUnqual (packIdent c)}}) + _ -> errorMessage r + ["Nested modules names should be a simple identifier."] + where + nm = mName m + r = srcRange nm -- | Make an unnamed module---gets the name @Main@. -mkAnonymousModule :: ([Located Import], [TopDecl PName]) -> - Module PName +mkAnonymousModule :: [TopDecl PName] -> Module PName mkAnonymousModule = mkModule Located { srcRange = emptyRange , thing = mkModName [T.pack "Main"] } @@ -756,12 +772,11 @@ mkAnonymousModule = mkModule Located { srcRange = emptyRange -- | Make a module which defines a functor instance. mkModuleInstance :: Located ModName -> Located ModName -> - ([Located Import], [TopDecl PName]) -> + [TopDecl PName] -> Module PName -mkModuleInstance nm fun (is,ds) = +mkModuleInstance nm fun ds = Module { mName = nm , mInstance = Just fun - , mImports = is , mDecls = ds } diff --git a/src/Cryptol/Parser/Position.hs b/src/Cryptol/Parser/Position.hs index e5912b931..cc3900037 100644 --- a/src/Cryptol/Parser/Position.hs +++ b/src/Cryptol/Parser/Position.hs @@ -10,6 +10,9 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE RecordWildCards #-} module Cryptol.Parser.Position where @@ -22,7 +25,8 @@ import Control.DeepSeq import Cryptol.Utils.PP data Located a = Located { srcRange :: !Range, thing :: !a } - deriving (Eq, Ord, Show, Generic, NFData) + deriving (Eq, Ord, Show, Generic, NFData + , Functor, Foldable, Traversable ) data Position = Position { line :: !Int, col :: !Int } @@ -65,8 +69,6 @@ rCombMaybe (Just x) (Just y) = Just (rComb x y) rCombs :: [Range] -> Range rCombs = foldl1 rComb -instance Functor Located where - fmap f l = l { thing = f (thing l) } -------------------------------------------------------------------------------- diff --git a/src/Cryptol/REPL/Browse.hs b/src/Cryptol/REPL/Browse.hs new file mode 100644 index 000000000..4722e5782 --- /dev/null +++ b/src/Cryptol/REPL/Browse.hs @@ -0,0 +1,155 @@ +{-# Language OverloadedStrings, BlockArguments #-} +module Cryptol.REPL.Browse (BrowseHow(..), browseModContext) where + +import qualified Data.Set as Set +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe(mapMaybe) +import Data.List(sortBy) +import qualified Text.PrettyPrint as PP + +import Cryptol.Parser.AST(Pragma(..)) +import qualified Cryptol.TypeCheck.Type as T + +import Cryptol.Utils.PP +import Cryptol.ModuleSystem.Env(ModContext(..)) +import Cryptol.ModuleSystem.NamingEnv(namingEnvNames) +import Cryptol.ModuleSystem.Name +import Cryptol.ModuleSystem.Interface + +data BrowseHow = BrowseExported | BrowseInScope + +browseModContext :: BrowseHow -> ModContext -> PP.Doc +browseModContext how mc = runDoc (env disp) (vcat sections) + where + sections = + [ browseMParams (env disp) (mctxParams mc) + , browseMods disp decls + , browseTSyns disp decls + , browsePrimTys disp decls + , browseNewtypes disp decls + , browseVars disp decls + ] + + disp = DispInfo { dispHow = how, env = mctxNameDisp mc } + decls = filterIfaceDecls (`Set.member` visNames) (mctxDecls mc) + allNames = namingEnvNames (mctxNames mc) + visNames = case how of + BrowseInScope -> allNames + BrowseExported -> mctxExported mc + +data DispInfo = DispInfo { dispHow :: BrowseHow, env :: NameDisp } + +-------------------------------------------------------------------------------- + + +browseMParams :: NameDisp -> IfaceParams -> Doc +browseMParams disp params = + ppSectionHeading "Module Parameters" + $ addEmpty + $ map ppParamTy (sortByName disp (Map.toList (ifParamTypes params))) ++ + map ppParamFu (sortByName disp (Map.toList (ifParamFuns params))) + where + ppParamTy p = hang ("type" <+> pp (T.mtpName p) <+> ":") 2 (pp (T.mtpKind p)) + ppParamFu p = hang (pp (T.mvpName p) <+> ":") 2 (pp (T.mvpType p)) + -- XXX: should we print the constraints somewhere too? + + addEmpty xs = case xs of + [] -> [] + _ -> xs ++ [" "] + + +browseMods :: DispInfo -> IfaceDecls -> Doc +browseMods disp decls = + ppSection disp "Modules" ppM (ifModules decls) + where + ppM m = "submodule" <+> pp (ifModName m) + -- XXX: can print a lot more information about the moduels, but + -- might be better to do that with a separate command + + + + +browseTSyns :: DispInfo -> IfaceDecls -> Doc +browseTSyns disp decls = + ppSection disp "Type Synonyms" pp tss + $$ ppSection disp "Constraint Synonyms" pp cts + where + (cts,tss) = Map.partition isCtrait (ifTySyns decls) + isCtrait t = T.kindResult (T.kindOf (T.tsDef t)) == T.KProp + +browsePrimTys :: DispInfo -> IfaceDecls -> Doc +browsePrimTys disp decls = + ppSection disp "Primitive Types" ppA (ifAbstractTypes decls) + where + ppA a = pp (T.atName a) <+> ":" <+> pp (T.atKind a) + +browseNewtypes :: DispInfo -> IfaceDecls -> Doc +browseNewtypes disp decls = + ppSection disp "Newtypes" T.ppNewtypeShort (ifNewtypes decls) + +browseVars :: DispInfo -> IfaceDecls -> Doc +browseVars disp decls = + ppSection disp "Properties" ppVar props + $$ ppSection disp "Symbols" ppVar syms + where + isProp p = PragmaProperty `elem` ifDeclPragmas p + (props,syms) = Map.partition isProp (ifDecls decls) + + ppVar d = hang (pp (ifDeclName d) <+> char ':') 2 (pp (ifDeclSig d)) + + +-------------------------------------------------------------------------------- + +ppSection :: DispInfo -> String -> (a -> Doc) -> Map Name a -> Doc +ppSection disp heading ppThing mp = + ppSectionHeading heading + case dispHow disp of + BrowseExported | [(_,xs)] <- grouped -> ppThings xs + _ -> concatMap ppMod grouped + where + grouped = groupDecls (env disp) mp + + ppThings xs = map ppThing xs ++ [" "] + + ppMod (nm,things) = + [ "From" <+> pp nm + , "-----" <.> text (map (const '-') (show (runDoc (env disp) (pp nm)))) + , " " + , nest 2 (vcat (ppThings things)) + ] + +ppSectionHeading :: String -> [Doc] -> Doc +ppSectionHeading heading body + | null body = empty + | otherwise = + vcat [ text heading + , text (map (const '=') heading) + , " " + , nest 2 (vcat body) + ] + + + + +-- | Organize by module where defined, then sort by name. +groupDecls :: NameDisp -> Map Name a -> [(ModPath,[a])] +groupDecls disp = Map.toList + . fmap (sortByName disp) + . Map.fromListWith (++) + . mapMaybe toEntry + . Map.toList + where + toEntry (n,a) = + case nameInfo n of + Declared m _ -> Just (m,[(n,a)]) + _ -> Nothing + + +sortByName :: NameDisp -> [(Name,a)] -> [a] +sortByName disp = map snd . sortBy cmpByDispName + where + cmpByDispName (x,_) (y,_) = cmpNameDisplay disp x y + + + diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 9afbe8ba1..7634ae9b6 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -55,6 +55,7 @@ module Cryptol.REPL.Command ( import Cryptol.REPL.Monad import Cryptol.REPL.Trie +import Cryptol.REPL.Browse import qualified Cryptol.ModuleSystem as M import qualified Cryptol.ModuleSystem.Name as M @@ -105,8 +106,7 @@ import qualified Data.ByteString.Char8 as BS8 import Data.Bits (shiftL, (.&.), (.|.)) import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii) import Data.Function (on) -import Data.List (intercalate, nub, sortBy, groupBy, - partition, isPrefixOf,intersperse) +import Data.List (intercalate, nub, isPrefixOf,intersperse) import Data.Maybe (fromMaybe,mapMaybe,isNothing) import System.Environment (lookupEnv) import System.Exit (ExitCode(ExitSuccess)) @@ -116,7 +116,6 @@ import System.FilePath((), isPathSeparator) import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist ,getTemporaryDirectory,setPermissions,removeFile ,emptyPermissions,setOwnerReadable) -import Data.Map (Map) import qualified Data.Map as Map import qualified Data.Set as Set import System.IO @@ -199,8 +198,12 @@ nbCommandList = "Check the type of an expression." "" , CommandDescr [ ":b", ":browse" ] ["[ MODULE ]"] (ModNameArg browseCmd) - "Display environment for all loaded modules, or for a specific module." - "" + "Display information about loaded modules." + (unlines + [ "With no arguent, :browse shows information about the names in scope." + , "With an argument M, shows information about the names exported from M" + ] + ) , CommandDescr [ ":version"] [] (NoArg versionCmd) "Display the version of this Cryptol executable" "" @@ -1155,212 +1158,18 @@ quitCmd :: REPL () quitCmd = stop browseCmd :: String -> REPL () -browseCmd input = do - let mnames = map (M.textToModName . T.pack) (words input) - validModNames <- (:) M.interactiveName <$> getModNames - let checkModName m = - unless (m `elem` validModNames) $ - rPutStrLn ("error: " ++ show m ++ " is not a loaded module.") - mapM_ checkModName mnames - - fe <- getFocusedEnv - - let params = M.mctxParams fe - iface = M.mctxDecls fe - names = M.mctxNames fe - disp = M.mctxNameDisp fe - provV = M.mctxValueProvenance fe - provT = M.mctxTypeProvenace fe - - - let f &&& g = \x -> f x && g x - isUser x = case M.nameInfo x of - M.Declared _ M.SystemName -> False - _ -> True - inSet s x = x `Set.member` s - - let (visibleTypes,visibleDecls) = M.visibleNames names - - restricted = if null mnames then const True else hasAnyModName mnames - - visibleType = isUser &&& restricted &&& inSet visibleTypes - visibleDecl = isUser &&& restricted &&& inSet visibleDecls - - browseMParams visibleType visibleDecl params disp - browseTSyns visibleType provT iface disp - browsePrimTys visibleType provT iface disp - browseNewtypes visibleType provT iface disp - browseVars visibleDecl provV iface disp - - -browseMParams :: (M.Name -> Bool) -> (M.Name -> Bool) -> - M.IfaceParams -> NameDisp -> REPL () -browseMParams visT visD M.IfaceParams { .. } names = - do ppBlock names ppParamTy "Type Parameters" - (sorted visT T.mtpName ifParamTypes) - ppBlock names ppParamFu "Value Parameters" - (sorted visD T.mvpName ifParamFuns) - - where - ppParamTy T.ModTParam { .. } = hang ("type" <+> pp mtpName <+> ":") - 2 (pp mtpKind) - ppParamFu T.ModVParam { .. } = hang (pp mvpName <+> ":") 2 (pp mvpType) - - sorted vis nm mp = sortBy (M.cmpNameDisplay names `on` nm) - $ filter (vis . nm) $ Map.elems mp - -type Prov = Map M.Name M.DeclProvenance - -browsePrimTys :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL () -browsePrimTys isVisible prov M.IfaceDecls { .. } names = - ppSection (Map.elems ifAbstractTypes) - Section { secName = "Primitive Types" - , secEntryName = T.atName - , secProvenance = prov - , secDisp = names - , secPP = ppA - , secVisible = isVisible - } - where - ppA a = pp (T.atName a) <+> ":" <+> pp (T.atKind a) - - -browseTSyns :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL () -browseTSyns isVisible prov M.IfaceDecls { .. } names = - do ppSection tss - Section { secName = "Type Synonyms" - , secEntryName = T.tsName - , secProvenance = prov - , secDisp = names - , secVisible = isVisible - , secPP = pp - } - ppSection cts - Section { secName = "Constraint Synonyms" - , secEntryName = T.tsName - , secProvenance = prov - , secDisp = names - , secVisible = isVisible - , secPP = pp - } - where - (cts,tss) = partition isCtrait (Map.elems ifTySyns) - isCtrait t = T.kindResult (T.kindOf (T.tsDef t)) == T.KProp - -browseNewtypes :: - (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL () -browseNewtypes isVisible prov M.IfaceDecls { .. } names = - ppSection (Map.elems ifNewtypes) - Section { secName = "Newtypes" - , secEntryName = T.ntName - , secVisible = isVisible - , secProvenance = prov - , secDisp = names - , secPP = T.ppNewtypeShort - } - -browseVars :: (M.Name -> Bool) -> Prov -> M.IfaceDecls -> NameDisp -> REPL () -browseVars isVisible prov M.IfaceDecls { .. } names = - do ppSection props Section { secName = "Properties" - , secEntryName = M.ifDeclName - , secVisible = isVisible - , secProvenance = prov - , secDisp = names - , secPP = ppVar - } - ppSection syms Section { secName = "Symbols" - , secEntryName = M.ifDeclName - , secVisible = isVisible - , secProvenance = prov - , secDisp = names - , secPP = ppVar - } - - where - isProp p = T.PragmaProperty `elem` (M.ifDeclPragmas p) - (props,syms) = partition isProp (Map.elems ifDecls) - - ppVar M.IfaceDecl { .. } = hang (pp ifDeclName <+> char ':') 2 (pp ifDeclSig) - - - -data Section a = Section - { secName :: String - , secEntryName :: a -> M.Name - , secVisible :: M.Name -> Bool - , secProvenance :: Map M.Name M.DeclProvenance - , secDisp :: NameDisp - , secPP :: a -> Doc - } - -ppSection :: [a] -> Section a -> REPL () -ppSection things s - | null grouped = pure () +browseCmd input + | null input = + do fe <- getFocusedEnv + rPrint (browseModContext BrowseInScope fe) | otherwise = - do let heading = secName s - rPutStrLn heading - rPutStrLn (map (const '=') heading) - rPutStrLn "" - mapM_ ppSub grouped - - where - ppSub (p,ts) = - do let heading = provHeading p - rPutStrLn (" " ++ heading) - rPutStrLn (" " ++ map (const '-') heading) - rPutStrLn "" - rPutStrLn $ show $ runDoc (secDisp s) $ nest 4 $ vcat $ map (secPP s) ts - rPutStrLn "" - - grouped = map rearrange $ - groupBy sameProv $ - sortBy cmpThings - [ (n,p,t) | t <- things, - let n = secEntryName s t, - secVisible s n, - let p = case Map.lookup n (secProvenance s) of - Just i -> i - Nothing -> panic "ppSection" - [ "Name with no provenance" - , show n ] - ] - - rearrange xs = (p, [ a | (_,_,a) <- xs ]) - where (_,p,_) : _ = xs - - cmpThings (n1, p1, _) (n2, p2, _) = - case cmpProv p1 p2 of - EQ -> M.cmpNameDisplay (secDisp s) n1 n2 - r -> r - - sameProv (_,p1,_) (_,p2,_) = provOrd p1 == provOrd p2 - - provOrd p = - case p of - M.NameIsParameter -> Left 1 :: Either Int P.ModName - M.NameIsDynamicDecl -> Left 2 - M.NameIsLocalPublic -> Left 3 - M.NameIsLocalPrivate -> Left 4 - M.NameIsImportedFrom x -> Right x - - cmpProv p1 p2 = compare (provOrd p1) (provOrd p2) - - provHeading p = - case p of - M.NameIsParameter -> "Parameters" - M.NameIsDynamicDecl -> "REPL" - M.NameIsLocalPublic -> "Public" - M.NameIsLocalPrivate -> "Private" - M.NameIsImportedFrom m -> "From " ++ show (pp m) - - - -ppBlock :: NameDisp -> (a -> Doc) -> String -> [a] -> REPL () -ppBlock names ppFun name xs = unless (null xs) $ - do rPutStrLn name - rPutStrLn (replicate (length name) '=') - rPrint (runDoc names (nest 4 (vcat (map ppFun xs)))) - rPutStrLn "" + case parseModName input of + Nothing -> rPutStrLn "Invalid module name" + Just m -> + do mb <- M.modContextOf m <$> getModuleEnv + case mb of + Nothing -> rPutStrLn ("Module " ++ show input ++ " is not loaded") + Just fe -> rPrint (browseModContext BrowseExported fe) setOptionCmd :: String -> REPL () @@ -1413,14 +1222,16 @@ helpCmd cmd vNames = M.lookupValNames qname rnEnv tNames = M.lookupTypeNames qname rnEnv + mNames = M.lookupNS M.NSModule qname rnEnv let helps = map (showTypeHelp params env disp) tNames ++ - map (showValHelp params env disp qname) vNames + map (showValHelp params env disp qname) vNames ++ + map (showModHelp env disp) mNames separ = rPutStrLn " ---------" sequence_ (intersperse separ helps) - when (null (vNames ++ tNames)) $ + when (null (vNames ++ tNames ++ mNames)) $ rPrint $ "Undefined name:" <+> pp qname Nothing -> rPutStrLn ("Unable to parse name: " ++ cmd) @@ -1433,6 +1244,9 @@ helpCmd cmd M.Parameter -> rPutStrLn "// No documentation is available." + showModHelp env disp x = + rPrint $ runDoc disp $ vcat [ "`" <> pp x <> "` is a module." ] + -- XXX: show doc. if any showTypeHelp params env nameEnv name = fromMaybe (noInfo nameEnv name) $ @@ -1595,13 +1409,6 @@ handleCtrlC a = do rPutStrLn "Ctrl-C" -- Utilities ------------------------------------------------------------------- -hasAnyModName :: [M.ModName] -> M.Name -> Bool -hasAnyModName mnames n = - case M.nameInfo n of - M.Declared m _ -> m `elem` mnames - M.Parameter -> False - - -- | Lift a parsing action into the REPL monad. replParse :: (String -> Either ParseError a) -> String -> REPL a replParse parse str = case parse str of diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 73cde1e6a..972dcd94f 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -533,7 +533,7 @@ validEvalContext a = badName nm bs = case M.nameInfo nm of - M.Declared m _ + M.Declared (M.TopModule m) _ -- XXX: can we focus nested modules? | M.isLoadedParamMod m (M.meLoadedModules me) -> Set.insert nm bs _ -> bs @@ -588,14 +588,14 @@ getFocusedEnv = M.focusedEnv <$> getModuleEnv getExprNames :: REPL [String] getExprNames = do fNames <- M.mctxNames <$> getFocusedEnv - return (map (show . pp) (Map.keys (M.neExprs fNames))) + return (map (show . pp) (Map.keys (M.namespaceMap M.NSValue fNames))) -- | Get visible type signature names. -- This is used for command line completition. getTypeNames :: REPL [String] getTypeNames = do fNames <- M.mctxNames <$> getFocusedEnv - return (map (show . pp) (Map.keys (M.neTypes fNames))) + return (map (show . pp) (Map.keys (M.namespaceMap M.NSType fNames))) -- | Return a list of property names, sorted by position in the file. getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp) @@ -636,7 +636,8 @@ uniqify :: M.Name -> REPL M.Name uniqify name = case M.nameInfo name of M.Declared ns s -> - M.liftSupply (M.mkDeclared ns s (M.nameIdent name) (M.nameFixity name) (M.nameLoc name)) + M.liftSupply (M.mkDeclared (M.nameNamespace name) + ns s (M.nameIdent name) (M.nameFixity name) (M.nameLoc name)) M.Parameter -> panic "[REPL] uniqify" ["tried to uniqify a parameter: " ++ pretty name] @@ -656,7 +657,8 @@ uniqify name = -- the "" namespace. freshName :: I.Ident -> M.NameSource -> REPL M.Name freshName i sys = - M.liftSupply (M.mkDeclared I.interactiveName sys i Nothing emptyRange) + M.liftSupply (M.mkDeclared I.NSValue mpath sys i Nothing emptyRange) + where mpath = M.TopModule I.interactiveName -- User Environment Interaction ------------------------------------------------ diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs index d31238087..a7574fb54 100644 --- a/src/Cryptol/Transform/MonoValues.hs +++ b/src/Cryptol/Transform/MonoValues.hs @@ -79,11 +79,11 @@ module Cryptol.Transform.MonoValues (rewModule) where import Cryptol.ModuleSystem.Name - (SupplyT,liftSupply,Supply,mkDeclared,NameSource(..)) + (SupplyT,liftSupply,Supply,mkDeclared,NameSource(..),ModPath(..)) import Cryptol.Parser.Position (emptyRange) import Cryptol.TypeCheck.AST hiding (splitTApp) -- XXX: just use this one import Cryptol.TypeCheck.TypeMap -import Cryptol.Utils.Ident (ModName) +import Cryptol.Utils.Ident(Namespace(..)) import Data.List(sortBy,groupBy) import Data.Either(partitionEithers) import Data.Map (Map) @@ -132,7 +132,7 @@ instance TrieMap RewMap' (Name,[Type],Int) where -- | Note that this assumes that this pass will be run only once for each -- module, otherwise we will get name collisions. rewModule :: Supply -> Module -> (Module,Supply) -rewModule s m = runM body (mName m) s +rewModule s m = runM body (TopModule (mName m)) s where body = do ds <- mapM (rewDeclGroup emptyTM) (mDecls m) return m { mDecls = ds } @@ -140,13 +140,13 @@ rewModule s m = runM body (mName m) s -------------------------------------------------------------------------------- type M = ReaderT RO (SupplyT Id) -type RO = ModName +type RO = ModPath -- | Produce a fresh top-level name. newName :: M Name newName = do ns <- ask - liftSupply (mkDeclared ns SystemName "$mono" Nothing emptyRange) + liftSupply (mkDeclared NSValue ns SystemName "$mono" Nothing emptyRange) newTopOrLocalName :: M Name newTopOrLocalName = newName diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs index d86c83115..103f5a623 100644 --- a/src/Cryptol/Transform/Specialize.hs +++ b/src/Cryptol/Transform/Specialize.hs @@ -242,9 +242,10 @@ destETAbs = go [] freshName :: Name -> [Type] -> SpecM Name freshName n _ = case nameInfo n of - Declared ns s -> liftSupply (mkDeclared ns s ident fx loc) - Parameter -> liftSupply (mkParameter ident loc) + Declared m s -> liftSupply (mkDeclared ns m s ident fx loc) + Parameter -> liftSupply (mkParameter ns ident loc) where + ns = nameNamespace n fx = nameFixity n ident = nameIdent n loc = nameLoc n diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs index fb358ba82..4043ee9d7 100644 --- a/src/Cryptol/TypeCheck.hs +++ b/src/Cryptol/TypeCheck.hs @@ -27,12 +27,14 @@ module Cryptol.TypeCheck , ppNamedError ) where +import Data.IORef(IORef,modifyIORef') + import Cryptol.ModuleSystem.Name - (liftSupply,mkDeclared,NameSource(..)) + (liftSupply,mkDeclared,NameSource(..),ModPath(..)) +import Cryptol.ModuleSystem.NamingEnv(NamingEnv,namingEnvRename) import qualified Cryptol.Parser.AST as P import Cryptol.Parser.Position(Range,emptyRange) import Cryptol.TypeCheck.AST -import Cryptol.TypeCheck.Depends (FromDecl) import Cryptol.TypeCheck.Error import Cryptol.TypeCheck.Monad ( runInferM @@ -41,16 +43,20 @@ import Cryptol.TypeCheck.Monad , NameSeeds , nameSeeds , lookupVar + , newLocalScope, endLocalScope + , newModuleScope, addParamType, addParameterConstraints + , endModuleInstance + , io ) -import Cryptol.TypeCheck.Infer (inferModule, inferBinds, inferDs) -import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..)) -import Cryptol.TypeCheck.Solve(proveModuleTopLevel) -import Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance) -import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints) -import Cryptol.TypeCheck.PP(WithNames(..),NameMap) -import Cryptol.Utils.Ident (exprModName,packIdent) -import Cryptol.Utils.PP -import Cryptol.Utils.Panic(panic) +import Cryptol.TypeCheck.Infer (inferModule, inferBinds, checkTopDecls) +import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..)) +import Cryptol.TypeCheck.Solve(proveModuleTopLevel) +import Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance) +-- import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints) +import Cryptol.TypeCheck.PP(WithNames(..),NameMap) +import Cryptol.Utils.Ident (exprModName,packIdent,Namespace(..)) +import Cryptol.Utils.PP +import Cryptol.Utils.Panic(panic) @@ -59,17 +65,22 @@ tcModule m inp = runInferM inp (inferModule m) -- | Check a module instantiation, assuming that the functor has already -- been checked. -tcModuleInst :: Module {- ^ functor -} -> - P.Module Name {- params -} -> +-- XXX: This will change +tcModuleInst :: IORef NamingEnv {- ^ renaming environment of functor -} -> + Module {- ^ functor -} -> + P.Module Name {- ^ params -} -> InferInput {- ^ TC settings -} -> IO (InferOutput Module) {- ^ new version of instance -} -tcModuleInst func m inp = runInferM inp - $ do x <- inferModule m - flip (foldr withParamType) (mParamTypes x) $ - withParameterConstraints (mParamConstraints x) $ - do y <- checkModuleInstance func x - proveModuleTopLevel - pure y +tcModuleInst renThis func m inp = runInferM inp $ + do x <- inferModule m + newModuleScope (mName func) [] mempty + mapM_ addParamType (mParamTypes x) + addParameterConstraints (mParamConstraints x) + (ren,y) <- checkModuleInstance func x + io $ modifyIORef' renThis (namingEnvRename ren) + proveModuleTopLevel + endModuleInstance + pure y tcExpr :: P.Expr Name -> InferInput -> IO (InferOutput (Expr,Schema)) tcExpr e0 inp = runInferM inp @@ -92,8 +103,9 @@ tcExpr e0 inp = runInferM inp , show e' , show t ] - _ -> do fresh <- liftSupply (mkDeclared exprModName SystemName - (packIdent "(expression)") Nothing loc) + _ -> do fresh <- liftSupply $ + mkDeclared NSValue (TopModule exprModName) SystemName + (packIdent "(expression)") Nothing loc res <- inferBinds True False [ P.Bind { P.bName = P.Located { P.srcRange = loc, P.thing = fresh } @@ -105,6 +117,7 @@ tcExpr e0 inp = runInferM inp , P.bInfix = False , P.bFixity = Nothing , P.bDoc = Nothing + , P.bExport = Public } ] case res of @@ -119,10 +132,12 @@ tcExpr e0 inp = runInferM inp : map show res ) -tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup]) -tcDecls ds inp = runInferM inp $ inferDs ds $ \dgs -> do - proveModuleTopLevel - return dgs +tcDecls :: [P.TopDecl Name] -> InferInput -> IO (InferOutput [DeclGroup]) +tcDecls ds inp = runInferM inp $ + do newLocalScope + checkTopDecls ds + proveModuleTopLevel + endLocalScope ppWarning :: (Range,Warning) -> Doc ppWarning (r,w) = text "[warning] at" <+> pp r <.> colon $$ nest 2 (pp w) diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 46c4cdd00..087351288 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -18,10 +18,10 @@ module Cryptol.TypeCheck.AST , Name() , TFun(..) , Selector(..) - , Import(..) + , Import, ImportG(..) , ImportSpec(..) , ExportType(..) - , ExportSpec(..), isExportedBind, isExportedType + , ExportSpec(..), isExportedBind, isExportedType, isExported , Pragma(..) , Fixity(..) , PrimMap(..) @@ -30,10 +30,12 @@ module Cryptol.TypeCheck.AST import Cryptol.Parser.Position(Located,Range,HasLoc(..)) import Cryptol.ModuleSystem.Name +import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Exports(ExportSpec(..) - , isExportedBind, isExportedType) + , isExportedBind, isExportedType, isExported) import Cryptol.Parser.AST ( Selector(..),Pragma(..) - , Import(..), ImportSpec(..), ExportType(..) + , Import + , ImportG(..), ImportSpec(..), ExportType(..) , Fixity(..)) import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim) import Cryptol.Utils.RecordMap @@ -50,57 +52,59 @@ import Data.Text (Text) -- | A Cryptol module. -data Module = Module { mName :: !ModName - , mExports :: ExportSpec Name - , mImports :: [Import] +data ModuleG mname = + Module { mName :: !mname + , mExports :: ExportSpec Name + , mImports :: [Import] + + {-| Interfaces of submodules, including functors. + This is only the directly nested modules. + Info about more nested modules is in the + corresponding interface. -} + , mSubModules :: Map Name (IfaceG Name) + + -- params, if functor + , mParamTypes :: Map Name ModTParam + , mParamConstraints :: [Located Prop] + , mParamFuns :: Map Name ModVParam - , mTySyns :: Map Name TySyn - -- ^ This is just the type-level type synonyms - -- of a module. + -- Declarations, including everything from non-functor + -- submodules + , mTySyns :: Map Name TySyn , mNewtypes :: Map Name Newtype , mPrimTypes :: Map Name AbstractType - , mParamTypes :: Map Name ModTParam - , mParamConstraints :: [Located Prop] - , mParamFuns :: Map Name ModVParam , mDecls :: [DeclGroup] + , mFunctors :: Map Name (ModuleG Name) } deriving (Show, Generic, NFData) +emptyModule :: mname -> ModuleG mname +emptyModule nm = + Module + { mName = nm + , mExports = mempty + , mImports = [] + , mSubModules = mempty + + , mParamTypes = mempty + , mParamConstraints = mempty + , mParamFuns = mempty + + , mTySyns = mempty + , mNewtypes = mempty + , mPrimTypes = mempty + , mDecls = mempty + , mFunctors = mempty + } + +type Module = ModuleG ModName + -- | Is this a parameterized module? -isParametrizedModule :: Module -> Bool +isParametrizedModule :: ModuleG mname -> Bool isParametrizedModule m = not (null (mParamTypes m) && null (mParamConstraints m) && null (mParamFuns m)) --- | A type parameter of a module. -data ModTParam = ModTParam - { mtpName :: Name - , mtpKind :: Kind - , mtpNumber :: !Int -- ^ The number of the parameter in the module - -- This is used when we move parameters from the module - -- level to individual declarations - -- (type synonyms in particular) - , mtpDoc :: Maybe Text - } deriving (Show,Generic,NFData) - -mtpParam :: ModTParam -> TParam -mtpParam mtp = TParam { tpUnique = nameUnique (mtpName mtp) - , tpKind = mtpKind mtp - , tpFlav = TPModParam (mtpName mtp) - , tpInfo = desc - } - where desc = TVarInfo { tvarDesc = TVFromModParam (mtpName mtp) - , tvarSource = nameLoc (mtpName mtp) - } - --- | A value parameter of a module. -data ModVParam = ModVParam - { mvpName :: Name - , mvpType :: Schema - , mvpDoc :: Maybe Text - , mvpFixity :: Maybe Fixity - } deriving (Show,Generic,NFData) - data Expr = EList [Expr] Type -- ^ List value (with type of elements) | ETuple [Expr] -- ^ Tuple value @@ -369,10 +373,10 @@ instance PP (WithNames DeclDef) where instance PP Decl where ppPrec = ppWithNamesPrec IntMap.empty -instance PP Module where +instance PP n => PP (ModuleG n) where ppPrec = ppWithNamesPrec IntMap.empty -instance PP (WithNames Module) where +instance PP n => PP (WithNames (ModuleG n)) where ppPrec _ (WithNames Module { .. } nm) = text "module" <+> pp mName $$ -- XXX: Print exports? diff --git a/src/Cryptol/TypeCheck/CheckModuleInstance.hs b/src/Cryptol/TypeCheck/CheckModuleInstance.hs index 37ca8aef0..396deb2f5 100644 --- a/src/Cryptol/TypeCheck/CheckModuleInstance.hs +++ b/src/Cryptol/TypeCheck/CheckModuleInstance.hs @@ -1,3 +1,4 @@ +{-# Language OverloadedStrings #-} module Cryptol.TypeCheck.CheckModuleInstance (checkModuleInstance) where import Data.Map ( Map ) @@ -19,17 +20,24 @@ import Cryptol.Utils.Panic -- | Check that the instance provides what the functor needs. checkModuleInstance :: Module {- ^ type-checked functor -} -> Module {- ^ type-checked instance -} -> - InferM Module -- ^ Instantiated module -checkModuleInstance func inst = + InferM (Name->Name,Module) + -- ^ Renaming,Instantiated module +checkModuleInstance func inst + | not (null (mSubModules func) && null (mSubModules inst)) = + do recordError $ TemporaryError + "Cannot combine nested modules with old-style parameterized modules" + pure (id,func) -- doesn't matter? + | otherwise = do tMap <- checkTyParams func inst vMap <- checkValParams func tMap inst - (ctrs, m) <- instantiateModule func (mName inst) tMap vMap + (ren, ctrs, m) <- instantiateModule func (mName inst) tMap vMap let toG p = Goal { goal = thing p , goalRange = srcRange p , goalSource = CtModuleInstance (mName inst) } addGoals (map toG ctrs) - return Module { mName = mName m + return ( ren + , Module { mName = mName m , mExports = mExports m , mImports = mImports inst ++ mImports m -- Note that this is just here to record @@ -43,7 +51,11 @@ checkModuleInstance func inst = , mParamConstraints = mParamConstraints inst , mParamFuns = mParamFuns inst , mDecls = mDecls inst ++ mDecls m + + , mSubModules = mempty + , mFunctors = mempty } + ) -- | Check that the type parameters of the functors all have appropriate -- definitions. @@ -179,6 +191,7 @@ makeValParamDef x sDef pDef = , P.bPragmas = [] , P.bMono = False , P.bDoc = Nothing + , P.bExport = Public } loc a = P.Located { P.srcRange = nameLoc x, P.thing = a } diff --git a/src/Cryptol/TypeCheck/Depends.hs b/src/Cryptol/TypeCheck/Depends.hs deleted file mode 100644 index fb562c7a3..000000000 --- a/src/Cryptol/TypeCheck/Depends.hs +++ /dev/null @@ -1,214 +0,0 @@ --- | --- Module : Cryptol.TypeCheck.Depends --- Copyright : (c) 2013-2016 Galois, Inc. --- License : BSD3 --- Maintainer : cryptol@galois.com --- Stability : provisional --- Portability : portable - -{-# LANGUAGE Safe #-} -{-# LANGUAGE FlexibleInstances #-} -module Cryptol.TypeCheck.Depends where - -import Cryptol.ModuleSystem.Name (Name) -import qualified Cryptol.Parser.AST as P -import Cryptol.Parser.Position(Range, Located(..), thing) -import Cryptol.Parser.Names (namesB, tnamesT, tnamesC, - boundNamesSet, boundNames) -import Cryptol.TypeCheck.Monad( InferM, getTVars ) -import Cryptol.TypeCheck.Error(Error(..)) -import Cryptol.Utils.Panic(panic) -import Cryptol.Utils.RecordMap(recordElements) - -import Data.List(sortBy, groupBy) -import Data.Function(on) -import Data.Maybe(mapMaybe) -import Data.Graph.SCC(stronglyConnComp) -import Data.Graph (SCC(..)) -import Data.Map (Map) -import qualified Data.Map as Map -import qualified Data.Set as Set -import Data.Text (Text) -import MonadLib (ExceptionT, runExceptionT, raise) - -data TyDecl = - TS (P.TySyn Name) (Maybe Text) -- ^ Type synonym - | NT (P.Newtype Name) (Maybe Text) -- ^ Newtype - | AT (P.ParameterType Name) (Maybe Text) -- ^ Parameter type - | PS (P.PropSyn Name) (Maybe Text) -- ^ Property synonym - | PT (P.PrimType Name) (Maybe Text) -- ^ A primitive/abstract typee - deriving Show - -setDocString :: Maybe Text -> TyDecl -> TyDecl -setDocString x d = - case d of - TS a _ -> TS a x - PS a _ -> PS a x - NT a _ -> NT a x - AT a _ -> AT a x - PT a _ -> PT a x - --- | Check for duplicate and recursive type synonyms. --- Returns the type-synonyms in dependency order. -orderTyDecls :: [TyDecl] -> InferM (Either Error [TyDecl]) -orderTyDecls ts = - do vs <- getTVars - ds <- combine $ map (toMap vs) ts - let ordered = mkScc [ (t,[x],deps) - | (x,(t,deps)) <- Map.toList (Map.map thing ds) ] - runExceptionT (concat `fmap` mapM check ordered) - - where - toMap vs ty@(PT p _) = - let x = P.primTName p - (as,cs) = P.primTCts p - in ( thing x - , x { thing = (ty, Set.toList $ - boundNamesSet vs $ - boundNames (map P.tpName as) $ - Set.unions $ - map tnamesC cs - ) - } - ) - - - toMap _ ty@(AT a _) = - let x = P.ptName a - in ( thing x, x { thing = (ty, []) } ) - - toMap vs ty@(NT (P.Newtype x as fs) _) = - ( thing x - , x { thing = (ty, Set.toList $ - boundNamesSet vs $ - boundNames (map P.tpName as) $ - Set.unions $ - map (tnamesT . snd) (recordElements fs) - ) - } - ) - - toMap vs ty@(TS (P.TySyn x _ as t) _) = - (thing x - , x { thing = (ty, Set.toList $ - boundNamesSet vs $ - boundNames (map P.tpName as) $ - tnamesT t - ) - } - ) - - toMap vs ty@(PS (P.PropSyn x _ as ps) _) = - (thing x - , x { thing = (ty, Set.toList $ - boundNamesSet vs $ - boundNames (map P.tpName as) $ - Set.unions $ - map tnamesC ps - ) - } - ) - getN (TS x _) = thing (P.tsName x) - getN (PS x _) = thing (P.psName x) - getN (NT x _) = thing (P.nName x) - getN (AT x _) = thing (P.ptName x) - getN (PT x _) = thing (P.primTName x) - - check :: SCC TyDecl -> ExceptionT Error InferM [TyDecl] - check (AcyclicSCC x) = return [x] - - -- We don't support any recursion, for now. - -- We could support recursion between newtypes, or newtypes and tysysn. - check (CyclicSCC xs) = raise (RecursiveTypeDecls (map getN xs)) - --- | Associate type signatures with bindings and order bindings by dependency. -orderBinds :: [P.Bind Name] -> [SCC (P.Bind Name)] -orderBinds bs = mkScc [ (b, map thing defs, Set.toList uses) - | b <- bs - , let (defs,uses) = namesB b - ] - -class FromDecl d where - toBind :: d -> Maybe (P.Bind Name) - toParamFun :: d -> Maybe (P.ParameterFun Name) - toParamConstraints :: d -> [P.Located (P.Prop Name)] - toTyDecl :: d -> Maybe TyDecl - isTopDecl :: d -> Bool - -instance FromDecl (P.TopDecl Name) where - toBind (P.Decl x) = toBind (P.tlValue x) - toBind _ = Nothing - - toParamFun (P.DParameterFun d) = Just d - toParamFun _ = Nothing - - toParamConstraints (P.DParameterConstraint xs) = xs - toParamConstraints _ = [] - - toTyDecl (P.DPrimType p) = Just (PT (P.tlValue p) (thing <$> P.tlDoc p)) - toTyDecl (P.DParameterType d) = Just (AT d (P.ptDoc d)) - toTyDecl (P.TDNewtype d) = Just (NT (P.tlValue d) (thing <$> P.tlDoc d)) - toTyDecl (P.Decl x) = setDocString (thing <$> P.tlDoc x) - <$> toTyDecl (P.tlValue x) - toTyDecl _ = Nothing - - isTopDecl _ = True - -instance FromDecl (P.Decl Name) where - toBind (P.DLocated d _) = toBind d - toBind (P.DBind b) = return b - toBind _ = Nothing - - toParamFun _ = Nothing - toParamConstraints _ = [] - - toTyDecl (P.DLocated d _) = toTyDecl d - toTyDecl (P.DType x) = Just (TS x Nothing) - toTyDecl (P.DProp x) = Just (PS x Nothing) - toTyDecl _ = Nothing - - isTopDecl _ = False - -{- | Given a list of declarations, annoted with (i) the names that they -define, and (ii) the names that they use, we compute a list of strongly -connected components of the declarations. The SCCs are in dependency order. -} -mkScc :: [(a,[Name],[Name])] -> [SCC a] -mkScc ents = stronglyConnComp $ zipWith mkGr keys ents - where - keys = [ 0 :: Integer .. ] - - mkGr i (x,_,uses) = (x,i,mapMaybe (`Map.lookup` nodeMap) uses) - - -- Maps names to node ids. - nodeMap = Map.fromList $ concat $ zipWith mkNode keys ents - mkNode i (_,defs,_) = [ (d,i) | d <- defs ] - -{- | Combine a bunch of definitions into a single map. Here we check -that each name is defined only onces. -} -combineMaps :: [Map Name (Located a)] -> InferM (Map Name (Located a)) -combineMaps ms = if null bad then return (Map.unions ms) - else panic "combineMaps" $ "Multiple definitions" - : map show bad - where - bad = do m <- ms - duplicates [ a { thing = x } | (x,a) <- Map.toList m ] - -{- | Combine a bunch of definitions into a single map. Here we check -that each name is defined only onces. -} -combine :: [(Name, Located a)] -> InferM (Map Name (Located a)) -combine m = if null bad then return (Map.fromList m) - else panic "combine" $ "Multiple definitions" - : map show bad - where - bad = duplicates [ a { thing = x } | (x,a) <- m ] - --- | Identify multiple occurances of something. -duplicates :: Ord a => [Located a] -> [(a,[Range])] -duplicates = mapMaybe multiple - . groupBy ((==) `on` thing) - . sortBy (compare `on` thing) - where - multiple xs@(x : _ : _) = Just (thing x, map srcRange xs) - multiple _ = Nothing - - diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index d4139eb09..5b030345b 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -139,6 +139,12 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind | TypeShadowing String Name String | MissingModTParam (Located Ident) | MissingModVParam (Located Ident) + + | TemporaryError Doc + -- ^ This is for errors that don't fit other cateogories. + -- We should not use it much, and is generally to be used + -- for transient errors, which are due to incomplete + -- implementation. deriving (Show, Generic, NFData) -- | When we have multiple errors on the same location, we show only the @@ -147,6 +153,10 @@ errorImportance :: Error -> Int errorImportance err = case err of BareTypeApp -> 11 -- basically a parse error + TemporaryError {} -> 11 + -- show these as usually means the user used something that doesn't work + + KindMismatch {} -> 10 TyVarWithParams {} -> 9 TypeMismatch {} -> 8 @@ -236,6 +246,8 @@ instance TVars Error where MissingModTParam {} -> err MissingModVParam {} -> err + TemporaryError {} -> err + instance FVS Error where fvs err = @@ -269,6 +281,8 @@ instance FVS Error where MissingModTParam {} -> Set.empty MissingModVParam {} -> Set.empty + TemporaryError {} -> Set.empty + instance PP Warning where ppPrec = ppWithNamesPrec IntMap.empty @@ -436,9 +450,7 @@ instance PP (WithNames Error) where MissingModVParam x -> "Missing definition for value parameter" <+> quotes (pp (thing x)) - - - + TemporaryError doc -> doc where bullets xs = vcat [ "•" <+> d | d <- xs ] diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 16e34db3e..95e201c6a 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -13,16 +13,18 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE RecursiveDo #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE BlockArguments #-} {-# LANGUAGE Safe #-} module Cryptol.TypeCheck.Infer ( checkE , checkSigB , inferModule , inferBinds - , inferDs + , checkTopDecls ) where +import Data.Text(Text) import qualified Data.Text as Text @@ -41,7 +43,6 @@ import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn, checkPrimType, checkParameterConstraints) import Cryptol.TypeCheck.Instantiate -import Cryptol.TypeCheck.Depends import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst) import Cryptol.Utils.Ident import Cryptol.Utils.Panic(panic) @@ -50,43 +51,24 @@ import Cryptol.Utils.RecordMap import qualified Data.Map as Map import Data.Map (Map) import qualified Data.Set as Set -import Data.List(foldl',sortBy) +import Data.List(foldl',sortBy,groupBy) import Data.Either(partitionEithers) -import Data.Maybe(mapMaybe,isJust, fromMaybe) +import Data.Maybe(isJust, fromMaybe, mapMaybe) import Data.List(partition) -import Data.Graph(SCC(..)) import Data.Ratio(numerator,denominator) import Data.Traversable(forM) -import Control.Monad(zipWithM,unless,foldM) +import Data.Function(on) +import Control.Monad(zipWithM,unless,foldM,forM_) inferModule :: P.Module Name -> InferM Module inferModule m = - inferDs (P.mDecls m) $ \ds1 -> - do proveModuleTopLevel - ts <- getTSyns - nts <- getNewtypes - ats <- getAbstractTypes - pTs <- getParamTypes - pCs <- getParamConstraints - pFuns <- getParamFuns - return Module { mName = thing (P.mName m) - , mExports = P.modExports m - , mImports = map thing (P.mImports m) - , mTySyns = Map.mapMaybe onlyLocal ts - , mNewtypes = Map.mapMaybe onlyLocal nts - , mPrimTypes = Map.mapMaybe onlyLocal ats - , mParamTypes = pTs - , mParamConstraints = pCs - , mParamFuns = pFuns - , mDecls = ds1 - } - where - onlyLocal (IsLocal, x) = Just x - onlyLocal (IsExternal, _) = Nothing - - + do newModuleScope (thing (P.mName m)) (map thing (P.mImports m)) + (P.modExports m) + checkTopDecls (P.mDecls m) + proveModuleTopLevel + endModule -- | Construct a Prelude primitive in the parsed AST. mkPrim :: String -> InferM (P.Expr Name) @@ -164,9 +146,8 @@ appTys expr ts tGoal = -- Here is an example of why this might be useful: -- f ` { x = T } where type T = ... P.EWhere e ds -> - inferDs ds $ \ds1 -> do e1 <- appTys e ts tGoal - return (EWhere e1 ds1) - -- XXX: Is there a scoping issue here? I think not, but check. + do (e1,ds1) <- checkLocalDecls ds (appTys e ts tGoal) + pure (EWhere e1 ds1) P.ELocated e r -> do e' <- inRange r (appTys e ts tGoal) @@ -349,6 +330,23 @@ checkE expr tGoal = ds <- combineMaps dss e' <- withMonoTypes ds (checkE e (WithSource a TypeOfSeqElement)) return (EComp len a e' mss') + where + -- the renamer should have made these checks already? + combineMaps ms = if null bad + then return (Map.unions ms) + else panic "combineMaps" $ "Multiple definitions" + : map show bad + where + bad = do m <- ms + duplicates [ a { thing = x } | (x,a) <- Map.toList m ] + duplicates = mapMaybe multiple + . groupBy ((==) `on` thing) + . sortBy (compare `on` thing) + where + multiple xs@(x : _ : _) = Just (thing x, map srcRange xs) + multiple _ = Nothing + + P.EAppT e fs -> appTys e (map uncheckedTypeArg fs) tGoal @@ -366,8 +364,8 @@ checkE expr tGoal = return (EIf e1' e2' e3') P.EWhere e ds -> - inferDs ds $ \ds1 -> do e1 <- checkE e tGoal - return (EWhere e1 ds1) + do (e1,ds1) <- checkLocalDecls ds (checkE e tGoal) + pure (EWhere e1 ds1) P.ETyped e t -> do tSig <- checkTypeOfKind t KType @@ -406,7 +404,7 @@ checkRecUpd mb fs tGoal = -- { _ | fs } ~~> \r -> { r | fs } Nothing -> - do r <- newParamName (packIdent "r") + do r <- newParamName NSValue (packIdent "r") let p = P.PVar Located { srcRange = nameLoc r, thing = r } fe = P.EFun P.emptyFunDesc [p] (P.EUpd (Just (P.EVar r)) fs) checkE fe tGoal @@ -432,7 +430,7 @@ checkRecUpd mb fs tGoal = v1 <- checkE v (WithSource (tFun ft ft) src) -- XXX: ^ may be used a different src? d <- newHasGoal s (twsType tGoal) ft - tmp <- newParamName (packIdent "rf") + tmp <- newParamName NSValue (packIdent "rf") let e' = EVar tmp pure $ hasDoSet d e' (EApp v1 (hasDoSelect d e')) `EWhere` @@ -581,10 +579,11 @@ checkHasType inferredType tGoal = checkFun :: - P.FunDesc Name -> [P.Pattern Name] -> P.Expr Name -> TypeWithSource -> InferM Expr + P.FunDesc Name -> [P.Pattern Name] -> + P.Expr Name -> TypeWithSource -> InferM Expr checkFun _ [] e tGoal = checkE e tGoal checkFun (P.FunDesc fun offset) ps e tGoal = - inNewScope $ + inNewScope do let descs = [ TypeOfArg (ArgDescr fun (Just n)) | n <- [ 1 + offset .. ] ] (tys,tRes) <- expectFun fun (length ps) tGoal @@ -965,68 +964,104 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of , dDoc = P.bDoc b } -inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a -inferDs ds continue = either onErr checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds) + +-------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +checkLocalDecls :: [P.Decl Name] -> InferM a -> InferM (a,[DeclGroup]) +checkLocalDecls ds0 k = + do newLocalScope + forM_ ds0 \d -> checkDecl False d Nothing + a <- k + ds <- endLocalScope + pure (a,ds) + + + +checkTopDecls :: [P.TopDecl Name] -> InferM () +checkTopDecls = mapM_ checkTopDecl + where + checkTopDecl decl = + case decl of + P.Decl tl -> checkDecl True (P.tlValue tl) (thing <$> P.tlDoc tl) + + P.TDNewtype tl -> + do t <- checkNewtype (P.tlValue tl) (thing <$> P.tlDoc tl) + addNewtype t + + P.DPrimType tl -> + do t <- checkPrimType (P.tlValue tl) (thing <$> P.tlDoc tl) + addPrimType t + + P.DParameterType ty -> + do t <- checkParameterType ty (P.ptDoc ty) + addParamType t + + P.DParameterConstraint cs -> + do cs1 <- checkParameterConstraints cs + addParameterConstraints cs1 + + P.DParameterFun pf -> + do x <- checkParameterFun pf + addParamFun x + + P.DModule tl -> + do let P.NestedModule m = P.tlValue tl + newSubmoduleScope (thing (P.mName m)) (map thing (P.mImports m)) + (P.modExports m) + checkTopDecls (P.mDecls m) + endSubmodule + + P.DImport {} -> pure () + P.Include {} -> panic "checkTopDecl" [ "Unexpected `inlude`" ] + + +checkDecl :: Bool -> P.Decl Name -> Maybe Text -> InferM () +checkDecl isTopLevel d mbDoc = + case d of + + P.DBind c -> + do ~[b] <- inferBinds isTopLevel False [c] + addDecls (NonRecursive b) + + P.DRec bs -> + do bs1 <- inferBinds isTopLevel True bs + addDecls (Recursive bs1) + + P.DType t -> + do t1 <- checkTySyn t mbDoc + addTySyn t1 + + P.DProp t -> + do t1 <- checkPropSyn t mbDoc + addTySyn t1 + + P.DLocated d' r -> inRange r (checkDecl isTopLevel d' mbDoc) + + P.DSignature {} -> bad "DSignature" + P.DFixity {} -> bad "DFixity" + P.DPragma {} -> bad "DPragma" + P.DPatBind {} -> bad "DPatBind" + where - onErr err = recordError err >> continue [] - - isTopLevel = isTopDecl (head ds) - - checkTyDecls (AT t mbD : ts) = - do t1 <- checkParameterType t mbD - withParamType t1 (checkTyDecls ts) - - checkTyDecls (TS t mbD : ts) = - do t1 <- checkTySyn t mbD - withTySyn t1 (checkTyDecls ts) - - checkTyDecls (PS t mbD : ts) = - do t1 <- checkPropSyn t mbD - withTySyn t1 (checkTyDecls ts) - - checkTyDecls (NT t mbD : ts) = - do t1 <- checkNewtype t mbD - withNewtype t1 (checkTyDecls ts) - - checkTyDecls (PT p mbD : ts) = - do p1 <- checkPrimType p mbD - withPrimType p1 (checkTyDecls ts) - - -- We checked all type synonyms, now continue with value-level definitions: - checkTyDecls [] = - do cs <- checkParameterConstraints (concatMap toParamConstraints ds) - withParameterConstraints cs $ - do xs <- mapM checkParameterFun (mapMaybe toParamFun ds) - withParamFuns xs $ checkBinds [] $ orderBinds $ mapMaybe toBind ds - - - checkParameterFun x = - do (s,gs) <- checkSchema NoWildCards (P.pfSchema x) - su <- proveImplication (Just (thing (P.pfName x))) - (sVars s) (sProps s) gs - unless (isEmptySubst su) $ - panic "checkParameterFun" ["Subst not empty??"] - let n = thing (P.pfName x) - return ModVParam { mvpName = n - , mvpType = s - , mvpDoc = P.pfDoc x - , mvpFixity = P.pfFixity x - } - - checkBinds decls (CyclicSCC bs : more) = - do bs1 <- inferBinds isTopLevel True bs - foldr (\b m -> withVar (dName b) (dSignature b) m) - (checkBinds (Recursive bs1 : decls) more) - bs1 - - checkBinds decls (AcyclicSCC c : more) = - do ~[b] <- inferBinds isTopLevel False [c] - withVar (dName b) (dSignature b) $ - checkBinds (NonRecursive b : decls) more - - -- We are done with all value-level definitions. - -- Now continue with anything that's in scope of the declarations. - checkBinds decls [] = continue (reverse decls) + bad x = panic "checkDecl" [x] + + +checkParameterFun :: P.ParameterFun Name -> InferM ModVParam +checkParameterFun x = + do (s,gs) <- checkSchema NoWildCards (P.pfSchema x) + su <- proveImplication (Just (thing (P.pfName x))) + (sVars s) (sProps s) gs + unless (isEmptySubst su) $ + panic "checkParameterFun" ["Subst not empty??"] + let n = thing (P.pfName x) + return ModVParam { mvpName = n + , mvpType = s + , mvpDoc = P.pfDoc x + , mvpFixity = P.pfFixity x + } + + tcPanic :: String -> [String] -> a tcPanic l msg = panic ("[TypeCheck] " ++ l) msg diff --git a/src/Cryptol/TypeCheck/Interface.hs b/src/Cryptol/TypeCheck/Interface.hs new file mode 100644 index 000000000..372e936fa --- /dev/null +++ b/src/Cryptol/TypeCheck/Interface.hs @@ -0,0 +1,73 @@ +module Cryptol.TypeCheck.Interface where + +import qualified Data.Map as Map + +import Cryptol.Utils.Ident(Namespace(..)) +import Cryptol.ModuleSystem.Interface +import Cryptol.TypeCheck.AST + + +mkIfaceDecl :: Decl -> IfaceDecl +mkIfaceDecl d = IfaceDecl + { ifDeclName = dName d + , ifDeclSig = dSignature d + , ifDeclPragmas = dPragmas d + , ifDeclInfix = dInfix d + , ifDeclFixity = dFixity d + , ifDeclDoc = dDoc d + } + +-- | Generate an Iface from a typechecked module. +genIface :: ModuleG mname -> IfaceG mname +genIface m = Iface + { ifModName = mName m + + , ifPublic = IfaceDecls + { ifTySyns = tsPub + , ifNewtypes = ntPub + , ifAbstractTypes = atPub + , ifDecls = dPub + , ifModules = mPub + } + + , ifPrivate = IfaceDecls + { ifTySyns = tsPriv + , ifNewtypes = ntPriv + , ifAbstractTypes = atPriv + , ifDecls = dPriv + , ifModules = mPriv + } + + , ifParams = IfaceParams + { ifParamTypes = mParamTypes m + , ifParamConstraints = mParamConstraints m + , ifParamFuns = mParamFuns m + } + } + where + + (tsPub,tsPriv) = + Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m ) + (mTySyns m) + (ntPub,ntPriv) = + Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m ) + (mNewtypes m) + + (atPub,atPriv) = + Map.partitionWithKey (\qn _ -> qn `isExportedType` mExports m) + (mPrimTypes m) + + (dPub,dPriv) = + Map.partitionWithKey (\ qn _ -> qn `isExportedBind` mExports m) + $ Map.fromList [ (qn,mkIfaceDecl d) | dg <- mDecls m + , d <- groupDecls dg + , let qn = dName d + ] + + (mPub,mPriv) = + Map.partitionWithKey (\ qn _ -> isExported NSModule qn (mExports m)) + $ mSubModules m + + + + diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 5ce035be5..3e129f405 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -13,11 +13,30 @@ {-# LANGUAGE RecursiveDo #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE BlockArguments #-} module Cryptol.TypeCheck.Monad ( module Cryptol.TypeCheck.Monad , module Cryptol.TypeCheck.InferTypes ) where +import qualified Control.Applicative as A +import qualified Control.Monad.Fail as Fail +import Control.Monad.Fix(MonadFix(..)) +import qualified Data.Map as Map +import qualified Data.Set as Set +import Data.Map (Map) +import Data.Set (Set) +import Data.List(find, foldl') +import Data.List.NonEmpty(NonEmpty((:|))) +import Data.Semigroup(sconcat) +import Data.Maybe(mapMaybe,fromMaybe) +import Data.IORef + +import GHC.Generics (Generic) +import Control.DeepSeq + +import MonadLib hiding (mapM) + import Cryptol.ModuleSystem.Name (FreshM(..),Supply,mkParameter , nameInfo, NameInfo(..),NameSource(..)) @@ -25,6 +44,7 @@ import Cryptol.Parser.Position import qualified Cryptol.Parser.AST as P import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst +import Cryptol.TypeCheck.Interface(genIface) import Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..)) import Cryptol.TypeCheck.InferTypes import Cryptol.TypeCheck.Error( Warning(..),Error(..) @@ -34,26 +54,9 @@ import qualified Cryptol.TypeCheck.SimpleSolver as Simple import qualified Cryptol.TypeCheck.Solver.SMT as SMT import Cryptol.TypeCheck.PP(NameMap) import Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets) -import Cryptol.Utils.Ident(Ident) +import Cryptol.Utils.Ident(Ident,Namespace(..)) import Cryptol.Utils.Panic(panic) -import qualified Control.Applicative as A -import qualified Control.Monad.Fail as Fail -import Control.Monad.Fix(MonadFix(..)) -import qualified Data.Map as Map -import qualified Data.Set as Set -import Data.Map (Map) -import Data.Set (Set) -import Data.List(find, foldl') -import Data.Maybe(mapMaybe,fromMaybe) -import MonadLib hiding (mapM) - -import Data.IORef - - -import GHC.Generics (Generic) -import Control.DeepSeq - -- | Information needed for type inference. data InferInput = InferInput { inpRange :: Range -- ^ Location of program source @@ -118,16 +121,21 @@ bumpCounter = do RO { .. } <- IM ask runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a) runInferM info (IM m) = do counter <- newIORef 0 + let env = Map.map ExtVar (inpVars info) + <> Map.map (ExtVar . newtypeConType) (inpNewtypes info) + rec ro <- return RO { iRange = inpRange info - , iVars = Map.map ExtVar (inpVars info) - , iTVars = [] - , iTSyns = fmap mkExternal (inpTSyns info) - , iNewtypes = fmap mkExternal (inpNewtypes info) - , iAbstractTypes = mkExternal <$> inpAbstractTypes info - , iParamTypes = inpParamTypes info - , iParamFuns = inpParamFuns info - , iParamConstraints = inpParamConstraints info + , iVars = env + , iExtScope = (emptyModule ExternalScope) + { mTySyns = inpTSyns info + , mNewtypes = inpNewtypes info + , mPrimTypes = inpAbstractTypes info + , mParamTypes = inpParamTypes info + , mParamFuns = inpParamFuns info + , mParamConstraints = inpParamConstraints info + } + , iTVars = [] , iSolvedHasLazy = iSolvedHas finalRW -- RECURSION , iMonoBinds = inpMonoBinds info , iCallStacks = inpCallStacks info @@ -167,7 +175,6 @@ runInferM info (IM m) = in pure (InferFailed (computeFreeVarNames ws es1) ws es1) - mkExternal x = (IsExternal, x) rw = RW { iErrors = [] , iWarnings = [] , iSubst = emptySubst @@ -180,6 +187,9 @@ runInferM info (IM m) = , iSolvedHas = Map.empty , iSupply = inpSupply info + + , iScope = [] + , iBindTypes = mempty } @@ -190,38 +200,31 @@ runInferM info (IM m) = newtype InferM a = IM { unIM :: ReaderT RO (StateT RW IO) a } -data DefLoc = IsLocal | IsExternal + +data ScopeName = ExternalScope + | LocalScope + | SubModule Name + | MTopModule P.ModName -- | Read-only component of the monad. data RO = RO - { iRange :: Range -- ^ Source code being analysed - , iVars :: Map Name VarType -- ^ Type of variable that are in scope - - {- NOTE: We assume no shadowing between these two, so it does not matter - where we look first. Similarly, we assume no shadowing with - the existential type variable (in RW). See 'checkTShadowing'. -} - - , iTVars :: [TParam] -- ^ Type variable that are in scope - , iTSyns :: Map Name (DefLoc, TySyn) -- ^ Type synonyms that are in scope - , iNewtypes :: Map Name (DefLoc, Newtype) - -- ^ Newtype declarations in scope - -- - -- NOTE: type synonyms take precedence over newtype. The reason is - -- that we can define local type synonyms, but not local newtypes. - -- So, either a type-synonym shadows a newtype, or it was declared - -- at the top-level, but then there can't be a newtype with the - -- same name (this should be caught by the renamer). - , iAbstractTypes :: Map Name (DefLoc, AbstractType) + { iRange :: Range -- ^ Source code being analysed + , iVars :: Map Name VarType + -- ^ Type of variable that are in scope + -- These are only parameters vars that are in recursive component we + -- are checking at the moment. If a var is not there, keep looking in + -- the 'iScope' - , iParamTypes :: Map Name ModTParam - -- ^ Parameter types - , iParamConstraints :: [Located Prop] - -- ^ Constraints on the type parameters + , iTVars :: [TParam] -- ^ Type variable that are in scope - , iParamFuns :: Map Name ModVParam - -- ^ Parameter functions + , iExtScope :: ModuleG ScopeName + -- ^ These are things we know about, but are not part of the + -- modules we are currently constructing. + -- XXX: this sould probably be an interface + -- ^ Information about top-level declarations in modules under + -- construction, most nested first. , iSolvedHasLazy :: Map Int HasGoalSln -- ^ NOTE: This field is lazy in an important way! It is the @@ -277,9 +280,17 @@ data RW = RW {- ^ Tuple/record projection constraints. The 'Int' is the "name" of the constraint, used so that we can name its solution properly. -} + , iScope :: ![ModuleG ScopeName] + -- ^ Nested scopes we are currently checking, most nested first. + + , iBindTypes :: !(Map Name Schema) + -- ^ Types of variables that we know about. We don't worry about scoping + -- here because we assume the bindings all have different names. + , iSupply :: !Supply } + instance Functor InferM where fmap f (IM m) = IM (fmap f m) @@ -451,10 +462,10 @@ solveHasGoal n e = -------------------------------------------------------------------------------- -- | Generate a fresh variable name to be used in a local binding. -newParamName :: Ident -> InferM Name -newParamName x = +newParamName :: Namespace -> Ident -> InferM Name +newParamName ns x = do r <- curRange - liftSupply (mkParameter x r) + liftSupply (mkParameter ns x r) newName :: (NameSeeds -> (a , NameSeeds)) -> InferM a newName upd = IM $ sets $ \s -> let (x,seeds) = upd (iNameSeeds s) @@ -633,17 +644,13 @@ lookupVar :: Name -> InferM VarType lookupVar x = do mb <- IM $ asks $ Map.lookup x . iVars case mb of - Just t -> return t + Just a -> pure a Nothing -> - do mbNT <- lookupNewtype x - case mbNT of - Just nt -> return (ExtVar (newtypeConType nt)) - Nothing -> - do mbParamFun <- lookupParamFun x - case mbParamFun of - Just pf -> return (ExtVar (mvpType pf)) - Nothing -> panic "lookupVar" [ "Undefined type variable" - , show x] + do mb1 <- Map.lookup x . iBindTypes <$> IM get + case mb1 of + Just a -> pure (ExtVar a) + Nothing -> panic "lookupVar" [ "Undefined vairable" + , show x ] -- | Lookup a type variable. Return `Nothing` if there is no such variable -- in scope, in which case we must be dealing with a type constant. @@ -653,14 +660,14 @@ lookupTParam x = IM $ asks $ find this . iTVars -- | Lookup the definition of a type synonym. lookupTSyn :: Name -> InferM (Maybe TySyn) -lookupTSyn x = fmap (fmap snd . Map.lookup x) getTSyns +lookupTSyn x = Map.lookup x <$> getTSyns -- | Lookup the definition of a newtype lookupNewtype :: Name -> InferM (Maybe Newtype) -lookupNewtype x = fmap (fmap snd . Map.lookup x) getNewtypes +lookupNewtype x = Map.lookup x <$> getNewtypes lookupAbstractType :: Name -> InferM (Maybe AbstractType) -lookupAbstractType x = fmap (fmap snd . Map.lookup x) getAbstractTypes +lookupAbstractType x = Map.lookup x <$> getAbstractTypes -- | Lookup the kind of a parameter type lookupParamType :: Name -> InferM (Maybe ModTParam) @@ -692,28 +699,28 @@ existVar x k = -- | Returns the type synonyms that are currently in scope. -getTSyns :: InferM (Map Name (DefLoc,TySyn)) -getTSyns = IM $ asks iTSyns +getTSyns :: InferM (Map Name TySyn) +getTSyns = getScope mTySyns -- | Returns the newtype declarations that are in scope. -getNewtypes :: InferM (Map Name (DefLoc,Newtype)) -getNewtypes = IM $ asks iNewtypes +getNewtypes :: InferM (Map Name Newtype) +getNewtypes = getScope mNewtypes -- | Returns the abstract type declarations that are in scope. -getAbstractTypes :: InferM (Map Name (DefLoc,AbstractType)) -getAbstractTypes = IM $ asks iAbstractTypes +getAbstractTypes :: InferM (Map Name AbstractType) +getAbstractTypes = getScope mPrimTypes -- | Returns the parameter functions declarations getParamFuns :: InferM (Map Name ModVParam) -getParamFuns = IM $ asks iParamFuns +getParamFuns = getScope mParamFuns -- | Returns the abstract function declarations getParamTypes :: InferM (Map Name ModTParam) -getParamTypes = IM $ asks iParamTypes +getParamTypes = getScope mParamTypes -- | Constraints on the module's parameters. getParamConstraints :: InferM [Located Prop] -getParamConstraints = IM $ asks iParamConstraints +getParamConstraints = getScope mParamConstraints -- | Get the set of bound type variables that are in scope. getTVars :: InferM (Set Name) @@ -723,8 +730,8 @@ getTVars = IM $ asks $ Set.fromList . mapMaybe tpName . iTVars getBoundInScope :: InferM (Set TParam) getBoundInScope = do ro <- IM ask - let params = Set.fromList (map mtpParam (Map.elems (iParamTypes ro))) - bound = Set.fromList (iTVars ro) + params <- Set.fromList . map mtpParam . Map.elems <$> getParamTypes + let bound = Set.fromList (iTVars ro) return $! Set.union params bound -- | Retrieve the value of the `mono-binds` option. @@ -739,12 +746,14 @@ because it is confusing. As a bonus, in the implementation we don't need to worry about where we lookup things (i.e., in the variable or type synonym environment. -} +-- XXX: this should be done in renamer checkTShadowing :: String -> Name -> InferM () checkTShadowing this new = - do ro <- IM ask + do tsyns <- getTSyns + ro <- IM ask rw <- IM get let shadowed = - do _ <- Map.lookup new (iTSyns ro) + do _ <- Map.lookup new tsyns return "type synonym" `mplus` do guard (new `elem` mapMaybe tpName (iTVars ro)) @@ -759,7 +768,6 @@ checkTShadowing this new = recordError (TypeShadowing this new that) - -- | The sub-computation is performed with the given type parameter in scope. withTParam :: TParam -> InferM a -> InferM a withTParam p (IM m) = @@ -771,31 +779,148 @@ withTParam p (IM m) = withTParams :: [TParam] -> InferM a -> InferM a withTParams ps m = foldr withTParam m ps + +-- | Execute the given computation in a new top scope. +-- The sub-computation would typically be validating a module. +newScope :: ScopeName -> InferM () +newScope nm = IM $ sets_ \rw -> rw { iScope = emptyModule nm : iScope rw } + +newLocalScope :: InferM () +newLocalScope = newScope LocalScope + +newSubmoduleScope :: Name -> [Import] -> ExportSpec Name -> InferM () +newSubmoduleScope x is e = + do newScope (SubModule x) + updScope \m -> m { mImports = is, mExports = e } + +newModuleScope :: P.ModName -> [Import] -> ExportSpec Name -> InferM () +newModuleScope x is e = + do newScope (MTopModule x) + updScope \m -> m { mImports = is, mExports = e } + +-- | Update the current scope (first in the list). Assumes there is one. +updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM () +updScope f = IM $ sets_ \rw -> rw { iScope = upd (iScope rw) } + where + upd r = + case r of + [] -> panic "updTopScope" [ "No top scope" ] + s : more -> f s : more + +endLocalScope :: InferM [DeclGroup] +endLocalScope = + IM $ sets \rw -> + case iScope rw of + x : xs | LocalScope <- mName x -> + (reverse (mDecls x), rw { iScope = xs }) + -- ^ This ignores local type synonyms... Where should we put them? + + _ -> panic "endLocalScope" ["Missing local scope"] + +endSubmodule :: InferM () +endSubmodule = + IM $ sets_ \rw -> + case iScope rw of + x@Module { mName = SubModule m } : y : more -> rw { iScope = z : more } + where + x1 = x { mName = m } + iface = genIface x1 + me = if isParametrizedModule x1 then Map.singleton m x1 else mempty + z = y { mImports = mImports x ++ mImports y -- just for deps + , mSubModules = Map.insert m iface (mSubModules y) + + , mTySyns = mTySyns x <> mTySyns y + , mNewtypes = mNewtypes x <> mNewtypes y + , mPrimTypes = mPrimTypes x <> mPrimTypes y + , mDecls = mDecls x <> mDecls y + , mFunctors = me <> mFunctors x <> mFunctors y + } + + _ -> panic "endSubmodule" [ "Not a submodule" ] + + +endModule :: InferM Module +endModule = + IM $ sets \rw -> + case iScope rw of + [ x ] | MTopModule m <- mName x -> + ( x { mName = m, mDecls = reverse (mDecls x) } + , rw { iScope = [] } + ) + _ -> panic "endModule" [ "Not a single top module" ] + +endModuleInstance :: InferM () +endModuleInstance = + IM $ sets_ \rw -> + case iScope rw of + [ x ] | MTopModule _ <- mName x -> rw { iScope = [] } + _ -> panic "endModuleInstance" [ "Not single top module" ] + + +-- | Get an environment combining all nested scopes. +getScope :: Semigroup a => (ModuleG ScopeName -> a) -> InferM a +getScope f = + do ro <- IM ask + rw <- IM get + pure (sconcat (f (iExtScope ro) :| map f (iScope rw))) + +addDecls :: DeclGroup -> InferM () +addDecls ds = + do updScope \r -> r { mDecls = ds : mDecls r } + IM $ sets_ \rw -> rw { iBindTypes = new rw } + where + add d = Map.insert (dName d) (dSignature d) + new rw = foldr add (iBindTypes rw) (groupDecls ds) + -- | The sub-computation is performed with the given type-synonym in scope. -withTySyn :: TySyn -> InferM a -> InferM a -withTySyn t (IM m) = +addTySyn :: TySyn -> InferM () +addTySyn t = do let x = tsName t checkTShadowing "synonym" x - IM $ mapReader (\r -> r { iTSyns = Map.insert x (IsLocal,t) (iTSyns r) }) m + updScope \r -> r { mTySyns = Map.insert x t (mTySyns r) } + +addNewtype :: Newtype -> InferM () +addNewtype t = + do updScope \r -> r { mNewtypes = Map.insert (ntName t) t (mNewtypes r) } + IM $ sets_ \rw -> rw { iBindTypes = Map.insert (ntName t) + (newtypeConType t) + (iBindTypes rw) } + +addPrimType :: AbstractType -> InferM () +addPrimType t = + updScope \r -> + r { mPrimTypes = Map.insert (atName t) t (mPrimTypes r) } + +addParamType :: ModTParam -> InferM () +addParamType a = + updScope \r -> r { mParamTypes = Map.insert (mtpName a) a (mParamTypes r) } -withNewtype :: Newtype -> InferM a -> InferM a -withNewtype t (IM m) = - IM $ mapReader - (\r -> r { iNewtypes = Map.insert (ntName t) (IsLocal,t) - (iNewtypes r) }) m +-- | The sub-computation is performed with the given abstract function in scope. +addParamFun :: ModVParam -> InferM () +addParamFun x = + do updScope \r -> r { mParamFuns = Map.insert (mvpName x) x (mParamFuns r) } + IM $ sets_ \rw -> rw { iBindTypes = Map.insert (mvpName x) (mvpType x) + (iBindTypes rw) } + +-- | Add some assumptions for an entire module +addParameterConstraints :: [Located Prop] -> InferM () +addParameterConstraints ps = + updScope \r -> r { mParamConstraints = ps ++ mParamConstraints r } -withPrimType :: AbstractType -> InferM a -> InferM a -withPrimType t (IM m) = - IM $ mapReader - (\r -> r { iAbstractTypes = Map.insert (atName t) (IsLocal,t) - (iAbstractTypes r) }) m -withParamType :: ModTParam -> InferM a -> InferM a -withParamType a (IM m) = - IM $ mapReader - (\r -> r { iParamTypes = Map.insert (mtpName a) a (iParamTypes r) }) - m + +-- | Perform the given computation in a new scope (i.e., the subcomputation +-- may use existential type variables). This is a different kind of scope +-- from the nested modules one. +inNewScope :: InferM a -> InferM a +inNewScope m = + do curScopes <- iExistTVars <$> IM get + IM $ sets_ $ \s -> s { iExistTVars = Map.empty : curScopes } + a <- m + IM $ sets_ $ \s -> s { iExistTVars = curScopes } + return a + -- | The sub-computation is performed with the given variable in scope. withVarType :: Name -> VarType -> InferM a -> InferM a @@ -808,19 +933,6 @@ withVarTypes xs m = foldr (uncurry withVarType) m xs withVar :: Name -> Schema -> InferM a -> InferM a withVar x s = withVarType x (ExtVar s) --- | The sub-computation is performed with the given abstract function in scope. -withParamFuns :: [ModVParam] -> InferM a -> InferM a -withParamFuns xs (IM m) = - IM $ mapReader (\r -> r { iParamFuns = foldr add (iParamFuns r) xs }) m - where - add x = Map.insert (mvpName x) x - --- | Add some assumptions for an entire module -withParameterConstraints :: [Located Prop] -> InferM a -> InferM a -withParameterConstraints ps (IM m) = - IM $ mapReader (\r -> r { iParamConstraints = ps ++ iParamConstraints r }) m - - -- | The sub-computation is performed with the given variables in scope. withMonoType :: (Name,Located Type) -> InferM a -> InferM a withMonoType (x,lt) = withVar x (Forall [] [] (thing lt)) @@ -829,25 +941,6 @@ withMonoType (x,lt) = withVar x (Forall [] [] (thing lt)) withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a withMonoTypes xs m = foldr withMonoType m (Map.toList xs) --- | The sub-computation is performed with the given type synonyms --- and variables in scope. -withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a -withDecls (ts,vs) m = foldr withTySyn (foldr add m (Map.toList vs)) ts - where - add (x,t) = withVar x t - --- | Perform the given computation in a new scope (i.e., the subcomputation --- may use existential type variables). -inNewScope :: InferM a -> InferM a -inNewScope m = - do curScopes <- iExistTVars <$> IM get - IM $ sets_ $ \s -> s { iExistTVars = Map.empty : curScopes } - a <- m - IM $ sets_ $ \s -> s { iExistTVars = curScopes } - return a - - - -------------------------------------------------------------------------------- -- Kind checking diff --git a/src/Cryptol/TypeCheck/Solver/Selector.hs b/src/Cryptol/TypeCheck/Solver/Selector.hs index 83a4be4e3..7b9492e9c 100644 --- a/src/Cryptol/TypeCheck/Solver/Selector.hs +++ b/src/Cryptol/TypeCheck/Solver/Selector.hs @@ -15,7 +15,7 @@ import Cryptol.TypeCheck.Monad( InferM, unify, newGoals , newParamName ) import Cryptol.TypeCheck.Subst (listParamSubst, apSubst) -import Cryptol.Utils.Ident (Ident, packIdent) +import Cryptol.Utils.Ident (Ident, packIdent,Namespace(..)) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap @@ -163,9 +163,9 @@ mkSelSln s outerT innerT = -- xs.s ~~> [ x.s | x <- xs ] -- { xs | s = ys } ~~> [ { x | s = y } | x <- xs | y <- ys ] liftSeq len el = - do x1 <- newParamName (packIdent "x") - x2 <- newParamName (packIdent "x") - y2 <- newParamName (packIdent "y") + do x1 <- newParamName NSValue (packIdent "x") + x2 <- newParamName NSValue (packIdent "x") + y2 <- newParamName NSValue (packIdent "y") case tNoUser innerT of TCon _ [_,eli] -> do d <- mkSelSln s el eli @@ -187,8 +187,8 @@ mkSelSln s outerT innerT = -- f.s ~~> \x -> (f x).s -- { f | s = g } ~~> \x -> { f x | s = g x } liftFun t1 t2 = - do x1 <- newParamName (packIdent "x") - x2 <- newParamName (packIdent "x") + do x1 <- newParamName NSValue (packIdent "x") + x2 <- newParamName NSValue (packIdent "x") case tNoUser innerT of TCon _ [_,inT] -> do d <- mkSelSln s t2 inT diff --git a/src/Cryptol/TypeCheck/TCon.hs b/src/Cryptol/TypeCheck/TCon.hs index 351ba68ec..f4a8df4e9 100644 --- a/src/Cryptol/TypeCheck/TCon.hs +++ b/src/Cryptol/TypeCheck/TCon.hs @@ -41,9 +41,9 @@ builtInType :: M.Name -> Maybe TCon builtInType nm = case M.nameInfo nm of M.Declared m _ - | m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes - | m == floatName -> Map.lookup (M.nameIdent nm) builtInFloat - | m == arrayName -> Map.lookup (M.nameIdent nm) builtInArray + | m == M.TopModule preludeName -> Map.lookup (M.nameIdent nm) builtInTypes + | m == M.TopModule floatName -> Map.lookup (M.nameIdent nm) builtInFloat + | m == M.TopModule arrayName -> Map.lookup (M.nameIdent nm) builtInArray _ -> Nothing where diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 6d2c94460..6cd396541 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -2,6 +2,11 @@ {-# Language FlexibleInstances, FlexibleContexts #-} {-# Language PatternGuards #-} {-# Language OverloadedStrings #-} +{-| This module contains types related to typechecking and the output of the +typechecker. In particular, it should contain the types needed by +interface files (see 'Crytpol.ModuleSystem.Interface'), which are (kind of) +the output of the typechker. +-} module Cryptol.TypeCheck.Type ( module Cryptol.TypeCheck.Type , module Cryptol.TypeCheck.TCon @@ -32,6 +37,38 @@ import Prelude infix 4 =#=, >== infixr 5 `tFun` +-- | A type parameter of a module. +data ModTParam = ModTParam + { mtpName :: Name + , mtpKind :: Kind + , mtpNumber :: !Int -- ^ The number of the parameter in the module + -- This is used when we move parameters from the module + -- level to individual declarations + -- (type synonyms in particular) + , mtpDoc :: Maybe Text + } deriving (Show,Generic,NFData) + + +mtpParam :: ModTParam -> TParam +mtpParam mtp = TParam { tpUnique = nameUnique (mtpName mtp) + , tpKind = mtpKind mtp + , tpFlav = TPModParam (mtpName mtp) + , tpInfo = desc + } + where desc = TVarInfo { tvarDesc = TVFromModParam (mtpName mtp) + , tvarSource = nameLoc (mtpName mtp) + } + +-- | A value parameter of a module. +data ModVParam = ModVParam + { mvpName :: Name + , mvpType :: Schema + , mvpDoc :: Maybe Text + , mvpFixity :: Maybe Fixity + } deriving (Show,Generic,NFData) + + + -- | The types of polymorphic values. @@ -957,9 +994,8 @@ instance PP (WithNames Type) where TUser c ts t -> withNameDisp $ \disp -> - case nameInfo c of - Declared m _ - | NotInScope <- getNameFormat m (nameIdent c) disp -> + case asOrigName c of + Just og | NotInScope <- getNameFormat og disp -> go prec t -- unfold type synonym if not in scope _ -> case ts of @@ -1076,7 +1112,7 @@ pickTVarName k src uni = TypeParamInstPos f n -> mk (sh f ++ "_" ++ show n) DefinitionOf x -> case nameInfo x of - Declared m SystemName | m == exprModName -> mk "it" + Declared m SystemName | m == TopModule exprModName -> mk "it" _ -> using x LenOfCompGen -> mk "n" GeneratorOfListComp -> "seq" diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index b573ecc32..47134016b 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -7,10 +7,16 @@ -- Portability : portable {-# LANGUAGE DeriveGeneric, OverloadedStrings #-} +{-# LANGUAGE DeriveAnyClass #-} module Cryptol.Utils.Ident ( -- * Module names - ModName + ModPath(..) + , apPathRoot + , modPathCommon + , topModuleFor + + , ModName , modNameToText , textToModName , modNameChunks @@ -41,6 +47,13 @@ module Cryptol.Utils.Ident , identText , modParamIdent + -- * Namespaces + , Namespace(..) + , allNamespaces + + -- * Original names + , OrigName(..) + -- * Identifiers for primitives , PrimIdent(..) , prelPrim @@ -58,7 +71,64 @@ import Data.String (IsString(..)) import GHC.Generics (Generic) --- | Module names are just text. +-------------------------------------------------------------------------------- + +-- | Namespaces for names +data Namespace = NSValue | NSType | NSModule + deriving (Generic,Show,NFData,Eq,Ord,Enum,Bounded) + +allNamespaces :: [Namespace] +allNamespaces = [ minBound .. maxBound ] + +-- | Idnetifies a possibly nested module +data ModPath = TopModule ModName + | Nested ModPath Ident + deriving (Eq,Ord,Show,Generic,NFData) + +apPathRoot :: (ModName -> ModName) -> ModPath -> ModPath +apPathRoot f path = + case path of + TopModule m -> TopModule (f m) + Nested p q -> Nested (apPathRoot f p) q + +topModuleFor :: ModPath -> ModName +topModuleFor m = + case m of + TopModule x -> x + Nested p _ -> topModuleFor p + +-- | Compute a common prefix between two module paths, if any. +-- This is basically "anti-unification" of the two paths, where we +-- compute the longest common prefix, and the remaining differences for +-- each module. +modPathCommon :: ModPath -> ModPath -> Maybe (ModPath, [Ident], [Ident]) +modPathCommon p1 p2 + | top1 == top2 = Just (findCommon (TopModule top1) as bs) + | otherwise = Nothing + where + (top1,as) = modPathSplit p1 + (top2,bs) = modPathSplit p2 + + findCommon com xs ys = + case (xs,ys) of + (x:xs',y:ys') | x == y -> findCommon (Nested com x) xs' ys' + _ -> (com, xs, ys) + +modPathSplit :: ModPath -> (ModName, [Ident]) +modPathSplit p0 = (top,reverse xs) + where + (top,xs) = go p0 + go p = + case p of + TopModule a -> (a, []) + Nested b i -> (a, i:bs) + where (a,bs) = go b + + + + +-------------------------------------------------------------------------------- +-- | Top-level Module names are just text. data ModName = ModName T.Text deriving (Eq,Ord,Show,Generic) @@ -137,6 +207,15 @@ exprModName :: ModName exprModName = packModName [""] +-------------------------------------------------------------------------------- +-- | Identifies an entitiy +data OrigName = OrigName + { ogNamespace :: Namespace + , ogModule :: ModPath + , ogName :: Ident + } deriving (Eq,Ord,Show,Generic,NFData) + + -------------------------------------------------------------------------------- -- | Identifiers, along with a flag that indicates whether or not they're infix diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs index 3d8050684..ba197c5a3 100644 --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -66,14 +66,14 @@ Getting a value of 'Nothing' from the NameDisp function indicates that the display has no opinion on how this name should be displayed, and some other display should be tried out. -} data NameDisp = EmptyNameDisp - | NameDisp (ModName -> Ident -> Maybe NameFormat) + | NameDisp (OrigName -> Maybe NameFormat) deriving (Generic, NFData) instance Show NameDisp where show _ = "" instance S.Semigroup NameDisp where - NameDisp f <> NameDisp g = NameDisp (\m n -> f m n `mplus` g m n) + NameDisp f <> NameDisp g = NameDisp (\n -> f n `mplus` g n) EmptyNameDisp <> EmptyNameDisp = EmptyNameDisp EmptyNameDisp <> x = x x <> _ = x @@ -88,21 +88,13 @@ data NameFormat = UnQualified deriving (Show) -- | Never qualify names from this module. -neverQualifyMod :: ModName -> NameDisp -neverQualifyMod mn = NameDisp $ \ mn' _ -> - if mn == mn' then Just UnQualified - else Nothing - -alwaysQualify :: NameDisp -alwaysQualify = NameDisp $ \ mn _ -> Just (Qualified mn) +neverQualifyMod :: ModPath -> NameDisp +neverQualifyMod mn = NameDisp $ \n -> + if ogModule n == mn then Just UnQualified else Nothing neverQualify :: NameDisp -neverQualify = NameDisp $ \ _ _ -> Just UnQualified +neverQualify = NameDisp $ \ _ -> Just UnQualified -fmtModName :: ModName -> NameFormat -> T.Text -fmtModName _ UnQualified = T.empty -fmtModName _ (Qualified mn) = modNameToText mn -fmtModName mn NotInScope = modNameToText mn -- | Compose two naming environments, preferring names from the left -- environment. @@ -111,9 +103,9 @@ extend = mappend -- | Get the format for a name. When 'Nothing' is returned, the name is not -- currently in scope. -getNameFormat :: ModName -> Ident -> NameDisp -> NameFormat -getNameFormat m i (NameDisp f) = fromMaybe NotInScope (f m i) -getNameFormat _ _ EmptyNameDisp = NotInScope +getNameFormat :: OrigName -> NameDisp -> NameFormat +getNameFormat m (NameDisp f) = fromMaybe NotInScope (f m) +getNameFormat _ EmptyNameDisp = NotInScope -- | Produce a document in the context of the current 'NameDisp'. withNameDisp :: (NameDisp -> Doc) -> Doc @@ -163,6 +155,11 @@ class PP a => PPName a where -- | Print a name as an infix operator: @a + b@ ppInfixName :: a -> Doc +instance PPName ModName where + ppNameFixity _ = Nothing + ppPrefixName = pp + ppInfixName = pp + pp :: PP a => a -> Doc pp = ppPrec 0 @@ -325,6 +322,7 @@ instance PP Ident where instance PP ModName where ppPrec _ = text . T.unpack . modNameToText + instance PP Assoc where ppPrec _ LeftAssoc = text "left-associative" ppPrec _ RightAssoc = text "right-associative" @@ -333,3 +331,31 @@ instance PP Assoc where instance PP Fixity where ppPrec _ (Fixity assoc level) = text "precedence" <+> int level <.> comma <+> pp assoc + +instance PP ModPath where + ppPrec _ p = + case p of + TopModule m -> pp m + Nested q t -> pp q <.> "::" <.> pp t + +instance PP OrigName where + ppPrec _ og = + withNameDisp $ \disp -> + case getNameFormat og disp of + UnQualified -> pp (ogName og) + Qualified m -> ppQual (TopModule m) (pp (ogName og)) + NotInScope -> ppQual (ogModule og) (pp (ogName og)) + where + ppQual mo x = + case mo of + TopModule m + | m == exprModName -> x + | otherwise -> pp m <.> "::" <.> x + Nested m y -> ppQual m (pp y <.> "::" <.> x) + +instance PP Namespace where + ppPrec _ ns = + case ns of + NSValue -> "/*value*/" + NSType -> "/*type*/" + NSModule -> "/*module*/" diff --git a/tests/examples/allexamples.icry.stdout b/tests/examples/allexamples.icry.stdout index 051f143f8..c7df185d5 100644 --- a/tests/examples/allexamples.icry.stdout +++ b/tests/examples/allexamples.icry.stdout @@ -5,15 +5,15 @@ Loading module Cryptol Loading module AES Loading module Cryptol Loading module ChaCha20 -[warning] at ChaChaPolyCryptolIETF.md:340:32--340:33 Unused name: b -[warning] at ChaChaPolyCryptolIETF.md:2117:20--2117:21 - Unused name: b [warning] at ChaChaPolyCryptolIETF.md:1984:5--1984:15 This binding for `cypherText` shadows the existing binding at ChaChaPolyCryptolIETF.md:1982:24--1982:34 [warning] at ChaChaPolyCryptolIETF.md:2062:20--2062:27 This binding for `AeadAAD` shadows the existing binding at ChaChaPolyCryptolIETF.md:1149:1--1149:8 +[warning] at ChaChaPolyCryptolIETF.md:340:32--340:33 Unused name: b +[warning] at ChaChaPolyCryptolIETF.md:2117:20--2117:21 + Unused name: b Loading module Cryptol Loading module Cipher Loading module Cryptol diff --git a/tests/issues/issue1040.icry.stdout b/tests/issues/issue1040.icry.stdout index b07174804..9d8c4b100 100644 --- a/tests/issues/issue1040.icry.stdout +++ b/tests/issues/issue1040.icry.stdout @@ -2,6 +2,5 @@ Loading module Cryptol Loading module Cryptol Loading module binarytree -[error] at issue1040.cry:1:1--6:36: - Recursive type declarations: - `binarytree::Tree` +[error] Invalid recursive dependency: + • type binarytree::Tree, defined at 3:9--3:13 diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index 9b189b24d..94257d1f0 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -4,32 +4,32 @@ Loading module issue226r2 Loading module issue226 Type Synonyms ============= - + From Cryptol ------------ - + type Bool = Bit type Char = [8] type lg2 n = width (max 1 n - 1) type String n = [n]Char type Word n = [n] - + Constraint Synonyms =================== - + From Cryptol ------------ - + type constraint i < j = j >= 1 + i type constraint i <= j = j >= i type constraint i > j = i >= 1 + j - + Primitive Types =============== - + From Cryptol ------------ - + (!=) : # -> # -> Prop (==) : # -> # -> Prop (>=) : # -> # -> Prop @@ -64,18 +64,13 @@ Primitive Types width : # -> # Z : # -> * Zero : * -> Prop - + Symbols ======= - - Public - ------ - - foo : {a} a -> a - + From Cryptol ------------ - + (/.) : {a} (Field a) => a -> a -> a (==>) : Bit -> Bit -> Bit (\/) : Bit -> Bit -> Bit @@ -217,4 +212,9 @@ Symbols zext : {m, n} (fin m, m >= n) => [n] -> [m] zip : {n, a, b} [n]a -> [n]b -> [n](a, b) zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c - + + From issue226 + ------------- + + foo : {a} a -> a + diff --git a/tests/issues/issue567.icry.stdout b/tests/issues/issue567.icry.stdout index 2e56bafee..1f4b40e99 100644 --- a/tests/issues/issue567.icry.stdout +++ b/tests/issues/issue567.icry.stdout @@ -11,12 +11,12 @@ Loading module Cryptol This binding for `x` shadows the existing binding at issue567.icry:3:6--3:7 (\(x, y) x -> x) : {a, b, c} (a, b) -> c -> c -[warning] at issue567.icry:4:16--4:17 - This binding for `y` shadows the existing binding at - issue567.icry:4:9--4:10 [warning] at issue567.icry:4:13--4:14 This binding for `x` shadows the existing binding at issue567.icry:4:6--4:7 +[warning] at issue567.icry:4:16--4:17 + This binding for `y` shadows the existing binding at + issue567.icry:4:9--4:10 (\(x, y) (x, y) -> x) : {a, b, c, d} (a, b) -> (c, d) -> c [warning] at issue567.icry:5:8--5:9 This binding for `x` shadows the existing binding at diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout index 1b3284587..54bcc34b4 100644 --- a/tests/issues/issue723.icry.stdout +++ b/tests/issues/issue723.icry.stdout @@ -4,7 +4,7 @@ Loading module Main [error] at issue723.cry:7:5--7:19: Failed to validate user-specified signature. - in the definition of 'Main::g', at issue723.cry:7:5--7:6, + in the definition of 'g', at issue723.cry:7:5--7:6, we need to show that for any type k assuming diff --git a/tests/issues/issue731.icry.stdout b/tests/issues/issue731.icry.stdout index 970bf839a..d97ed83b8 100644 --- a/tests/issues/issue731.icry.stdout +++ b/tests/issues/issue731.icry.stdout @@ -3,12 +3,9 @@ Loading module Cryptol Loading module Main Constraint Synonyms =================== - - Public - ------ - - type constraint (<=>) i j = (i <= j, i >= j) - type constraint Both p q = (p, q) - type constraint Fin2 i j = Both (fin i) (fin j) - type constraint T n = (fin n, n >= 1) - + + type constraint (<=>) i j = (i <= j, i >= j) + type constraint Both p q = (p, q) + type constraint Fin2 i j = Both (fin i) (fin j) + type constraint T n = (fin n, n >= 1) + diff --git a/tests/modsys/T10.icry.stdout b/tests/modsys/T10.icry.stdout index b8d9327be..15dfd7181 100644 --- a/tests/modsys/T10.icry.stdout +++ b/tests/modsys/T10.icry.stdout @@ -3,9 +3,6 @@ Loading module Cryptol Loading module T10::Main Symbols ======= - - Public - ------ - - f : {T} {x : T} -> T - + + f : {T} {x : T} -> T + diff --git a/tests/modsys/T4.icry.stdout b/tests/modsys/T4.icry.stdout index a5cea211c..698fea6a1 100644 --- a/tests/modsys/T4.icry.stdout +++ b/tests/modsys/T4.icry.stdout @@ -2,5 +2,5 @@ Loading module Cryptol Loading module Cryptol Loading module T4::A Loading module T4::Main -main : T +main : [8] 0x02 diff --git a/tests/modsys/nested/T1.cry b/tests/modsys/nested/T1.cry new file mode 100644 index 000000000..30e7e7e7a --- /dev/null +++ b/tests/modsys/nested/T1.cry @@ -0,0 +1,6 @@ +module T1 where + +submodule A where + x = 0x02 + +y = x diff --git a/tests/modsys/nested/T1.icry b/tests/modsys/nested/T1.icry new file mode 100644 index 000000000..c56bfe31c --- /dev/null +++ b/tests/modsys/nested/T1.icry @@ -0,0 +1 @@ +:load T1.cry diff --git a/tests/modsys/nested/T1.icry.stdout b/tests/modsys/nested/T1.icry.stdout new file mode 100644 index 000000000..8b3058328 --- /dev/null +++ b/tests/modsys/nested/T1.icry.stdout @@ -0,0 +1,5 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T1 + +[error] at T1.cry:6:5--6:6 Value not in scope: x diff --git a/tests/modsys/nested/T10.cry b/tests/modsys/nested/T10.cry new file mode 100644 index 000000000..b41d4dc86 --- /dev/null +++ b/tests/modsys/nested/T10.cry @@ -0,0 +1,8 @@ +module T6 where + +import T4 as X + +import submodule X::A + +f = y + diff --git a/tests/modsys/nested/T10.icry b/tests/modsys/nested/T10.icry new file mode 100644 index 000000000..c9df8b3f2 --- /dev/null +++ b/tests/modsys/nested/T10.icry @@ -0,0 +1,2 @@ +:load T10.cry +f diff --git a/tests/modsys/nested/T10.icry.stdout b/tests/modsys/nested/T10.icry.stdout new file mode 100644 index 000000000..82114fce4 --- /dev/null +++ b/tests/modsys/nested/T10.icry.stdout @@ -0,0 +1,5 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T4 +Loading module T6 +0x02 diff --git a/tests/modsys/nested/T11.cry b/tests/modsys/nested/T11.cry new file mode 100644 index 000000000..97705d446 --- /dev/null +++ b/tests/modsys/nested/T11.cry @@ -0,0 +1,10 @@ +module T11 where + +import submodule B + +submodule A where + propA = y > 5 + +submodule B where + y : Integer + y = 42 diff --git a/tests/modsys/nested/T11.icry b/tests/modsys/nested/T11.icry new file mode 100644 index 000000000..d6e9c8bc3 --- /dev/null +++ b/tests/modsys/nested/T11.icry @@ -0,0 +1,3 @@ +:load T11.cry +y +A::propA diff --git a/tests/modsys/nested/T11.icry.stdout b/tests/modsys/nested/T11.icry.stdout new file mode 100644 index 000000000..d50f64021 --- /dev/null +++ b/tests/modsys/nested/T11.icry.stdout @@ -0,0 +1,5 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T11 +42 +True diff --git a/tests/modsys/nested/T12.cry b/tests/modsys/nested/T12.cry new file mode 100644 index 000000000..0c6418e14 --- /dev/null +++ b/tests/modsys/nested/T12.cry @@ -0,0 +1,8 @@ +module T12 where + +submodule A where + propA = B::y > 5 + +submodule B where + y : Integer + y = 42 diff --git a/tests/modsys/nested/T12.icry b/tests/modsys/nested/T12.icry new file mode 100644 index 000000000..4613496ed --- /dev/null +++ b/tests/modsys/nested/T12.icry @@ -0,0 +1,3 @@ +:load T12.cry +B::y +A::propA diff --git a/tests/modsys/nested/T12.icry.stdout b/tests/modsys/nested/T12.icry.stdout new file mode 100644 index 000000000..513643fea --- /dev/null +++ b/tests/modsys/nested/T12.icry.stdout @@ -0,0 +1,5 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T12 +42 +True diff --git a/tests/modsys/nested/T13.cry b/tests/modsys/nested/T13.cry new file mode 100644 index 000000000..44f52081b --- /dev/null +++ b/tests/modsys/nested/T13.cry @@ -0,0 +1,10 @@ +module T13 where + +import submodule B as C + +submodule A where + propA = C::y > 5 + +submodule B where + y : Integer + y = 42 diff --git a/tests/modsys/nested/T13.icry b/tests/modsys/nested/T13.icry new file mode 100644 index 000000000..7ad73e5ac --- /dev/null +++ b/tests/modsys/nested/T13.icry @@ -0,0 +1,3 @@ +:load T13.cry +B::y +A::propA diff --git a/tests/modsys/nested/T13.icry.stdout b/tests/modsys/nested/T13.icry.stdout new file mode 100644 index 000000000..12278cceb --- /dev/null +++ b/tests/modsys/nested/T13.icry.stdout @@ -0,0 +1,5 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T13 +42 +True diff --git a/tests/modsys/nested/T14.cry b/tests/modsys/nested/T14.cry new file mode 100644 index 000000000..98d35271a --- /dev/null +++ b/tests/modsys/nested/T14.cry @@ -0,0 +1,20 @@ +module T14 where + +submodule A where + x = 0x1 + + submodule B where + y = 0x2 + + submodule C where + z = 0x3 + +import submodule A::B +import submodule C as D + +output = { ex1 = A::x + , ex2 = A::B::y + , ex3 = A::B::C::z + , ex4 = y + , ex5 = D::z + } diff --git a/tests/modsys/nested/T14.icry b/tests/modsys/nested/T14.icry new file mode 100644 index 000000000..df422eb2e --- /dev/null +++ b/tests/modsys/nested/T14.icry @@ -0,0 +1,2 @@ +:load T14.cry +output diff --git a/tests/modsys/nested/T14.icry.stdout b/tests/modsys/nested/T14.icry.stdout new file mode 100644 index 000000000..0e906146d --- /dev/null +++ b/tests/modsys/nested/T14.icry.stdout @@ -0,0 +1,4 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T14 +{ex1 = 0x1, ex2 = 0x2, ex3 = 0x3, ex4 = 0x2, ex5 = 0x3} diff --git a/tests/modsys/nested/T15.cry b/tests/modsys/nested/T15.cry new file mode 100644 index 000000000..6d8f1fa90 --- /dev/null +++ b/tests/modsys/nested/T15.cry @@ -0,0 +1,12 @@ +module T15 where + +submodule A where + x = 1 + submodule A where + y = 2 + submodule A where + z = 3 + +import submodule A::A + +out = y diff --git a/tests/modsys/nested/T15.icry b/tests/modsys/nested/T15.icry new file mode 100644 index 000000000..fe8861813 --- /dev/null +++ b/tests/modsys/nested/T15.icry @@ -0,0 +1,2 @@ +:load T15.cry +out diff --git a/tests/modsys/nested/T15.icry.stdout b/tests/modsys/nested/T15.icry.stdout new file mode 100644 index 000000000..24f083668 --- /dev/null +++ b/tests/modsys/nested/T15.icry.stdout @@ -0,0 +1,15 @@ +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 diff --git a/tests/modsys/nested/T2.cry b/tests/modsys/nested/T2.cry new file mode 100644 index 000000000..bf15f6b8a --- /dev/null +++ b/tests/modsys/nested/T2.cry @@ -0,0 +1,8 @@ +module T1 where + +submodule A where + x = 0x02 + +import submodule A + +y = x diff --git a/tests/modsys/nested/T2.icry b/tests/modsys/nested/T2.icry new file mode 100644 index 000000000..242f39b86 --- /dev/null +++ b/tests/modsys/nested/T2.icry @@ -0,0 +1,5 @@ +:load T2.icry +:t x +:t y +x +y diff --git a/tests/modsys/nested/T2.icry.stdout b/tests/modsys/nested/T2.icry.stdout new file mode 100644 index 000000000..0c579d24b --- /dev/null +++ b/tests/modsys/nested/T2.icry.stdout @@ -0,0 +1,13 @@ +Loading module Cryptol + +Parse error at T2.icry:1:1, + unexpected: : + expected: a declaration + +[error] at T2.icry:2:4--2:5 Value not in scope: x + +[error] at T2.icry:3:4--3:5 Value not in scope: y + +[error] at T2.icry:4:1--4:2 Value not in scope: x + +[error] at T2.icry:5:1--5:2 Value not in scope: y diff --git a/tests/modsys/nested/T3.cry b/tests/modsys/nested/T3.cry new file mode 100644 index 000000000..e3d35d223 --- /dev/null +++ b/tests/modsys/nested/T3.cry @@ -0,0 +1,11 @@ +module T3 where + +import submodule A +x = y + +submodule A where + y = x + + + + diff --git a/tests/modsys/nested/T3.icry b/tests/modsys/nested/T3.icry new file mode 100644 index 000000000..54258f844 --- /dev/null +++ b/tests/modsys/nested/T3.icry @@ -0,0 +1 @@ +:load T3.cry diff --git a/tests/modsys/nested/T3.icry.stdout b/tests/modsys/nested/T3.icry.stdout new file mode 100644 index 000000000..17380e26e --- /dev/null +++ b/tests/modsys/nested/T3.icry.stdout @@ -0,0 +1,7 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T3 + +[error] Invalid recursive dependency: + • submodule T3::A, defined at 6:11--6:12 + • T3::x, defined at 4:1--4:2 diff --git a/tests/modsys/nested/T4.cry b/tests/modsys/nested/T4.cry new file mode 100644 index 000000000..929b68f2f --- /dev/null +++ b/tests/modsys/nested/T4.cry @@ -0,0 +1,11 @@ +module T4 where + +x = 0x02 + +submodule A where + y = x + +import submodule A + +z = y + diff --git a/tests/modsys/nested/T4.icry b/tests/modsys/nested/T4.icry new file mode 100644 index 000000000..f3aeb18ba --- /dev/null +++ b/tests/modsys/nested/T4.icry @@ -0,0 +1,4 @@ +:load T4.cry +x +y +z diff --git a/tests/modsys/nested/T4.icry.stdout b/tests/modsys/nested/T4.icry.stdout new file mode 100644 index 000000000..318462d75 --- /dev/null +++ b/tests/modsys/nested/T4.icry.stdout @@ -0,0 +1,6 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T4 +0x02 +0x02 +0x02 diff --git a/tests/modsys/nested/T5.cry b/tests/modsys/nested/T5.cry new file mode 100644 index 000000000..a5488fdce --- /dev/null +++ b/tests/modsys/nested/T5.cry @@ -0,0 +1,7 @@ +module T5 where + +import T4 + +import submodule A + +a = x diff --git a/tests/modsys/nested/T5.icry b/tests/modsys/nested/T5.icry new file mode 100644 index 000000000..f3f7f8ad1 --- /dev/null +++ b/tests/modsys/nested/T5.icry @@ -0,0 +1,4 @@ +:load T5.cry +a +:browse T4 +:browse T5 diff --git a/tests/modsys/nested/T5.icry.stdout b/tests/modsys/nested/T5.icry.stdout new file mode 100644 index 000000000..73f1f89ef --- /dev/null +++ b/tests/modsys/nested/T5.icry.stdout @@ -0,0 +1,21 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T4 +Loading module T5 +0x02 +Modules +======= + + submodule A + +Symbols +======= + + x : [8] + z : [8] + +Symbols +======= + + a : [8] + diff --git a/tests/modsys/nested/T6.cry b/tests/modsys/nested/T6.cry new file mode 100644 index 000000000..a988d0c4a --- /dev/null +++ b/tests/modsys/nested/T6.cry @@ -0,0 +1,7 @@ +module T6 where + +import T4 as X + +import submodule X::A + + diff --git a/tests/modsys/nested/T6.icry b/tests/modsys/nested/T6.icry new file mode 100644 index 000000000..3c4fa2861 --- /dev/null +++ b/tests/modsys/nested/T6.icry @@ -0,0 +1,3 @@ +:load T6.cry +:browse T6 +:browse T4 diff --git a/tests/modsys/nested/T6.icry.stdout b/tests/modsys/nested/T6.icry.stdout new file mode 100644 index 000000000..8e70e8b15 --- /dev/null +++ b/tests/modsys/nested/T6.icry.stdout @@ -0,0 +1,16 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T4 +Loading module T6 + +Modules +======= + + submodule A + +Symbols +======= + + x : [8] + z : [8] + diff --git a/tests/modsys/nested/T7.cry b/tests/modsys/nested/T7.cry new file mode 100644 index 000000000..54aa38c1e --- /dev/null +++ b/tests/modsys/nested/T7.cry @@ -0,0 +1,5 @@ + +// Recursive definition in a submodule +submodule A where + x = x + diff --git a/tests/modsys/nested/T7.icry b/tests/modsys/nested/T7.icry new file mode 100644 index 000000000..e464a05e5 --- /dev/null +++ b/tests/modsys/nested/T7.icry @@ -0,0 +1 @@ +:load T7.cry diff --git a/tests/modsys/nested/T7.icry.stdout b/tests/modsys/nested/T7.icry.stdout new file mode 100644 index 000000000..57a1d7a1c --- /dev/null +++ b/tests/modsys/nested/T7.icry.stdout @@ -0,0 +1,3 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main diff --git a/tests/modsys/nested/T8.cry b/tests/modsys/nested/T8.cry new file mode 100644 index 000000000..49833f1cc --- /dev/null +++ b/tests/modsys/nested/T8.cry @@ -0,0 +1,10 @@ +module T9 where + +x = y + +submodule A where + submodule B where + y = x + +import submodule A +import submodule B diff --git a/tests/modsys/nested/T8.icry b/tests/modsys/nested/T8.icry new file mode 100644 index 000000000..5980b9ded --- /dev/null +++ b/tests/modsys/nested/T8.icry @@ -0,0 +1 @@ +:load T8.cry diff --git a/tests/modsys/nested/T8.icry.stdout b/tests/modsys/nested/T8.icry.stdout new file mode 100644 index 000000000..a5ac17067 --- /dev/null +++ b/tests/modsys/nested/T8.icry.stdout @@ -0,0 +1,7 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T9 + +[error] Invalid recursive dependency: + • submodule T9::A, defined at 5:11--5:12 + • T9::x, defined at 3:1--3:2 diff --git a/tests/modsys/nested/T9.cry b/tests/modsys/nested/T9.cry new file mode 100644 index 000000000..01e402f6c --- /dev/null +++ b/tests/modsys/nested/T9.cry @@ -0,0 +1,10 @@ +module T9 where + +x = y + +submodule A where + submodule B where + y = 2 + +import submodule A +import submodule B diff --git a/tests/modsys/nested/T9.icry b/tests/modsys/nested/T9.icry new file mode 100644 index 000000000..5cf0fe681 --- /dev/null +++ b/tests/modsys/nested/T9.icry @@ -0,0 +1,2 @@ +:load T9.cry +x diff --git a/tests/modsys/nested/T9.icry.stdout b/tests/modsys/nested/T9.icry.stdout new file mode 100644 index 000000000..618316a65 --- /dev/null +++ b/tests/modsys/nested/T9.icry.stdout @@ -0,0 +1,6 @@ +Loading module Cryptol +Loading module Cryptol +Loading module T9 +Showing a specific instance of polymorphic result: + * Using 'Integer' for 1st type argument of 'T9::A::B::y' +2 diff --git a/tests/mono-binds/test01.icry.stdout b/tests/mono-binds/test01.icry.stdout index 7eca45cc3..adb0e36f9 100644 --- a/tests/mono-binds/test01.icry.stdout +++ b/tests/mono-binds/test01.icry.stdout @@ -6,11 +6,11 @@ import Cryptol /* Not recursive */ test01::a : {n, a} (fin n) => [n]a -> [2 * n]a test01::a = \{n, a} (fin n) (x : [n]a) -> - test01::f n x + f n x where /* Not recursive */ - test01::f : {m} [m]a -> [n + m]a - test01::f = \{m} (y : [m]a) -> (Cryptol::#) n m a <> x y + f : {m} [m]a -> [n + m]a + f = \{m} (y : [m]a) -> (Cryptol::#) n m a <> x y @@ -21,11 +21,11 @@ import Cryptol /* Not recursive */ test01::a : {n, a} (fin n) => [n]a -> [2 * n]a test01::a = \{n, a} (fin n) (x : [n]a) -> - test01::f x + f x where /* Not recursive */ - test01::f : [n]a -> [2 * n]a - test01::f = \ (y : [n]a) -> (Cryptol::#) n n a <> x y + f : [n]a -> [2 * n]a + f = \ (y : [n]a) -> (Cryptol::#) n n a <> x y diff --git a/tests/mono-binds/test02.icry.stdout b/tests/mono-binds/test02.icry.stdout index 41f61ba57..ba8fc3764 100644 --- a/tests/mono-binds/test02.icry.stdout +++ b/tests/mono-binds/test02.icry.stdout @@ -6,13 +6,13 @@ import Cryptol /* Not recursive */ test02::test : {a, b} a -> b test02::test = \{a, b} (a : a) -> - test02::f b a + f b a where /* Recursive */ - test02::f : {c} a -> c - test02::f = \{c} (x : a) -> test02::g c a - test02::g : {c} a -> c - test02::g = \{c} (x : a) -> test02::f c x + f : {c} a -> c + f = \{c} (x : a) -> g c a + g : {c} a -> c + g = \{c} (x : a) -> f c x @@ -23,13 +23,13 @@ import Cryptol /* Not recursive */ test02::test : {a, b} b -> a test02::test = \{a, b} (a : b) -> - test02::f a + f a where /* Recursive */ - test02::f : b -> a - test02::f = \ (x : b) -> test02::g a - test02::g : b -> a - test02::g = \ (x : b) -> test02::f x + f : b -> a + f = \ (x : b) -> g a + g : b -> a + g = \ (x : b) -> f x diff --git a/tests/mono-binds/test03.icry.stdout b/tests/mono-binds/test03.icry.stdout index 2749e98d8..e17ed8fd9 100644 --- a/tests/mono-binds/test03.icry.stdout +++ b/tests/mono-binds/test03.icry.stdout @@ -6,11 +6,11 @@ import Cryptol /* Not recursive */ test03::test : {a} (fin a, a >= width a) => [a] test03::test = \{a} (fin a, a >= width a) -> - test03::foo [a] <> + foo [a] <> where /* Not recursive */ - test03::foo : {b} (Literal a b) => b - test03::foo = \{b} (Literal a b) -> Cryptol::number a b <> + foo : {b} (Literal a b) => b + foo = \{b} (Literal a b) -> Cryptol::number a b <> @@ -21,11 +21,11 @@ import Cryptol /* Not recursive */ test03::test : {a} (fin a, a >= width a) => [a] test03::test = \{a} (fin a, a >= width a) -> - test03::foo + foo where /* Not recursive */ - test03::foo : [a] - test03::foo = Cryptol::number a [a] <> + foo : [a] + foo = Cryptol::number a [a] <> diff --git a/tests/mono-binds/test04.icry.stdout b/tests/mono-binds/test04.icry.stdout index f7b58b6d4..7f8758d8c 100644 --- a/tests/mono-binds/test04.icry.stdout +++ b/tests/mono-binds/test04.icry.stdout @@ -6,18 +6,18 @@ import Cryptol /* Not recursive */ test04::test : {a, b} (Literal 10 b) => a -> ((a, ()), (a, b)) test04::test = \{a, b} (Literal 10 b) (a : a) -> - (test04::f () (), test04::f b (Cryptol::number 10 b <>)) + (f () (), f b (Cryptol::number 10 b <>)) where /* Not recursive */ - test04::f : {c} c -> (a, c) - test04::f = \{c} (x : c) -> (a, x) + f : {c} c -> (a, c) + f = \{c} (x : c) -> (a, x) Loading module Cryptol Loading module test04 -[error] at test04.cry:1:1--5:14: +[error] at test04.cry:3:1--5:14: • `10` is not a valid literal of type `()` arising from use of literal or demoted expression diff --git a/tests/mono-binds/test05.icry.stdout b/tests/mono-binds/test05.icry.stdout index 535a167b6..03ebf46b8 100644 --- a/tests/mono-binds/test05.icry.stdout +++ b/tests/mono-binds/test05.icry.stdout @@ -19,24 +19,24 @@ test05::test = \{n, a, b} (Zero b, Literal 10 a) (a : [n]b) -> Cryptol::number 10 a <> where /* Not recursive */ - test05::foo : [10] - test05::foo = Cryptol::number 10 [10] <> + foo : [10] + foo = Cryptol::number 10 [10] <> /* Not recursive */ - test05::f : {m} (fin m) => [n + m]b - test05::f = \{m} (fin m) -> - test05::bar m <> - where - /* Not recursive */ - test05::foo : [n]b - test05::foo = a - - /* Not recursive */ - test05::bar : {i} (fin i) => [i + n]b - test05::bar = \{i} (fin i) -> - (Cryptol::#) i n b <> (Cryptol::zero ([i]b) <>) test05::foo - - + f : {m} (fin m) => [n + m]b + f = \{m} (fin m) -> + bar m <> + where + /* Not recursive */ + foo : [n]b + foo = a + + /* Not recursive */ + bar : {i} (fin i) => [i + n]b + bar = \{i} (fin i) -> + (Cryptol::#) i n b <> (Cryptol::zero ([i]b) <>) foo + + diff --git a/tests/mono-binds/test06.icry.stdout b/tests/mono-binds/test06.icry.stdout index 4f3251a42..0555cc439 100644 --- a/tests/mono-binds/test06.icry.stdout +++ b/tests/mono-binds/test06.icry.stdout @@ -6,15 +6,15 @@ import Cryptol /* Not recursive */ test06::test : {a} (Zero a) => a -> a test06::test = \{a} (Zero a) (a : a) -> - test06::bar + bar where /* Not recursive */ - test06::foo : a - test06::foo = Cryptol::zero a <> + foo : a + foo = Cryptol::zero a <> /* Not recursive */ - test06::bar : a - test06::bar = test06::foo + bar : a + bar = foo @@ -25,15 +25,15 @@ import Cryptol /* Not recursive */ test06::test : {a} (Zero a) => a -> a test06::test = \{a} (Zero a) (a : a) -> - test06::bar + bar where /* Not recursive */ - test06::foo : a - test06::foo = Cryptol::zero a <> + foo : a + foo = Cryptol::zero a <> /* Not recursive */ - test06::bar : a - test06::bar = test06::foo + bar : a + bar = foo diff --git a/tests/regression/array.icry.stdout b/tests/regression/array.icry.stdout index d27d30254..cd311dc6c 100644 --- a/tests/regression/array.icry.stdout +++ b/tests/regression/array.icry.stdout @@ -3,19 +3,13 @@ Loading module Cryptol Loading module Array Primitive Types =============== - - Public - ------ - - Array : * -> * -> * - + + Array : * -> * -> * + Symbols ======= - - Public - ------ - - arrayConstant : {a, b} b -> Array a b - arrayLookup : {a, b} Array a b -> a -> b - arrayUpdate : {a, b} Array a b -> a -> b -> Array a b - + + arrayConstant : {a, b} b -> Array a b + arrayLookup : {a, b} Array a b -> a -> b + arrayUpdate : {a, b} Array a b -> a -> b -> Array a b + diff --git a/tests/regression/layout01.icry.stdout b/tests/regression/layout01.icry.stdout index fa2d51c9f..c9eba7d9b 100644 --- a/tests/regression/layout01.icry.stdout +++ b/tests/regression/layout01.icry.stdout @@ -1,13 +1,13 @@ Loading module Cryptol Showing a specific instance of polymorphic result: - * Using 'Integer' for the type of '::x' + * Using 'Integer' for the type of 'x' 1 Showing a specific instance of polymorphic result: - * Using 'Integer' for the type of '::x' + * Using 'Integer' for the type of 'x' [1, 2] Showing a specific instance of polymorphic result: - * Using 'Integer' for the type of '::x' - * Using 'Integer' for the type of '::y' + * Using 'Integer' for the type of 'x' + * Using 'Integer' for the type of 'y' {x = 1, y = 2} Showing a specific instance of polymorphic result: * Using 'Integer' for type of 0th tuple field diff --git a/tests/regression/specialize.icry.stdout b/tests/regression/specialize.icry.stdout index 08f5161e2..fea323d51 100644 --- a/tests/regression/specialize.icry.stdout +++ b/tests/regression/specialize.icry.stdout @@ -11,30 +11,30 @@ where /* Not recursive */ specialize::f : (Bit, Bit) -> (Bit, Bit) specialize::f = \ (__p1 : (Bit, Bit)) -> - (specialize::x, specialize::y) + (x, y) where /* Not recursive */ - specialize::y : Bit - specialize::y = __p1 .1 /* of 2 */ + y : Bit + y = __p1 .1 /* of 2 */ /* Not recursive */ - specialize::x : Bit - specialize::x = __p1 .0 /* of 2 */ + x : Bit + x = __p1 .0 /* of 2 */ /* Not recursive */ specialize::top : (Bit, Bit) -> (Bit, Bit) specialize::top = \ (__p0 : (Bit, Bit)) -> - specialize::f (specialize::x, specialize::y) + specialize::f (x, y) where /* Not recursive */ - specialize::y : Bit - specialize::y = __p0 .1 /* of 2 */ + y : Bit + y = __p0 .1 /* of 2 */ /* Not recursive */ - specialize::x : Bit - specialize::x = __p0 .0 /* of 2 */ + x : Bit + x = __p0 .0 /* of 2 */ diff --git a/tests/regression/superclass.icry.stdout b/tests/regression/superclass.icry.stdout index 0ce9d8188..d8ce8b3ba 100644 --- a/tests/regression/superclass.icry.stdout +++ b/tests/regression/superclass.icry.stdout @@ -3,22 +3,19 @@ Loading module Cryptol Loading module superclass Symbols ======= - - Public - ------ - - compareRound : {a} (Round a) => a -> a -> Bit - eqCmp : {a} (Cmp a) => a -> a -> Bit - fromIntField : {a} (Field a) => a - fromIntIntegral : {a} (Integral a) => a - fromIntRound : {a} (Round a) => a - recipRound : {a} (Round a) => a -> Integer - zeroField : {a} (Field a) => a - zeroIntegral : {a} (Integral a) => a - zeroLogic : {a} (Logic a) => a - zeroRing : {a} (Ring a) => a - zeroRound : {a} (Round a) => a - + + compareRound : {a} (Round a) => a -> a -> Bit + eqCmp : {a} (Cmp a) => a -> a -> Bit + fromIntField : {a} (Field a) => a + fromIntIntegral : {a} (Integral a) => a + fromIntRound : {a} (Round a) => a + recipRound : {a} (Round a) => a -> Integer + zeroField : {a} (Field a) => a + zeroIntegral : {a} (Integral a) => a + zeroLogic : {a} (Logic a) => a + zeroRing : {a} (Ring a) => a + zeroRound : {a} (Round a) => a + (fromInteger 42 + zero) : {a} (Ring a) => a (trunc (recip (fromInteger 5))) : {a} (Round a) => Integer (\x -> x < fromInteger (floor (recip x))) : {a} (Round a) => diff --git a/tests/regression/tc-errors.icry.stdout b/tests/regression/tc-errors.icry.stdout index e2560fccb..e0526e783 100644 --- a/tests/regression/tc-errors.icry.stdout +++ b/tests/regression/tc-errors.icry.stdout @@ -51,9 +51,8 @@ Loading module Main Loading module Cryptol Loading module Main -[error] at :1:1--1:11: - Recursive type declarations: - `Main::T` +[error] Invalid recursive dependency: + • type Main::T, defined at 1:6--1:7 Loading module Cryptol Loading module Main @@ -96,7 +95,7 @@ Loading module Main [error] at tc-errors-6.cry:4:7--4:8: The type ?a is not sufficiently polymorphic. It cannot depend on quantified variables: b`776 - When checking the type of 'Main::g' + When checking the type of 'g' where ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4 b`776 is signature variable 'b' at tc-errors-6.cry:3:8--3:9