Skip to content

Commit

Permalink
Implementation of nested modules.
Browse files Browse the repository at this point in the history 
  * Limitations:
    Does not work in combination parameterized modules, as I am
    about to redo how that works.

  * General refeactorings:
    * Namespaces:
      - We have an explicit type for namespaces, see `Cryptol.Util.Ident`
      - Display environments should now be aware of the namespace of the
        name being displayed.

    * Renamer:
      - Factor out the renamer monad and error type into separate modules
      - All name resultion is done through a single function `resolveName`
      - The renamer now computes the dependencies between declarations,
         orders things in dependency order, and checks for bad recursion.

    * Typechecker: Redo checking of declarations (both top-level and local).
      Previously we used a sort of CPS to add things in scope.   Now we use
      a state monad and add things to the state.  We assume that the renamer
      has been run, which means that declarations are ordered in dependency
      order, and things have unique name, so we don't need to worry about
      scoping too much.

  * Change specific to nested modules:
    - We have a new namespace for module names
    - The interface file of a module contains the interfaces for nested modules
    - Most of the changes related to nested modules in the renamer are
      in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename`
        - There is some trickiness when resolving module names when importing
          submodules (seed `processOpen` and `openLoop`)
    - There are some changes to the representation of modules in the typechecked
      syntax, in particular:
        - During type-checking we "flatten" nested module declarations into
          a single big declaration.  Hopefully, this means that passes after
          the type checker don't need to worry about nested modules
        - There is a new field containing the interfaces of the nested modules,
          this is needed so that when we import the module we know we have the
          nested structure
        - Declarations in functor/parameterzied modules do not appear in the
          flattened list of declarations.  Instead thouse modules are collected
          in a separate field, and the plan is that they would be used from
          there when we implmenet functor instantiation.
  • Loading branch information
@yav
yav committed Mar 12, 2021
1 parent 8a0a009 commit 34b1d87
Show file tree
Hide file tree
Showing 72 changed files with 2,644 additions and 1,641 deletions.
15 changes: 13 additions & 2 deletions cryptol-remote-api/src/CryptolServer/Data/Expression.hs
View file
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
View file
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
View file
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
View file
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)
88 changes: 41 additions & 47 deletions src/Cryptol/ModuleSystem/Base.hs
View file
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
32 changes: 23 additions & 9 deletions src/Cryptol/ModuleSystem/Env.hs
View file
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 @@ -197,6 +198,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 @@ -214,18 +218,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 @@ -258,7 +270,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 @@ -267,14 +279,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 @@ -390,7 +403,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 @@ -444,7 +457,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

0 comments on commit 34b1d87

Please sign in to comment.