diff --git a/bench/Main.hs b/bench/Main.hs index aa1886f43..761c3c5c4 100644 --- a/bench/Main.hs +++ b/bench/Main.hs @@ -26,7 +26,6 @@ import qualified Cryptol.ModuleSystem.Base as M import qualified Cryptol.ModuleSystem.Env as M import qualified Cryptol.ModuleSystem.Monad as M import qualified Cryptol.ModuleSystem.NamingEnv as M -import Cryptol.ModuleSystem.Interface (noIfaceParams) import qualified Cryptol.Parser as P import qualified Cryptol.Parser.AST as P @@ -130,7 +129,7 @@ tc cd name path = , M.tcLinter = M.moduleLinter (P.thing (P.mName scm)) , M.tcPrims = prims } - M.typecheck act scm noIfaceParams tcEnv + M.typecheck act scm mempty tcEnv ceval :: String -> String -> FilePath -> T.Text -> Benchmark ceval cd name path expr = diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs index b64cfcdbf..aa1048b05 100644 --- a/cryptol-remote-api/cryptol-eval-server/Main.hs +++ b/cryptol-remote-api/cryptol-eval-server/Main.hs @@ -26,7 +26,7 @@ import CryptolServer.Interrupt ( interruptServer, interruptServerDescr ) import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName) import Cryptol.ModuleSystem.Monad (runModuleM, setFocusedModule) -import Cryptol.TypeCheck.AST (mName) +import Cryptol.TypeCheck.AST (tcTopEntitytName) import Cryptol.Utils.Ident (ModName, modNameToText, textToModName, preludeName) import Cryptol.Utils.Logger (quietLogger) @@ -77,7 +77,7 @@ main = customMain initMod initMod initMod initMod description buildApp case res of Left err -> die err Right (m, menv') -> - do res' <- fst <$> runModuleM minp{ minpModuleEnv = menv' } (setFocusedModule (mName (snd m))) + do res' <- fst <$> runModuleM minp{ minpModuleEnv = menv' } (setFocusedModule (tcTopEntitytName (snd m))) case res' of Left err -> die err Right (_, menv'') -> pure menv'' diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index b6d4ee26e..5bb043ab6 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -47,7 +47,7 @@ import qualified Cryptol.ModuleSystem.Base as Base import qualified Cryptol.ModuleSystem.Renamer as R import Cryptol.ModuleSystem.Name (Name, mkDeclared, NameSource( UserName ), liftSupply, nameIdent) -import Cryptol.ModuleSystem.NamingEnv (singletonE, shadowing, namespaceMap) +import Cryptol.ModuleSystem.NamingEnv (singletonNS, shadowing, namespaceMap) import qualified Cryptol.Parser as CP import qualified Cryptol.Parser.AST as CP @@ -649,7 +649,7 @@ bindValToFreshName nameBase ty val = do liftModuleCmd (evalDecls [TC.NonRecursive decl]) modifyModuleEnv $ \me -> let denv = meDynEnv me - in me {meDynEnv = denv { deNames = singletonE (CP.UnQual (mkIdent txt)) name `shadowing` deNames denv }} + in me {meDynEnv = denv { deNames = singletonNS NSValue (CP.UnQual (mkIdent txt)) name `shadowing` deNames denv }} return $ Just txt where genFresh :: CryptolCommand (Text, Name) @@ -660,7 +660,7 @@ bindValToFreshName nameBase ty val = do mpath = TopModule interactiveName name <- liftSupply (mkDeclared NSValue mpath UserName ident Nothing emptyRange) pure (txt, name) - where nextNewName :: Map CP.PName [Name] -> Int -> Text + where nextNewName :: Map CP.PName a -> Int -> Text nextNewName ns n = let txt = "CryptolServer'" <> nameBase <> (T.pack $ show n) pname = CP.UnQual (mkIdent txt) diff --git a/cryptol-remote-api/src/CryptolServer/Exceptions.hs b/cryptol-remote-api/src/CryptolServer/Exceptions.hs index ace98053b..214624b9c 100644 --- a/cryptol-remote-api/src/CryptolServer/Exceptions.hs +++ b/cryptol-remote-api/src/CryptolServer/Exceptions.hs @@ -102,16 +102,6 @@ cryptolError modErr warns = (20610, [ ("name", jsonPretty name) , ("paths", jsonList [jsonString path1, jsonString path2]) ]) - ImportedParamModule x -> - (20630, [ ("module", jsonPretty x) - ]) - FailedToParameterizeModDefs x xs -> - (20640, [ ("module", jsonPretty x) - , ("parameters", jsonList (map (jsonString . pretty) xs)) - ]) - NotAParameterizedModule x -> - (20650, [ ("module", jsonPretty x) - ]) FFILoadErrors x errs -> (20660, [ ("module", jsonPretty x) , ("errors", jsonList (map jsonPretty errs)) diff --git a/cryptol-remote-api/src/CryptolServer/Names.hs b/cryptol-remote-api/src/CryptolServer/Names.hs index 12b73e89c..3377fd383 100644 --- a/cryptol-remote-api/src/CryptolServer/Names.hs +++ b/cryptol-remote-api/src/CryptolServer/Names.hs @@ -15,6 +15,7 @@ import Data.Aeson ((.=)) import qualified Data.Map as Map import Data.Map (Map) import Data.Text (unpack) +import Data.Maybe(maybeToList) import Data.Typeable (Proxy(..), typeRep) import Cryptol.Parser.Name (PName(..)) @@ -22,7 +23,8 @@ import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), import Cryptol.ModuleSystem.Interface (IfaceDecl(..), IfaceDecls(..)) import Cryptol.ModuleSystem.Name (Name) import Cryptol.ModuleSystem.NamingEnv - (NamingEnv, namespaceMap, lookupValNames, shadowing) + (NamingEnv, namespaceMap, lookupNS, shadowing) +import Cryptol.ModuleSystem.Names(namesToList) import Cryptol.TypeCheck.Type (Schema(..)) import Cryptol.Utils.PP (pp) import Cryptol.Utils.Ident(Namespace(..)) @@ -71,7 +73,7 @@ getInfo rnEnv info n' = let ty = ifDeclSig i nameDocs = ifDeclDoc i in NameInfo (show (pp n')) (show (pp ty)) ty (unpack <$> nameDocs) - | n <- lookupValNames n' rnEnv + | ns <- maybeToList (lookupNS NSValue n' rnEnv), n <- namesToList ns ] data NameInfo = diff --git a/cryptol.cabal b/cryptol.cabal index 3b91b2683..0d18bfc43 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -71,6 +71,7 @@ library parameterized-utils >= 2.0.2, pretty, prettyprinter >= 1.7.0, + pretty-show, process >= 1.2, sbv >= 8.10 && < 9.1, simple-smt >= 0.9.7, @@ -137,10 +138,13 @@ library Cryptol.ModuleSystem.Interface, Cryptol.ModuleSystem.Monad, Cryptol.ModuleSystem.Name, + Cryptol.ModuleSystem.Names, Cryptol.ModuleSystem.NamingEnv, + Cryptol.ModuleSystem.Binds Cryptol.ModuleSystem.Exports, - Cryptol.ModuleSystem.InstantiateModule, Cryptol.ModuleSystem.Renamer, + Cryptol.ModuleSystem.Renamer.Imports, + Cryptol.ModuleSystem.Renamer.ImplicitImports, Cryptol.ModuleSystem.Renamer.Monad, Cryptol.ModuleSystem.Renamer.Error, @@ -153,7 +157,6 @@ library Cryptol.TypeCheck.Parseable, Cryptol.TypeCheck.Monad, Cryptol.TypeCheck.Infer, - Cryptol.TypeCheck.CheckModuleInstance, Cryptol.TypeCheck.InferTypes, Cryptol.TypeCheck.Interface, Cryptol.TypeCheck.Error, @@ -171,6 +174,8 @@ library Cryptol.TypeCheck.FFI, Cryptol.TypeCheck.FFI.Error, Cryptol.TypeCheck.FFI.FFIType, + Cryptol.TypeCheck.Module, + Cryptol.TypeCheck.ModuleInstance, Cryptol.TypeCheck.Solver.Types, Cryptol.TypeCheck.Solver.SMT, @@ -186,9 +191,9 @@ library Cryptol.Transform.MonoValues, Cryptol.Transform.Specialize, - Cryptol.Transform.AddModParams, Cryptol.IR.FreeVars, + Cryptol.IR.TraverseNames, Cryptol.Backend, Cryptol.Backend.Arch, @@ -227,6 +232,7 @@ library Cryptol.Symbolic.What4, Cryptol.REPL.Command, + Cryptol.REPL.Help, Cryptol.REPL.Browse, Cryptol.REPL.Monad, Cryptol.REPL.Trie diff --git a/docs/RefMan/Modules.rst b/docs/RefMan/Modules.rst index 7c8fafadd..d8e992314 100644 --- a/docs/RefMan/Modules.rst +++ b/docs/RefMan/Modules.rst @@ -335,11 +335,6 @@ another top-level module ``B`` requires two steps: Parameterized Modules --------------------- -.. warning:: - The documentation in this section is for the upcoming variant of - the feature, which is not yet part of main line Cryptol. - - Interface Modules ~~~~~~~~~~~~~~~~~ diff --git a/docs/RefMan/_build/doctrees/BasicSyntax.doctree b/docs/RefMan/_build/doctrees/BasicSyntax.doctree index 61a0b9c4a..7f66ad2d9 100644 Binary files a/docs/RefMan/_build/doctrees/BasicSyntax.doctree and b/docs/RefMan/_build/doctrees/BasicSyntax.doctree differ diff --git a/docs/RefMan/_build/doctrees/BasicTypes.doctree b/docs/RefMan/_build/doctrees/BasicTypes.doctree index dade46df2..44b4ed1a0 100644 Binary files a/docs/RefMan/_build/doctrees/BasicTypes.doctree and b/docs/RefMan/_build/doctrees/BasicTypes.doctree differ diff --git a/docs/RefMan/_build/doctrees/Expressions.doctree b/docs/RefMan/_build/doctrees/Expressions.doctree index 3b164e8fa..f3b3fcd84 100644 Binary files a/docs/RefMan/_build/doctrees/Expressions.doctree and b/docs/RefMan/_build/doctrees/Expressions.doctree differ diff --git a/docs/RefMan/_build/doctrees/FFI.doctree b/docs/RefMan/_build/doctrees/FFI.doctree index 4223404b1..c850378ca 100644 Binary files a/docs/RefMan/_build/doctrees/FFI.doctree and b/docs/RefMan/_build/doctrees/FFI.doctree differ diff --git a/docs/RefMan/_build/doctrees/Modules.doctree b/docs/RefMan/_build/doctrees/Modules.doctree index 5de0831f5..b1fb46f17 100644 Binary files a/docs/RefMan/_build/doctrees/Modules.doctree and b/docs/RefMan/_build/doctrees/Modules.doctree differ diff --git a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree index 8797caaeb..31c32fdb5 100644 Binary files a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree and b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree differ diff --git a/docs/RefMan/_build/doctrees/RefMan.doctree b/docs/RefMan/_build/doctrees/RefMan.doctree index b6debdce8..360f7fca7 100644 Binary files a/docs/RefMan/_build/doctrees/RefMan.doctree and b/docs/RefMan/_build/doctrees/RefMan.doctree differ diff --git a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree index 353c3286b..e78a6ba9c 100644 Binary files a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree and b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree differ diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle index a6a301772..86245cd3e 100644 Binary files a/docs/RefMan/_build/doctrees/environment.pickle and b/docs/RefMan/_build/doctrees/environment.pickle differ diff --git a/docs/RefMan/_build/html/.buildinfo b/docs/RefMan/_build/html/.buildinfo index b0149fc3a..353327328 100644 --- a/docs/RefMan/_build/html/.buildinfo +++ b/docs/RefMan/_build/html/.buildinfo @@ -1,4 +1,4 @@ # Sphinx build info version 1 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done. -config: 69485412ee215e2257ea16f8a42506fe +config: 766b28421f9ffa9f611038e48286ed1c tags: 645f666f9bcd5a90fca523b33c5a78b7 diff --git a/docs/RefMan/_build/html/BasicSyntax.html b/docs/RefMan/_build/html/BasicSyntax.html index 3bbc07fbb..79fc359cf 100644 --- a/docs/RefMan/_build/html/BasicSyntax.html +++ b/docs/RefMan/_build/html/BasicSyntax.html @@ -1,66 +1,34 @@ - - - - +
- - - - -