Merge pull request #1363 from GaloisInc/functors-merge

New module system

CHANGES.md

@@ -40,6 +40,10 @@
   `sbv-cvc5` is non-functional on Windows at this time due to a downstream issue
   with CVC5 1.0.4 and earlier.)
 
+* Add `:file-deps` commands to the REPL and Python API.
+  It shows information about the source files and dependencies of
+  modules or Cryptol files.
+
 ## Bug fixes
 
 * Fix a bug in the What4 backend that could cause applications of `(@)` with

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 =

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''

cryptol-remote-api/cryptol-remote-api.cabal

@@ -13,8 +13,8 @@ flag static
   description: Create a statically-linked binary
 
 flag NotThreaded
-  default: false
-  manual: true
+  default: False
+  manual: True
   description: Omit the -threaded ghc flag
 
 common warnings
@@ -80,6 +80,7 @@ library
     CryptolServer.Names
     CryptolServer.Sat
     CryptolServer.TypeCheck
+    CryptolServer.FileDeps
 
   other-modules:
     CryptolServer.AesonCompat

cryptol-remote-api/cryptol-remote-api/Main.hs

@@ -33,6 +33,7 @@ import CryptolServer.LoadModule
 import CryptolServer.Names ( visibleNames, visibleNamesDescr )
 import CryptolServer.Sat ( proveSat, proveSatDescr )
 import CryptolServer.TypeCheck ( checkType, checkTypeDescr )
+import CryptolServer.FileDeps( fileDeps, fileDepsDescr )
 
 main :: IO ()
 main =
@@ -91,6 +92,10 @@ cryptolMethods =
      "load file"
      loadFileDescr
      loadFile
+  , command
+     "file-deps"
+     fileDepsDescr
+     fileDeps
   , command
      "focused module"
      focusedModuleDescr

cryptol-remote-api/docs/Cryptol.rst

@@ -388,6 +388,55 @@ No return fields
 
 
 
+file-deps (command)
+~~~~~~~~~~~~~~~~~~~
+
+Get information about the dependencies of a file or module. The dependencies include the dependencies of modules nested in this one.
+
+Parameter fields
+++++++++++++++++
+
+
+``name``
+  Get information about this entity.
+
+
+
+``is-file``
+  Indicates if the name is a file (true) or module (false)
+
+
+
+Return fields
++++++++++++++
+
+
+``source``
+  File containing the module. For internal modules this is an object { internal: "LABEL" }.
+
+
+
+``fingerprint``
+  A hash of the module content.
+
+
+
+``includes``
+  Files included in this module.
+
+
+
+``imports``
+  Modules imported by this module.
+
+
+
+``foreign``
+  Foreign libraries loaded by this module.
+
+
+
+
 focused module (command)
 ~~~~~~~~~~~~~~~~~~~~~~~~
 

cryptol-remote-api/python/cryptol/commands.py

@@ -75,6 +75,21 @@ def __init__(self, connection : HasProtocolState, filename : str, timeout: Optio
     def process_result(self, res : Any) -> Any:
         return res
 
+class CryptolFileDeps(argo.Command):
+  def __init__( self
+              , connection : HasProtocolState
+              , name : str, isFile : bool
+              , timeout: Optional[float]
+              ) -> None:
+    super(CryptolFileDeps, self).__init__('file-deps'
+                                         , {'name': name, 'is-file': isFile }
+                                         , connection
+                                         , timeout=timeout
+                                         )
+
+  def process_result(self, res : Any) -> Any:
+      return res
+
 class CryptolExtendSearchPath(argo.Command):
     def __init__(self, connection : HasProtocolState, dirs : List[str], timeout: Optional[float]) -> None:
         super(CryptolExtendSearchPath, self).__init__('extend search path', {'paths': dirs}, connection, timeout=timeout)
@@ -83,6 +98,8 @@ def process_result(self, res : Any) -> Any:
         return res
 
 
+
+
 class CryptolEvalExprRaw(argo.Command):
     def __init__(self, connection : HasProtocolState, expr : Any, timeout: Optional[float]) -> None:
         super(CryptolEvalExprRaw, self).__init__(

cryptol-remote-api/python/cryptol/connection.py

@@ -213,6 +213,15 @@ def load_module(self, module_name : str, *, timeout:Optional[float] = None) -> a
         self.most_recent_result = CryptolLoadModule(self, module_name, timeout)
         return self.most_recent_result
 
+    def file_deps(self, name : str, isFile : bool, *, timeout:Optional[float] = None) -> argo.Command:
+        """Get information about a module or a file.
+
+        :param timeout: Optional timeout for this request (in seconds).
+        """
+        timeout = timeout if timeout is not None else self.timeout
+        self.most_recent_result = CryptolFileDeps(self, name, isFile, timeout)
+        return self.most_recent_result
+
     def eval_raw(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
         """Like the member method ``eval``, but does not call
         ``from_cryptol_arg`` on the ``.result()``.

cryptol-remote-api/python/cryptol/file_deps.py

@@ -0,0 +1,14 @@
+from typing import Dict, Any
+
+def nestedFileDeps(getDeps : Any, name : str, isFile : bool) -> Any:
+  done : Dict[str,Any]  = {}
+  start = getDeps(name, isFile)
+  todo  = start["imports"].copy()
+  while len(todo) > 0:
+    m = todo.pop()
+    if m in done:
+      continue
+    deps = getDeps(m, False)
+    todo.extend(deps["imports"])
+  return (start, deps)
+

cryptol-remote-api/python/cryptol/single_connection.py

@@ -252,3 +252,9 @@ def interrupt() -> None:
 def logging(on : bool, *, dest : TextIO = sys.stderr) -> None:
     """Whether to log received and transmitted JSON."""
     __get_designated_connection().logging(on=on,dest=dest)
+
+def file_deps(m : str, isFile:bool, timeout:Optional[float] = None) -> Any:
+    """Get information about a module or a file."""
+    return __get_designated_connection().file_deps(m,isFile,timeout=timeout)
+
+

cryptol-remote-api/python/cryptol/synchronous.py

@@ -393,3 +393,9 @@ def interrupt(self) -> None:
     def logging(self, on : bool, *, dest : TextIO = sys.stderr) -> None:
         """Whether to log received and transmitted JSON."""
         self.connection.server_connection.logging(on=on,dest=dest)
+
+    def file_deps( self
+                 , m : str, isFile:bool
+                 , timeout:Optional[float] = None) -> Any:
+        """Get information about a module or a file."""
+        return self.connection.file_deps(m,isFile,timeout=timeout).result()

cryptol-remote-api/python/tests/cryptol/test_filedeps.py

@@ -0,0 +1,20 @@
+import unittest
+from pathlib import Path
+import unittest
+import cryptol
+from cryptol.single_connection import *
+
+
+class TestFileDeps(unittest.TestCase):
+    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['foreign'],[])
+        self.assertEqual(result['imports'],['Cryptol'])
+        self.assertEqual(result['includes'],[])
+        # we don't check source because it is system dependent
+
+if __name__ == "__main__":
+    unittest.main()

cryptol-remote-api/src/CryptolServer.hs

@@ -15,7 +15,7 @@ import Data.Text (Text)
 import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv(..), ModuleInput(..))
 import Cryptol.ModuleSystem.Env
-  (getLoadedModules, lmFilePath, lmFingerprint,
+  (getLoadedModules, lmFilePath, lmFileInfo, fiFingerprint,
    initialModuleEnv, ModulePath(..))
 import Cryptol.ModuleSystem.Name (FreshM(..))
 import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
@@ -180,6 +180,6 @@ validateServerState =
         InMem{} -> continue
         InFile file ->
           do fp <- fingerprintFile file
-             if fp == Just (lmFingerprint lm)
+             if fp == Just (fiFingerprint (lmFileInfo lm))
                then continue
                else return False

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)

cryptol-remote-api/src/CryptolServer/Exceptions.hs

@@ -10,12 +10,14 @@ module CryptolServer.Exceptions
   , proverError
   , cryptolParseErr
   , cryptolError
+  , moduleNotLoaded
   ) where
 
 import qualified Data.Aeson as JSON
 import qualified Data.Text as Text
 import qualified Data.Vector as Vector
 
+import Cryptol.Parser.AST(ModName)
 import Cryptol.ModuleSystem (ModuleError(..), ModuleWarning(..))
 import Cryptol.ModuleSystem.Name as CM
 import Cryptol.Utils.PP (pretty, PP)
@@ -102,16 +104,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))
@@ -216,3 +208,10 @@ jsonTypeAndString ty =
   fromListKM
     [ "type" .= JSONSchema (TC.Forall [] [] ty)
     , "type string" .= pretty ty ]
+
+moduleNotLoaded :: ModName -> JSONRPCException
+moduleNotLoaded m =
+  makeJSONRPCException
+    20100 "Module not loaded"
+    (Just (JSON.object ["error" .= show (pretty m)]))
+