diff --git a/CHANGES.md b/CHANGES.md index 11ffd01cd..1805b5143 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -24,6 +24,10 @@ * The REPL properly supports tab completion for the `:t` and `:check` commands. ([#1780](https://github.com/GaloisInc/cryptol/issues/1780)) +* Add support for incrementally loading projects via cryptol's `--project` + flag as documented in the reference manual. + ([#1641](https://github.com/GaloisInc/cryptol/issues/1641)) + # 3.2.0 -- 2024-08-20 ## Language changes diff --git a/cryptol-remote-api/python/tests/cryptol/test_filedeps.py b/cryptol-remote-api/python/tests/cryptol/test_filedeps.py index ddd66387e..0bd36436f 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_filedeps.py +++ b/cryptol-remote-api/python/tests/cryptol/test_filedeps.py @@ -10,7 +10,7 @@ def test_FileDeps(self) -> None: connect(verify=False) path = str(Path('tests','cryptol','test-files','Id.cry')) result = file_deps(path,True) - self.assertEqual(result['fingerprint'],"8A49C6A461AF276DF56C4FE4279BCFC51D891214") + self.assertEqual(result['fingerprint'],"8316fb4e38d33ec3b9f89d355597c058b2e4baf653bf18dc4ead7e166a8a32f8") self.assertEqual(result['foreign'],[]) self.assertEqual(result['imports'],['Cryptol']) self.assertEqual(result['includes'],[]) diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs index bacf3f2b2..31c1e01a0 100644 --- a/cryptol-remote-api/src/CryptolServer.hs +++ b/cryptol-remote-api/src/CryptolServer.hs @@ -195,6 +195,6 @@ validateServerState = InMem{} -> continue InFile file -> do fp <- fingerprintFile file - if fp == Just (fiFingerprint (lmFileInfo lm)) + if fp == Right (fiFingerprint (lmFileInfo lm)) then continue else return False diff --git a/cryptol-remote-api/src/CryptolServer/Exceptions.hs b/cryptol-remote-api/src/CryptolServer/Exceptions.hs index b6af366ba..f2fc91672 100644 --- a/cryptol-remote-api/src/CryptolServer/Exceptions.hs +++ b/cryptol-remote-api/src/CryptolServer/Exceptions.hs @@ -57,17 +57,19 @@ cryptolError modErr warns = CantFindFile path -> (20050, [ ("path", jsonString path) ]) - BadUtf8 path ue -> + BadUtf8 path fp ue -> (20010, [ ("path", jsonShow path) , ("error", jsonShow ue) + , ("fingerprint", jsonShow fp) ]) OtherIOError path exn -> (20060, [ ("path", jsonString path) , ("error", jsonShow exn) ]) - ModuleParseError source message -> + ModuleParseError source fp message -> (20540, [ ("source", jsonShow source) , ("error", jsonShow message) + , ("fingerprint", jsonShow fp) ]) RecursiveModules mods -> (20550, [ ("modules", jsonList (reverse (map jsonPretty mods))) diff --git a/cryptol-remote-api/src/CryptolServer/FileDeps.hs b/cryptol-remote-api/src/CryptolServer/FileDeps.hs index 0318badf0..e79cda5cd 100644 --- a/cryptol-remote-api/src/CryptolServer/FileDeps.hs +++ b/cryptol-remote-api/src/CryptolServer/FileDeps.hs @@ -9,6 +9,7 @@ module CryptolServer.FileDeps import Data.Text (Text) import qualified Data.Map as Map import qualified Data.Set as Set +import qualified Data.Map.Strict as Map import qualified Data.Aeson as JSON import Data.Aeson (FromJSON(..),ToJSON(..),(.=),(.:)) @@ -67,7 +68,7 @@ instance ToJSON FileDeps where InFile f -> toJSON f InMem l _ -> JSON.object [ "internal" .= l ] , "fingerprint" .= fingerprintHexString (fiFingerprint fi) - , "includes" .= Set.toList (fiIncludeDeps fi) + , "includes" .= Map.keys (fiIncludeDeps fi) , "imports" .= map (show . pp) (Set.toList (fiImportDeps fi)) , "foreign" .= Map.toList (fiForeignDeps fi) ] diff --git a/cryptol-repl-internal/REPL/Haskeline.hs b/cryptol-repl-internal/REPL/Haskeline.hs index 4d0bdc797..ddd350e93 100644 --- a/cryptol-repl-internal/REPL/Haskeline.hs +++ b/cryptol-repl-internal/REPL/Haskeline.hs @@ -14,6 +14,7 @@ module REPL.Haskeline where +import qualified Cryptol.Project as Project import Cryptol.REPL.Command import Cryptol.REPL.Monad import Cryptol.REPL.Trie @@ -131,22 +132,33 @@ loadCryRC cryrc = else return status -- | Haskeline-specific repl implementation. -repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult -repl cryrc replMode callStacks stopOnError begin = +repl :: + Cryptolrc -> + Maybe Project.Config -> + Bool {- ^ refresh project -} -> + ReplMode -> Bool -> Bool -> REPL () -> IO CommandResult +repl cryrc projectConfig projectRefresh replMode callStacks stopOnError begin = runREPL isBatch callStacks stdoutLogger replAction where -- this flag is used to suppress the logo and prompts - isBatch = case replMode of - InteractiveRepl -> False - Batch _ -> True - InteractiveBatch _ -> True + isBatch = + case projectConfig of + Just _ -> True + Nothing -> + case replMode of + InteractiveRepl -> False + Batch _ -> True + InteractiveBatch _ -> True replAction = do status <- loadCryRC cryrc - if crSuccess status - then begin >> crySession replMode stopOnError - else return status + if crSuccess status then do + begin + case projectConfig of + Just config -> loadProjectREPL projectRefresh config + Nothing -> crySession replMode stopOnError + else return status -- | Try to set the history file. setHistoryFile :: Settings REPL -> IO (Settings REPL) diff --git a/cryptol.cabal b/cryptol.cabal index f7a6b69e1..587dc4b3e 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -54,7 +54,7 @@ library array >= 0.4, containers >= 0.5, criterion-measurement, - cryptohash-sha1 >= 0.11 && < 0.12, + cryptohash-sha256 >= 0.11 && < 0.12, deepseq >= 1.3, directory >= 1.2.2.0, exceptions, @@ -63,6 +63,7 @@ library gitrev >= 1.0, ghc-prim, GraphSCC >= 1.0.4, + heredoc >= 0.2, language-c99, language-c99-simple, libBF >= 0.6 && < 0.7, @@ -80,6 +81,7 @@ library strict, text >= 1.1, tf-random >= 0.5, + toml-parser >= 2.0 && <2.1, transformers-base >= 0.4, vector, mtl >= 2.2.1, @@ -238,7 +240,12 @@ library Cryptol.REPL.Help, Cryptol.REPL.Browse, Cryptol.REPL.Monad, - Cryptol.REPL.Trie + Cryptol.REPL.Trie, + + Cryptol.Project + Cryptol.Project.Config + Cryptol.Project.Monad + Cryptol.Project.Cache Other-modules: Cryptol.Parser.LexerUtils, Cryptol.Parser.ParserUtils, diff --git a/cryptol/Main.hs b/cryptol/Main.hs index 85beccf28..519d4bbc7 100644 --- a/cryptol/Main.hs +++ b/cryptol/Main.hs @@ -8,6 +8,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} module Main where @@ -18,6 +19,7 @@ import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle, io,prependSearchPath,setSearchPath,parseSearchPath) import qualified Cryptol.REPL.Monad as REPL import Cryptol.ModuleSystem.Env(ModulePath(..)) +import qualified Cryptol.Project as Project import REPL.Haskeline import REPL.Logo @@ -26,6 +28,7 @@ import Cryptol.Utils.PP import Cryptol.Version (displayVersion) import Control.Monad (when, void) +import Data.Maybe (isJust, isNothing) import GHC.IO.Encoding (setLocaleEncoding, utf8) import System.Console.GetOpt (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo) @@ -47,6 +50,8 @@ data Options = Options , optVersion :: Bool , optHelp :: Bool , optBatch :: ReplMode + , optProject :: Maybe FilePath + , optProjectRefresh :: Bool , optCallStacks :: Bool , optCommands :: [String] , optColorMode :: ColorMode @@ -62,6 +67,8 @@ defaultOptions = Options , optVersion = False , optHelp = False , optBatch = InteractiveRepl + , optProject = Nothing + , optProjectRefresh = False , optCallStacks = True , optCommands = [] , optColorMode = AutoColor @@ -79,6 +86,13 @@ options = , Option "" ["interactive-batch"] (ReqArg setInteractiveBatchScript "FILE") "run the script provided and exit, but behave as if running an interactive session" + , Option "p" ["project"] (ReqArg setProject "CRYPROJECT") + ("Load and verify a Cryptol project using the provided project " + ++ "configuration file or directory containing 'cryproject.toml'") + + , Option "" ["refresh-project"] (NoArg setProjectRefresh) + "Ignore a pre-existing cache file when loading a project." + , Option "e" ["stop-on-error"] (NoArg setStopOnError) "stop script execution as soon as an error occurs." @@ -137,6 +151,12 @@ setBatchScript path = modify $ \ opts -> opts { optBatch = Batch path } setInteractiveBatchScript :: String -> OptParser Options setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = InteractiveBatch path } +setProject :: String -> OptParser Options +setProject path = modify $ \opts -> opts { optProject = Just path } + +setProjectRefresh :: OptParser Options +setProjectRefresh = modify $ \opts -> opts { optProjectRefresh = True } + -- | Set the color mode of the terminal output. setColorMode :: String -> OptParser Options setColorMode "auto" = modify $ \ opts -> opts { optColorMode = AutoColor } @@ -225,11 +245,14 @@ main = do | optVersion opts -> displayVersion putStrLn | otherwise -> do (opts', mCleanup) <- setupCmdScript opts - status <- repl (optCryptolrc opts') - (optBatch opts') - (optCallStacks opts') - (optStopOnError opts') - (setupREPL opts') + (opts'', mConfig) <- setupProject opts' + status <- repl (optCryptolrc opts'') + mConfig + (optProjectRefresh opts'') + (optBatch opts'') + (optCallStacks opts'') + (optStopOnError opts'') + (setupREPL opts'') case mCleanup of Nothing -> return () Just cmdFile -> removeFile cmdFile @@ -249,7 +272,27 @@ setupCmdScript opts = hClose h when (optBatch opts /= InteractiveRepl) $ putStrLn "[warning] --command argument specified; ignoring batch file" - return (opts { optBatch = InteractiveBatch path }, Just path) + when (isJust (optProject opts)) $ + putStrLn $ + "[warning] --command argument specified; " + ++ "ignoring project configuration file" + return + ( opts { optBatch = InteractiveBatch path, optProject = Nothing } + , Just path ) + +setupProject :: Options -> IO (Options, Maybe Project.Config) +setupProject opts = + case optProject opts of + Nothing -> pure (opts, Nothing) + Just path -> do + when (optBatch opts /= InteractiveRepl) $ + putStrLn "[warning] --project argument specified; ignoring batch file" + Project.loadConfig path >>= \case + Left err -> do + print $ pp err + exitFailure + Right config -> + pure (opts { optBatch = InteractiveRepl }, Just config) setupREPL :: Options -> REPL () setupREPL opts = do @@ -281,18 +324,20 @@ setupREPL opts = do Batch file -> prependSearchPath [ takeDirectory file ] _ -> return () - case optLoad opts of - [] -> loadPrelude `REPL.catch` \x -> io $ print $ pp x - [l] -> void (loadCmd l) `REPL.catch` \x -> do - io $ print $ pp x - -- If the requested file fails to load, load the prelude instead... - loadPrelude `REPL.catch` \y -> do - io $ print $ pp y - -- ... but make sure the loaded module is set to the file - -- we tried, instead of the Prelude - REPL.setEditPath l - REPL.setLoadedMod REPL.LoadedModule - { REPL.lFocus = Nothing - , REPL.lPath = InFile l - } - _ -> io $ putStrLn "Only one file may be loaded at the command line." + when (isNothing (optProject opts)) $ + case optLoad opts of + [] -> loadPrelude `REPL.catch` \x -> io $ print $ pp x + [l] -> void (loadCmd l) `REPL.catch` \x -> do + io $ print $ pp x + -- If the requested file fails to load, + -- load the prelude instead... + loadPrelude `REPL.catch` \y -> do + io $ print $ pp y + -- ... but make sure the loaded module is set to the file + -- we tried, instead of the Prelude + REPL.setEditPath l + REPL.setLoadedMod REPL.LoadedModule + { REPL.lFocus = Nothing + , REPL.lPath = InFile l + } + _ -> io $ putStrLn "Only one file may be loaded at the command line." diff --git a/docs/RefMan/Project.rst b/docs/RefMan/Project.rst new file mode 100644 index 000000000..3092dde07 --- /dev/null +++ b/docs/RefMan/Project.rst @@ -0,0 +1,132 @@ +Project Files +============= + +Cryptol supports specifying a *project* file that can accelerate the +repeated loading and testing of a large, interconnected set of source +files. Cryptol will remember the hashes of the files previously checked +and use this to avoid type-checking and testing files that are unchanged +since the previous loading of the project. + +To use this feature a ``cryproject.toml`` should be created in the root +directory of the cryptol source files that lists all of the top-level +modules of the project. The dependencies of these modules will implicitly +be added to the project. + +To check a whole project, Cryptol can be invoked with the ``--project`` +or ``-p`` flag using the directory containing the project as an +argument. This will type-check all of the modules in the project and +check the docstrings for all modules in the project. + +All errors are reported to stdout. When all modules load and all tests +pass cryptol's exit code will be ``0``. When the project does not load +successfully the exit code is ``1``. + +After loading a project the cache information is saved into a Cryptol- +managed file in the project root directory ``.cryproject/loadcache.toml``. + +Example: + +.. code:: shell + + cryptol -p myproject/ + +To discard the previous cached results and reload a whole project use +``--refresh-project``. This can be useful when versions of external +tools have changed or simply to get confidence that everything is still +in a working state. + +Example: + +.. code:: shell + + cryptol -p myproject/ --refresh-project + +``cryproject.toml`` Format +-------------------------- + +Project files are described by a `TOML `__ file +using the following top-level key-value assignments: + +- ``root`` - *optional* - *string* - can optionally be specified to override the directory that + Cryptol files are located in. Otherwise modules are loaded relative + to the directory containing the ``cryproject.toml``. + +- ``modules`` - *required* - *list of strings* - is a list of filenames containing the top-level modules in a + project. These modules, and all of their dependencies, will be loaded + when the project is loaded. + +Example directory structure: + +.. code:: + + project + ├── Id.c + ├── Id.cry + ├── Id.dylib + ├── Main.cry + └── cryproject.toml + +Example ``cryproject.toml``: + +.. code:: toml + + modules = [ + "Id.cry", + "Main.cry", + ] + +``loadcache.toml`` Format +------------------------- + +After loading a project a cache file is generated and stored in +``.cryproject/loadcache.toml``. This file contains a version number to +allow caches to automatically invalidate when the project subsystem +updates. Modules that fail to load at all are not listed in the cache +file and will be reprocessed on subsequent project loads even if unchanged. + +- ``version`` - *integer* - specifies the cache file format version in order to allow + old caches to be invalidated when Cryptol changes the meaning of this + file. + +- ``file`` - *string* - specifies the absolute path to a Cryptol module for those + stored in files. + +- ``memory`` - *string* - specifies the module name of a primitive module built into + Cryptol. + +- ``fingerprint`` - *string* - specifies a SHA2-256 hash of the source file which is + used to detect when the source file has changed from the previous run. + +- ``foreign_fingerprints`` - *list of string* - is a list of SHA2-256 hashes of dynamic + libraries that this Cryptol file directly loads. + +- ``include_fingerprints`` - *list of string* - is a list of SHA2-256 hashes of pre-processor + included files that this Cryptol files directly includes. + +- ``docstring_result`` - *boolean* - is ``true`` when ``:check-docstrings`` + previously succeeded for this module and ``false`` when it previously + failed. It will be missing if tests were never run on this module. + +.. code:: toml + + version = 1 + + [[modules]] + fingerprint = "2f671b21f2933a006b6a843c7f281388e6b8227f9944b111f87711dc9ca8448f" + foreign_fingerprints = [] + include_fingerprints = [] + memory = "Cryptol" + + [[modules]] + docstring_result = true + file = "/path/to/project/Id.cry" + fingerprint = "a9e6f7a4b65ead6bd8e27442717d6b0dc54afc73e34b18c32f005ceb7a8f3c34" + foreign_fingerprints = [ "c7767a13281a56631c72b9b6f69a17746dc02213e7f2b24a8a4a6fe7afd9ee0a" ] + include_fingerprints = [] + + [[modules]] + docstring_result = true + file = "/path/to/project/Main.cry" + fingerprint = "6b36f965ebb1a68cf76d689a966806ec879540aa6576a76c1aaa7705a4af09d5" + foreign_fingerprints = [] + include_fingerprints = [] diff --git a/docs/RefMan/RefMan.rst b/docs/RefMan/RefMan.rst index 02fa7eabf..3d4f3d837 100644 --- a/docs/RefMan/RefMan.rst +++ b/docs/RefMan/RefMan.rst @@ -13,4 +13,5 @@ Cryptol Reference Manual TypeDeclarations Modules FFI + Project diff --git a/examples/AE.cry b/examples/AE.cry index 1ac25e774..333e4b051 100644 --- a/examples/AE.cry +++ b/examples/AE.cry @@ -5,6 +5,7 @@ Implementation of the algorithms from the paper "Automated Analysis and Synthesis of Authenticated Encryption Schemes" by Viet Tung Hoang, Jonathan Katz, and Alex J. Malozemoff */ +module AE where parameter type A : * // State type diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 63c91bb39..f9a26a1bc 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -12,8 +12,8 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-} +{-# Language DisambiguateRecordFields #-} {-# LANGUAGE BlockArguments #-} module Cryptol.ModuleSystem.Base where @@ -41,6 +41,7 @@ import System.FilePath ( addExtension ) import qualified System.IO.Error as IOE import qualified Data.Map as Map +import qualified Data.Map.Strict as MapS import Prelude () import Prelude.Compat hiding ( (<>) ) @@ -82,7 +83,7 @@ import qualified Cryptol.Backend.FFI.Error as FFI import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName , preludeReferenceName, interactiveName, modNameChunks - , modNameToNormalModName, Namespace(NSModule) ) + , modNamesMatch, Namespace(NSModule) ) import Cryptol.Utils.PP (pretty, pp, hang, vcat, ($$), (<+>), (<.>), colon) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Logger(logPutStrLn, logPrint) @@ -133,7 +134,7 @@ renameImpNameInCurrentEnv (P.ImpNested pname) = fail ("Undefined submodule name: " ++ show (pp pname)) _:_:_ -> do fail ("Ambiguous submodule name: " ++ show (pp pname)) - [name] -> pure (P.ImpNested name) + [n] -> pure (P.ImpNested n) -- NoPat ----------------------------------------------------------------------- @@ -159,7 +160,8 @@ expandPropGuards a = -- Returns a fingerprint of the module, and a set of dependencies due -- to `include` directives. parseModule :: - ModulePath -> ModuleM (Fingerprint, Set FilePath, [P.Module PName]) + ModulePath -> + ModuleM (Fingerprint, MapS.Map FilePath Fingerprint, [P.Module PName]) parseModule path = do getBytes <- getByteReader @@ -175,13 +177,15 @@ parseModule path = do | IOE.isDoesNotExistError exn -> cantFindFile p | otherwise -> otherIOError p exn InMem p _ -> panic "parseModule" - [ "IOError for in-memory contetns???" + [ "IOError for in-memory contents???" , "Label: " ++ show p , "Exception: " ++ show exn ] + let fp = fingerprint bytes txt <- case decodeUtf8' bytes of - Right txt -> return $! (T.replace "\r\n" "\n" txt) - Left e -> badUtf8 path e + Right txt -> return $! T.replace "\r\n" "\n" txt + Left e -> badUtf8 path fp e + let cfg = P.defaultConfig { P.cfgSource = case path of @@ -192,8 +196,7 @@ parseModule path = do case P.parseModule cfg txt of Right pms -> - do let fp = fingerprint bytes - (pm1,deps) <- + do (pm1,deps) <- case path of InFile p -> do r <- getByteReader @@ -203,7 +206,7 @@ parseModule path = do case mb of Right ok -> pure ok Left err -> noIncludeErrors err - pure (mo, Set.unions d) + pure (mo, MapS.unions d) {- We don't do "include" resolution for in-memory files because at the moment the include resolution pass requires @@ -211,7 +214,7 @@ parseModule path = do looking for other inlcude files. This could be generalized, but we can do it once we have a concrete use case as it would help guide the design. -} - InMem {} -> pure (pms, Set.empty) + InMem {} -> pure (pms, MapS.empty) {- case path of @@ -220,7 +223,7 @@ parseModule path = do --} fp `seq` return (fp, deps, pm1) - Left err -> moduleParseError path err + Left err -> moduleParseError path fp err -- Top Level Modules and Signatures -------------------------------------------- @@ -248,7 +251,8 @@ loadModuleByPath eval path = withPrependedSearchPath [ takeDirectory path ] $ do case lookupTCEntity n env of -- loadModule will calculate the canonical path again Nothing -> - doLoadModule eval False (FromModule n) (InFile foundPath) fp deps pm + loadModuleAndDeps eval False + (FromModule n) (InFile foundPath) fp deps pm Just lm | path' == loaded -> return (lmData lm) | otherwise -> duplicateModuleName n path' loaded @@ -267,25 +271,38 @@ loadModuleFrom quiet isrc = do path <- findModule n errorInFile path $ do (fp, deps, pms) <- parseModule path - ms <- mapM (doLoadModule True quiet isrc path fp deps) pms + ms <- mapM (loadModuleAndDeps True quiet isrc path fp deps) pms return (path,last ms) -- | Load dependencies, typecheck, and add to the eval environment. -doLoadModule :: +loadModuleAndDeps :: Bool {- ^ evaluate declarations in the module -} -> Bool {- ^ quiet mode: true suppresses the "loading module" message -} -> ImportSource -> ModulePath -> Fingerprint -> - Set FilePath {- ^ `include` dependencies -} -> + MapS.Map FilePath Fingerprint {- ^ `include` dependencies -} -> P.Module PName -> ModuleM T.TCTopEntity -doLoadModule eval quiet isrc path fp incDeps pm0 = +loadModuleAndDeps eval quiet isrc path fp incDeps pm0 = loading isrc $ do let pm = addPrelude pm0 impDeps <- loadDeps pm + fst <$> doLoadModule eval quiet isrc path fp incDeps pm impDeps - let what = case P.mDef pm of +-- | Typecheck and add to the eval environment. +doLoadModule :: + Bool {- ^ evaluate declarations in the module -} -> + Bool {- ^ quiet mode: true suppresses the "loading module" message -} -> + ImportSource -> + ModulePath -> + Fingerprint -> + MapS.Map FilePath Fingerprint {- ^ `include` dependencies -} -> + P.Module PName -> + Set ModName -> + ModuleM (T.TCTopEntity, FileInfo) +doLoadModule eval quiet isrc path fp incDeps pm impDeps = + do let what = case P.mDef pm of P.InterfaceModule {} -> "interface module" _ -> "module" @@ -315,7 +332,7 @@ doLoadModule eval quiet isrc path fp incDeps pm0 = let fi = fileInfo fp incDeps impDeps foreignSrc loadedModule path fi nameEnv foreignSrc tcm - return tcm + return (tcm, fi) where evalForeign tcm @@ -467,10 +484,26 @@ findDepsOfModule m = findDepsOf mpath findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo) -findDepsOf mpath = +findDepsOf mpath' = + do mpath <- case mpath' of + InFile file -> InFile <$> io (canonicalizePath file) + InMem {} -> pure mpath' + (fi, _) <- parseWithDeps mpath + pure (mpath, fi) + +{- | Parse the given module path and find its dependencies. +The reason we return a list here, is that sometime files may +contain multiple modules (e.g., due to desugaring `parameter` blocks +in functors. -} +parseWithDeps :: + ModulePath -> + ModuleM (FileInfo, [(Module PName, [ImportSource])]) +parseWithDeps mpath = do (fp, incs, ms) <- parseModule mpath - let (anyF,imps) = mconcat (map (findDeps' . addPrelude) ms) - fdeps <- if getAny anyF + let ms' = map addPrelude ms + depss = map findDeps' ms' + let (anyF,imps) = mconcat depss + fpath <- if getAny anyF then do mb <- io case mpath of InFile path -> foreignLibPath path InMem {} -> pure Nothing @@ -480,13 +513,13 @@ findDepsOf mpath = Map.singleton fpath exists else pure Map.empty pure - ( mpath - , FileInfo + ( FileInfo { fiFingerprint = fp , fiIncludeDeps = incs , fiImportDeps = Set.fromList (map importedModule (appEndo imps [])) - , fiForeignDeps = fdeps + , fiForeignDeps = fpath } + , zip ms' $ map ((`appEndo` []) . snd) depss ) -- | Find the set of top-level modules imported by a module. @@ -622,8 +655,7 @@ checkModule isrc m = do -- check that the name of the module matches expectations let nm = importedModule isrc - unless (modNameToNormalModName nm == - modNameToNormalModName (thing (P.mName m))) + unless (modNamesMatch nm (thing (P.mName m))) (moduleNameMismatch nm (mName m)) -- remove pattern bindings diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index e37785b62..db5e4d114 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -360,7 +360,7 @@ focusedEnv me = -- | The location of a module data ModulePath = InFile FilePath | InMem String ByteString -- ^ Label, content - deriving (Show, Generic, NFData) + deriving (Show, Read, Generic, NFData) -- | In-memory things are compared by label. instance Eq ModulePath where @@ -426,11 +426,18 @@ getLoadedEntities lm = getLoadedModules :: LoadedModules -> [LoadedModule] getLoadedModules x = lmLoadedParamModules x ++ lmLoadedModules x +getLoadedField :: Ord a => + (forall b. LoadedModuleG b -> a) -> LoadedModules -> Set a +getLoadedField f lm = Set.fromList + $ map f (lmLoadedModules lm) + ++ map f (lmLoadedParamModules lm) + ++ map f (lmLoadedSignatures lm) + getLoadedNames :: LoadedModules -> Set ModName -getLoadedNames lm = Set.fromList - $ map lmName (lmLoadedModules lm) - ++ map lmName (lmLoadedParamModules lm) - ++ map lmName (lmLoadedSignatures lm) +getLoadedNames = getLoadedField lmName + +getLoadedIds :: LoadedModules -> Set String +getLoadedIds = getLoadedField lmModuleId instance Semigroup LoadedModules where l <> r = LoadedModules @@ -503,6 +510,10 @@ isLoaded (ImpNested nn) lm = any (check . lmModule) (getLoadedModules lm) Map.member nn (T.mSubmodules m) || any check (T.mFunctors m) +isLoadedStrict :: ImpName Name -> String -> LoadedModules -> Bool +isLoadedStrict mn modId lm = + isLoaded mn lm && modId `Set.member` getLoadedIds lm + -- | Is this a loaded parameterized module. isLoadedParamMod :: ImpName Name -> LoadedModules -> Bool isLoadedParamMod (ImpTop mn) lm = any ((mn ==) . lmName) (lmLoadedParamModules lm) @@ -568,13 +579,20 @@ lookupTCEntity m env = -- | Try to find a previously loaded module lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule -lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules +lookupModule mn = lookupModuleWith ((mn ==) . lmName) + +lookupModuleWith :: (LoadedModule -> Bool) -> ModuleEnv -> Maybe LoadedModule +lookupModuleWith p me = + search lmLoadedModules `mplus` search lmLoadedParamModules where - search how = List.find ((mn ==) . lmName) (how (meLoadedModules me)) + search how = List.find p (how (meLoadedModules me)) lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature -lookupSignature mn me = - List.find ((mn ==) . lmName) (lmLoadedSignatures (meLoadedModules me)) +lookupSignature mn = lookupSignatureWith ((mn ==) . lmName) + +lookupSignatureWith :: + (LoadedSignature -> Bool) -> ModuleEnv -> Maybe LoadedSignature +lookupSignatureWith p me = List.find p (lmLoadedSignatures (meLoadedModules me)) addLoadedSignature :: ModulePath -> String -> @@ -583,7 +601,7 @@ addLoadedSignature :: ModName -> T.ModParamNames -> LoadedModules -> LoadedModules addLoadedSignature path ident fi nameEnv nm si lm - | isLoaded (ImpTop nm) lm = lm + | isLoadedStrict (ImpTop nm) ident lm = lm | otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm } where loaded = LoadedModule @@ -605,7 +623,7 @@ addLoadedModule :: Maybe ForeignSrc -> T.Module -> LoadedModules -> LoadedModules addLoadedModule path ident fi nameEnv fsrc tm lm - | isLoaded (ImpTop (T.mName tm)) lm = lm + | isLoadedStrict (ImpTop (T.mName tm)) ident lm = lm | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded : lmLoadedParamModules lm } | otherwise = lm { lmLoadedModules = @@ -640,15 +658,16 @@ removeLoadedModule rm lm = data FileInfo = FileInfo { fiFingerprint :: Fingerprint - , fiIncludeDeps :: Set FilePath + , fiIncludeDeps :: Map FilePath Fingerprint , fiImportDeps :: Set ModName , fiForeignDeps :: Map FilePath Bool + -- ^ The bool indicates if the library for the foreign import exists. } deriving (Show,Generic,NFData) fileInfo :: Fingerprint -> - Set FilePath -> + Map FilePath Fingerprint -> Set ModName -> Maybe ForeignSrc -> FileInfo diff --git a/src/Cryptol/ModuleSystem/Fingerprint.hs b/src/Cryptol/ModuleSystem/Fingerprint.hs index 6439ec9dd..1f17e212e 100644 --- a/src/Cryptol/ModuleSystem/Fingerprint.hs +++ b/src/Cryptol/ModuleSystem/Fingerprint.hs @@ -14,14 +14,17 @@ module Cryptol.ModuleSystem.Fingerprint ) where import Control.DeepSeq (NFData (rnf)) -import Crypto.Hash.SHA1 (hash) -import Data.ByteString (ByteString) import Control.Exception (try) +import Control.Monad ((<$!>)) +import Crypto.Hash.SHA256 (hash) +import Data.ByteString (ByteString) +import Data.Char (intToDigit, digitToInt, isHexDigit) import qualified Data.ByteString as B -import qualified Data.Vector as Vector +import qualified Toml +import qualified Toml.Schema as Toml newtype Fingerprint = Fingerprint ByteString - deriving (Eq, Show) + deriving (Eq, Ord, Show, Read) instance NFData Fingerprint where rnf (Fingerprint fp) = rnf fp @@ -31,21 +34,34 @@ fingerprint :: ByteString -> Fingerprint fingerprint = Fingerprint . hash -- | Attempt to compute the fingerprint of the file at the given path. --- Returns 'Nothing' in the case of an error. -fingerprintFile :: FilePath -> IO (Maybe Fingerprint) +-- Returns 'Left' in the case of an error. +fingerprintFile :: FilePath -> IO (Either IOError Fingerprint) fingerprintFile path = do res <- try (B.readFile path) - return $! - case res :: Either IOError ByteString of - Left{} -> Nothing - Right b -> Just $! fingerprint b + return $! fingerprint <$!> (res :: Either IOError ByteString) fingerprintHexString :: Fingerprint -> String fingerprintHexString (Fingerprint bs) = B.foldr hex "" bs where - digits = Vector.fromList "0123456789ABCDEF" - digit x = digits Vector.! fromIntegral x - hex b cs = let (x,y) = divMod b 16 - in digit x : digit y : cs + hex b cs = let (x,y) = divMod (fromIntegral b) 16 + in intToDigit x : intToDigit y : cs + +fingerprintFromHexString :: String -> Maybe Fingerprint +fingerprintFromHexString str = Fingerprint . B.pack <$> go str + where + go [] = Just [] + go (x:y:z) + | isHexDigit x + , isHexDigit y + = (fromIntegral (digitToInt x * 16 + digitToInt y):) <$> go z + go _ = Nothing +instance Toml.ToValue Fingerprint where + toValue = Toml.toValue . fingerprintHexString +instance Toml.FromValue Fingerprint where + fromValue x = + do str <- Toml.fromValue x + case fingerprintFromHexString str of + Nothing -> Toml.failAt (Toml.valueAnn x) "malformed fingerprint hex-string" + Just fp -> pure fp diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index 90e1193dd..dcd34dfee 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -26,6 +26,7 @@ import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Name (FreshM(..),Supply) import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning()) import Cryptol.ModuleSystem.NamingEnv(NamingEnv) +import Cryptol.ModuleSystem.Fingerprint(Fingerprint) import qualified Cryptol.Parser as Parser import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Panic (panic) @@ -94,11 +95,11 @@ data ModuleError -- ^ Unable to find the module given, tried looking in these paths | CantFindFile FilePath -- ^ Unable to open a file - | BadUtf8 ModulePath UnicodeException + | BadUtf8 ModulePath Fingerprint UnicodeException -- ^ Bad UTF-8 encoding in while decoding this file | OtherIOError FilePath IOException -- ^ Some other IO error occurred while reading this file - | ModuleParseError ModulePath Parser.ParseError + | ModuleParseError ModulePath Fingerprint Parser.ParseError -- ^ Generated this parse error when parsing the file for module m | RecursiveModules [ImportSource] -- ^ Recursive module group discovered @@ -124,7 +125,7 @@ data ModuleError | ErrorInFile ModulePath ModuleError -- ^ This is just a tag on the error, indicating the file containing it. -- It is convenient when we had to look for the module, and we'd like - -- to communicate the location of pthe problematic module to the handler. + -- to communicate the location of the problematic module to the handler. deriving (Show) @@ -132,9 +133,9 @@ instance NFData ModuleError where rnf e = case e of ModuleNotFound src path -> src `deepseq` path `deepseq` () CantFindFile path -> path `deepseq` () - BadUtf8 path ue -> rnf (path, ue) + BadUtf8 path fp ue -> rnf (path, fp, ue) OtherIOError path exn -> path `deepseq` exn `seq` () - ModuleParseError source err -> source `deepseq` err `deepseq` () + ModuleParseError source fp err -> rnf (source, fp, err) RecursiveModules mods -> mods `deepseq` () RenamerErrors src errs -> src `deepseq` errs `deepseq` () NoPatErrors src errs -> src `deepseq` errs `deepseq` () @@ -165,7 +166,7 @@ instance PP ModuleError where text "[error]" <+> text "can't find file:" <+> text path - BadUtf8 path _ue -> + BadUtf8 path _fp _ue -> text "[error]" <+> text "bad utf-8 encoding:" <+> pp path @@ -174,7 +175,7 @@ instance PP ModuleError where text "IO error while loading file:" <+> text path <.> colon) 4 (text (show exn)) - ModuleParseError _source err -> Parser.ppError err + ModuleParseError _source _fp err -> Parser.ppError err RecursiveModules mods -> hang (text "[error] module imports form a cycle:") @@ -217,15 +218,15 @@ moduleNotFound name paths = ModuleT (raise (ModuleNotFound name paths)) cantFindFile :: FilePath -> ModuleM a cantFindFile path = ModuleT (raise (CantFindFile path)) -badUtf8 :: ModulePath -> UnicodeException -> ModuleM a -badUtf8 path ue = ModuleT (raise (BadUtf8 path ue)) +badUtf8 :: ModulePath -> Fingerprint -> UnicodeException -> ModuleM a +badUtf8 path fp ue = ModuleT (raise (BadUtf8 path fp ue)) otherIOError :: FilePath -> IOException -> ModuleM a otherIOError path exn = ModuleT (raise (OtherIOError path exn)) -moduleParseError :: ModulePath -> Parser.ParseError -> ModuleM a -moduleParseError path err = - ModuleT (raise (ModuleParseError path err)) +moduleParseError :: ModulePath -> Fingerprint -> Parser.ParseError -> ModuleM a +moduleParseError path fp err = + ModuleT (raise (ModuleParseError path fp err)) recursiveModules :: [ImportSource] -> ModuleM a recursiveModules loaded = ModuleT (raise (RecursiveModules loaded)) @@ -274,6 +275,9 @@ errorInFile file (ModuleT m) = ModuleT (m `handle` h) ErrorInFile {} -> e _ -> ErrorInFile file e +tryModule :: ModuleM a -> ModuleM (Either ModuleError a) +tryModule (ModuleT m) = ModuleT (handle (Right <$> m) (pure . Left)) + -- Warnings -------------------------------------------------------------------- data ModuleWarning @@ -435,6 +439,11 @@ isLoaded mn = do env <- ModuleT get pure (MEnv.isLoaded (T.ImpTop mn) (meLoadedModules env)) +isLoadedStrict :: P.ModName -> ModulePath -> ModuleM Bool +isLoadedStrict mn mpath = + do env <- ModuleT get + pure (MEnv.isLoadedStrict (T.ImpTop mn) (modulePathLabel mpath) (meLoadedModules env)) + loadingImport :: Located P.Import -> ModuleM a -> ModuleM a loadingImport = loading . FromImport diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs index c04d482d1..3d761b6d0 100644 --- a/src/Cryptol/Parser/NoInclude.hs +++ b/src/Cryptol/Parser/NoInclude.hs @@ -20,8 +20,8 @@ import Control.DeepSeq import qualified Control.Exception as X import qualified Control.Monad.Fail as Fail -import Data.Set(Set) -import qualified Data.Set as Set +import Data.Map.Strict(Map) +import qualified Data.Map.Strict as Map import Data.ByteString (ByteString) import Data.Either (partitionEithers) import Data.Text(Text) @@ -38,12 +38,13 @@ import Cryptol.Parser.AST import Cryptol.Parser.LexerUtils (Config(..),defaultConfig) import Cryptol.Parser.ParserUtils import Cryptol.Parser.Unlit (guessPreProc) +import Cryptol.ModuleSystem.Fingerprint removeIncludesModule :: (FilePath -> IO ByteString) -> FilePath -> Module PName -> - IO (Either [IncludeError] (Module PName, Set FilePath)) + IO (Either [IncludeError] (Module PName, Map FilePath Fingerprint)) removeIncludesModule reader modPath m = runNoIncM reader modPath (noIncludeModule m) @@ -82,7 +83,7 @@ newtype NoIncM a = M IO )) a } -type Deps = Set FilePath +type Deps = Map FilePath Fingerprint data Env = Env { envSeen :: [Located FilePath] -- ^ Files that have been loaded @@ -106,7 +107,7 @@ runNoIncM reader sourcePath m = , envIncPath = incPath , envFileReader = reader } - Set.empty + Map.empty pure do ok <- mb pure (ok,s) @@ -135,10 +136,10 @@ fromIncPath path do Env { .. } <- ask return (envIncPath path) -addDep :: FilePath -> NoIncM () -addDep path = M +addDep :: FilePath -> Fingerprint -> NoIncM () +addDep path fp = M do s <- get - let s1 = Set.insert path s + let s1 = Map.insert path fp s s1 `seq` set s1 @@ -247,12 +248,13 @@ readInclude :: Located FilePath -> NoIncM Text readInclude path = do readBytes <- envFileReader <$> M ask file <- fromIncPath (thing path) - addDep file sourceBytes <- readBytes file `failsWith` handler sourceText <- X.evaluate (T.decodeUtf8' sourceBytes) `failsWith` handler case sourceText of Left encodingErr -> M (raise [IncludeDecodeFailed path encodingErr]) - Right txt -> return txt + Right txt -> do + addDep file (fingerprint sourceBytes) + return txt where handler :: X.IOException -> NoIncM a handler _ = includeFailed path diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index b5d92f81f..c3658fa99 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -14,6 +14,7 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE LambdaCase #-} -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.Parser.ParserUtils where @@ -31,6 +32,7 @@ import Data.Text(Text) import qualified Data.Text as T import qualified Data.Map as Map import Text.Read(readMaybe) +import Data.Foldable (for_) import GHC.Generics (Generic) import Control.DeepSeq @@ -47,7 +49,7 @@ import Cryptol.Parser.Utils (translateExprToNumT,widthIdent) import Cryptol.Utils.Ident( packModName,packIdent,modNameChunks , identAnonArg, identAnonIfaceMod , modNameArg, modNameIfaceMod - , modNameToText, modNameIsNormal + , modNameToText, mainModName, modNameIsNormal , modNameToNormalModName , unpackIdent, isUpperIdent ) @@ -73,6 +75,8 @@ parse cfg p cs = case unP p cfg eofPos S { sPrevTok = Nothing newtype ParseM a = P { unP :: Config -> Position -> S -> Either ParseError (a,S) } +askConfig :: ParseM Config +askConfig = P \cfg _ s -> Right (cfg, s) lexerP :: (Located Token -> ParseM a) -> ParseM a lexerP k = P $ \cfg p s -> @@ -1203,10 +1207,22 @@ mkIfacePropSyn mbDoc d = -- | Make an unnamed module---gets the name @Main@. mkAnonymousModule :: [TopDecl PName] -> ParseM [Module PName] -mkAnonymousModule = mkTopMods Nothing - . mkModule Located { srcRange = emptyRange - , thing = mkModName [T.pack "Main"] - } +mkAnonymousModule ds = + do for_ ds \case + DParamDecl l _ -> mainParamError l + DModParam p -> mainParamError (srcRange (mpSignature p)) + DInterfaceConstraint _ ps -> mainParamError (srcRange ps) + _ -> pure () + src <- cfgSource <$> askConfig + mkTopMods Nothing $ + mkModule Located + { srcRange = emptyRange + , thing = mainModName src + } + ds + where + mainParamError l = errorMessage l + ["Unnamed module cannot be parameterized"] -- | Make a module which defines a functor instance. mkModuleInstanceAnon :: Located ModName -> diff --git a/src/Cryptol/Project.hs b/src/Cryptol/Project.hs new file mode 100644 index 000000000..6b601afee --- /dev/null +++ b/src/Cryptol/Project.hs @@ -0,0 +1,205 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE LambdaCase #-} +module Cryptol.Project + ( Config(..) + , loadConfig + , ScanStatus(..) + , ChangeStatus(..) + , InvalidStatus(..) + , Parsed + , loadProject + , depMap + ) where + +import Control.Monad (void) +import Data.Foldable +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Traversable +import System.Directory +import System.FilePath as FP + +import Cryptol.ModuleSystem.Base as M +import Cryptol.ModuleSystem.Env +import Cryptol.ModuleSystem.Fingerprint +import Cryptol.ModuleSystem.Monad as M +import Cryptol.Project.Config +import Cryptol.Project.Cache +import Cryptol.Project.Monad +import qualified Cryptol.Parser.AST as P +import Cryptol.Parser.Position (Located(..)) + +-- | Load a project. +-- Returns information about the modules that are part of the project. +loadProject :: Bool -> Config -> M.ModuleM (Map CacheModulePath FullFingerprint, Map ModulePath ScanStatus, Map CacheModulePath (Maybe Bool)) +loadProject refresh cfg = + do (fps, statuses, out) <- runLoadM refresh cfg (for_ (modules cfg) scanPath >> getOldDocstringResults) + let deps = depMap [p | Scanned _ _ ps <- Map.elems statuses, p <- ps] + let needLoad = [thing (P.mName m) | Scanned Changed _ ps <- Map.elems statuses, (m, _) <- ps] + let order = loadOrder deps needLoad + + let modDetails = Map.fromList [(thing (P.mName m), (m, mp, fp)) | (mp, Scanned _ fp ps) <- Map.assocs statuses, (m, _) <- ps] + + let fingerprints = Map.fromList [(path, moduleFingerprint ffp) | (CacheInFile path, ffp) <- Map.assocs fps] + + for_ order \name -> + let (m, path, fp) = modDetails Map.! name in + -- XXX: catch modules that don't load? + doLoadModule + True {- eval -} + False {- quiet -} + (FromModule name) + path + (moduleFingerprint fp) + fingerprints + m + (Map.findWithDefault mempty name deps) + + let oldResults = + case out of + Left{} -> mempty + Right x -> x + pure (fps, statuses, oldResults) + + +-------------------------------------------------------------------------------- + +-- | Process all .cry files in the given path. +scanPath :: FilePath -> LoadM any () +scanPath path = + tryLoadM (doIO (doesDirectoryExist path)) >>= + \case + Left {} -> pure () + + Right True -> + tryLoadM (doIO (listDirectory path)) >>= + \case + Left {} -> pure () + Right entries -> + for_ entries \entry -> scanPath (path FP. entry) + + Right False -> + -- XXX: This should probably handle other extenions + -- (literate Cryptol) + case takeExtension path of + ".cry" -> void (tryLoadM (scanFromPath path)) + -- XXX: failure: file disappeared. + _ -> pure () + + +-- | Process a particular file path. +-- Fails if we can't find the module at this path. +scanFromPath :: FilePath -> LoadM Err ScanStatus +scanFromPath fpath = + liftCallback (withPrependedSearchPath [takeDirectory fpath]) + do foundFPath <- doModule (M.findFile fpath) + mpath <- doIO (InFile <$> canonicalizePath foundFPath) + scan mpath + + +-- | Process the given module, and return information about what happened. +-- Also, saves the status of the module path. +scan :: ModulePath -> LoadM any ScanStatus +scan mpath = + + tryIt $ + do mbStat <- getStatus mpath + case mbStat of + Just status -> pure status + + Nothing -> + do (newFp,parsed) <- doParse mpath + mbOldFP <- getCachedFingerprint mpath + let needLoad = mbOldFP /= Just newFp + let deps = [ dep + | (_,ds) <- parsed + , dep@(_,otherPath) <- ds + , mpath /= otherPath + ] + mb <- checkDeps False deps + case mb of + Left (a,b) -> addScanned mpath (Invalid (InvalidDep a b)) + Right depChanges -> + do let ch = if needLoad || depChanges + then Changed else Unchanged + addScanned mpath (Scanned ch newFp parsed) + where + tryIt m = + do mb <- tryLoadM m + case mb of + Left err -> addScanned mpath (Invalid (InvalidModule err)) + Right a -> pure a + + +-- | Parse a module. +doParse :: ModulePath -> LoadM Err (FullFingerprint, Parsed) +doParse mpath = + do lab <- getModulePathLabel mpath + lPutStrLn ("Scanning " ++ lab) + + (parsed, newFp) <- + doModule + do (fi, parsed) <- parseWithDeps mpath + foreignFps <- getForeignFps (fiForeignDeps fi) + pure ( parsed + , FullFingerprint + { moduleFingerprint = fiFingerprint fi + , includeFingerprints = fiIncludeDeps fi + , foreignFingerprints = foreignFps + } + ) + addFingerprint mpath newFp + ps <- forM parsed \(m,ds) -> + do paths <- mapM findModule' ds + pure (m, zip ds paths) + pure (newFp, ps) + +-- | Get the fingerprints for external libraries. +getForeignFps :: Map FilePath Bool -> ModuleM (Set Fingerprint) +getForeignFps fsrcPaths = + Set.fromList <$> + let foundFiles = Map.keys (Map.filter id fsrcPaths) in + for foundFiles \fsrcPath -> + M.io (fingerprintFile fsrcPath) >>= + \case + Left ioe -> otherIOError fsrcPath ioe + Right fp -> pure fp + +-- | Scan the dependencies of a module. +checkDeps :: + Bool {- ^ Should we load the dependencies -} -> + [(ImportSource,ModulePath)] {- ^ The dependencies -} -> + LoadM err (Either (ImportSource,ModulePath) Bool) + -- ^ Returns `Left bad_dep` if one of the dependencies fails to load. + -- Returns `Right changes` if all dependencies were validated correctly. + -- The boolean flag `changes` indicates if any of the dependencies contain + -- changes and so we should also load the main module. +checkDeps shouldLoad ds = + case ds of + [] -> pure (Right shouldLoad) + (imp, mpath) : more -> + do status <- scan mpath + case status of + Invalid {} -> pure (Left (imp,mpath)) + Scanned ch _ _ -> + case ch of + Changed -> checkDeps True more + Unchanged -> checkDeps shouldLoad more + + +depMap :: Parsed -> Map P.ModName (Set P.ModName) +depMap xs = Map.fromList [(thing (P.mName k), Set.fromList [importedModule i | (i, _) <- v]) | (k, v) <- xs] + +loadOrder :: Map P.ModName (Set P.ModName) -> [P.ModName] -> [P.ModName] +loadOrder deps roots0 = snd (go Set.empty roots0) [] + where + go seen mms = + case mms of + [] -> (seen, id) + m : ms + | Set.member m seen -> go seen ms + | (seen1, out1) <- go (Set.insert m seen) (Set.toList (Map.findWithDefault mempty m deps)) + , (seen2, out2) <- go seen1 ms + -> (seen2, out1 . (m:) . out2) diff --git a/src/Cryptol/Project/Cache.hs b/src/Cryptol/Project/Cache.hs new file mode 100644 index 000000000..e9f251bdc --- /dev/null +++ b/src/Cryptol/Project/Cache.hs @@ -0,0 +1,126 @@ +{-# Language OverloadedStrings, BlockArguments #-} +module Cryptol.Project.Cache where + +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set +import qualified Data.Text.IO as Text +import Data.Set (Set) +import System.Directory +import System.FilePath as FP +import System.IO.Error +import qualified Toml +import qualified Toml.Schema as Toml +import Cryptol.ModuleSystem.Fingerprint ( Fingerprint ) +import Cryptol.ModuleSystem.Env + +-- | The load cache. This is what persists across invocations. +newtype LoadCache = LoadCache + { cacheModules :: Map CacheModulePath CacheEntry + } + deriving (Show, Read) + +toCacheModulePath :: ModulePath -> CacheModulePath +toCacheModulePath mpath = + case mpath of + InMem x _ -> CacheInMem x + InFile x -> CacheInFile x + +data CacheModulePath + = CacheInMem String -- ^ module name + | CacheInFile FilePath -- ^ absolute file path + deriving (Show, Read, Ord, Eq) + +instance Toml.ToValue LoadCache where + toValue = Toml.defaultTableToValue + +instance Toml.ToTable LoadCache where + toTable x = Toml.table [ + "version" Toml..= (1 :: Int), -- increase this to invalidate old files + "modules" Toml..= [ + Toml.table $ [ + case k of + CacheInFile a -> "file" Toml..= a + CacheInMem a -> "memory" Toml..= a, + "fingerprint" Toml..= moduleFingerprint fp, + "foreign_fingerprints" Toml..= Set.toList (foreignFingerprints fp), + "include_fingerprints" Toml..= [ + Toml.table [ + "file" Toml..= k1, + "fingerprint" Toml..= v1 + ] + | (k1, v1) <- Map.assocs (includeFingerprints fp) + ] + ] ++ + [ "docstring_result" Toml..= result + | Just result <- [cacheDocstringResult v] + ] + | (k,v) <- Map.assocs (cacheModules x) + , let fp = cacheFingerprint v + ]] + +instance Toml.FromValue LoadCache where + fromValue = Toml.parseTableFromValue + do 1 <- Toml.reqKey "version" :: Toml.ParseTable l Int + kvs <- Toml.reqKeyOf "modules" + $ Toml.listOf \ _ix -> + Toml.parseTableFromValue + do k <- Toml.pickKey [ + Toml.Key "memory" (fmap CacheInMem . Toml.fromValue), + Toml.Key "file" (fmap CacheInFile . Toml.fromValue) + ] + fp <- Toml.reqKey "fingerprint" + foreigns <- Toml.reqKey "foreign_fingerprints" + includes <- Toml.reqKeyOf "include_fingerprints" + $ Toml.listOf \ _ix -> + Toml.parseTableFromValue + $ (,) <$> Toml.reqKey "file" + <*> Toml.reqKey "fingerprint" + checkResult <- Toml.optKey "docstring_result" + pure (k, CacheEntry + { cacheFingerprint = FullFingerprint + { moduleFingerprint = fp + , foreignFingerprints = Set.fromList foreigns + , includeFingerprints = Map.fromList includes + } + , cacheDocstringResult = checkResult + }) + pure LoadCache { + cacheModules = Map.fromList kvs + } + +data CacheEntry = CacheEntry + { cacheFingerprint :: FullFingerprint + , cacheDocstringResult :: Maybe Bool + } + deriving (Show, Read) + +-- | The full fingerprint hashes the module, but +-- also the contents of included files and foreign libraries. +data FullFingerprint = FullFingerprint + { moduleFingerprint :: Fingerprint + , includeFingerprints :: Map FilePath Fingerprint + , foreignFingerprints :: Set Fingerprint + } + deriving (Eq, Show, Read) + +-- XXX: This should probably be a parameter +metaDir, loadCachePath :: FilePath +metaDir = ".cryproject" +loadCachePath = metaDir FP. "loadcache.toml" + +emptyLoadCache :: LoadCache +emptyLoadCache = LoadCache { cacheModules = mempty } + +loadLoadCache :: IO LoadCache +loadLoadCache = + do txt <- Text.readFile loadCachePath + case Toml.decode txt of + Toml.Success _ c -> pure c + Toml.Failure _ -> pure emptyLoadCache + `catchIOError` \_ -> pure emptyLoadCache + +saveLoadCache :: LoadCache -> IO () +saveLoadCache cache = + do createDirectoryIfMissing False metaDir + writeFile loadCachePath (show (Toml.encode cache)) diff --git a/src/Cryptol/Project/Config.hs b/src/Cryptol/Project/Config.hs new file mode 100644 index 000000000..d2fa7e9fb --- /dev/null +++ b/src/Cryptol/Project/Config.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE OverloadedStrings #-} +module Cryptol.Project.Config where + +import Data.Maybe (fromMaybe) +import qualified Data.Text.IO as Text +import Toml +import Toml.Schema +import Data.Bifunctor (first) +import System.Directory +import System.FilePath as FP +import System.IO.Error + +import Cryptol.Utils.PP as PP + +data Config = Config + { root :: FilePath + , modules :: [FilePath] + } + +instance FromValue Config where + fromValue = + parseTableFromValue + do mbRoot <- optKey "root" + mbModules <- optKey "modules" + pure Config + { root = fromMaybe "." mbRoot + , modules = fromMaybe ["."] mbModules + } + +data ConfigLoadError = ConfigLoadError FilePath ConfigLoadErrorInfo + +data ConfigLoadErrorInfo + = ConfigParseError [String] + | SetRootFailed IOError + +instance PP ConfigLoadError where + ppPrec _ (ConfigLoadError path info) = + case info of + ConfigParseError errs -> text (unlines errs) + SetRootFailed ioe -> + hang topMsg + 4 (hang "Failed to set project root:" + 4 (text (show ioe))) + where + topMsg = "Error loading project configuration" <+> text path PP.<.> ":" + +-- | Parse project configuration. +loadConfig :: FilePath -> IO (Either ConfigLoadError Config) +loadConfig path = + do isDir <- doesDirectoryExist path + let filePath = if isDir then path FP. "cryproject.toml" else path + -- Use strict IO since we are writing to the same file later + file <- Text.readFile filePath + first (ConfigLoadError filePath) <$> + case decode file of + Failure errs -> pure (Left (ConfigParseError errs)) + Success _warns config -> + first SetRootFailed <$> + tryIOError + do setCurrentDirectory (takeDirectory filePath FP. root config) + pure config diff --git a/src/Cryptol/Project/Monad.hs b/src/Cryptol/Project/Monad.hs new file mode 100644 index 000000000..38d35cd43 --- /dev/null +++ b/src/Cryptol/Project/Monad.hs @@ -0,0 +1,211 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE OverloadedStrings #-} +module Cryptol.Project.Monad + ( LoadM, Err, NoErr + , ScanStatus(..), ChangeStatus(..), InvalidStatus(..), Parsed + , runLoadM + , doModule + , doModuleNonFail + , doIO + , tryLoadM + , liftCallback + , addFingerprint + , addScanned + , getModulePathLabel + , getCachedFingerprint + , findModule' + , getStatus + , getFingerprint + , lPutStrLn + , getOldDocstringResults + ) where + +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Control.Monad.Reader +import Control.Monad.State +import Control.Monad.Except hiding (tryError) +import System.Directory +import System.FilePath (makeRelative) + +import Cryptol.Utils.Ident +import Cryptol.Parser.AST (Module,PName) +import Cryptol.ModuleSystem.Base as M +import Cryptol.ModuleSystem.Monad as M +import Cryptol.ModuleSystem.Env +import Cryptol.Utils.Logger (logPutStrLn) + +import Cryptol.Project.Config +import Cryptol.Project.Cache + +newtype LoadM err a = + LoadM (ReaderT LoadConfig (ExceptT ModuleError (StateT LoadState ModuleM)) a) + deriving (Functor,Applicative,Monad) + +-- | Computations may raise an error +data Err + +-- | Computations may not raise errors +data NoErr + +type Parsed = [ (Module PName, [(ImportSource, ModulePath)]) ] + +data ScanStatus = + Scanned ChangeStatus FullFingerprint Parsed + | Invalid InvalidStatus + deriving Show + +data ChangeStatus = + Changed -- ^ The module, or one of its dependencies changed. + | Unchanged -- ^ The module did not change. + deriving Show + +data InvalidStatus = + InvalidModule ModuleError + -- ^ Error in one of the modules in this file + + | InvalidDep ImportSource ModulePath + -- ^ Error in one of our dependencies + deriving Show + + +data LoadState = LoadState + { findModuleCache :: Map (ModName, [FilePath]) ModulePath + -- ^ Map (module name, search path) -> module path + + , fingerprints :: Map CacheModulePath FullFingerprint + -- ^ Hashes of known things. + + , scanned :: Map ModulePath ScanStatus + -- ^ Information about the proccessed top-level modules. + } + + +-- | Information about the current project. +data LoadConfig = LoadConfig + { canonRoot :: FilePath + -- ^ Path to the project root, cannoicalized. + + , loadCache :: LoadCache + -- ^ The state of the cache before we started loading the project. + } + + +-- | Do an operation in the module monad. +doModuleNonFail :: M.ModuleM a -> LoadM any a +doModuleNonFail m = + do mb <- LoadM (lift (lift (lift (M.tryModule m)))) + case mb of + Left err -> LoadM (throwError err) + Right a -> pure a + +-- | Do an operation in the module monad. +doModule :: M.ModuleM a -> LoadM Err a +doModule = doModuleNonFail + +-- | Do an operation in the IO monad +doIO :: IO a -> LoadM Err a +doIO m = doModule (M.io m) + +tryLoadM :: LoadM Err a -> LoadM any (Either M.ModuleError a) +tryLoadM (LoadM m) = LoadM (tryError m) + +-- Introduced in mtl-2.3.1 which we can't rely upon yet +tryError :: MonadError e m => m a -> m (Either e a) +tryError action = (Right <$> action) `catchError` (pure . Left) + +-- | Print a line +lPutStrLn :: String -> LoadM any () +lPutStrLn msg = doModuleNonFail (withLogger logPutStrLn msg) + +-- | Lift a module level operation to the LoadM monad. +liftCallback :: (forall a. ModuleM a -> ModuleM a) -> LoadM any b -> LoadM Err b +liftCallback f (LoadM m) = + do r <- LoadM ask + s <- LoadM get + (mb,s1) <- doModule (f (runStateT (runExceptT (runReaderT m r)) s)) + LoadM (put s1) + case mb of + Left err -> LoadM (throwError err) + Right a -> pure a + +-- | Run a LoadM computation using the given configuration. +runLoadM :: + Bool {- ^ force a refresh -} -> + Config -> + LoadM NoErr a -> + M.ModuleM (Map CacheModulePath FullFingerprint, Map ModulePath ScanStatus, Either ModuleError a) +runLoadM refresh cfg (LoadM m) = + do loadCfg <- + M.io + do path <- canonicalizePath (root cfg) + cache <- if refresh then pure emptyLoadCache else loadLoadCache + pure LoadConfig { canonRoot = path + , loadCache = cache + } + let loadState = LoadState { findModuleCache = mempty + , fingerprints = mempty + , scanned = mempty + } + (result, s) <- runStateT (runExceptT (runReaderT m loadCfg)) loadState + pure (fingerprints s, scanned s, result) + +addFingerprint :: ModulePath -> FullFingerprint -> LoadM any () +addFingerprint mpath fp = + LoadM + (modify' \ls -> ls { fingerprints = Map.insert (toCacheModulePath mpath) fp (fingerprints ls) }) + + +-- | Add information about the status of a module path. +addScanned :: ModulePath -> ScanStatus -> LoadM any ScanStatus +addScanned mpath status = + do LoadM + (modify' \ls -> ls { scanned = Map.insert mpath status (scanned ls) }) + pure status + + +-- | Get a label for the given module path. +-- Typically used for output. +getModulePathLabel :: ModulePath -> LoadM any String +getModulePathLabel mpath = + case mpath of + InFile p -> LoadM (asks ((`makeRelative` p) . canonRoot)) + InMem l _ -> pure l + + +-- | Get the fingerprint for the given module path. +getCachedFingerprint :: ModulePath -> LoadM any (Maybe FullFingerprint) +getCachedFingerprint mpath = + LoadM (asks (fmap cacheFingerprint . Map.lookup (toCacheModulePath mpath) . cacheModules . loadCache)) + + +-- | Module path for the given import +findModule' :: ImportSource -> LoadM Err ModulePath +findModule' isrc = + do ls <- LoadM get + let mname = modNameToNormalModName (importedModule isrc) + searchPath <- doModule M.getSearchPath + case Map.lookup (mname, searchPath) (findModuleCache ls) of + Just mpath -> pure mpath + Nothing -> + do modLoc <- doModule (findModule mname) + mpath <- case modLoc of + InFile path -> InFile <$> doIO (canonicalizePath path) + InMem l c -> pure (InMem l c) + LoadM $ put ls { findModuleCache = Map.insert (mname, searchPath) + mpath (findModuleCache ls) } + pure mpath + +-- | Check if the given file has beein processed. +getStatus :: ModulePath -> LoadM any (Maybe ScanStatus) +getStatus mpath = LoadM (gets (Map.lookup mpath . scanned)) + +-- | Get the fingerpint for the ginve path, if any. +getFingerprint :: ModulePath -> LoadM any (Maybe FullFingerprint) +getFingerprint mpath = LoadM (gets (Map.lookup (toCacheModulePath mpath) . fingerprints)) + +getOldDocstringResults :: LoadM any (Map CacheModulePath (Maybe Bool)) +getOldDocstringResults = + LoadM (asks (fmap cacheDocstringResult . cacheModules . loadCache)) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index c8fa5d0ed..913f08016 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -55,11 +55,14 @@ module Cryptol.REPL.Command ( , handleCtrlC , sanitize , withRWTempFile + , printModuleWarnings -- To support Notebook interface (might need to refactor) , replParse , liftModuleCmd , moduleCmdResult + + , loadProjectREPL ) where import Cryptol.REPL.Monad @@ -106,6 +109,7 @@ import Cryptol.Utils.PP hiding (()) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.RecordMap import qualified Cryptol.Parser.AST as P +import qualified Cryptol.Project as Proj import qualified Cryptol.Transform.Specialize as S import Cryptol.Symbolic ( ProverCommand(..), QueryType(..) @@ -122,6 +126,7 @@ import Control.Monad.IO.Class(liftIO) import Text.Read (readMaybe) import Control.Applicative ((<|>)) import qualified Data.Set as Set +import qualified Data.Map.Strict as Map import Data.ByteString (ByteString) import qualified Data.ByteString as BS import qualified Data.ByteString.Char8 as BS8 @@ -129,7 +134,6 @@ import Data.Bits (shiftL, (.&.), (.|.)) import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii) import Data.Function (on) import Data.List (intercalate, nub, isPrefixOf) -import qualified Data.Map as Map import Data.Maybe (fromMaybe,mapMaybe,isNothing) import System.Environment (lookupEnv) import System.Exit (ExitCode(ExitSuccess)) @@ -155,6 +159,7 @@ import Prelude.Compat import qualified Data.SBV.Internals as SBV (showTDiff) import Data.Foldable (foldl') +import qualified Cryptol.Project.Cache as Proj @@ -1587,25 +1592,12 @@ getPrimMap :: REPL M.PrimMap getPrimMap = liftModuleCmd M.getPrimMap liftModuleCmd :: M.ModuleCmd a -> REPL a -liftModuleCmd cmd = - do evo <- getEvalOptsAction - env <- getModuleEnv - callStacks <- getCallStacks - tcSolver <- getTCSolver - let minp = - M.ModuleInput - { minpCallStacks = callStacks - , minpEvalOpts = evo - , minpByteReader = BS.readFile - , minpModuleEnv = env - , minpTCSolver = tcSolver - } - moduleCmdResult =<< io (cmd minp) - --- TODO: add filter for my exhaustie prop guards warning here +liftModuleCmd cmd = moduleCmdResult =<< io . cmd =<< getModuleInput -moduleCmdResult :: M.ModuleRes a -> REPL a -moduleCmdResult (res,ws0) = do +-- TODO: add filter for my exhaustive prop guards warning here + +printModuleWarnings :: [M.ModuleWarning] -> REPL () +printModuleWarnings ws0 = do warnDefaulting <- getKnownUser "warnDefaulting" warnShadowing <- getKnownUser "warnShadowing" warnPrefixAssoc <- getKnownUser "warnPrefixAssoc" @@ -1644,6 +1636,10 @@ moduleCmdResult (res,ws0) = do $ ws0 names <- M.mctxNameDisp <$> getFocusedEnv mapM_ (rPrint . runDoc names . pp) ws + +moduleCmdResult :: M.ModuleRes a -> REPL a +moduleCmdResult (res,ws) = do + printModuleWarnings ws case res of Right (a,me') -> setModuleEnv me' >> return a Left err -> @@ -1655,6 +1651,7 @@ moduleCmdResult (res,ws0) = do do setEditPath file return e _ -> return err + names <- M.mctxNameDisp <$> getFocusedEnv raise (ModuleSystemError names e) @@ -1987,7 +1984,7 @@ moduleInfoCmd isFile name mapM_ (\j -> rPutStrLn (" , " ++ f j)) is rPutStrLn " ]" - depList show "includes" (Set.toList (M.fiIncludeDeps fi)) + depList show "includes" (Map.keys (M.fiIncludeDeps fi)) depList (show . show . pp) "imports" (Set.toList (M.fiImportDeps fi)) depList show "foreign" (Map.toList (M.fiForeignDeps fi)) @@ -2194,53 +2191,111 @@ checkDocStringsCmd input pure emptyCommandResult { crSuccess = False } Just mn -> checkModName mn +countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int) +countOutcomes = foldl' countOutcomes1 (0, 0, 0) where + countOutcomes1 (successes, nofences, failures) [] + = (successes, nofences + 1, failures) + countOutcomes1 acc result = foldl' countOutcomes2 acc result - countOutcomes :: [[SubcommandResult]] -> (Int, Int, Int) - countOutcomes = foldl' countOutcomes1 (0, 0, 0) - where - countOutcomes1 (successes, nofences, failures) [] - = (successes, nofences + 1, failures) - countOutcomes1 acc result = foldl' countOutcomes2 acc result - - countOutcomes2 (successes, nofences, failures) result - | crSuccess (srResult result) = (successes + 1, nofences, failures) - | otherwise = (successes, nofences, failures + 1) + countOutcomes2 (successes, nofences, failures) result + | crSuccess (srResult result) = (successes + 1, nofences, failures) + | otherwise = (successes, nofences, failures + 1) - checkModName :: P.ModName -> REPL CommandResult - checkModName mn = - do env <- getModuleEnv - case M.lookupModule mn env of +checkModName :: P.ModName -> REPL CommandResult +checkModName mn = + do env <- getModuleEnv + case M.lookupModule mn env of + Nothing -> + case M.lookupSignature mn env of Nothing -> - case M.lookupSignature mn env of - Nothing -> - do rPutStrLn ("Module " ++ show input ++ " is not loaded") - pure emptyCommandResult { crSuccess = False } - Just{} -> - do rPutStrLn "Skipping docstrings on interface module" - pure emptyCommandResult - - Just fe - | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do - rPutStrLn "Skipping docstrings on parameterized module" + do rPutStrLn ("Module " ++ show mn ++ " is not loaded") + pure emptyCommandResult { crSuccess = False } + Just{} -> + do rPutStrLn "Skipping docstrings on interface module" pure emptyCommandResult + Just fe + | T.isParametrizedModule (M.lmdModule (M.lmData fe)) -> do + rPutStrLn "Skipping docstrings on parameterized module" + pure emptyCommandResult + | otherwise -> do + results <- checkDocStrings fe + let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results] + forM_ results $ \dr -> + unless (null (drFences dr)) $ + do rPutStrLn "" + rPutStrLn ("\nChecking " ++ show (pp (drName dr))) + forM_ (drFences dr) $ \fence -> + forM_ fence $ \line -> do + rPutStrLn "" + rPutStrLn (T.unpack (srInput line)) + rPutStr (srLog line) + rPutStrLn "" + rPutStrLn ("Successes: " ++ show successes ++ ", No fences: " ++ show nofences ++ ", Failures: " ++ show failures) + pure emptyCommandResult { crSuccess = failures == 0 } + +-- | Load a project. +-- Note that this does not update the Cryptol environment, it only updates +-- the project cache. +loadProjectREPL :: Bool -> Proj.Config -> REPL CommandResult +loadProjectREPL refresh cfg = + do minp <- getModuleInput + (res, warnings) <- io $ M.runModuleM minp $ Proj.loadProject refresh cfg + printModuleWarnings warnings + case res of + Left err -> + do names <- M.mctxNameDisp <$> getFocusedEnv + rPrint (pp (ModuleSystemError names err)) + pure emptyCommandResult { crSuccess = False } - | otherwise -> do - results <- checkDocStrings fe - let (successes, nofences, failures) = countOutcomes [concat (drFences r) | r <- results] - - forM_ results $ \dr -> - unless (null (drFences dr)) $ - do rPutStrLn "" - rPutStrLn ("\nChecking " ++ show (pp (drName dr))) - forM_ (drFences dr) $ \fence -> - forM_ fence $ \line -> do - rPutStrLn "" - rPutStrLn (T.unpack (srInput line)) - rPutStr (srLog line) - - rPutStrLn "" - rPutStrLn ("Successes: " ++ show successes ++ ", No fences: " ++ show nofences ++ ", Failures: " ++ show failures) + Right ((fps, mp, docstringResults),env) -> + do setModuleEnv env + let cache0 = fmap (\fp -> Proj.CacheEntry { cacheDocstringResult = Nothing, cacheFingerprint = fp }) fps + (cache, success) <- + foldM (\(fpAcc, success) (k, v) -> + case k of + M.InMem{} -> pure (fpAcc, success) + M.InFile path -> + case v of + Proj.Invalid e -> + do rPrint ("Failed to process module:" <+> (text path <> ":") $$ + indent 2 (ppInvalidStatus e)) + pure (fpAcc, False) -- report failure + Proj.Scanned Proj.Unchanged _ ((m,_):_) -> + do let name = P.thing (P.mName m) + let prevResult = join (Map.lookup (Proj.CacheInFile path) docstringResults) + case prevResult of + Just True -> rPrint ("Skipping unmodified module (tests passed): " <> pp name) + Just False -> rPrint ("Skipping unmodified module (tests failed): " <> pp name) + Nothing -> rPrint ("Skipping unmodified module: " <> pp name) + let fpAcc' = Map.adjust (\e -> e{ Proj.cacheDocstringResult = prevResult }) (Proj.CacheInFile path) fpAcc + pure (fpAcc', success && prevResult == Just True) -- preserve success + Proj.Scanned Proj.Changed _ ((m,_):_) -> + do let name = P.thing (P.mName m) + rPrint ("Checking docstrings on changed module: " <> pp name) + checkRes <- checkModName name + let fpAcc' = Map.adjust (\fp -> fp { Proj.cacheDocstringResult = Just (crSuccess checkRes) }) (Proj.CacheInFile path) fpAcc + pure (fpAcc', success && crSuccess checkRes) + Proj.Scanned _ _ [] -> panic "Cryptol.REPL.Command" ["malformed change entry"] + + ) (cache0, True) (Map.assocs mp) + + let (passing, failing, missing) = + foldl + (\(a,b,c) x -> + case Proj.cacheDocstringResult x of + Nothing -> (a,b,c+1) + Just True -> (a+1,b,c) + Just False -> (a,b+1,c)) + (0::Int,0::Int,0::Int) (Map.elems cache) + + rPutStrLn ("Passing: " ++ show passing ++ " Failing: " ++ show failing ++ " Missing: " ++ show missing) + + io (Proj.saveLoadCache (Proj.LoadCache cache)) + pure emptyCommandResult { crSuccess = success } - pure emptyCommandResult { crSuccess = failures == 0 } +ppInvalidStatus :: Proj.InvalidStatus -> Doc +ppInvalidStatus = \case + Proj.InvalidModule modErr -> pp modErr + Proj.InvalidDep d _ -> "Error in dependency: " <> pp d diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 47900b1ac..16f09eeba 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -63,6 +63,7 @@ module Cryptol.REPL.Monad ( , withRandomGen , setRandomGen , getRandomGen + , getModuleInput -- ** Config Options , EnvVal(..) @@ -127,6 +128,7 @@ import Control.Monad.Base import qualified Control.Monad.Catch as Ex import Control.Monad.IO.Class import Control.Monad.Trans.Control +import qualified Data.ByteString as BS import Data.Char (isSpace, toLower) import Data.IORef (IORef,newIORef,readIORef,atomicModifyIORef) @@ -702,6 +704,20 @@ withRandomGen repl = setRandomGen g' pure result +getModuleInput :: REPL (M.ModuleInput IO) +getModuleInput = do + evo <- getEvalOptsAction + env <- getModuleEnv + callStacks <- getCallStacks + tcSolver <- getTCSolver + pure M.ModuleInput + { minpCallStacks = callStacks + , minpEvalOpts = evo + , minpByteReader = BS.readFile + , minpModuleEnv = env + , minpTCSolver = tcSolver + } + -- | Given an existing qualified name, prefix it with a -- relatively-unique string. We make it unique by prefixing with a -- character @#@ that is not lexically valid in a module name. diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index c63423348..507387556 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -23,6 +23,7 @@ module Cryptol.Utils.Ident , ModName , modNameToText , textToModName + , mainModName , modNameChunks , modNameChunksText , packModName @@ -40,6 +41,7 @@ module Cryptol.Utils.Ident , modNameArg , modNameIfaceMod , modNameToNormalModName + , modNamesMatch , modNameIsNormal -- * Identifiers @@ -161,6 +163,7 @@ modPathIsNormal p = modNameIsNormal m && all identIsNormal is -------------------------------------------------------------------------------- -- | Top-level Module names are just text. data ModName = ModName Text MaybeAnon + | ModMain FilePath deriving (Eq,Ord,Show,Generic) instance NFData ModName @@ -170,9 +173,10 @@ instance NFData ModName modNameArg :: ModName -> ModName modNameArg (ModName m fl) = case fl of - NormalName -> ModName m AnonModArgName - _ -> panic "modNameArg" ["Name is not normal"] - + NormalName -> ModName m AnonModArgName + AnonModArgName -> panic "modNameArg" ["Name is not normal"] + AnonIfaceModName -> panic "modNameArg" ["Name is not normal"] +modNameArg (ModMain _) = panic "modNameArg" ["Name is not normal"] -- | Change a normal module name to a module name to be used for an -- anonnymous interface. @@ -180,24 +184,37 @@ modNameIfaceMod :: ModName -> ModName modNameIfaceMod (ModName m fl) = case fl of NormalName -> ModName m AnonIfaceModName - _ -> panic "modNameIfaceMod" ["Name is not normal"] + AnonModArgName -> panic "modNameIfaceMod" ["Name is not normal"] + AnonIfaceModName -> panic "modNameIfaceMod" ["Name is not normal"] +modNameIfaceMod (ModMain _) = panic "modNameIfaceMod" ["Name is not normal"] --- | This is used when we check that the name of a module matches the --- file where it is defined. modNameToNormalModName :: ModName -> ModName modNameToNormalModName (ModName t _) = ModName t NormalName +modNameToNormalModName (ModMain p) = ModMain p + +-- | This is used when we check that the name of a module matches the +-- file where it is defined. +modNamesMatch :: ModName -> ModName -> Bool +modNamesMatch (ModName a _) (ModName b _) = a == b +modNamesMatch (ModMain a) (ModMain b) = a == b +modNamesMatch _ _ = False modNameToText :: ModName -> Text modNameToText (ModName x fl) = maybeAnonText fl x +modNameToText (ModMain _) = "Main" -- | This is useful when we want to hide anonymous modules. modNameIsNormal :: ModName -> Bool modNameIsNormal (ModName _ fl) = isNormal fl +modNameIsNormal (ModMain _) = False -- | Make a normal module name out of text. textToModName :: T.Text -> ModName textToModName txt = ModName txt NormalName +mainModName :: FilePath -> ModName +mainModName = ModMain + -- | Break up a module name on the separators, `Text` version. modNameChunksText :: ModName -> [T.Text] modNameChunksText (ModName x fl) = unfoldr step x @@ -209,6 +226,8 @@ modNameChunksText (ModName x fl) = unfoldr step x (a,b) | T.null b -> Just (maybeAnonText fl str, b) | otherwise -> Just (a,T.drop (T.length modSep) b) +modNameChunksText (ModMain _) = panic "modNameChunksText" + ["Cannot get chunks of main module name"] -- | Break up a module name on the separators, `String` version modNameChunks :: ModName -> [String] diff --git a/tests/examples/allexamples.icry.stdout b/tests/examples/allexamples.icry.stdout index c5972d2b7..6ac8d480c 100644 --- a/tests/examples/allexamples.icry.stdout +++ b/tests/examples/allexamples.icry.stdout @@ -1,7 +1,7 @@ Loading module Cryptol Loading module Cryptol -Loading interface module `parameter` interface of Main -Loading module Main +Loading interface module `parameter` interface of AE +Loading module AE Loading module Cryptol Loading module AES Loading module Cryptol diff --git a/tests/issues/T1440.cry b/tests/issues/T1440.cry index 089285c1e..86e51e877 100644 --- a/tests/issues/T1440.cry +++ b/tests/issues/T1440.cry @@ -1,3 +1,5 @@ +module T1440 where + import interface submodule X import submodule Y diff --git a/tests/issues/T1440.icry.stdout b/tests/issues/T1440.icry.stdout index 12b4d1ca6..d74531fc9 100644 --- a/tests/issues/T1440.icry.stdout +++ b/tests/issues/T1440.icry.stdout @@ -1,12 +1,12 @@ Loading module Cryptol Loading module Cryptol -Loading module Main +Loading module T1440 -[error] at T1440.cry:1:28--1:29 +[error] at T1440.cry:3:28--3:29 Module not in scope: X -[error] at T1440.cry:3:1--3:19 +[error] at T1440.cry:5:1--5:19 Module not in scope: Y -[error] at T1440.cry:14:40--14:42 +[error] at T1440.cry:16:40--16:42 Module not in scope: U1 -[error] at T1440.cry:15:26--15:28 +[error] at T1440.cry:17:26--17:28 Module not in scope: U2 diff --git a/tests/issues/T1494_1.cry b/tests/issues/T1494_1.cry index d60028501..621d6014a 100644 --- a/tests/issues/T1494_1.cry +++ b/tests/issues/T1494_1.cry @@ -1,3 +1,4 @@ +module T1494_1 where parameter type n : # diff --git a/tests/issues/T1494_1.icry.stdout b/tests/issues/T1494_1.icry.stdout index f57e993b3..90190df26 100644 --- a/tests/issues/T1494_1.icry.stdout +++ b/tests/issues/T1494_1.icry.stdout @@ -1,4 +1,4 @@ Loading module Cryptol Loading module Cryptol -Loading interface module `parameter` interface of Main -Loading module Main +Loading interface module `parameter` interface of T1494_1 +Loading module T1494_1 diff --git a/tests/issues/issue731.cry b/tests/issues/issue731.cry index 726a6605b..37d6c3f64 100644 --- a/tests/issues/issue731.cry +++ b/tests/issues/issue731.cry @@ -1,3 +1,5 @@ +module issue731 where + type constraint T n = (fin n, n >= 1) type constraint Both p q = (p, q) diff --git a/tests/issues/issue731.icry b/tests/issues/issue731.icry index 241ac1980..5a2d57d7e 100644 --- a/tests/issues/issue731.icry +++ b/tests/issues/issue731.icry @@ -1,2 +1,2 @@ :l issue731.cry -:browse Main +:browse issue731 diff --git a/tests/issues/issue731.icry.stdout b/tests/issues/issue731.icry.stdout index d97ed83b8..177c7159a 100644 --- a/tests/issues/issue731.icry.stdout +++ b/tests/issues/issue731.icry.stdout @@ -1,6 +1,6 @@ Loading module Cryptol Loading module Cryptol -Loading module Main +Loading module issue731 Constraint Synonyms ===================