feat(rpc): newtype (and other complex value) support for RPC server/c…

…lients

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

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

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

@@ -11,6 +11,7 @@
 from argo_client.interaction import HasProtocolState
 from . import solver
 from .bitvector import BV
+from .opaque import Opaque
 
 
 def extend_hex(string : str) -> str:
@@ -49,6 +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 Opaque(int(val['unique']), str(val['identifier']))
         else:
             raise ValueError("Unknown expression tag " + tag)
     else:

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

@@ -5,6 +5,7 @@
 from math import ceil
 import BitVector #type: ignore
 from .bitvector import BV
+from .opaque import Opaque
 
 from typing import Any, Dict, Iterable, List, NoReturn, Optional, TypeVar, Union
 
@@ -30,6 +31,16 @@ def __init__(self, code : str) -> None:
     def __to_cryptol__(self, ty : CryptolType) -> Any:
         return self._code
 
+# class CryptolNewtype(CryptolCode):
+#     def __init__(self, newtype : Newtype, fields : Dict[str, Any]) -> None:
+#         self._newtype = newtype
+#         self._fields = fields
+
+#     def __to_cryptol__(self, ty : CryptolType) -> Any:
+#         return {'expression': 'newtype',
+#                 'newtype': self._name,
+#                 'arguments': [to_cryptol(arg) for arg in self._rands]}
+
 class CryptolApplication(CryptolCode):
     def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None:
         self._rator = rator
@@ -163,6 +174,10 @@ def convert(self, val : Any) -> Any:
                     'encoding': 'hex',
                     'width': val.size(), # N.B. original length, not padded
                     'data': val.hex()[2:]}
+        elif isinstance(val, Opaque):
+            return {'expression': 'unique name',
+                    'unique': val.unique,
+                    'identifier': val.identifier}
         else:
             raise TypeError("Unsupported value: " + str(val))
 
@@ -407,6 +422,16 @@ def __init__(self, fields : Dict[str, CryptolType]) -> None:
     def __repr__(self) -> str:
         return f"Record({self.fields!r})"
 
+
+# class Newtype(CryptolType):
+#     def __init__(self, name : str, uid : int, args : List[CryptolType]) -> None:
+#         self.name = name
+#         self.uid  = uid
+#         self.args = args
+
+#     def __repr__(self) -> str:
+#         return f"Newtype({self.name!r}, {self.uid!r}, {self.args!r})"
+
 def to_type(t : Any) -> CryptolType:
     if t['type'] == 'variable':
         return Var(t['name'], to_kind(t['kind']))
@@ -450,6 +475,8 @@ def to_type(t : Any) -> CryptolType:
         return Tuple(*map(to_type, t['contents']))
     elif t['type'] == 'record':
         return Record({k : to_type(t['fields'][k]) for k in t['fields']})
+    # elif t['type'] == 'newtype':
+    #     return Newtype(t['name'], t['uid'], map(to_type, t['arguments']))
     elif t['type'] == 'Integer':
         return Integer()
     elif t['type'] == 'Rational':

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

@@ -0,0 +1,11 @@
+
+class Opaque():
+  unique : int
+  identifier : str
+
+  def __init__(self, unique : int, identifier : str) -> None:
+    self.unique = unique
+    self.identifier = identifier
+
+  def __repr__(self) -> str:
+      return f"Opaque({self.unique!r}, {self.identifier!r})"

cryptol-remote-api/python/tests/cryptol/test-files/CplxQNewtype.cry

@@ -0,0 +1,50 @@
+// This is a development of rational complex numbers
+
+type Q = Rational
+
+fortyTwo : Q
+fortyTwo = 42
+
+// Complex rational numbers in rectangular coordinates
+newtype CplxQ =
+  { real : Q, imag : Q }
+
+embedQ : Q -> CplxQ
+embedQ x = CplxQ{ real = x, imag = 0 }
+
+cplxTwo : CplxQ
+cplxTwo = embedQ 2
+
+cplxForty : CplxQ
+cplxForty = embedQ 40
+
+cplxFortyTwo : CplxQ
+cplxFortyTwo = embedQ 42
+
+
+cplxAdd : CplxQ -> CplxQ -> CplxQ
+cplxAdd x y = CplxQ { real = r, imag = i }
+  where
+  r = x.real + y.real
+  i = x.imag + y.imag
+
+cplxMul : CplxQ -> CplxQ -> CplxQ
+cplxMul x y = CplxQ { real = r, imag = i }
+  where
+  r = x.real * y.real - x.imag * y.imag
+  i = x.real * y.imag + x.imag * y.real
+
+cplxEq : CplxQ -> CplxQ -> Bit
+cplxEq x y = (x.real == y.real) && (x.imag == y.imag)
+
+property cplxAddAssoc x y z =
+  cplxEq (cplxAdd (cplxAdd x y) z)
+         (cplxAdd x (cplxAdd y z))
+
+property cplxMulAssoc x y z =
+  cplxEq (cplxMul (cplxMul x y) z)
+         (cplxMul x (cplxMul y z))
+
+property cplxMulDistrib x y z =
+  cplxEq (cplxMul x (cplxAdd y z))
+         (cplxAdd (cplxMul x y) (cplxMul x z))

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

@@ -0,0 +1,41 @@
+import unittest
+from pathlib import Path
+import unittest
+import cryptol
+from cryptol.bitvector import BV
+
+
+class TestCplxQ(unittest.TestCase):
+    def test_CplxQ(self):
+        c = cryptol.connect(reset_server=True)
+        c.load_file(str(Path('tests','cryptol','test-files', 'CplxQNewtype.cry')))
+
+        forty_two = c.eval("fortyTwo").result()
+        cplx_forty_two1 = c.call("embedQ", forty_two).result()
+        cplx_forty_two2 = c.eval("CplxQ{ real = 42, imag = 0 }").result()
+        cplx_two = c.eval("cplxTwo").result()
+        cplx_forty = c.eval("cplxForty").result()
+        cplx_forty_two3 = c.call("cplxAdd", cplx_two, cplx_forty).result()
+        cplx_forty_two4 = c.eval("cplxMul (CplxQ{ real = 21, imag = 0 }) (CplxQ{ real = 2, imag = 0 })").result()
+        cplx_forty_two5 = c.eval("cplxAdd (CplxQ{ real = 41, imag = 0 }) (CplxQ{ real = 1, imag = 0 })").result()
+        cplx_forty_two6 = c.eval("CplxQ{ real = 42, imag = 0 }").result()
+
+        res = c.call("cplxEq", cplx_forty_two1, cplx_forty_two2).result()
+        self.assertTrue(res)
+        res = c.call("cplxEq", cplx_two, cplx_forty_two2).result()
+        self.assertFalse(res)
+        res = c.call("cplxEq", cplx_forty_two1, cplx_forty_two3).result()
+        self.assertTrue(res)
+        res = c.call("cplxEq", cplx_forty_two1, cplx_forty_two4).result()
+        self.assertTrue(res)
+        res = c.call("cplxEq", cplx_forty_two1, cplx_forty_two5).result()
+        self.assertTrue(res)
+        res = c.call("cplxEq", cplx_forty_two1, cplx_forty_two6).result()
+        self.assertTrue(res)
+
+        # self.assertTrue(c.check("cplxMulAssoc").result().success)
+
+
+
+if __name__ == "__main__":
+    unittest.main()

cryptol-remote-api/src/CryptolServer.hs

@@ -10,21 +10,26 @@ 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 (ModuleCmd, ModuleEnv(..), ModuleInput(..))
 import Cryptol.ModuleSystem.Env
-  (getLoadedModules, lmFilePath, lmFingerprint, meLoadedModules,
-   initialModuleEnv, meSearchPath, ModulePath(..))
+  (getLoadedModules, lmFilePath, lmFingerprint,
+   initialModuleEnv, ModulePath(..))
+import Cryptol.ModuleSystem.Name (Name, FreshM(..), nameUnique, nameIdent)
 import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
-import Cryptol.Parser.AST (ModName)
+import Cryptol.Parser.AST (ModName, identText, isInfixIdent)
 import Cryptol.TypeCheck( defaultSolverConfig )
 import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 
 import qualified Argo
 import qualified Argo.Doc as Doc
-import CryptolServer.Exceptions ( cryptolError )
+import CryptolServer.Data.FreshName
+import CryptolServer.Exceptions
+    ( cryptolError, unknownFreshName, invalidName)
 import CryptolServer.Options
     ( WithOptions(WithOptions), Options(Options, optEvalOpts) )
 
@@ -73,15 +78,19 @@ instance CryptolMethod CryptolNotification where
 getModuleEnv :: CryptolCommand ModuleEnv
 getModuleEnv = CryptolCommand $ const $ view moduleEnv <$> Argo.getState
 
-getTCSolver :: CryptolCommand SMT.Solver
-getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
-
 setModuleEnv :: ModuleEnv -> CryptolCommand ()
 setModuleEnv me =
   CryptolCommand $ const $ Argo.getState >>= \s -> Argo.setState (set moduleEnv me s)
 
-runModuleCmd :: ModuleCmd a -> CryptolCommand a
-runModuleCmd cmd =
+modifyModuleEnv :: (ModuleEnv -> ModuleEnv) -> CryptolCommand ()
+modifyModuleEnv f =
+  CryptolCommand $ const $ Argo.getState >>= \s -> Argo.setState (set moduleEnv (f (view moduleEnv s)) s)
+
+getTCSolver :: CryptolCommand SMT.Solver
+getTCSolver = CryptolCommand $ const $ view tcSolver <$> Argo.getState
+
+liftModuleCmd :: ModuleCmd a -> CryptolCommand a
+liftModuleCmd cmd =
     do Options callStacks evOpts <- getOptions
        s <- CryptolCommand $ const Argo.getState
        reader <- CryptolCommand $ const Argo.getFileReader
@@ -118,6 +127,7 @@ data ServerState =
   ServerState { _loadedModule :: Maybe LoadedModule
               , _moduleEnv :: ModuleEnv
               , _tcSolver :: SMT.Solver
+              , _freshNameEnv :: IntMap Name
               }
 
 loadedModule :: Lens' ServerState (Maybe LoadedModule)
@@ -129,17 +139,61 @@ 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 Name
+resolveFreshName fnm =
+  CryptolCommand $ const $ Argo.getState >>= \s ->
+    case IntMap.lookup (freshNameUnique fnm) (view freshNameEnv s) of
+      Nothing -> Argo.raise $ unknownFreshName fnm
+      Just nm -> pure nm
+
+
 initialState :: IO ServerState
 initialState =
   do modEnv <- initialModuleEnv
      s <- SMT.startSolver (defaultSolverConfig (meSearchPath modEnv))
-     pure (ServerState Nothing modEnv s)
+     pure (ServerState Nothing modEnv s IntMap.empty)
 
 extendSearchPath :: [FilePath] -> ServerState -> ServerState
 extendSearchPath paths =
   over moduleEnv $ \me -> me { meSearchPath = nubOrd $ paths ++ meSearchPath me }
 
 
+instance FreshM CryptolCommand where
+  liftSupply f = do
+    serverState <- CryptolCommand $ const Argo.getState
+    let mEnv = view moduleEnv serverState
+        (res, supply') = f (meSupply $ mEnv)
+        mEnv' = mEnv { meSupply = supply' }
+    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

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

@@ -35,13 +35,13 @@ import Cryptol.TypeCheck.Solve (defaultReplExpr)
 import CryptolServer
     ( getTCSolver,
       getModuleEnv,
-      runModuleCmd,
+      liftModuleCmd,
       CryptolMethod(raise),
       CryptolCommand )
 import CryptolServer.Exceptions (evalPolyErr)
 import CryptolServer.Data.Expression
-    ( readBack, observe, getExpr, Expression )
-import CryptolServer.Data.Type
+    ( readBack, getExpr, typecheckExpr, Expression)
+import CryptolServer.Data.Type ( JSONType(..) )
 import Cryptol.Utils.PP (pretty)
 
 checkDescr :: Doc.Block
@@ -53,7 +53,7 @@ checkDescr =
 check :: CheckParams -> CryptolCommand CheckResult
 check (CheckParams jsonExpr cMode) =
   do e <- getExpr jsonExpr
-     (_expr, ty, schema) <- runModuleCmd (CM.checkExpr e)
+     (ty, schema) <- typecheckExpr e
      -- TODO? validEvalContext expr, ty, schema
      s <- getTCSolver
      perhapsDef <- liftIO (defaultReplExpr s ty schema)
@@ -65,7 +65,7 @@ check (CheckParams jsonExpr cMode) =
            let theType = apSubst su (AST.sType schema)
            tenv  <- CEE.envTypes . deEnv . meDynEnv <$> getModuleEnv
            let tval = CET.evalValType tenv theType
-           val <- runModuleCmd (CM.evalExpr checked)
+           val <- liftModuleCmd (CM.evalExpr checked)
            pure (val,tval)
          let (isExaustive, randomTestNum) = case cMode of
                                               ExhaustiveCheckMode -> (True, 0)
@@ -85,8 +85,10 @@ check (CheckParams jsonExpr cMode) =
 
 convertTestArg :: (CET.TValue, CEC.Value) -> CryptolCommand (JSONType, Expression)
 convertTestArg (t, v) = do
-   e <- observe $ readBack t v
-   return (JSONType mempty (CET.tValTy t), e)
+   me <- readBack t v
+   case me of
+     Nothing -> error $ "type is not convertable: " ++ (show t)
+     Just e -> return (JSONType mempty (CET.tValTy t), e)
 
 convertTestResult ::
   [CET.TValue] {- ^ Argument types -} ->