Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Nested modules #1048

Merged
merged 15 commits into from
Apr 6, 2021
Merged
Show file tree
Hide file tree
Changes from 13 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 13 additions & 2 deletions cryptol-remote-api/src/CryptolServer/Data/Expression.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 4 additions & 2 deletions cryptol-remote-api/src/CryptolServer/Names.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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]
Expand Down
6 changes: 4 additions & 2 deletions cryptol.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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,
Expand Down
11 changes: 8 additions & 3 deletions src/Cryptol/ModuleSystem.hs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ module Cryptol.ModuleSystem (
, renameType

-- * Interfaces
, Iface(..), IfaceParams(..), IfaceDecls(..), genIface
, Iface, IfaceG(..), IfaceParams(..), IfaceDecls(..), T.genIface
, IfaceTySyn, IfaceDecl(..)
) where

Expand All @@ -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 ------------------------------------------------------------
Expand Down Expand Up @@ -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)
92 changes: 44 additions & 48 deletions src/Cryptol/ModuleSystem/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,37 @@
{-# 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 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(..)
Expand Down Expand Up @@ -53,33 +76,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)

Expand All @@ -89,12 +100,9 @@ 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 (IfaceDecls,R.NamingEnv,P.Module Name)
renameModule m = rename (thing (mName m)) mempty (R.renameModule m)


-- NoPat -----------------------------------------------------------------------
Expand Down Expand Up @@ -231,17 +239,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))

Expand Down Expand Up @@ -299,13 +296,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
}
Expand Down Expand Up @@ -360,11 +357,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 }
Expand Down Expand Up @@ -529,7 +523,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
Expand All @@ -538,6 +532,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)
Expand Down
32 changes: 23 additions & 9 deletions src/Cryptol/ModuleSystem/Env.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,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)

Expand Down Expand Up @@ -188,6 +189,9 @@ data ModContext = ModContext
, mctxDecls :: IfaceDecls
, mctxNames :: R.NamingEnv
, mctxNameDisp :: NameDisp

-- XXX: use namespace
, mctxModProvenace :: Map Name DeclProvenance
, mctxTypeProvenace :: Map Name DeclProvenance
, mctxValueProvenance :: Map Name DeclProvenance
}
Expand All @@ -205,18 +209,26 @@ data DeclProvenance =
-- | Given the state of the environment, compute information about what's
-- in scope on the REPL. This includes what's in the focused module, plus any
-- additional definitions from the REPL (e.g., let bound names, and @it@).
-- XXX: nested modules.
-- XXX: it seems that this does a bunch of work that should be happening
-- somewhere else too...
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
, mctxModProvenace = fst3 provenance
, mctxTypeProvenace = snd3 provenance
, mctxValueProvenance = trd3 provenance
}

where
fst3 (x,_,_) = x
snd3 (_,x,_) = x
trd3 (_,_,x) = x

(importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports)
localDecls = publicDecls `mappend` privateDecls
localNames = R.unqualifiedEnv localDecls `mappend`
Expand Down Expand Up @@ -249,7 +261,7 @@ focusedEnv me =
case lookupModule (iModule imp) me of
Just lm ->
let decls = ifPublic (lmInterface lm)
in ( R.interpImport imp decls
in ( R.interpImportIface imp decls
, decls
, declsProv (NameIsImportedFrom (iModule imp)) decls
)
Expand All @@ -258,14 +270,15 @@ focusedEnv me =


-- earlier ones shadow
shadowProvs ps = let (tss,vss) = unzip ps
in (Map.unions tss, Map.unions vss)
shadowProvs ps = let (mss,tss,vss) = unzip3 ps
in (Map.unions mss, Map.unions tss, Map.unions vss)

paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns)
paramProv IfaceParams { .. } = (mempty, doMap ifParamTypes, doMap ifParamFuns)
where doMap mp = const NameIsParameter <$> mp

declsProv prov IfaceDecls { .. } =
( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ]
( doMap ifModules
, Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ]
, doMap ifDecls
)
where doMap mp = const prov <$> mp
Expand Down Expand Up @@ -381,7 +394,7 @@ addLoadedModule path ident fp tm lm
{ lmName = T.mName tm
, lmFilePath = path
, lmModuleId = ident
, lmInterface = genIface tm
, lmInterface = T.genIface tm
, lmModule = tm
, lmFingerprint = fp
}
Expand Down Expand Up @@ -435,7 +448,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
]
Loading