From affee13ad62389cb392d2e8da1306a1c30e97fe4 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Thu, 27 May 2021 10:51:51 -0700 Subject: [PATCH 1/2] feat(rpc): newtype (and other complex value) support for RPC server/clients --- cryptol-remote-api/cryptol-remote-api.cabal | 1 + cryptol-remote-api/python/cryptol/commands.py | 3 + .../python/cryptol/cryptoltypes.py | 7 + cryptol-remote-api/python/cryptol/opaque.py | 30 ++ .../tests/cryptol/test-files/CplxQNewtype.cry | 50 ++ .../python/tests/cryptol/test_CplxQNewtype.py | 33 ++ .../tests/cryptol/test_low_level_ops.py | 73 +-- cryptol-remote-api/src/CryptolServer.hs | 76 ++- cryptol-remote-api/src/CryptolServer/Check.hs | 16 +- .../src/CryptolServer/Data/Expression.hs | 510 +++++++++++------- .../src/CryptolServer/Data/FreshName.hs | 42 ++ .../src/CryptolServer/Data/Type.hs | 2 +- .../src/CryptolServer/EvalExpr.hs | 55 +- .../src/CryptolServer/Exceptions.hs | 20 +- .../src/CryptolServer/LoadModule.hs | 4 +- cryptol-remote-api/src/CryptolServer/Sat.hs | 13 +- .../src/CryptolServer/TypeCheck.hs | 14 +- 17 files changed, 657 insertions(+), 292 deletions(-) create mode 100644 cryptol-remote-api/python/cryptol/opaque.py create mode 100644 cryptol-remote-api/python/tests/cryptol/test-files/CplxQNewtype.cry create mode 100644 cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py create mode 100644 cryptol-remote-api/src/CryptolServer/Data/FreshName.hs diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index 7ee65548b..bf9c25d3d 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/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 diff --git a/cryptol-remote-api/python/cryptol/commands.py b/cryptol-remote-api/python/cryptol/commands.py index d5d184d5f..f219bafc1 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/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 OpaqueValue 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 OpaqueValue(int(val['unique']), str(val['identifier'])) else: raise ValueError("Unknown expression tag " + tag) else: diff --git a/cryptol-remote-api/python/cryptol/cryptoltypes.py b/cryptol-remote-api/python/cryptol/cryptoltypes.py index 28f7f06c7..2a442345e 100644 --- a/cryptol-remote-api/python/cryptol/cryptoltypes.py +++ b/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 OpaqueValue from typing import Any, Dict, Iterable, List, NoReturn, Optional, TypeVar, Union @@ -30,6 +31,7 @@ def __init__(self, code : str) -> None: def __to_cryptol__(self, ty : CryptolType) -> Any: return self._code + class CryptolApplication(CryptolCode): def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None: self._rator = rator @@ -163,6 +165,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, OpaqueValue): + return {'expression': 'unique name', + 'unique': val.unique, + 'identifier': val.identifier} else: raise TypeError("Unsupported value: " + str(val)) @@ -407,6 +413,7 @@ def __init__(self, fields : Dict[str, CryptolType]) -> None: def __repr__(self) -> str: return f"Record({self.fields!r})" + def to_type(t : Any) -> CryptolType: if t['type'] == 'variable': return Var(t['name'], to_kind(t['kind'])) diff --git a/cryptol-remote-api/python/cryptol/opaque.py b/cryptol-remote-api/python/cryptol/opaque.py new file mode 100644 index 000000000..9933b8d5a --- /dev/null +++ b/cryptol-remote-api/python/cryptol/opaque.py @@ -0,0 +1,30 @@ +from typing import Any + +class OpaqueValue(): + """A value from the Cryptol server which cannot be directly represented and/or + marshalled to an RPC client. + + 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 + self.identifier = identifier + + def __str__(self) -> str: + return self.identifier + + def __repr__(self) -> str: + return f"Opaque({self.unique!r}, {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 + + def __hash__(self) -> int: + return hash((self.unique, self.identifier)) diff --git a/cryptol-remote-api/python/tests/cryptol/test-files/CplxQNewtype.cry b/cryptol-remote-api/python/tests/cryptol/test-files/CplxQNewtype.cry new file mode 100644 index 000000000..4d3a273d6 --- /dev/null +++ b/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)) diff --git a/cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py b/cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py new file mode 100644 index 000000000..3326cf48b --- /dev/null +++ b/cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py @@ -0,0 +1,33 @@ +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() + + self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two2).result()) + self.assertFalse(c.call("cplxEq", cplx_two, cplx_forty_two2).result()) + self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two3).result()) + self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two4).result()) + self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two5).result()) + self.assertTrue(c.call("cplxEq", cplx_forty_two1, cplx_forty_two6).result()) + + + +if __name__ == "__main__": + unittest.main() diff --git a/cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py b/cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py index 82d6f7e67..c27d136a6 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py +++ b/cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py @@ -12,23 +12,24 @@ # cryptol_path = dir_path.joinpath('data') # Test empty options -def do_test_options(c, state, options): +def do_test_options(test : unittest.TestCase, c, state, options): id_opt = c.send_command("evaluate expression", {"state": state, "expression": "four", "options": options}) reply = c.wait_for_reply_to(id_opt) - assert('result' in reply) - assert('answer' in reply['result']) - assert('value' in reply['result']['answer']) - assert(reply['result']['answer']['value'] == {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'}) + test.assertIn('result', reply) + test.assertIn('answer', reply['result']) + test.assertIn('value', reply['result']['answer']) + test.assertEqual(reply['result']['answer']['value'], {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'}) return reply['result']['state'] -def do_test_instantiation(c, state, t, expected=None): +def do_test_instantiation(test : unittest.TestCase, c, state, t, expected=None): if expected is None: expected = t id_t = c.send_command("check type", {"state": state, "expression": {"expression": "instantiate", "generic": "id", "arguments": {"a": t}}}) reply = c.wait_for_reply_to(id_t) - assert('result' in reply) - assert('answer' in reply['result']) - assert('type schema' in reply['result']['answer']) - assert(reply['result']['answer']['type schema']['type']['domain'] == expected) + test.assertIn('result', reply) + test.assertIn('result', reply) + test.assertIn('answer', reply['result']) + test.assertIn('type schema', reply['result']['answer']) + test.assertEqual(reply['result']['answer']['type schema']['type']['domain'], expected) return reply['result']['state'] class LowLevelCryptolApiTests(unittest.TestCase): @@ -119,27 +120,7 @@ def test_low_level_api(self): 'unit': {'expression': 'unit'}}}) state = reply['result']['state'] - - uid = c.send_command("evaluate expression", - {"state": state, - "expression": {"expression": "let", - "binders": [{"name": "theRecord", "definition": a_record}], - "body": {"expression": "tuple", - "data": [a_record, "theRecord"]}}}) - reply = c.wait_for_reply_to(uid) - self.assertIn('result', reply) - self.assertIn('answer', reply['result']) - self.assertIn('value', reply['result']['answer']) - self.assertEqual(reply['result']['answer']['value'], - {'expression': 'tuple', - 'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}, - {'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}]}) - state = reply['result']['state'] - + uid = c.send_command("evaluate expression", {"state": state, "expression": {"expression": "sequence", @@ -161,8 +142,8 @@ def test_low_level_api(self): uid = c.send_command("evaluate expression", {"state": state, "expression": {"expression": "integer modulo", - "integer": 14, - "modulus": 42}}) + "integer": 14, + "modulus": 42}}) reply = c.wait_for_reply_to(uid) self.assertIn('result', reply) self.assertIn('answer', reply['result']) @@ -211,29 +192,29 @@ def test_low_level_api(self): self.assertEqual(reply['result']['answer']['value'], {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'}) state = reply['result']['state'] - state = do_test_options(c, state, dict()) - state = do_test_options(c, state, {"call stacks": True}) - state = do_test_options(c, state, {"call stacks": False}) - state = do_test_options(c, state, {"call stacks": False, "output": dict()}) - state = do_test_options(c, state, {"call stacks": False, "output": {"ASCII": True}}) - state = do_test_options(c, state, {"call stacks": False, "output": {"base": 16}}) - state = do_test_options(c, state, {"call stacks": False, "output": {"prefix of infinite lengths": 3}}) + state = do_test_options(self, c, state, dict()) + state = do_test_options(self, c, state, {"call stacks": True}) + state = do_test_options(self, c, state, {"call stacks": False}) + state = do_test_options(self, c, state, {"call stacks": False, "output": dict()}) + state = do_test_options(self, c, state, {"call stacks": False, "output": {"ASCII": True}}) + state = do_test_options(self, c, state, {"call stacks": False, "output": {"base": 16}}) + state = do_test_options(self, c, state, {"call stacks": False, "output": {"prefix of infinite lengths": 3}}) # These test both the type instantiation form and the serialization/deserialization of the types involved - state = do_test_instantiation(c, state, {"type": "Integer"}) - state = do_test_instantiation(c, state, {"type": "record", + state = do_test_instantiation(self, c, state, {"type": "Integer"}) + state = do_test_instantiation(self, c, state, {"type": "record", "fields": {'a': {'type': 'Integer'}, 'b': {'type': 'sequence', 'length': {'type': 'inf'}, 'contents': {'type': 'unit'}}}}) - state = do_test_instantiation(c, state, {'type': 'sequence', + state = do_test_instantiation(self, c, state, {'type': 'sequence', 'length': {'type': 'number', 'value': 42}, 'contents': {'type': 'Rational'}}) - state = do_test_instantiation(c, state, {'type': 'bitvector', + state = do_test_instantiation(self, c, state, {'type': 'bitvector', 'width': {'type': 'number', 'value': 432}}) - state = do_test_instantiation(c, state, {'type': 'variable', + state = do_test_instantiation(self, c, state, {'type': 'variable', 'name': 'Word8'}, {'type': 'bitvector', 'width': {'type': 'number', 'value': 8}}) - state = do_test_instantiation(c, state, {'type': 'variable', + state = do_test_instantiation(self, c, state, {'type': 'variable', 'name': 'Twenty', 'arguments': [{'type': 'Z', 'modulus': {'type': 'number', 'value': 5}}]}, { 'type': 'sequence', diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs index 59f5ffde5..345a5f5dc 100644 --- a/cryptol-remote-api/src/CryptolServer.hs +++ b/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, 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 (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) + 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 diff --git a/cryptol-remote-api/src/CryptolServer/Check.hs b/cryptol-remote-api/src/CryptolServer/Check.hs index ba76820d4..c8cd223b2 100644 --- a/cryptol-remote-api/src/CryptolServer/Check.hs +++ b/cryptol-remote-api/src/CryptolServer/Check.hs @@ -36,13 +36,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 @@ -54,7 +54,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) @@ -66,7 +66,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) @@ -86,8 +86,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 -} -> diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index c6cb6ca1c..48fd246ed 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -3,6 +3,8 @@ {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} @@ -11,7 +13,6 @@ module CryptolServer.Data.Expression ) where import Control.Applicative -import Control.Exception (throwIO) import Control.Monad.IO.Class import Data.Aeson as JSON hiding (Encoding, Value, decode) import qualified Data.ByteString as BS @@ -31,8 +32,7 @@ import Data.Text.Encoding (encodeUtf8) import Numeric (showHex) import Cryptol.Backend.Monad -import Cryptol.Backend.Concrete hiding (Concrete) -import qualified Cryptol.Backend.Concrete as C +import qualified Cryptol.Eval.Concrete as Concrete import Cryptol.Backend.SeqMap (enumerateSeqMap) import Cryptol.Backend.WordValue (asWordVal) @@ -40,13 +40,22 @@ import Cryptol.Eval (evalSel) import Cryptol.Eval.Concrete (Value) import Cryptol.Eval.Type (TValue(..), tValTy) import Cryptol.Eval.Value (GenValue(..)) - - -import Cryptol.Parser -import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type, - ExportType(..)) +import Cryptol.ModuleSystem + (ModuleEnv, ModuleCmd, getPrimMap, evalDecls, renameType, renameVar, checkExpr, focusedEnv) +import Cryptol.ModuleSystem.Env (deNames,meDynEnv, mctxParams, mctxDecls, mctxNames) +import Cryptol.ModuleSystem.Monad (runModuleM, interactive, getFocusedEnv) +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) + +import qualified Cryptol.Parser as CP +import qualified Cryptol.Parser.AST as CP import Cryptol.Parser.Position (Located(..), emptyRange) import Cryptol.Parser.Selector +import qualified Cryptol.TypeCheck as TC +import qualified Cryptol.TypeCheck.AST as TC import Cryptol.Utils.Ident import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields) @@ -54,6 +63,7 @@ import Argo import qualified Argo.Doc as Doc import CryptolServer import CryptolServer.Exceptions +import CryptolServer.Data.FreshName import CryptolServer.Data.Type data Encoding = Base64 | Hex @@ -85,6 +95,8 @@ instance JSON.ToJSON LetBinding where , "definition" .= def ] +-- | Cryptol expressions which can be serialized into JSON and sent +-- to an RPC client. data Expression = Bit !Bool | Unit @@ -94,17 +106,28 @@ data Expression = | Tuple ![Expression] | Integer !Integer | IntegerModulo !Integer !Integer -- ^ value, modulus - | Concrete !Text - | Let ![LetBinding] !Expression + | UniqueName !FreshName + -- ^ Essentially a Cryptol.ModuleSystem.Name's nameUnique and nameIdent. + -- Used when we need to send a result back to an RPC client + | Concrete !Text -- ^ Concrete Cryptol syntax as a string -- the Cryptol parser + -- will establish it's meaning based on the current focus/context | Application !Expression !(NonEmpty Expression) | TypeApplication !Expression !TypeArguments deriving (Eq, Show) newtype TypeArguments = TypeArguments (Map Ident JSONPType) - deriving (Eq, Show) via Map Ident (Type PName) - -data ExpressionTag = - TagNum | TagRecord | TagSequence | TagTuple | TagUnit | TagLet | TagApp | TagTypeApp | TagIntMod + deriving (Eq, Show) via Map Ident (CP.Type CP.PName) + +data ExpressionTag + = TagNum + | TagRecord + | TagSequence + | TagTuple + | TagUnit + | TagApp + | TagTypeApp + | TagIntMod + | TagUniqueName instance JSON.FromJSON ExpressionTag where parseJSON = @@ -115,22 +138,22 @@ instance JSON.FromJSON ExpressionTag where "record" -> pure TagRecord "sequence" -> pure TagSequence "tuple" -> pure TagTuple - "let" -> pure TagLet "call" -> pure TagApp "instantiate" -> pure TagTypeApp "integer modulo" -> pure TagIntMod + "unique name" -> pure TagUniqueName _ -> empty instance JSON.ToJSON ExpressionTag where - toJSON TagNum = "bits" - toJSON TagRecord = "record" - toJSON TagSequence = "sequence" - toJSON TagTuple = "tuple" - toJSON TagUnit = "unit" - toJSON TagLet = "let" - toJSON TagApp = "call" - toJSON TagTypeApp = "instantiate" - toJSON TagIntMod = "integer modulo" + toJSON TagNum = "bits" + toJSON TagRecord = "record" + toJSON TagSequence = "sequence" + toJSON TagTuple = "tuple" + toJSON TagUnit = "unit" + toJSON TagApp = "call" + toJSON TagTypeApp = "instantiate" + toJSON TagIntMod = "integer modulo" + toJSON TagUniqueName = "unique name" instance JSON.FromJSON TypeArguments where parseJSON = @@ -177,14 +200,16 @@ instance JSON.FromJSON Expression where do contents <- o .: "data" flip (withArray "tuple") contents $ \s -> Tuple . V.toList <$> traverse parseJSON s - TagLet -> - Let <$> o .: "binders" <*> o .: "body" TagApp -> Application <$> o .: "function" <*> o .: "arguments" TagTypeApp -> TypeApplication <$> o .: "generic" <*> o .: "arguments" TagIntMod -> IntegerModulo <$> o .: "integer" <*> o .: "modulus" + TagUniqueName -> do + contents <- o .: "unique" + ident <- o .: "identifier" + pure $ UniqueName $ unsafeFreshName contents ident instance ToJSON Encoding where toJSON Hex = String "hex" @@ -220,23 +245,21 @@ instance JSON.ToJSON Expression where object [ "expression" .= TagTuple , "data" .= Array (V.fromList (map toJSON projs)) ] - toJSON (Let binds body) = - object [ "expression" .= TagLet - , "binders" .= Array (V.fromList (map toJSON binds)) - , "body" .= toJSON body - ] toJSON (Application fun args) = object [ "expression" .= TagApp , "function" .= fun , "arguments" .= args ] - toJSON (TypeApplication gen _args) = - -- It would be dead code to do anything here, as type - -- instantiations are not values. This code is called only as part - -- of translating values (e.g. from "evaluate expression"). So we - -- just fall through, rather than writing complicated code to - -- serialize Type PName that never gets called and just bitrots. - toJSON gen + toJSON (UniqueName nm) = + object [ "expression" .= TagUniqueName + , "unique" .= toJSON (freshNameUnique nm) + , "identifier" .= toJSON (freshNameText nm) + ] + toJSON (TypeApplication _gen (TypeArguments _args)) = + -- Presumably this is dead code, since values are what are sent back to + -- the user and type applications won't appear there ever. + error "JSON conversion of type applications is not yet supported" + instance Doc.Described Expression where typeName = "JSON Cryptol Expressions" @@ -352,118 +375,153 @@ instance Doc.Described Expression where ] -decode :: (Argo.Method m, Monad m) => Encoding -> Text -> m Integer -decode Base64 txt = +decode :: + (Monad m) => + (forall a. JSONRPCException -> m a) -> + Encoding -> + Text -> + m Integer +decode raiseJSONErr Base64 txt = let bytes = encodeUtf8 txt in case Base64.decode bytes of - Left err -> - Argo.raise (invalidBase64 bytes err) - Right decoded -> return $ bytesToInt decoded -decode Hex txt = - squish <$> traverse hexDigit (T.unpack txt) + Left err -> raiseJSONErr (invalidBase64 bytes err) + Right decoded -> pure $ bytesToInt decoded +decode raiseJSONErr Hex txt = + squish <$> traverse (hexDigit raiseJSONErr) (T.unpack txt) where squish = foldl (\acc i -> (acc * 16) + i) 0 -hexDigit :: (Argo.Method m, Monad m) => Num a => Char -> m a -hexDigit '0' = pure 0 -hexDigit '1' = pure 1 -hexDigit '2' = pure 2 -hexDigit '3' = pure 3 -hexDigit '4' = pure 4 -hexDigit '5' = pure 5 -hexDigit '6' = pure 6 -hexDigit '7' = pure 7 -hexDigit '8' = pure 8 -hexDigit '9' = pure 9 -hexDigit 'a' = pure 10 -hexDigit 'A' = pure 10 -hexDigit 'b' = pure 11 -hexDigit 'B' = pure 11 -hexDigit 'c' = pure 12 -hexDigit 'C' = pure 12 -hexDigit 'd' = pure 13 -hexDigit 'D' = pure 13 -hexDigit 'e' = pure 14 -hexDigit 'E' = pure 14 -hexDigit 'f' = pure 15 -hexDigit 'F' = pure 15 -hexDigit c = Argo.raise (invalidHex c) - - -getExpr :: Expression -> CryptolCommand (Expr PName) -getExpr = CryptolCommand . const . getCryptolExpr - --- N.B., used in SAWServer as well, hence the more generic monad -getCryptolExpr :: (Argo.Method m, Monad m) => Expression -> m (Expr PName) -getCryptolExpr Unit = - return $ - ETyped - (ETuple []) - (TTuple []) -getCryptolExpr (Bit b) = - return $ - ETyped - (EVar (UnQual (mkIdent $ if b then "True" else "False"))) - TBit -getCryptolExpr (Integer i) = - return $ - ETyped - (ELit (ECNum i (DecLit (pack (show i))))) - (TUser (UnQual (mkIdent "Integer")) []) -getCryptolExpr (IntegerModulo i n) = - return $ - ETyped - (ELit (ECNum i (DecLit (pack (show i))))) - (TUser (UnQual (mkIdent "Z")) [TNum n]) -getCryptolExpr (Num enc txt w) = - do d <- decode enc txt - return $ ETyped - (ELit (ECNum d (DecLit txt))) - (TSeq (TNum w) TBit) -getCryptolExpr (Record fields) = - fmap (ERecord . recordFromFields) $ for (HM.toList fields) $ - \(recName, spec) -> - (mkIdent recName,) . (emptyRange,) <$> getCryptolExpr spec -getCryptolExpr (Sequence elts) = - EList <$> traverse getCryptolExpr elts -getCryptolExpr (Tuple projs) = - ETuple <$> traverse getCryptolExpr projs -getCryptolExpr (Concrete syntax) = - case parseExpr syntax of - Left err -> - Argo.raise (cryptolParseErr syntax err) - Right e -> pure e -getCryptolExpr (Let binds body) = - EWhere <$> getCryptolExpr body <*> traverse mkBind binds +hexDigit :: + (Monad m, Num a) => + (forall b. JSONRPCException -> m b) -> + Char -> + m a +hexDigit raiseJSONErr = + \case + '0' -> pure 0 + '1' -> pure 1 + '2' -> pure 2 + '3' -> pure 3 + '4' -> pure 4 + '5' -> pure 5 + '6' -> pure 6 + '7' -> pure 7 + '8' -> pure 8 + '9' -> pure 9 + 'a' -> pure 10 + 'A' -> pure 10 + 'b' -> pure 11 + 'B' -> pure 11 + 'c' -> pure 12 + 'C' -> pure 12 + 'd' -> pure 13 + 'D' -> pure 13 + 'e' -> pure 14 + 'E' -> pure 14 + 'f' -> pure 15 + 'F' -> pure 15 + c -> raiseJSONErr (invalidHex c) + + +-- | Given a textual unqualified type name as `Text`, get the corresponding +-- `Name` for the type in the current module environment. +getTypeName :: + (Monad m) => + m ModuleEnv -> + (forall a. ModuleCmd a -> m a) -> + Text -> + m Name +getTypeName getModEnv runModuleCmd ty = do + nmEnv <- (mctxNames . focusedEnv) <$> getModEnv + runModuleCmd $ renameType nmEnv (CP.UnQual (mkIdent ty)) + +getCryptolType :: + (Monad m) => + m ModuleEnv -> + (forall a. ModuleCmd a -> m a) -> + JSONPType -> + m (CP.Type Name) +getCryptolType getModEnv runModuleCmd (JSONPType rawTy) = do + nmEnv <- (mctxNames . focusedEnv) <$> getModEnv + runModuleCmd $ \env -> runModuleM env $ interactive $ + Base.rename interactiveName nmEnv (R.rename rawTy) + +getExpr :: Expression -> CryptolCommand (CP.Expr Name) +getExpr = getCryptolExpr resolveFreshName + getModuleEnv + liftModuleCmd + CryptolServer.raise + +-- N.B., used in SAWServer as well, hence the more generic monad and +-- parameterized monadic functions. +getCryptolExpr :: forall m. + (Monad m) => + (FreshName -> m (Maybe Name)) {- ^ How to resolve a FreshName in the server. -} -> + m ModuleEnv {- ^ Getter for Cryptol ModuleEnv. -} -> + (forall a. ModuleCmd a -> m a) {- ^ Runner for Cryptol ModuleCmd. -} -> + (forall a. JSONRPCException -> m a) {- ^ JSONRPCException error raiser. -} -> + Expression {- Syntactic expression to convert to Cryptol. -} -> + m (CP.Expr Name) +getCryptolExpr getName getModEnv runModuleCmd raiseJSONErr = go where - mkBind (LetBinding x rhs) = - DBind . - (\bindBody -> - Bind { bName = fakeLoc (UnQual (mkIdent x)) - , bParams = [] - , bDef = bindBody - , bSignature = Nothing - , bInfix = False - , bFixity = Nothing - , bPragmas = [] - , bMono = True - , bDoc = Nothing - , bExport = Public - }) . - fakeLoc . - DExpr <$> - getCryptolExpr rhs - - fakeLoc = Located emptyRange -getCryptolExpr (Application fun (arg :| [])) = - EApp <$> getCryptolExpr fun <*> getCryptolExpr arg -getCryptolExpr (Application fun (arg1 :| (arg : args))) = - getCryptolExpr (Application (Application fun (arg1 :| [])) (arg :| args)) -getCryptolExpr (TypeApplication gen (TypeArguments args)) = - EAppT <$> getCryptolExpr gen <*> pure (map inst (Map.toList args)) - where - inst (n, t) = NamedInst (Named (Located emptyRange n) (unJSONPType t)) + go (UniqueName fnm) = do + mNm <- getName fnm + case mNm of + Nothing -> raiseJSONErr $ unknownFreshName fnm + Just nm -> pure $ CP.EVar nm + go Unit = + return $ + CP.ETyped + (CP.ETuple []) + (CP.TTuple []) + go (Bit b) = + return $ CP.ETyped + (if b + then CP.ELit $ CP.ECNum 1 (CP.BinLit "1" 1) + else CP.ELit $ CP.ECNum 0 (CP.BinLit "0" 0)) + CP.TBit + go (Integer i) = do + intTy <- getTypeName getModEnv runModuleCmd "Integer" + pure $ + CP.ETyped + (CP.ELit (CP.ECNum i (CP.DecLit (pack (show i))))) + (CP.TUser intTy []) + go (IntegerModulo i n) = do + zTy <- getTypeName getModEnv runModuleCmd "Z" + return $ + CP.ETyped + (CP.ELit (CP.ECNum i (CP.DecLit (pack (show i))))) + (CP.TUser zTy [CP.TNum n]) + go (Num enc txt w) = do + d <- decode raiseJSONErr enc txt + return $ CP.ETyped + (CP.ELit (CP.ECNum d (CP.DecLit txt))) + (CP.TSeq (CP.TNum w) CP.TBit) + go (Record fields) = + fmap (CP.ERecord . recordFromFields) $ for (HM.toList fields) $ + \(recName, spec) -> + (mkIdent recName,) . (emptyRange,) <$> go spec + go (Sequence elts) = + CP.EList <$> traverse go elts + go (Tuple projs) = + CP.ETuple <$> traverse go projs + go (Concrete syntax) = + case CP.parseExpr syntax of + Left err -> + raiseJSONErr $ cryptolParseErr syntax err + Right e -> do + (expr, _ty, _schema) <- runModuleCmd (checkExpr e) + pure expr + go (Application fun (arg :| [])) = + CP.EApp <$> go fun <*> go arg + go (Application fun (arg1 :| (arg : args))) = + go (Application (Application fun (arg1 :| [])) (arg :| args)) + go (TypeApplication gen (TypeArguments args)) = + CP.EAppT <$> go gen <*> (mapM inst (Map.toList args)) + inst (n, t) = do + t' <- getCryptolType getModEnv runModuleCmd t + pure $ CP.NamedInst (CP.Named (Located emptyRange n) t') -- TODO add tests that this is big-endian -- | Interpret a ByteString as an Integer @@ -471,61 +529,149 @@ bytesToInt :: BS.ByteString -> Integer bytesToInt bs = BS.foldl' (\acc w -> (acc * 256) + toInteger w) 0 bs -readBack :: TValue -> Value -> Eval Expression +-- | Read back a typed value (if possible) into syntax which can be sent to an +-- RPC client. For some values which do not have a guaranteed syntactic +-- representation, a fresh variable will be generated and bound to +-- the value so the variable can instead be sent to the RPC client. +readBack :: TValue -> Value -> CryptolCommand (Maybe Expression) readBack ty val = case ty of - -- TODO, add actual support for newtypes - TVNewtype _u _ts _tfs -> liftIO $ throwIO (invalidType (tValTy ty)) - - TVRec tfs -> - Record . HM.fromList <$> - sequence [ do fv <- evalSel C.Concrete val (RecordSel f Nothing) - fa <- readBack t fv - return (identText f, fa) - | (f, t) <- canonicalFields tfs - ] + TVRec tfs -> do + vals <- mapM readBackRecFld $ canonicalFields tfs + pure $ (Record . HM.fromList) <$> sequence vals TVTuple [] -> - pure Unit - TVTuple ts -> - Tuple <$> sequence [ do v <- evalSel C.Concrete val (TupleSel n Nothing) - a <- readBack t v - return a - | (n, t) <- zip [0..] ts - ] + pure $ Just Unit + TVTuple ts -> do + vals <- mapM readBackTupleFld $ zip [0..] ts + pure $ Tuple <$> sequence vals TVBit -> case val of - VBit b -> pure (Bit b) + VBit b -> pure $ Just $ Bit b _ -> mismatchPanic TVInteger -> case val of - VInteger i -> pure (Integer i) + VInteger i -> pure $ Just $ Integer i _ -> mismatchPanic TVIntMod n -> case val of - VInteger i -> pure (IntegerModulo i n) + VInteger i -> pure $ Just $ IntegerModulo i n _ -> mismatchPanic - TVSeq len contents - | contents == TVBit - , VWord width wv <- val -> - do BV w v <- asWordVal C.Concrete wv - let hexStr = T.pack $ showHex v "" - let paddedLen = fromIntegral ((width `quot` 4) + (if width `rem` 4 == 0 then 0 else 1)) - return $ Num Hex (T.justifyRight paddedLen '0' hexStr) w - | VSeq _l (enumerateSeqMap len -> vs) <- val -> - Sequence <$> mapM (>>= readBack contents) vs - - other -> liftIO $ throwIO (invalidType (tValTy other)) + TVSeq len elemTy + | elemTy == TVBit + , VWord width wv <- val -> do + Concrete.BV w v <- liftEval $ asWordVal Concrete.Concrete wv + let hexStr = T.pack $ showHex v "" + let paddedLen = fromIntegral ((width `quot` 4) + (if width `rem` 4 == 0 then 0 else 1)) + pure $ Just $ Num Hex (T.justifyRight paddedLen '0' hexStr) w + | VSeq _l (enumerateSeqMap len -> mVals) <- val -> do + vals <- liftEval $ sequence mVals + es <- mapM (readBack elemTy) vals + pure $ Sequence <$> sequence es + + _ -> do + -- The above cases are for types that can unambiguously be converted into + -- syntax; this case instead tries to essentially let-bind the value to a + -- fresh variable so we can send that to the RPC client instead. They + -- obviously won't be able to directly inspect the value, but they can + -- pass it to other functions/commands via a RPC. + mName <- bindValToFreshName (varName ty) ty val + case mName of + Nothing -> pure Nothing + Just name -> pure $ Just $ UniqueName name where + mismatchPanic :: CryptolCommand (Maybe Expression) mismatchPanic = error $ "Internal error: readBack: value '" <> show val <> "' didn't match type '" <> show (tValTy ty) <> "'" - - -observe :: Eval a -> CryptolCommand a -observe e = liftIO (runEval mempty e) - -mkEApp :: Expr PName -> [Expr PName] -> Expr PName -mkEApp f args = foldl EApp f args + readBackRecFld :: (Ident, TValue) -> CryptolCommand (Maybe (Text, Expression)) + readBackRecFld (fldId, fldTy) = do + fldVal <- liftEval $ evalSel Concrete.Concrete val (RecordSel fldId Nothing) + fldExpr <- readBack fldTy fldVal + pure $ (identText fldId,) <$> fldExpr + readBackTupleFld :: (Int, TValue) -> CryptolCommand (Maybe Expression) + readBackTupleFld (i, iTy) = do + iVal <- liftEval $ evalSel Concrete.Concrete val (TupleSel i Nothing) + readBack iTy iVal + varName :: TValue -> Text + varName = + \case + TVBit{} -> "bit" + TVInteger{} -> "integer" + TVFloat{} -> "float" + TVIntMod n -> "z" <> (T.pack $ show n) + TVRational{} -> "rational" + TVArray{} -> "array" + TVSeq{} -> "seq" + TVStream{} -> "stream" + TVTuple{} -> "tuple" + TVRec{} -> "record" + TVFun{} -> "fun" + TVNewtype nt _ _ -> identText $ nameIdent $ TC.ntName nt + TVAbstract{} -> "abstract" + + +-- | Given a suggested `name` and a type and value, attempt to bind the value +-- to a freshly generated name in the current server environment. If successful, +-- the generated name will be of the form `CryptolServer'nameN` (where `N` is a +-- natural number) and the `FreshName` that is returned can be serialized into an +-- `Expression` and sent to an RPC client. +bindValToFreshName :: Text -> TValue -> Concrete.Value -> CryptolCommand (Maybe FreshName) +bindValToFreshName nameBase ty val = do + prims <- liftModuleCmd getPrimMap + mb <- liftEval (Concrete.toExpr prims ty val) + case mb of + Nothing -> return Nothing + Just expr -> do + name <- genFreshName + fName <- registerName name + let schema = TC.Forall { TC.sVars = [] + , TC.sProps = [] + , TC.sType = tValTy ty + } + decl = TC.Decl { TC.dName = name + , TC.dSignature = schema + , TC.dDefinition = TC.DExpr expr + , TC.dPragmas = [] + , TC.dInfix = False + , TC.dFixity = Nothing + , TC.dDoc = Nothing + } + liftModuleCmd (evalDecls [TC.NonRecursive decl]) + modifyModuleEnv $ \me -> + let denv = meDynEnv me + in me {meDynEnv = denv { deNames = singletonE (CP.UnQual (nameIdent name)) name + `shadowing` deNames denv }} + return $ Just fName + where + genFreshName :: CryptolCommand Name + genFreshName = do + cnt <- freshNameCount + let ident = mkIdent $ "CryptolServer'" <> nameBase <> (T.pack $ show cnt) + mpath = TopModule interactiveName + liftSupply (mkDeclared NSValue mpath UserName ident Nothing emptyRange) + + +liftEval :: Eval a -> CryptolCommand a +liftEval e = liftIO (runEval mempty e) + +mkEApp :: CP.Expr Name -> [CP.Expr Name] -> CP.Expr Name +mkEApp f args = foldl CP.EApp f args + + + +-- | Typecheck a single expression, yielding a typechecked core expression and a type schema. +typecheckExpr :: CP.Expr Name -> CryptolCommand (TC.Expr,TC.Schema) +typecheckExpr e = liftModuleCmd $ \env -> runModuleM env $ interactive $ do + fe <- getFocusedEnv + let params = mctxParams fe + decls = mctxDecls fe + -- merge the dynamic and opened environments for typechecking + prims <- Base.getPrimMap + let act = Base.TCAction { Base.tcAction = TC.tcExpr + , Base.tcLinter = Base.exprLinter + , Base.tcPrims = prims } + (te,s) <- Base.typecheck act e params decls + return (te,s) diff --git a/cryptol-remote-api/src/CryptolServer/Data/FreshName.hs b/cryptol-remote-api/src/CryptolServer/Data/FreshName.hs new file mode 100644 index 000000000..e2ff0913c --- /dev/null +++ b/cryptol-remote-api/src/CryptolServer/Data/FreshName.hs @@ -0,0 +1,42 @@ + +module CryptolServer.Data.FreshName + ( FreshName + , freshNameUnique + , freshNameText + , unsafeFreshName + , unsafeToFreshName + ) where + + +import Cryptol.ModuleSystem.Name (Name, nameUnique, nameIdent) +import Cryptol.Parser.AST (identText) +import Data.Text (Text) + +-- | Minimal representative for fresh names generated by the server +-- when marshalling complex values back to the user. The `Int` +-- corresponds to the `nameUnique` of a `Name`, and the `Text` +-- is the non-infix `Ident`'s textual representation. +data FreshName = FreshName !Int !Text + deriving (Eq, Show) + +-- | Corresponds to the `nameUnique` field of a `Name`. +freshNameUnique :: FreshName -> Int +freshNameUnique (FreshName n _) = n + +-- | Corresponds to the `nameIdent` field of a `Name` (except we know +-- if is not infix, so we just store the `Text`). +freshNameText :: FreshName -> Text +freshNameText (FreshName _ txt) = txt + + +-- | Get a `FreshName` which corresopnds to then given `Name`. N.B., this does +-- _not_ register any names with the server or ensure the ident is not infix, +-- and so should this function only be used by code which maintains +-- these invariants. +unsafeToFreshName :: Name -> FreshName +unsafeToFreshName nm = FreshName (nameUnique nm) (identText (nameIdent nm)) + +-- | Creates a FreshName -- users should take care to ensure any generated +-- `FreshName` has a mapping from `Int` to `FreshName` recorded in the server! +unsafeFreshName :: Int -> Text -> FreshName +unsafeFreshName n txt = FreshName n txt diff --git a/cryptol-remote-api/src/CryptolServer/Data/Type.hs b/cryptol-remote-api/src/CryptolServer/Data/Type.hs index 19e496f20..07ca9d52c 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Type.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Type.hs @@ -214,7 +214,7 @@ instance JSON.ToJSON JSONType where ] convert (TUser _n _args def) = convert def convert (TNewtype _nt _ts) = - error "JSON conversion of newtypes is not yet supported TODO" + JSON.object [ "type" .= T.pack "newtype" ] convert (TRec fields) = JSON.object [ "type" .= T.pack "record" diff --git a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs index fdd2c1365..68807e251 100644 --- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs +++ b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs @@ -9,18 +9,19 @@ module CryptolServer.EvalExpr ) where import qualified Argo.Doc as Doc +import Control.Exception (throwIO) import Control.Monad.IO.Class import Data.Aeson as JSON import Data.Typeable (Proxy(..), typeRep) -import Cryptol.ModuleSystem (checkExpr, evalExpr) +import Cryptol.ModuleSystem (evalExpr) +import Cryptol.ModuleSystem.Name (Name) import Cryptol.ModuleSystem.Env (deEnv,meDynEnv) import Cryptol.TypeCheck.Solve (defaultReplExpr) import Cryptol.TypeCheck.Subst (apSubst, listParamSubst) import Cryptol.TypeCheck.Type (Schema(..)) import qualified Cryptol.Parser.AST as P -import Cryptol.Parser.Name (PName) import Cryptol.Utils.PP (pretty) import qualified Cryptol.Eval.Env as E import qualified Cryptol.Eval.Type as E @@ -39,30 +40,32 @@ evalExpression (EvalExprParams jsonExpr) = do e <- getExpr jsonExpr evalExpression' e -evalExpression' :: P.Expr PName -> CryptolCommand JSON.Value -evalExpression' e = - do (_expr, ty, schema) <- runModuleCmd (checkExpr e) - -- TODO: see Cryptol REPL for how to check whether we - -- can actually evaluate things, which we can't do in - -- a parameterized module - s <- getTCSolver - perhapsDef <- liftIO (defaultReplExpr s ty schema) - case perhapsDef of - Nothing -> - raise (evalPolyErr schema) - Just (tys, checked) -> - do -- TODO: warnDefaults here - let su = listParamSubst tys - let theType = apSubst su (sType schema) - tenv <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv - let tval = E.evalValType tenv theType - res <- runModuleCmd (evalExpr checked) - val <- observe $ readBack tval res - return (JSON.object [ "value" .= val - , "type string" .= pretty theType - , "type" .= JSONSchema (Forall [] [] theType) - ]) - +evalExpression' :: P.Expr Name -> CryptolCommand JSON.Value +evalExpression' e = do + (ty, schema) <- typecheckExpr e + -- TODO: see Cryptol REPL for how to check whether we + -- can actually evaluate things, which we can't do in + -- a parameterized module + s <- getTCSolver + perhapsDef <- liftIO (defaultReplExpr s ty schema) + case perhapsDef of + Nothing -> + raise (evalPolyErr schema) + Just (tys, checked) -> + do -- TODO: warnDefaults here + let su = listParamSubst tys + let theType = apSubst su (sType schema) + tenv <- E.envTypes . deEnv . meDynEnv <$> getModuleEnv + let tval = E.evalValType tenv theType + val <- liftModuleCmd (evalExpr checked) + mExpr<- readBack tval val + case mExpr of + Just expr -> + pure $ JSON.object [ "value" .= expr + , "type string" .= pretty theType + , "type" .= JSONSchema (Forall [] [] theType) + ] + Nothing -> liftIO $ throwIO (invalidType theType) newtype EvalExprParams = EvalExprParams Expression diff --git a/cryptol-remote-api/src/CryptolServer/Exceptions.hs b/cryptol-remote-api/src/CryptolServer/Exceptions.hs index deede65bf..304107f66 100644 --- a/cryptol-remote-api/src/CryptolServer/Exceptions.hs +++ b/cryptol-remote-api/src/CryptolServer/Exceptions.hs @@ -4,7 +4,9 @@ module CryptolServer.Exceptions , invalidBase64 , invalidHex , invalidType + , invalidName , unwantedDefaults + , unknownFreshName , evalInParamMod , evalPolyErr , proverError @@ -26,11 +28,13 @@ import Data.Text (Text) import qualified Data.Text as T import qualified Data.HashMap.Strict as HashMap -import Cryptol.ModuleSystem.Name (Name) +import Cryptol.ModuleSystem.Name (Name, nameIdent) +import Cryptol.Parser.AST (identText) import Cryptol.Parser import qualified Cryptol.TypeCheck.Type as TC import Argo +import CryptolServer.Data.FreshName import CryptolServer.Data.Type cryptolError :: ModuleError -> [ModuleWarning] -> JSONRPCException @@ -162,6 +166,20 @@ invalidType ty = 20040 "Can't convert Cryptol data from this type to JSON" (Just (jsonTypeAndString ty)) +invalidName :: Name -> JSONRPCException +invalidName nm = + makeJSONRPCException + 20041 "Internal error: invalid fresh name for a Cryptol server marshalled value." + (Just (JSON.object ["name" .= (identText (nameIdent nm))])) + +unknownFreshName :: FreshName -> JSONRPCException +unknownFreshName nm = + makeJSONRPCException + 20042 "Internal error: fresh name is not known in the server." + (Just (JSON.object [ "unique" .= (freshNameUnique nm) + , "ident" .= (freshNameText nm) + ])) + unwantedDefaults :: [(TC.TParam, TC.Type)] -> JSONRPCException unwantedDefaults defs = makeJSONRPCException diff --git a/cryptol-remote-api/src/CryptolServer/LoadModule.hs b/cryptol-remote-api/src/CryptolServer/LoadModule.hs index 1bd64849a..4f29aa001 100644 --- a/cryptol-remote-api/src/CryptolServer/LoadModule.hs +++ b/cryptol-remote-api/src/CryptolServer/LoadModule.hs @@ -26,7 +26,7 @@ loadFileDescr = Doc.Paragraph [Doc.Text "Load the specified module (by file path loadFile :: LoadFileParams -> CryptolCommand () loadFile (LoadFileParams fn) = - void $ runModuleCmd (loadModuleByPath fn) + void $ liftModuleCmd (loadModuleByPath fn) newtype LoadFileParams = LoadFileParams FilePath @@ -50,7 +50,7 @@ loadModuleDescr = Doc.Paragraph [Doc.Text "Load the specified module (by name)." loadModule :: LoadModuleParams -> CryptolCommand () loadModule (LoadModuleParams mn) = - void $ runModuleCmd (loadModuleByName mn) + void $ liftModuleCmd (loadModuleByName mn) newtype JSONModuleName = JSONModuleName { unJSONModName :: ModName } diff --git a/cryptol-remote-api/src/CryptolServer/Sat.hs b/cryptol-remote-api/src/CryptolServer/Sat.hs index 02d1f4119..affd90db7 100644 --- a/cryptol-remote-api/src/CryptolServer/Sat.hs +++ b/cryptol-remote-api/src/CryptolServer/Sat.hs @@ -23,7 +23,6 @@ import qualified Data.Text as T import Cryptol.Eval.Concrete (Value) import Cryptol.Eval.Type (TValue, tValTy) -import Cryptol.ModuleSystem (checkExpr) import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv) import Cryptol.Symbolic ( ProverCommand(..), ProverResult(..), QueryType(..) , SatNum(..), CounterExampleType(..)) @@ -45,7 +44,7 @@ proveSatDescr = proveSat :: ProveSatParams -> CryptolCommand ProveSatResult proveSat (ProveSatParams queryType (Prover name) jsonExpr) = do e <- getExpr jsonExpr - (_expr, ty, schema) <- runModuleCmd (checkExpr e) + (ty, schema) <- typecheckExpr e -- TODO validEvalContext expr, ty, schema me <- getModuleEnv let decls = deDecls (meDynEnv me) @@ -73,7 +72,7 @@ proveSat (ProveSatParams queryType (Prover name) jsonExpr) = sbvCfg <- liftIO (setupProver name) >>= \case Left msg -> error msg Right (_ws, sbvCfg) -> return sbvCfg - (_firstProver, res) <- runModuleCmd $ satProve sbvCfg cmd + (_firstProver, res) <- liftModuleCmd $ satProve sbvCfg cmd _stats <- liftIO (readIORef timing) case res of ProverError msg -> raise (proverError msg) @@ -87,9 +86,11 @@ proveSat (ProveSatParams queryType (Prover name) jsonExpr) = satResult :: [(TValue, Expr, Value)] -> CryptolCommand [(JSONType, Expression)] satResult es = traverse result es - result (t, _, v) = - do e <- observe $ readBack t v - return (JSONType mempty (tValTy t), e) + result (t, _, v) = do + me <- readBack t v + case me of + Nothing -> error $ "type is not convertable: " ++ (show t) + Just e -> pure (JSONType mempty (tValTy t), e) data ProveSatResult = Unsatisfiable diff --git a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs index 6477d836b..accfc1201 100644 --- a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs +++ b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs @@ -13,10 +13,8 @@ import qualified Argo.Doc as Doc import Data.Aeson as JSON import Data.Typeable -import Cryptol.ModuleSystem (checkExpr) import CryptolServer -import CryptolServer.Exceptions import CryptolServer.Data.Expression import CryptolServer.Data.Type @@ -25,14 +23,10 @@ checkTypeDescr = Doc.Paragraph [Doc.Text "Check and return the type of the given expression."] checkType :: TypeCheckParams -> CryptolCommand JSON.Value -checkType (TypeCheckParams e) = - do e' <- getExpr e - (_expr, _ty, schema) <- runModuleCmd (checkExpr e') - return (JSON.object [ "type schema" .= JSONSchema schema ]) - where - -- FIXME: Why is this check not being used? - _noDefaults [] = return () - _noDefaults xs@(_:_) = raise (unwantedDefaults xs) +checkType (TypeCheckParams e) = do + e' <- getExpr e + (_ty, schema) <- typecheckExpr e' + return (JSON.object [ "type schema" .= JSONSchema schema ]) newtype TypeCheckParams = TypeCheckParams Expression From d456663ad6bc6d06fa166ea1eca4b9eab1743a7a Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Wed, 2 Jun 2021 10:37:57 -0700 Subject: [PATCH 2/2] chore: address GHC warnings --- cryptol-remote-api/src/CryptolServer.hs | 2 +- cryptol-remote-api/src/CryptolServer/Data/Expression.hs | 2 +- src/Cryptol/REPL/Command.hs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs index 345a5f5dc..5a00e9edd 100644 --- a/cryptol-remote-api/src/CryptolServer.hs +++ b/cryptol-remote-api/src/CryptolServer.hs @@ -29,7 +29,7 @@ import qualified Argo import qualified Argo.Doc as Doc import CryptolServer.Data.FreshName import CryptolServer.Exceptions - ( cryptolError, unknownFreshName, invalidName) + ( cryptolError, invalidName) import CryptolServer.Options ( WithOptions(WithOptions), Options(Options, optEvalOpts) ) diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index 48fd246ed..3e46a7a7e 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -41,7 +41,7 @@ import Cryptol.Eval.Concrete (Value) import Cryptol.Eval.Type (TValue(..), tValTy) import Cryptol.Eval.Value (GenValue(..)) import Cryptol.ModuleSystem - (ModuleEnv, ModuleCmd, getPrimMap, evalDecls, renameType, renameVar, checkExpr, focusedEnv) + (ModuleEnv, ModuleCmd, getPrimMap, evalDecls, renameType, checkExpr, focusedEnv) import Cryptol.ModuleSystem.Env (deNames,meDynEnv, mctxParams, mctxDecls, mctxNames) import Cryptol.ModuleSystem.Monad (runModuleM, interactive, getFocusedEnv) import qualified Cryptol.ModuleSystem.Base as Base diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 141f3bfee..72754ea7a 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -1245,7 +1245,7 @@ helpCmd cmd M.Parameter -> rPutStrLn "// No documentation is available." - showModHelp env disp x = + showModHelp _env disp x = rPrint $ runDoc disp $ vcat [ "`" <> pp x <> "` is a module." ] -- XXX: show doc. if any