Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

New module system #1363

Merged
merged 172 commits into from
Jun 16, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
172 commits
Select commit Hold shift + click to select a range
6ab1470
New module system
yav Jun 13, 2022
1e3ad37
Don't crash on undefined names.
yav Jun 14, 2022
3839b3a
Add an example of passing a submodule as an argument to a functor.
yav Jun 14, 2022
ed90c0a
Remove unused things
yav Jun 14, 2022
67b5bde
Make the remote API compile
yav Jun 14, 2022
a643a19
only use top-level imports in implicit interface, get more tests working
m-yac Jun 15, 2022
70d9600
fix error for parameterized module instantiations, add tests like T5
m-yac Jun 21, 2022
4b3eac5
Fix fixities not registering when defined in REPL
qsctr Jun 24, 2022
2c179b1
fix #1372 by excluding defns from functor instances in `warnUnused`
m-yac Jul 14, 2022
2a8f755
fix remaining tests
m-yac Jul 14, 2022
1419108
Implement functor imports with instantiation.
yav Jul 14, 2022
26121c9
Update docs to document `where` imports
yav Jul 14, 2022
488ceec
Fix spacing in a test
yav Jul 14, 2022
18e1b92
Implement insantiating imports with { }
yav Jul 14, 2022
b76ec46
Update documentation
yav Jul 14, 2022
f9cd75b
accept whitespace changes in mono-binds tests
m-yac Jul 14, 2022
510d185
update AES examples with import instantiation syntax
m-yac Jul 14, 2022
83f4575
Rename `ModuleInstanceArg` to `ModuleInstanceNamedArg`
yav Jul 15, 2022
5ece8bb
Correct the order of declaratoins in functors.
yav Jul 15, 2022
a2bc669
First stab at passing through functor parameters
yav Jul 15, 2022
694282e
Add more tests for passing on parameters
yav Jul 18, 2022
ff30033
Document passing through arguments
yav Jul 18, 2022
62dddb0
Change 'signature' to interface, and also list funcotors
yav Jul 25, 2022
5bf24a2
Use more descriptive names for internally generated names.
yav Jul 25, 2022
84694d7
Don't show unusable anonymous modules when browsing.
yav Jul 25, 2022
24b1ba6
Clean up browsing of signatures
yav Jul 25, 2022
9c9d0db
Don't discrad documentation during type checking
yav Jul 25, 2022
180c90f
Use simple language
yav Jul 25, 2022
d413e35
Detailed help for interfaces.
yav Jul 25, 2022
5c1b0bc
Fix tests
yav Jul 25, 2022
d5d9f42
Print documentation for module parameters when inside a functor
yav Jul 26, 2022
ccb563c
Show fixities for value parameters.
yav Jul 26, 2022
6e8ab5a
Show documentation for modules, functors, and interfaces
yav Jul 26, 2022
25f92f5
Update test with new naming convention
yav Jul 26, 2022
a370845
Fix more tests
yav Jul 26, 2022
3eae908
Fix special cases for windows
yav Jul 26, 2022
5b801fc
Merge branch 'master' into functors-merge
yav Aug 4, 2022
dfdbd12
Merge branch 'master' into functors-merge
yav Aug 4, 2022
f77e5cc
Merge remote-tracking branch 'origin/master' into functors-merge
yav Aug 12, 2022
bd55b96
Fix typo
yav Aug 12, 2022
516ad74
Remove unused functoion
yav Sep 22, 2022
ddcc67b
Resolve Has selectors for each nested module separately.
yav Sep 22, 2022
09b68e2
Fix typos in comments
yav Sep 24, 2022
b72a5d9
Don't try to get information for undefined names.
yav Sep 24, 2022
441e163
Merge branch 'master' into functors-merge
yav Sep 27, 2022
489ded4
Fix tests
yav Sep 27, 2022
6fea305
Fix test
yav Sep 27, 2022
bed32f8
`TraverseNames` for `EPropGuards`
yav Sep 28, 2022
4f8bc65
Disallow foreign with the same name and in functors
yav Sep 28, 2022
58a351c
Update evaluator to account for TError of kind prop.
yav Sep 28, 2022
29e71d1
Merge branch 'master' into functors-merge
yav Sep 28, 2022
12967c4
Fix tests for Mac and Windows
yav Sep 28, 2022
39c6026
Handle some more cases where fake names caused problems.
yav Sep 29, 2022
e1e3fe6
Squash yet another fake name issue
yav Sep 29, 2022
3dc316a
Remove unused function
yav Oct 11, 2022
043bd69
Add a function to support translation to SAW core
yav Oct 11, 2022
91dbed4
Add a function that can split up a module name in Text, rather than s…
yav Oct 11, 2022
efc3fe7
Include one Ubuntu 20.04 configuration (#1447)
RyanGlScott Oct 6, 2022
fa3cc20
Pretty printing for Core Lint errors
yav Oct 13, 2022
0cefb92
Don't use syntactic equality for numeric types, collect constraints i…
yav Oct 13, 2022
f35648c
Filter out really trivial goals, so we can see the actual interesting…
yav Oct 13, 2022
ab0d1c8
Merge remote-tracking branch 'origin/T1451' into functors-merge
yav Oct 13, 2022
b0ccbb7
Preserve number of predicates in schema when applying a substitution
yav Oct 14, 2022
b66d990
Rename "signature" to "interface" to follow standard naming
yav Oct 14, 2022
8de5a79
Add pretty printing instances for parameters.
yav Oct 14, 2022
8922877
Allow loading interfaces.
yav Oct 14, 2022
9701b37
Check that when evaluating things we do not use either value or type …
yav Oct 20, 2022
20f8a36
Add/improve haddocks
yav Oct 21, 2022
c5e8662
Rename Signature to Iface + comments
yav Oct 21, 2022
dc4b344
Have a go at allowing type synonyms in interfaces.
yav Oct 25, 2022
bde2ecc
Use the location of the parameters as it is more accurate.
yav Oct 25, 2022
d0562af
Refactor to separate constraints and declarations. Order declaration…
yav Oct 25, 2022
4f4c202
Make the help work for type synonyms defined in interfaces.
yav Oct 25, 2022
1f6f7cc
Add some tests
yav Oct 25, 2022
2d35953
Update the documentation
yav Oct 25, 2022
13cb103
Merge pull request #1461 from GaloisInc/functors-iface-tysyn
yav Oct 26, 2022
520eeae
Fix the pretty printing for interfaces.
yav Nov 14, 2022
233caca
Comment typo
yav Nov 16, 2022
151efaf
Add a PP instance for TopEntity and improve PP instance for modules
yav Nov 16, 2022
2c3bc87
Fixes scoping issues with renaming instantiations
yav Nov 16, 2022
ced1c56
Add some tests
yav Nov 16, 2022
7faf665
Fix tests
yav Nov 16, 2022
b5d7cfe
Don't touch fake names
yav Nov 16, 2022
c2cda89
Another white space fix
yav Nov 16, 2022
18e3563
Don't panic if we fail to resolve a top-level instnatiation
yav Nov 21, 2022
fa8fa46
Merge remote-tracking branch 'origin/master' into functors-merge
yav Nov 22, 2022
b6f744f
Checkpoint: store `include`-ed files
yav Nov 22, 2022
fe00904
Remove `mImports` from typechecked modules.
yav Nov 22, 2022
74ceb6b
Keep track of the files used by a module
yav Nov 22, 2022
ef8391f
Group file related information together.
yav Nov 22, 2022
8416a91
Add a command to show dependencies in JSON
yav Nov 23, 2022
9071432
Fix capitalization
yav Nov 23, 2022
6c88622
Make it build
yav Nov 23, 2022
20130d3
Add "file deps" to the Cryptol API
yav Nov 24, 2022
ff6b9ac
Merge remote-tracking branch 'origin/master' into file-deps
yav Nov 28, 2022
b250383
Update docs
yav Nov 29, 2022
e0560df
Fix some tests
yav Nov 29, 2022
3a66cea
Make the REPL and Python API more similar
yav Nov 29, 2022
1dd175b
Merge pull request #1473 from GaloisInc/file-deps
yav Nov 29, 2022
e54971e
Add support for getting the dependencies of a module without loading it.
yav Dec 1, 2022
1f1e56c
File/module dependencies without loading
yav Dec 2, 2022
5987dbd
Fix test
yav Dec 2, 2022
4014655
Add a function to compute a dependency tree
yav Dec 2, 2022
2ef0d0d
Remove typing stuff
yav Dec 2, 2022
a85c3a9
Add type annotations
yav Dec 2, 2022
b35170a
Merge pull request #1477 from GaloisInc/file-deps
yav Dec 5, 2022
f834e24
Add scaffolfing for backtick imports
yav Dec 12, 2022
02a5e80
Make a module for the instantiation code
yav Dec 13, 2022
e0d0135
Rearrange so that each functor parameter can be "backtick" instantiat…
yav Dec 13, 2022
99906b3
A not very tested implantation of backitick imports
yav Dec 16, 2022
3d4f2ab
Have a go at fixing #1483
yav Dec 19, 2022
e0d5952
Add some tests
yav Dec 20, 2022
bf99953
Fixes #1484
yav Dec 20, 2022
b3a0858
Remove a bunch of SAFE annotation.
yav Dec 20, 2022
cfa6d8f
Debugging code to dump parsed AST
yav Dec 20, 2022
f36dbb4
Disallow direct functor instantiation in interfaces.
yav Dec 20, 2022
4b70911
Remove debugging stuff
yav Dec 20, 2022
7f7fc61
Syntactic sugar to support backtick imports
yav Dec 20, 2022
40149dc
During backtick instantiation pass all value parameters in a record
yav Dec 21, 2022
213bb3a
Fix windows test
yav Dec 21, 2022
ca7c47b
Bugfix, apply substitution to schema's constraints.
yav Dec 21, 2022
b527506
Check for repeated parameter names in types
yav Dec 21, 2022
b96f77f
Apply the substitution after fixing up the types in module parameters.
yav Dec 21, 2022
e191927
Add a function for updating the identifier of a name
yav Dec 22, 2022
7c9e75e
Keep track of the qualifiers of module parameters in the typed AST
yav Dec 22, 2022
94d60a8
Change the names of the parametres in _ imports
yav Dec 22, 2022
7f793d7
Update the reference manual to document instantiating with `_`
yav Dec 22, 2022
98dc7f5
Merge pull request #1481 from GaloisInc/T1480
yav Dec 22, 2022
5906cbc
Sync up with `poetry.lock` on `master`
yav Jan 13, 2023
f2d8476
Merge branch 'master' into functors-merge
yav Jan 13, 2023
069957d
Fix comment to avoid confusing `haddock`
yav Jan 13, 2023
c0ff727
Eliminate location information when matching application/abstractions.
Jan 19, 2023
697d2c1
Change parsing of type declarations.
yav Feb 9, 2023
fa5b155
Rename test to match issues, and add expected output
yav Feb 9, 2023
ce8b1e2
Keep track of locations in constraints arising from module instantiating
yav Feb 9, 2023
14c4a89
Fix tests
yav Feb 10, 2023
46b1719
Fix incorrect conversion to JSON.
yav Feb 10, 2023
ed39cce
Pretty print intervals with a given name map
yav Feb 14, 2023
1dded87
Add a function that allows us to do some reasoning in the context of …
yav Feb 14, 2023
77f7b65
Expose some of the lower level operations for doing proofs
yav Feb 15, 2023
9b63a18
Merge branch 'master' into functors-merge
yav Mar 6, 2023
6ee9220
cryptol module docs: tightened some writing, fixed some typos, and in…
Mar 23, 2023
ca0310f
Use standard definition
yav Mar 23, 2023
b669a61
Remove `id` application that does nothing
yav Mar 23, 2023
ba30b60
Unused extensions
yav Mar 23, 2023
7f078c3
Apply substitution to embedded newtype definition as well
yav Mar 23, 2023
0d271bc
Some code to print a full newypt declaration
yav Mar 23, 2023
8a43ba6
Add a test
yav Mar 23, 2023
c9bdd5d
Merge branch 'master' into functors-merge
yav Mar 24, 2023
24a708b
bring up to date with functors-merge
Mar 24, 2023
3c5f6ff
Merge pull request #1509 from GaloisInc/functors-merge-doc-cleanup
yav Mar 24, 2023
f49261f
Print nested functors also
yav Mar 28, 2023
4c269e8
Apply substitution to nested functors as well
yav Mar 28, 2023
70a1592
Fix test
yav Mar 28, 2023
cbd87a8
Fix more tests
yav Mar 28, 2023
0289fbf
Add a test for #1510
yav Mar 28, 2023
cb551e4
Fix typos in comments
yav Mar 29, 2023
05412e9
Things that depend on newtype constructors should depend on the newtypes
yav Mar 29, 2023
396b02b
Add a PP instance to PrimIdent
yav Apr 20, 2023
abbece3
Merge branch 'master' into functors-merge
yav Apr 25, 2023
1543bed
Fix name export, to just put the module name the "module" field
yav May 5, 2023
5dafbe4
Merge branch 'master' into functors-merge
yav May 5, 2023
64d5800
Merge branch 'master' into functors-merge
yav May 15, 2023
31da6cb
Restrict PrimMap to only refer to actual primtives.
yav May 23, 2023
de33458
Make the remote-api build
yav May 23, 2023
9addbc6
Revert breaking change.
yav May 24, 2023
f7d6a14
Remove some warnings
yav May 24, 2023
141fe3a
Remove repeated extension
yav May 24, 2023
614898f
Refactor to avoid using eiter, and preserve a bit more context
yav May 24, 2023
ed0d3fb
Add a function to compute a mapping from original names to names from…
yav May 24, 2023
77fd64f
Merge branch 'master' into functors-merge
yav May 25, 2023
179c2cf
Merge branch 'master' into functors-merge
yav Jun 16, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
4 changes: 4 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions bench/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down
4 changes: 2 additions & 2 deletions cryptol-remote-api/cryptol-eval-server/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down Expand Up @@ -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''
Expand Down
5 changes: 3 additions & 2 deletions cryptol-remote-api/cryptol-remote-api.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -80,6 +80,7 @@ library
CryptolServer.Names
CryptolServer.Sat
CryptolServer.TypeCheck
CryptolServer.FileDeps

other-modules:
CryptolServer.AesonCompat
Expand Down
5 changes: 5 additions & 0 deletions cryptol-remote-api/cryptol-remote-api/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -91,6 +92,10 @@ cryptolMethods =
"load file"
loadFileDescr
loadFile
, command
"file-deps"
fileDepsDescr
fileDeps
, command
"focused module"
focusedModuleDescr
Expand Down
49 changes: 49 additions & 0 deletions cryptol-remote-api/docs/Cryptol.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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)
~~~~~~~~~~~~~~~~~~~~~~~~

Expand Down
17 changes: 17 additions & 0 deletions cryptol-remote-api/python/cryptol/commands.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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__(
Expand Down
9 changes: 9 additions & 0 deletions cryptol-remote-api/python/cryptol/connection.py
Original file line number Diff line number Diff line change
Expand Up @@ -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()``.
Expand Down
14 changes: 14 additions & 0 deletions cryptol-remote-api/python/cryptol/file_deps.py
Original file line number Diff line number Diff line change
@@ -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)

6 changes: 6 additions & 0 deletions cryptol-remote-api/python/cryptol/single_connection.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)


6 changes: 6 additions & 0 deletions cryptol-remote-api/python/cryptol/synchronous.py
Original file line number Diff line number Diff line change
Expand Up @@ -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()
20 changes: 20 additions & 0 deletions cryptol-remote-api/python/tests/cryptol/test_filedeps.py
Original file line number Diff line number Diff line change
@@ -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()
4 changes: 2 additions & 2 deletions cryptol-remote-api/src/CryptolServer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 )
Expand Down Expand Up @@ -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
6 changes: 3 additions & 3 deletions cryptol-remote-api/src/CryptolServer/Data/Expression.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down
19 changes: 9 additions & 10 deletions cryptol-remote-api/src/CryptolServer/Exceptions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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)]))

Loading