GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-17 17:09:35 +03:00
Code Issues Projects Releases Wiki Activity

cryptol-remote-api: submod bump and docs (#1038)

Browse Source 
* cryptol-remote-api: submod bump and docs

* bump submodule

* chore: improve cryptol-remote-api summary docs portion

* cryptol-remote-api/chore: dedup doc strings for servers

* chore: submodule bump (argo) and fixes
This commit is contained in:
Andrew Kent 2021-01-20 15:40:19 -08:00 committed by GitHub
parent c9307065b9
commit 70442e497f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
15 changed files with 283 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
cryptol-remote-api/cryptol-eval-server/Main.hs
View File

@ -1,11 +1,10 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main (main) where
import qualified Data.Aeson as JSON
import Control.Lens hiding (argument)
import Data.Text (Text)
import System.Environment (lookupEnv)
import System.Exit (exitFailure)
import System.FilePath (splitSearchPath)
@ -19,21 +18,24 @@ import Cryptol.TypeCheck.AST (mName)
import Cryptol.Utils.Ident (ModName, modNameToText, textToModName, preludeName)
import Cryptol.Utils.Logger (quietLogger)
import Argo (MethodType(..), Method, mkApp)
import Argo (MethodType(..), AppMethod, mkDefaultApp)
import Argo.DefaultMain
import qualified Argo.Doc as Doc
import CryptolServer
import CryptolServer.Call
import CryptolServer.EvalExpr
import CryptolServer.FocusedModule
import CryptolServer.Names
import CryptolServer.TypeCheck
import CryptolServer.Sat
main :: IO ()
main = customMain initMod initMod initMod description buildApp
main = customMain initMod initMod initMod initMod description buildApp
where
buildApp opts =
mkApp (startingState (userOptions opts)) cryptolEvalMethods
mkDefaultApp "Cryptol RPC Server" evalServerDocs (startingState (userOptions opts)) cryptolEvalMethods
startingState (StartingFile file) reader =
do paths <- getSearchPaths
@ -61,6 +63,14 @@ main = customMain initMod initMod initMod description buildApp
, evalPPOpts = defaultPPOpts
}
evalServerDocs :: [Doc.Block]
evalServerDocs =
[ Doc.Section "Summary" $ [ Doc.Paragraph
[Doc.Text "A remote server for ",
Doc.Link (Doc.URL "https://https://cryptol.net/") "Cryptol",
Doc.Text " that supports only type checking and evaluation of Cryptol code."]]]
description :: String
description =
"An RPC server for Cryptol that supports only type checking and evaluation of Cryptol code."
@ -87,10 +97,36 @@ initMod = StartingFile <$> (Left <$> filename <|> Right . textToModName <$> modu
help "Cryptol module to load on startup" <>
value (modNameToText preludeName)
cryptolEvalMethods :: [(Text, MethodType, JSON.Value -> Method ServerState JSON.Value)]
cryptolEvalMethods :: [AppMethod ServerState]
cryptolEvalMethods =
[ ("focused module", Query, method focusedModule)
, ("evaluate expression", Query, method evalExpression)
, ("visible names", Query, method visibleNames)
, ("check type", Query, method checkType)
[ method
"focused module"
Query
focusedModuleDescr
focusedModule
, method
"evaluate expression"
Query
evalExpressionDescr
evalExpression
, method
"call"
Query
(Doc.Paragraph [Doc.Text "Evaluate the result of calling a Cryptol function on one or more parameters."])
call
, method
"visible names"
Query
visibleNamesDescr
visibleNames
, method
"check type"
Query
(Doc.Paragraph [Doc.Text "Check and return the type of the given expression."])
checkType
, method
"satisfy"
Query
satDescr
sat
]

73
cryptol-remote-api/cryptol-remote-api/Main.hs
View File

@ -1,15 +1,15 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main (main) where
import qualified Data.Aeson as JSON
import Data.Text (Text)
import System.Environment (lookupEnv)
import System.FilePath (splitSearchPath)
import Argo (MethodType(..), Method, mkApp)
import Argo (MethodType(..), AppMethod, mkDefaultApp)
import Argo.DefaultMain
import qualified Argo.Doc as Doc
import CryptolServer
@ -26,26 +26,69 @@ main :: IO ()
main =
do paths <- getSearchPaths
initSt <- setSearchPath paths <$> initialState
theApp <- mkApp (const (pure initSt)) cryptolMethods
theApp <- mkDefaultApp "Cryptol RPC Server" serverDocs (const (pure initSt)) cryptolMethods
defaultMain description theApp
serverDocs :: [Doc.Block]
serverDocs =
[ Doc.Section "Summary" $ [ Doc.Paragraph
[Doc.Text "An RCP server for ",
Doc.Link (Doc.URL "https://https://cryptol.net/") "Cryptol",
Doc.Text " that supports type checking and evaluation of Cryptol code via the methods documented below."]]]
description :: String
description =
"An RPC server for Cryptol that supports type checking and evaluation of Cryptol code."
"An RPC server for Cryptol that supports type checking and evaluation of Cryptol code via the methods documented below."
getSearchPaths :: IO [FilePath]
getSearchPaths =
maybe [] splitSearchPath <$> lookupEnv "CRYPTOLPATH"
cryptolMethods :: [(Text, MethodType, JSON.Value -> Method ServerState JSON.Value)]
cryptolMethods :: [AppMethod ServerState]
cryptolMethods =
[ ("change directory", Command, method cd)
, ("load module", Command, method loadModule)
, ("load file", Command, method loadFile)
, ("focused module", Query, method focusedModule)
, ("evaluate expression", Query, method evalExpression)
, ("call", Query, method call)
, ("visible names", Query, method visibleNames)
, ("check type", Query, method checkType)
, ("satisfy", Query, method sat)
[ method
"change directory"
Command
cdDescr
cd
, method
"load module"
Command
loadModuleDescr
loadModule
, method
"load file"
Command
loadFileDescr
loadFile -- The "current" module. Used to decide how to print names, for example.
, method
"focused module"
Query
focusedModuleDescr
focusedModule
, method
"evaluate expression"
Query
evalExpressionDescr
evalExpression
, method
"call"
Query
callDescr
call
, method
"visible names"
Query
visibleNamesDescr
visibleNames
, method
"check type"
Query
checkTypeDescr
checkType
, method
"satisfy"
Query
satDescr
sat
]

16
cryptol-remote-api/src/CryptolServer.hs
View File

@ -9,6 +9,7 @@ import Control.Lens
import Control.Monad.IO.Class
import Control.Monad.Reader (ReaderT(ReaderT))
import qualified Data.Aeson as JSON
import Data.Text (Text)
import Cryptol.Eval (EvalOpts(..))
import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv, ModuleInput(..))
@ -19,6 +20,7 @@ import Cryptol.ModuleSystem.Fingerprint
import Cryptol.Parser.AST (ModName)
import qualified Argo
import qualified Argo.Doc as Doc
import CryptolServer.Exceptions
import CryptolServer.Options
@ -27,14 +29,14 @@ newtype CryptolMethod a = CryptolMethod { runCryptolMethod :: Options -> Argo.Me
method ::
forall params result.
(JSON.FromJSON params, JSON.ToJSON result) =>
(JSON.FromJSON params, JSON.ToJSON result, Doc.DescribedParams params) =>
Text ->
Argo.MethodType ->
Doc.Block ->
(params -> CryptolMethod result) ->
(JSON.Value -> Argo.Method ServerState JSON.Value)
method f p =
case JSON.fromJSON p of
JSON.Error msg -> Argo.raise $ Argo.invalidParams msg p
JSON.Success (WithOptions opts params) ->
JSON.toJSON <$> runCryptolMethod (f params) opts
Argo.AppMethod ServerState
method name ty doc f = Argo.method name ty doc f'
where f' (WithOptions opts params) = runCryptolMethod (f params) opts
getOptions :: CryptolMethod Options

15
cryptol-remote-api/src/CryptolServer/Call.hs
View File

@ -9,9 +9,11 @@ module CryptolServer.Call
, Encoding(..)
, LetBinding(..)
, call
, callDescr
, CallParams(..)
) where
import qualified Argo.Doc as Doc
import Data.Aeson as JSON hiding (Encoding, Value, decode)
import qualified Data.Aeson as JSON
@ -19,6 +21,11 @@ import CryptolServer
import CryptolServer.Data.Expression
import CryptolServer.EvalExpr (evalExpression')
callDescr :: Doc.Block
callDescr =
Doc.Paragraph
[Doc.Text "Evaluate the result of calling a Cryptol function on one or more parameters."]
call :: CallParams -> CryptolMethod JSON.Value
call (CallParams rawFun rawArgs) =
do fun <- getExpr rawFun
@ -34,3 +41,11 @@ instance FromJSON CallParams where
parseJSON =
withObject "params for \"call\"" $
\o -> CallParams <$> o .: "function" <*> o .: "arguments"
instance Doc.DescribedParams CallParams where
parameterFieldDescription =
[("function",
Doc.Paragraph [Doc.Text "The function being called."])
, ("arguments",
Doc.Paragraph [Doc.Text "The arguments the function is being applied to."])
]

17
cryptol-remote-api/src/CryptolServer/ChangeDir.hs
View File

@ -1,6 +1,11 @@
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.ChangeDir (cd, ChangeDirectoryParams(..)) where
module CryptolServer.ChangeDir
( cd
, cdDescr
, ChangeDirectoryParams(..)
) where
import qualified Argo.Doc as Doc
import Control.Monad.IO.Class
import Data.Aeson as JSON
import System.Directory
@ -9,6 +14,10 @@ import CryptolServer
import CryptolServer.Exceptions
cdDescr :: Doc.Block
cdDescr = Doc.Paragraph
[Doc.Text "Changes the server's working directory to the given path."]
cd :: ChangeDirectoryParams -> CryptolMethod ()
cd (ChangeDirectoryParams newDir) =
do exists <- liftIO $ doesDirectoryExist newDir
@ -23,3 +32,9 @@ instance FromJSON ChangeDirectoryParams where
parseJSON =
withObject "params for \"change directory\"" $
\o -> ChangeDirectoryParams <$> o .: "directory"
instance Doc.DescribedParams ChangeDirectoryParams where
parameterFieldDescription =
[("directory",
Doc.Paragraph [Doc.Text "The path to change the current directory."])
]

20
cryptol-remote-api/src/CryptolServer/EvalExpr.hs
View File

@ -1,12 +1,18 @@
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.EvalExpr (evalExpression, evalExpression', EvalExprParams(..)) where
module CryptolServer.EvalExpr
( evalExpression
, evalExpressionDescr
, evalExpression'
, EvalExprParams(..)
) where
import qualified Argo.Doc as Doc
import Control.Monad.IO.Class
import Data.Aeson as JSON
import Cryptol.ModuleSystem (checkExpr, evalExpr)
import Cryptol.ModuleSystem.Env (meSolverConfig,deEnv,meDynEnv,loadedNewtypes)
import Cryptol.ModuleSystem.Env (meSolverConfig,deEnv,meDynEnv)
import Cryptol.TypeCheck.Solve (defaultReplExpr)
import Cryptol.TypeCheck.Subst (apSubst, listParamSubst)
import Cryptol.TypeCheck.Type (Schema(..))
@ -22,6 +28,10 @@ import CryptolServer.Data.Expression
import CryptolServer.Data.Type
import CryptolServer.Exceptions
evalExpressionDescr :: Doc.Block
evalExpressionDescr =
Doc.Paragraph [Doc.Text "Evaluate the Cryptol expression to a value."]
evalExpression :: EvalExprParams -> CryptolMethod JSON.Value
evalExpression (EvalExprParams jsonExpr) =
do e <- getExpr jsonExpr
@ -59,3 +69,9 @@ instance JSON.FromJSON EvalExprParams where
parseJSON =
JSON.withObject "params for \"evaluate expression\"" $
\o -> EvalExprParams <$> o .: "expression"
instance Doc.DescribedParams EvalExprParams where
parameterFieldDescription =
[("expression",
Doc.Paragraph [Doc.Text "The expression to evaluate."])
]

15
cryptol-remote-api/src/CryptolServer/FocusedModule.hs
View File

@ -1,6 +1,11 @@
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.FocusedModule (focusedModule, FocusedModParams(..)) where
module CryptolServer.FocusedModule
( focusedModule
, focusedModuleDescr
, FocusedModParams(..)
) where
import qualified Argo.Doc as Doc
import Data.Aeson as JSON
import Cryptol.ModuleSystem (meFocusedModule, meLoadedModules)
@ -9,6 +14,11 @@ import Cryptol.Utils.PP
import CryptolServer
focusedModuleDescr :: Doc.Block
focusedModuleDescr =
Doc.Paragraph
[Doc.Text "The 'current' module. Used to decide how to print names, for example."]
focusedModule :: FocusedModParams -> CryptolMethod JSON.Value
focusedModule _ =
do me <- getModuleEnv
@ -25,3 +35,6 @@ data FocusedModParams = FocusedModParams
instance JSON.FromJSON FocusedModParams where
parseJSON _ = pure FocusedModParams
instance Doc.DescribedParams FocusedModParams where
parameterFieldDescription = []

23
cryptol-remote-api/src/CryptolServer/LoadModule.hs
View File

@ -1,11 +1,14 @@
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.LoadModule
( loadFile
, loadFileDescr
, loadModule
, loadModuleDescr
, LoadFileParams(..)
, LoadModuleParams(..)
) where
import qualified Argo.Doc as Doc
import Control.Applicative
import Data.Aeson as JSON
import qualified Data.Text as T
@ -17,6 +20,8 @@ import Cryptol.Parser.AST (ModName)
import CryptolServer
loadFileDescr :: Doc.Block
loadFileDescr = Doc.Paragraph [Doc.Text "Load the specified module (by file path)."]
loadFile :: LoadFileParams -> CryptolMethod ()
loadFile (LoadFileParams fn) =
@ -30,6 +35,18 @@ instance JSON.FromJSON LoadFileParams where
JSON.withObject "params for \"load module\"" $
\o -> LoadFileParams <$> o .: "file"
instance Doc.DescribedParams LoadFileParams where
parameterFieldDescription =
[("file",
Doc.Paragraph [Doc.Text "File path of the module to load."])
]
loadModuleDescr :: Doc.Block
loadModuleDescr = Doc.Paragraph [Doc.Text "Load the specified module (by name)."]
loadModule :: LoadModuleParams -> CryptolMethod ()
loadModule (LoadModuleParams mn) =
void $ runModuleCmd (loadModuleByName mn)
@ -52,3 +69,9 @@ instance JSON.FromJSON LoadModuleParams where
parseJSON =
JSON.withObject "params for \"load module\"" $
\o -> LoadModuleParams . unJSONModName <$> o .: "module name"
instance Doc.DescribedParams LoadModuleParams where
parameterFieldDescription =
[("module name",
Doc.Paragraph [Doc.Text "Name of module to load."])
]

19
cryptol-remote-api/src/CryptolServer/Names.hs
View File

@ -1,8 +1,12 @@
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.Names (visibleNames) where
module CryptolServer.Names
( visibleNames
, visibleNamesDescr
) where
import qualified Argo.Doc as Doc
import qualified Data.Aeson as JSON
import Data.Aeson ((.=))
import qualified Data.Map as Map
@ -20,8 +24,19 @@ import Cryptol.Utils.PP (pp)
import CryptolServer
import CryptolServer.Data.Type
data VisibleNamesParams = VisibleNamesParams
visibleNames :: JSON.Value -> CryptolMethod [NameInfo]
instance JSON.FromJSON VisibleNamesParams where
parseJSON _ = pure VisibleNamesParams
instance Doc.DescribedParams VisibleNamesParams where
parameterFieldDescription = []
visibleNamesDescr :: Doc.Block
visibleNamesDescr =
Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) names."]
visibleNames :: VisibleNamesParams -> CryptolMethod [NameInfo]
visibleNames _ =
do me <- getModuleEnv
let DEnv { deNames = dyNames } = meDynEnv me

6
cryptol-remote-api/src/CryptolServer/Options.hs
View File

@ -1,8 +1,11 @@
{-# OPTIONS_GHC -fno-warn-type-defaults -Wno-missing-deriving-strategies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
module CryptolServer.Options (Options(..), WithOptions(..)) where
import qualified Argo.Doc as Doc
import Data.Aeson hiding (Options)
import qualified Data.HashMap.Strict as HM
@ -51,6 +54,9 @@ instance FromJSON Options where
data WithOptions a = WithOptions Options a
deriving Functor
instance forall params . Doc.DescribedParams params => Doc.DescribedParams (WithOptions params) where
parameterFieldDescription = (Doc.parameterFieldDescription @params)
instance FromJSON a => FromJSON (WithOptions a) where
parseJSON = withObject "parameters with options" $
\o ->

29
cryptol-remote-api/src/CryptolServer/Sat.hs
View File

@ -3,8 +3,14 @@
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
module CryptolServer.Sat (sat, ProveSatParams(..)) where
module CryptolServer.Sat
( sat
, satDescr
, ProveSatParams(..)
)
where
import qualified Argo.Doc as Doc
import Control.Applicative
import Control.Monad.IO.Class
import Data.Aeson ((.=), (.:), FromJSON, ToJSON)
@ -29,6 +35,12 @@ import CryptolServer.Exceptions (evalPolyErr, proverError)
import CryptolServer.Data.Expression
import CryptolServer.Data.Type
satDescr :: Doc.Block
satDescr =
Doc.Paragraph
[ Doc.Text "Find a value which satisfies the given predicate "
, Doc.Text "(i.e., a value which when passed to the argument produces true)."]
sat :: ProveSatParams -> CryptolMethod SatResult
sat (ProveSatParams (Prover name) jsonExpr num) =
do e <- getExpr jsonExpr
@ -129,3 +141,18 @@ instance FromJSON ProveSatParams where
case floatingOrInteger s of
Left (_float :: Double) -> empty
Right int -> pure (SomeSat int)) v)
instance Doc.DescribedParams ProveSatParams where
parameterFieldDescription =
[("prover",
Doc.Paragraph ([Doc.Text "The SMT solver to use to check for satisfiability. I.e., one of the following: "]
++ (concat (map (\p -> [Doc.Literal (T.pack p), Doc.Text ", "]) proverNames))
++ [Doc.Text "."]))
, ("expression",
Doc.Paragraph [Doc.Text "The predicate (i.e., function) to check for satisfiability; "
, Doc.Text "must be a monomorphic function type with return type Bit." ])
, ("result count",
Doc.Paragraph [Doc.Text "How many satisfying results to search for; either a positive integer or "
, Doc.Literal "all", Doc.Text"."])
]

19
cryptol-remote-api/src/CryptolServer/TypeCheck.hs
View File

@ -1,10 +1,15 @@
{-# LANGUAGE OverloadedStrings #-}
module CryptolServer.TypeCheck (checkType, TypeCheckParams(..)) where
module CryptolServer.TypeCheck
( checkType
, checkTypeDescr
, TypeCheckParams(..)
) where
import qualified Argo.Doc as Doc
--import Control.Lens hiding ((.=))
import Data.Aeson as JSON
import Cryptol.ModuleSystem (checkExpr)
import Cryptol.ModuleSystem.Env (meSolverConfig)
@ -13,6 +18,10 @@ import CryptolServer.Exceptions
import CryptolServer.Data.Expression
import CryptolServer.Data.Type
checkTypeDescr :: Doc.Block
checkTypeDescr =
Doc.Paragraph [Doc.Text "Check and return the type of the given expression."]
checkType :: TypeCheckParams -> CryptolMethod JSON.Value
checkType (TypeCheckParams e) =
do e' <- getExpr e
@ -32,3 +41,9 @@ instance JSON.FromJSON TypeCheckParams where
parseJSON =
JSON.withObject "params for \"check type\"" $
\o -> TypeCheckParams <$> o .: "expression"
instance Doc.DescribedParams TypeCheckParams where
parameterFieldDescription =
[("expression",
Doc.Paragraph [Doc.Text "Expression to type check."])
]

28
cryptol-remote-api/test-scripts/cryptol-tests.py
View File

@ -17,14 +17,14 @@ cryptol_path = dir_path.joinpath('test-data')
def low_level_api_test(c):
id_1 = c.send_message("load module", {"module name": "M", "state": None})
id_1 = c.send_command("load module", {"module name": "M", "state": None})
reply_1 = c.wait_for_reply_to(id_1)
assert('result' in reply_1)
assert('state' in reply_1['result'])
assert('answer' in reply_1['result'])
state_1 = reply_1['result']['state']
id_2 = c.send_message("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1})
id_2 = c.send_query("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1})
reply_2 = c.wait_for_reply_to(id_2)
assert('result' in reply_2)
assert('answer' in reply_2['result'])
@ -34,7 +34,7 @@ def low_level_api_test(c):
{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
'expression': 'sequence'})
id_3 = c.send_message("evaluate expression", {"expression": {"expression":"call","function":"g","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1})
id_3 = c.send_query("evaluate expression", {"expression": {"expression":"call","function":"g","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1})
reply_3 = c.wait_for_reply_to(id_3)
assert('result' in reply_3)
assert('answer' in reply_3['result'])
@ -44,7 +44,7 @@ def low_level_api_test(c):
{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
'expression': 'sequence'})
id_4 = c.send_message("evaluate expression", {"expression":{"expression":"call","function":"h","arguments":[{"expression":"sequence","data":[{"expression":"bits","encoding":"hex","data":"ff","width":8},{"expression":"bits","encoding":"hex","data":"ff","width":8}]}]}, "state": state_1})
id_4 = c.send_query("evaluate expression", {"expression":{"expression":"call","function":"h","arguments":[{"expression":"sequence","data":[{"expression":"bits","encoding":"hex","data":"ff","width":8},{"expression":"bits","encoding":"hex","data":"ff","width":8}]}]}, "state": state_1})
reply_4 = c.wait_for_reply_to(id_4)
assert('result' in reply_4)
assert('answer' in reply_4['result'])
@ -61,7 +61,7 @@ def low_level_api_test(c):
"width": 4,
"data": "f"}}}
id_5 = c.send_message("evaluate expression", {"state": state_1, "expression": a_record})
id_5 = c.send_query("evaluate expression", {"state": state_1, "expression": a_record})
reply_5 = c.wait_for_reply_to(id_5)
assert('result' in reply_5)
assert('answer' in reply_5['result'])
@ -76,7 +76,7 @@ def low_level_api_test(c):
'unit':
{'expression': 'unit'}}})
id_6 = c.send_message("evaluate expression",
id_6 = c.send_query("evaluate expression",
{"state": state_1,
"expression": {"expression": "let",
"binders": [{"name": "theRecord", "definition": a_record}],
@ -95,7 +95,7 @@ def low_level_api_test(c):
'unit': {'expression': 'unit'}},
'expression': 'record'}]})
id_7 = c.send_message("evaluate expression",
id_7 = c.send_query("evaluate expression",
{"state": state_1,
"expression": {"expression": "sequence",
"data": [a_record, a_record]}})
@ -112,7 +112,7 @@ def low_level_api_test(c):
'unit': {'expression': 'unit'}},
'expression': 'record'}]})
id_8 = c.send_message("evaluate expression",
id_8 = c.send_query("evaluate expression",
{"state": state_1,
"expression": {"expression": "integer modulo",
"integer": 14,
@ -126,7 +126,7 @@ def low_level_api_test(c):
"integer": 14,
"modulus": 42})
id_9 = c.send_message("evaluate expression",
id_9 = c.send_query("evaluate expression",
{"state": state_1,
"expression": "m `{a=60}"})
reply_9 = c.wait_for_reply_to(id_9)
@ -139,21 +139,21 @@ def low_level_api_test(c):
"modulus": 60})
id_10 = c.send_message("evaluate expression", {"state": state_1, "expression": "two"})
id_10 = c.send_query("evaluate expression", {"state": state_1, "expression": "two"})
reply_10 = c.wait_for_reply_to(id_10)
assert('result' in reply_10)
assert('answer' in reply_10['result'])
assert('value' in reply_10['result']['answer'])
assert(reply_10['result']['answer']['value'] == {'data': '0002', 'width': 15, 'expression': 'bits', 'encoding': 'hex'})
id_11 = c.send_message("evaluate expression", {"state": state_1, "expression": "three"})
id_11 = c.send_query("evaluate expression", {"state": state_1, "expression": "three"})
reply_11 = c.wait_for_reply_to(id_11)
assert('result' in reply_11)
assert('answer' in reply_11['result'])
assert('value' in reply_11['result']['answer'])
assert(reply_11['result']['answer']['value'] == {'data': '0003', 'width': 16, 'expression': 'bits', 'encoding': 'hex'})
id_12 = c.send_message("evaluate expression", {"state": state_1, "expression": "four"})
id_12 = c.send_query("evaluate expression", {"state": state_1, "expression": "four"})
reply_12 = c.wait_for_reply_to(id_12)
assert('result' in reply_12)
assert('answer' in reply_12['result'])
@ -162,7 +162,7 @@ def low_level_api_test(c):
# Test empty options
def test_options(options):
id_opt = c.send_message("evaluate expression", {"state": state_1, "expression": "four", "options": options})
id_opt = c.send_query("evaluate expression", {"state": state_1, "expression": "four", "options": options})
reply_opt = c.wait_for_reply_to(id_opt)
assert('result' in reply_opt)
assert('answer' in reply_opt['result'])
@ -179,7 +179,7 @@ def low_level_api_test(c):
def test_instantiation(t, expected=None):
if expected is None: expected = t
id_t = c.send_message("check type", {"state": state_1, "expression": {"expression": "instantiate", "generic": "id", "arguments": {"a": t}}})
id_t = c.send_query("check type", {"state": state_1, "expression": {"expression": "instantiate", "generic": "id", "arguments": {"a": t}}})
reply_t = c.wait_for_reply_to(id_t)
assert('result' in reply_t)
assert('answer' in reply_t['result'])

2
cryptol-remote-api/test-scripts/eval-server-test.py
View File

@ -34,7 +34,7 @@ assert(poll_result is None)
c = argo.ServerConnection(argo.HttpProcess('http://localhost:50005/'))
mid = c.send_message("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": None})
mid = c.send_query("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": None})
reply = c.wait_for_reply_to(mid)
assert('result' in reply)
assert('answer' in reply['result'])

2
deps/argo vendored

@ -1 +1 @@
Subproject commit 7d2c2085021825668412c62d31534568447d0fdc
Subproject commit 61c8f59525e13773e31f579cff4d816d76a86796