chore: tweak rpc cryptol expr parser (#1215)

* chore: tweak rpc cryptol expr parser
* chore: update Cryptol server Expression docs

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

@@ -63,7 +63,6 @@ library
     CryptolServer.Check
     CryptolServer.ClearState
     CryptolServer.Data.Expression
-    CryptolServer.Data.FreshName
     CryptolServer.Data.Type
     CryptolServer.EvalExpr
     CryptolServer.ExtendSearchPath

cryptol-remote-api/docs/Cryptol.rst

@@ -208,6 +208,11 @@ The tag values in objects can be:
 
 
 
+``variable``
+  The expression is a variable bound by the server. The field ``identifier`` contains the name of the variable.
+
+
+
 .. _JSONSchema:
 JSON Cryptol Types
 ~~~~~~~~~~~~~~~~~~

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

@@ -50,8 +50,8 @@ def from_cryptol_arg(val : Any) -> Any:
             else:
                 raise ValueError("Unknown encoding " + str(enc))
             return BV(size, n)
-        elif tag == 'unique name':
-            return OpaqueValue(int(val['unique']), str(val['identifier']))
+        elif tag == 'variable':
+            return OpaqueValue(str(val['identifier']))
         else:
             raise ValueError("Unknown expression tag " + tag)
     else:

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

@@ -166,8 +166,7 @@ def convert(self, val : Any) -> Any:
                     'width': val.size(), # N.B. original length, not padded
                     'data': val.hex()[2:]}
         elif isinstance(val, OpaqueValue):
-            return {'expression': 'unique name',
-                    'unique': val.unique,
+            return {'expression': 'variable',
                     'identifier': val.identifier}
         else:
             raise TypeError("Unsupported value: " + str(val))

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

@@ -7,24 +7,22 @@ class OpaqueValue():
   Note that as far as Python is concerned these values are only equal to
   themselves. If a richer notion of equality is required then the server should
   be consulted to compute the result."""
-  unique : int
   identifier : str
 
-  def __init__(self, unique : int, identifier : str) -> None:
-    self.unique = unique
+  def __init__(self, identifier : str) -> None:
     self.identifier = identifier
 
   def __str__(self) -> str:
     return self.identifier
 
   def __repr__(self) -> str:
-      return f"Opaque({self.unique!r}, {self.identifier!r})"
+      return f"Opaque({self.identifier!r})"
 
   def __eq__(self, other : Any) -> bool:
     if not isinstance(other, OpaqueValue):
         return False
     else:
-      return self.unique == other.unique and self.identifier == other.identifier
+      return self.identifier == other.identifier
 
   def __hash__(self) -> int:
-      return hash((self.unique, self.identifier))
+      return hash(self.identifier)

cryptol-remote-api/src/CryptolServer.hs

@@ -10,26 +10,22 @@ import Control.Monad.IO.Class
 import Control.Monad.Reader (ReaderT(ReaderT))
 import qualified Data.Aeson as JSON
 import Data.Containers.ListUtils (nubOrd)
-import Data.IntMap.Strict (IntMap)
-import qualified Data.IntMap.Strict as IntMap
 import Data.Text (Text)
 
 import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv(..), ModuleInput(..))
 import Cryptol.ModuleSystem.Env
   (getLoadedModules, lmFilePath, lmFingerprint,
    initialModuleEnv, ModulePath(..))
-import Cryptol.ModuleSystem.Name (Name, FreshM(..), nameUnique, nameIdent)
+import Cryptol.ModuleSystem.Name (FreshM(..))
 import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
-import Cryptol.Parser.AST (ModName, isInfixIdent)
+import Cryptol.Parser.AST (ModName)
 import Cryptol.TypeCheck( defaultSolverConfig )
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 
 import qualified Argo
 import qualified Argo.Doc as Doc
-import CryptolServer.Data.FreshName
-import CryptolServer.Exceptions
-    ( cryptolError, invalidName)
+import CryptolServer.Exceptions ( cryptolError )
 import CryptolServer.Options
     ( WithOptions(WithOptions), Options(Options, optEvalOpts) )
 
@@ -127,7 +123,6 @@ data ServerState =
   ServerState { _loadedModule :: Maybe LoadedModule
               , _moduleEnv :: ModuleEnv
               , _tcSolver :: SMT.Solver
-              , _freshNameEnv :: IntMap Name
               }
 
 loadedModule :: Lens' ServerState (Maybe LoadedModule)
@@ -139,42 +134,12 @@ moduleEnv = lens _moduleEnv (\v n -> v { _moduleEnv = n })
 tcSolver :: Lens' ServerState SMT.Solver
 tcSolver = lens _tcSolver (\v n -> v { _tcSolver = n })
 
--- | Names generated when marshalling complex values to an RPC client;
--- maps `nameUnique`s to `Name`s.
-freshNameEnv :: Lens' ServerState (IntMap Name)
-freshNameEnv = lens _freshNameEnv (\v n -> v { _freshNameEnv = n })
-
-
--- | Take and remember the given name so it can later be recalled
--- via it's `nameUnique` unique identifier. Return a `FreshName`
--- which can be easily serialized/pretty-printed and marshalled
--- across an RPC interface.
-registerName :: Name -> CryptolCommand FreshName
-registerName nm =
-  if isInfixIdent (nameIdent nm)
-  then raise $ invalidName nm
-  else
-    CryptolCommand $ const $ Argo.getState >>= \s ->
-      let nmEnv = IntMap.insert (nameUnique nm) nm (view freshNameEnv s)
-      in do Argo.setState (set freshNameEnv nmEnv s)
-            pure $ unsafeToFreshName nm
-
--- | Return the underlying `Name` the given `FreshName` refers to. The
--- `FreshName` should have previously been returned by `registerName` at some
--- point, or else a JSON exception will be raised.
-resolveFreshName :: FreshName -> CryptolCommand (Maybe Name)
-resolveFreshName fnm =
-  CryptolCommand $ const $ Argo.getState >>= \s ->
-    case IntMap.lookup (freshNameUnique fnm) (view freshNameEnv s) of
-      Nothing -> pure Nothing
-      Just nm -> pure $ Just nm
-
 
 initialState :: IO ServerState
 initialState =
   do modEnv <- initialModuleEnv
      s <- SMT.startSolver (defaultSolverConfig (meSearchPath modEnv))
-     pure (ServerState Nothing modEnv s IntMap.empty)
+     pure (ServerState Nothing modEnv s)
 
 extendSearchPath :: [FilePath] -> ServerState -> ServerState
 extendSearchPath paths =
@@ -190,12 +155,6 @@ instance FreshM CryptolCommand where
     CryptolCommand $ const (Argo.modifyState $ set moduleEnv mEnv')
     pure res
 
-freshNameCount :: CryptolCommand Int
-freshNameCount = CryptolCommand $ const $ do
-  fEnv <- view freshNameEnv <$> Argo.getState
-  pure $ IntMap.size fEnv
-
-
 -- | Check that all of the modules loaded in the Cryptol environment
 -- currently have fingerprints that match those when they were loaded.
 validateServerState :: ServerState -> IO Bool

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

@@ -41,7 +41,7 @@ import CryptolServer
       CryptolCommand )
 import CryptolServer.Exceptions (evalPolyErr)
 import CryptolServer.Data.Expression
-    ( readBack, getExpr, typecheckExpr, Expression)
+    ( readBack, getExpr, Expression)
 import CryptolServer.Data.Type ( JSONType(..) )
 import Cryptol.Utils.PP (pretty)
 
@@ -54,7 +54,7 @@ checkDescr =
 check :: CheckParams -> CryptolCommand CheckResult
 check (CheckParams jsonExpr cMode) =
   do e <- getExpr jsonExpr
-     (ty, schema) <- typecheckExpr e
+     (_expr, ty, schema) <- liftModuleCmd (CM.checkExpr e)
      -- TODO? validEvalContext expr, ty, schema
      s <- getTCSolver
      perhapsDef <- liftIO (defaultReplExpr s ty schema)