From d7814a959b64b91b9584ee50192965f8fbe4b24e Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 29 May 2021 18:46:23 -0400 Subject: [PATCH 1/2] Bump argo submodule to include docs for method results This bumps the `argo` submodule to include commit https://github.com/GaloisInc/argo/commit/b9b3edd992e57ca31224530f763f313fcf24bab7, which adds the ability to document the results of methods (in addition to their parameters). In addition to dealing with the breaking API changes from that commit, this adds missing documentation for each method's results. --- .../cryptol-eval-server/Main.hs | 8 +- cryptol-remote-api/cryptol-remote-api/Main.hs | 8 +- cryptol-remote-api/src/CryptolServer.hs | 4 +- cryptol-remote-api/src/CryptolServer/Call.hs | 21 +++- cryptol-remote-api/src/CryptolServer/Check.hs | 29 ++++- .../src/CryptolServer/ClearState.hs | 7 +- .../src/CryptolServer/Data/Expression.hs | 116 ++++++++++++++++++ .../src/CryptolServer/Data/Type.hs | 30 +++++ .../src/CryptolServer/EvalExpr.hs | 20 ++- .../src/CryptolServer/ExtendSearchPath.hs | 3 +- .../src/CryptolServer/FocusedModule.hs | 16 ++- .../src/CryptolServer/LoadModule.hs | 5 +- cryptol-remote-api/src/CryptolServer/Names.hs | 19 ++- .../src/CryptolServer/Options.hs | 8 +- cryptol-remote-api/src/CryptolServer/Sat.hs | 33 ++++- .../src/CryptolServer/TypeCheck.hs | 10 +- deps/argo | 2 +- 17 files changed, 319 insertions(+), 20 deletions(-) diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs index 037e0667e..aad844457 100644 --- a/cryptol-remote-api/cryptol-eval-server/Main.hs +++ b/cryptol-remote-api/cryptol-eval-server/Main.hs @@ -36,6 +36,8 @@ import qualified Argo.Doc as Doc import CryptolServer ( ServerState, moduleEnv, tcSolver, initialState, extendSearchPath, command, notification ) import CryptolServer.Call ( call ) +import CryptolServer.Data.Expression ( Expression ) +import CryptolServer.Data.Type ( JSONSchema ) import CryptolServer.EvalExpr ( evalExpressionDescr, evalExpression ) import CryptolServer.ExtendSearchPath @@ -90,7 +92,11 @@ 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."]]] + Doc.Text " that supports only type checking and evaluation of Cryptol code."]] + , Doc.Section "Terms and Types" + [Doc.datatype @Expression, + Doc.datatype @JSONSchema] + ] description :: String description = diff --git a/cryptol-remote-api/cryptol-remote-api/Main.hs b/cryptol-remote-api/cryptol-remote-api/Main.hs index c681f67bf..50df6f28c 100644 --- a/cryptol-remote-api/cryptol-remote-api/Main.hs +++ b/cryptol-remote-api/cryptol-remote-api/Main.hs @@ -18,6 +18,8 @@ import CryptolServer.Call ( call, callDescr ) import CryptolServer.Check ( check, checkDescr ) import CryptolServer.ClearState ( clearState, clearStateDescr, clearAllStates, clearAllStatesDescr ) +import CryptolServer.Data.Expression ( Expression ) +import CryptolServer.Data.Type ( JSONSchema ) import CryptolServer.EvalExpr ( evalExpression, evalExpressionDescr ) import CryptolServer.ExtendSearchPath @@ -47,7 +49,11 @@ 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."]]] + Doc.Text " that supports type checking and evaluation of Cryptol code via the methods documented below."]] + , Doc.Section "Terms and Types" + [Doc.datatype @Expression, + Doc.datatype @JSONSchema] + ] description :: String description = diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs index 051462045..59f5ffde5 100644 --- a/cryptol-remote-api/src/CryptolServer.hs +++ b/cryptol-remote-api/src/CryptolServer.hs @@ -36,7 +36,7 @@ newtype CryptolNotification a = CryptolNotification { runCryptolNotification :: command :: forall params result. - (JSON.FromJSON params, JSON.ToJSON result, Doc.DescribedParams params) => + (JSON.FromJSON params, JSON.ToJSON result, Doc.DescribedMethod params result) => Text -> Doc.Block -> (params -> CryptolCommand result) -> @@ -47,7 +47,7 @@ command name doc f = Argo.command name doc f' notification :: forall params. - (JSON.FromJSON params, Doc.DescribedParams params) => + (JSON.FromJSON params, Doc.DescribedMethod params ()) => Text -> Doc.Block -> (params -> CryptolNotification ()) -> diff --git a/cryptol-remote-api/src/CryptolServer/Call.hs b/cryptol-remote-api/src/CryptolServer/Call.hs index 058269685..2b0b11f4e 100644 --- a/cryptol-remote-api/src/CryptolServer/Call.hs +++ b/cryptol-remote-api/src/CryptolServer/Call.hs @@ -1,8 +1,10 @@ {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} module CryptolServer.Call ( Expression(..) @@ -16,9 +18,11 @@ module CryptolServer.Call import qualified Argo.Doc as Doc import Data.Aeson as JSON hiding (Encoding, Value, decode) import qualified Data.Aeson as JSON +import Data.Typeable (Proxy(..), typeRep) import CryptolServer import CryptolServer.Data.Expression +import CryptolServer.Data.Type import CryptolServer.EvalExpr (evalExpression') callDescr :: Doc.Block @@ -42,10 +46,25 @@ instance FromJSON CallParams where withObject "params for \"call\"" $ \o -> CallParams <$> o .: "function" <*> o .: "arguments" -instance Doc.DescribedParams CallParams where +instance Doc.DescribedMethod CallParams JSON.Value where parameterFieldDescription = [("function", Doc.Paragraph [Doc.Text "The function being called."]) , ("arguments", Doc.Paragraph [Doc.Text "The arguments the function is being applied to."]) ] + + resultFieldDescription = + [ ("value", + Doc.Paragraph [ Doc.Text "A " + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression" + , Doc.Text " that denotes the value" + ]) + , ("type", + Doc.Paragraph [ Doc.Text " A" + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type" + , Doc.Text " that denotes the result type" + ]) + , ("type string", + Doc.Paragraph [Doc.Text "A human-readable representation of the result type"]) + ] diff --git a/cryptol-remote-api/src/CryptolServer/Check.hs b/cryptol-remote-api/src/CryptolServer/Check.hs index 794956f14..ba76820d4 100644 --- a/cryptol-remote-api/src/CryptolServer/Check.hs +++ b/cryptol-remote-api/src/CryptolServer/Check.hs @@ -1,4 +1,5 @@ {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE OverloadedStrings #-} @@ -166,7 +167,7 @@ instance FromJSON CheckParams where Right n -> pure $ Just $ RandomCheckMode $ (toInteger :: Int -> Integer) n) v) num Nothing = pure Nothing -instance Doc.DescribedParams CheckParams where +instance Doc.DescribedMethod CheckParams CheckResult where parameterFieldDescription = [ ("expression", Doc.Paragraph [Doc.Text "The predicate (i.e., function) to check; " @@ -182,3 +183,29 @@ instance Doc.DescribedParams CheckParams where , Doc.Text " sufficiently small, checking may take longer than you are willing to wait!" ]) ] + + resultFieldDescription = + [ ("tests run", + Doc.Paragraph [Doc.Text "The number of tests that were successfully run."]) + , ("tests possible", + Doc.Paragraph [Doc.Text "The maximum number of possible tests."]) + , ("result", + Doc.Paragraph [ Doc.Text "The overall test result, represented as one of three string values:" + , Doc.Literal "pass", Doc.Text " (all tests succeeded), " + , Doc.Literal "fail", Doc.Text " (a test evaluated to ", Doc.Literal "False", Doc.Text "), or" + , Doc.Literal "error", Doc.Text " (an exception was raised during evaluation)." + ]) + , ("arguments", + Doc.Paragraph [ Doc.Text "Only returned if the ", Doc.Literal "result" + , Doc.Text " is ", Doc.Literal "fail", Doc.Text " or ", Doc.Literal "error", Doc.Text ". " + , Doc.Text "An array of JSON objects indicating the arguments passed to the property " + , Doc.Text "which triggered the failure or error. Each object has an " + , Doc.Literal "expr", Doc.Text " field, which is an individual argument expression, and a " + , Doc.Literal "type", Doc.Text " field, which is the type of the argument expression." + ]) + , ("error message", + Doc.Paragraph [ Doc.Text "Only returned if the ", Doc.Literal "result" + , Doc.Text " is ", Doc.Literal "error", Doc.Text ". " + , Doc.Text "A human-readable representation of the exception that was raised during evaluation." + ]) + ] diff --git a/cryptol-remote-api/src/CryptolServer/ClearState.hs b/cryptol-remote-api/src/CryptolServer/ClearState.hs index efe18b9c5..0eed35120 100644 --- a/cryptol-remote-api/src/CryptolServer/ClearState.hs +++ b/cryptol-remote-api/src/CryptolServer/ClearState.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} module CryptolServer.ClearState ( clearState @@ -20,8 +21,8 @@ instance JSON.FromJSON ClearStateParams where JSON.withObject "params for \"clear state\"" $ \o -> ClearStateParams <$> o .: "state to clear" -instance Doc.DescribedParams ClearStateParams where - parameterFieldDescription = +instance Doc.DescribedMethod ClearStateParams () where + parameterFieldDescription = [("state to clear", Doc.Paragraph [Doc.Text "The state to clear from the server to make room for other unrelated states."]) ] @@ -42,7 +43,7 @@ instance JSON.FromJSON ClearAllStatesParams where JSON.withObject "params for \"clear all states\"" $ \_ -> pure ClearAllStatesParams -instance Doc.DescribedParams ClearAllStatesParams where +instance Doc.DescribedMethod ClearAllStatesParams () where parameterFieldDescription = [] clearAllStatesDescr :: Doc.Block diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index ba537997a..c6cb6ca1c 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -4,6 +4,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} module CryptolServer.Data.Expression ( module CryptolServer.Data.Expression @@ -24,6 +25,7 @@ import qualified Data.Scientific as Sc import Data.Text (Text, pack) import qualified Data.Text as T import Data.Traversable +import Data.Typeable (Proxy(..), typeRep) import qualified Data.Vector as V import Data.Text.Encoding (encodeUtf8) import Numeric (showHex) @@ -49,6 +51,7 @@ import Cryptol.Utils.Ident import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields) import Argo +import qualified Argo.Doc as Doc import CryptolServer import CryptolServer.Exceptions import CryptolServer.Data.Type @@ -235,6 +238,119 @@ instance JSON.ToJSON Expression where -- serialize Type PName that never gets called and just bitrots. toJSON gen +instance Doc.Described Expression where + typeName = "JSON Cryptol Expressions" + description = + [ Doc.Paragraph [Doc.Text "In the API, Cryptol expressions can be represented by the following:"] + , Doc.DescriptionList + [ (pure $ Doc.Text "JSON Booleans", + Doc.Paragraph [Doc.Text "Represent the corresponding Cryptol Booleans"]) + , (pure $ Doc.Text "JSON Integers", + Doc.Paragraph [Doc.Text "Cryptol integer literals, that can be used at a variety of types"]) + , (pure $ Doc.Text "JSON Strings", + Doc.Paragraph [Doc.Text "Cryptol concrete syntax"]) + , (pure $ Doc.Text "JSON Objects", + Doc.Paragraph [ Doc.Text "Objects can represent a variety of Cryptol expressions. The field " + , Doc.Literal "expression" + , Doc.Text " contains a tag that can be used to determine the remaining fields." + ]) + ] + , Doc.Paragraph [Doc.Text "The tag values in objects can be:"] + , Doc.DescriptionList + [ (pure $ Doc.Literal "bits", + Doc.BulletedList + [ Doc.Paragraph [Doc.Text "The expression is a bitvector. Further fields are:"] + , Doc.Paragraph [ Doc.Literal "encoding", Doc.Text ": Either the string " + , Doc.Literal "base64", Doc.Text " or ", Doc.Literal "hex" + , Doc.Text ", for base-64 or hexadecimal representations of the bitvector" + ] + , Doc.Paragraph [Doc.Literal "data", Doc.Text ": A string containing the actual data"] + , Doc.Paragraph [Doc.Literal "width", Doc.Text ": An integer: the bit-width of the represented bit vector"] + ]) + , (pure $ Doc.Literal "record", + Doc.Paragraph [ Doc.Text "The expression is a record. The field " + , Doc.Literal "data", Doc.Text " is a JSON object that maps record field names to " + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expressions" + , Doc.Text "." + ]) + , (pure $ Doc.Literal "sequence", + Doc.Paragraph [ Doc.Text "The expression is a sequence. The field " + , Doc.Literal "data" + , Doc.Text "contains a JSON array of the elements of the sequence; " + , Doc.Text "each is a JSON Cryptol expression." + ]) + , (pure $ Doc.Literal "tuple", + Doc.Paragraph [ Doc.Text "The expression is a tuple. The field " + , Doc.Literal "data" + , Doc.Text "contains a JSON array of the elements of the tuple; " + , Doc.Text "each is a JSON Cryptol expression." + ]) + , (pure $ Doc.Literal "unit", + Doc.Paragraph [Doc.Text "The expression is the unit constructor, and there are no further fields."]) + , (pure $ Doc.Literal "let", + Doc.BulletedList + [ Doc.Paragraph [ Doc.Text "The expression is a ", Doc.Literal "where" + , Doc.Text "binding. The fields are:" + ] + , Doc.DescriptionList + [ (pure $ Doc.Literal "binders", + Doc.BulletedList + [ Doc.Paragraph [Doc.Text "A list of binders. Each binder is an object with two fields:"] + , Doc.Paragraph [ Doc.Literal "name" + , Doc.Text ": A string that is the name to be bound, and" + ] + , Doc.Paragraph [ Doc.Literal "definition" + , Doc.Text "A " + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression" + , Doc.Text "." + ] + ]) + , (pure $ Doc.Literal "body", + Doc.Paragraph [ Doc.Text "A " + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression" + , Doc.Text " in which the bound names may be used." + ]) + ] + ]) + , (pure $ Doc.Literal "call", + Doc.BulletedList + [ Doc.Paragraph [Doc.Text "The expression is a function application. Further fields are:"] + , Doc.Paragraph [ Doc.Literal "function", Doc.Text ": A " + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression" + , Doc.Text "." + ] + , Doc.Paragraph [ Doc.Literal "arguments", Doc.Text ": A JSON array of " + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expressions" + , Doc.Text "." + ] + ]) + , (pure $ Doc.Literal "instantiate", + Doc.BulletedList + [ Doc.Paragraph [Doc.Text "The expression is a type application. Further fields are:"] + , Doc.Paragraph [ Doc.Literal "generic" + , Doc.Text ": The polymorphic expression to be instantiated" + ] + , Doc.Paragraph [ Doc.Literal "arguments" + , Doc.Text ": A JSON object in which keys are the names of type parameters and values are " + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol types" + , Doc.Text "." + ] + ]) + , (pure $ Doc.Literal "integer modulo", + Doc.BulletedList + [ Doc.Paragraph [ Doc.Text "The expression is an integer with a modulus (the Cryptol " + , Doc.Literal "Z", Doc.Text " type). Further fields are:" + ] + , Doc.Paragraph [ Doc.Literal "integer" + , Doc.Text ": A JSON number, representing the integer" + ] + , Doc.Paragraph [ Doc.Literal "modulus" + , Doc.Text ": A JSON number, representing the modulus" + ] + ]) + ] + ] + decode :: (Argo.Method m, Monad m) => Encoding -> Text -> m Integer decode Base64 txt = diff --git a/cryptol-remote-api/src/CryptolServer/Data/Type.hs b/cryptol-remote-api/src/CryptolServer/Data/Type.hs index b511f2eaa..19e496f20 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Type.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Type.hs @@ -26,6 +26,8 @@ import Cryptol.Utils.Ident (mkIdent) import Cryptol.Utils.PP (pp) import Cryptol.Utils.RecordMap (canonicalFields) +import qualified Argo.Doc as Doc + newtype JSONSchema = JSONSchema Schema @@ -294,3 +296,31 @@ instance JSON.FromJSON JSONPType where unaryPropF prop f o = unaryProp prop <$> typeField o f binTC tc f1 f2 o = tc <$> typeField o f1 <*> typeField o f2 tyFun tf o = C.TUser (name tf) <$> typeListField o "arguments" + +instance Doc.Described JSONSchema where + typeName = "JSON Cryptol Types" + description = + [ Doc.Paragraph [Doc.Text "JSON representations of types are type schemas. A type schema has three fields:"] + , Doc.DescriptionList + [ (pure $ Doc.Literal "forall", + Doc.Paragraph [ Doc.Text "Contains an array of objects. Each object has two fields: " + , Doc.Literal "name", Doc.Text " is the name of a type variable, and " + , Doc.Literal "kind", Doc.Text " is its kind. There are four kind formers: the string " + , Doc.Literal "Type", Doc.Text " represents ordinary datatypes, the string " + , Doc.Literal "Num", Doc.Text " is the kind of numbers, and " + , Doc.Literal "Prop", Doc.Text " is the kind of propositions. " + , Doc.Text "Arrow kinds are represented by objects in which the field " + , Doc.Literal "kind", Doc.Text " is the string " + , Doc.Literal "arrow", Doc.Text ", and the fields " + , Doc.Literal "from", Doc.Text " and ", Doc.Literal "to" + , Doc.Text " are the kinds on the left and right side of the arrow, respectively." + ]) + , (pure $ Doc.Literal "propositions", + Doc.Paragraph [Doc.Text "A JSON array of the constraints in the type."]) + , (pure $ Doc.Literal "type", + Doc.Paragraph [ Doc.Text "The type in which the variables from " + , Doc.Literal "forall", Doc.Text " are in scope and the constraints in " + , Doc.Literal "propositions", Doc.Text " are in effect." + ]) + ] + ] diff --git a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs index 77f6c5853..fdd2c1365 100644 --- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs +++ b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs @@ -1,4 +1,6 @@ +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} module CryptolServer.EvalExpr ( evalExpression , evalExpressionDescr @@ -9,6 +11,7 @@ module CryptolServer.EvalExpr import qualified Argo.Doc as Doc import Control.Monad.IO.Class import Data.Aeson as JSON +import Data.Typeable (Proxy(..), typeRep) import Cryptol.ModuleSystem (checkExpr, evalExpr) @@ -68,8 +71,23 @@ instance JSON.FromJSON EvalExprParams where JSON.withObject "params for \"evaluate expression\"" $ \o -> EvalExprParams <$> o .: "expression" -instance Doc.DescribedParams EvalExprParams where +instance Doc.DescribedMethod EvalExprParams JSON.Value where parameterFieldDescription = [("expression", Doc.Paragraph [Doc.Text "The expression to evaluate."]) ] + + resultFieldDescription = + [ ("value", + Doc.Paragraph [ Doc.Text "A " + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @Expression))) "JSON Cryptol expression" + , Doc.Text " that denotes the value" + ]) + , ("type", + Doc.Paragraph [ Doc.Text " A" + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type" + , Doc.Text " that denotes the result type" + ]) + , ("type string", + Doc.Paragraph [Doc.Text "A human-readable representation of the result type"]) + ] diff --git a/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs b/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs index eccd21dcc..f4d37ff93 100644 --- a/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs +++ b/cryptol-remote-api/src/CryptolServer/ExtendSearchPath.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} module CryptolServer.ExtendSearchPath ( extSearchPath @@ -31,7 +32,7 @@ instance FromJSON ExtendSearchPathParams where withObject "params for \"extend search path\"" $ \o -> ExtendSearchPathParams <$> o .: "paths" -instance Doc.DescribedParams ExtendSearchPathParams where +instance Doc.DescribedMethod ExtendSearchPathParams () where parameterFieldDescription = [("paths", Doc.Paragraph [Doc.Text "The paths to add to the search path."]) diff --git a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs index 318468c75..4ea5a6c39 100644 --- a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs +++ b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} module CryptolServer.FocusedModule ( focusedModule @@ -36,5 +37,18 @@ data FocusedModParams = FocusedModParams instance JSON.FromJSON FocusedModParams where parseJSON _ = pure FocusedModParams -instance Doc.DescribedParams FocusedModParams where +instance Doc.DescribedMethod FocusedModParams JSON.Value where parameterFieldDescription = [] + + resultFieldDescription = + [ ("module", + Doc.Paragraph [ Doc.Text "The name of the focused module, which would be shown in the " + , Doc.Text "prompt in the Cryptol REPL, or " + , Doc.Literal "null", Doc.Text " if there is no such focused module." + ]) + , ("parameterized", + Doc.Paragraph [ Doc.Text "A Boolean value indicating whether the focused module is " + , Doc.Text "parameterized. This field is only present when the module name is not " + , Doc.Literal "null", Doc.Text "." + ]) + ] diff --git a/cryptol-remote-api/src/CryptolServer/LoadModule.hs b/cryptol-remote-api/src/CryptolServer/LoadModule.hs index 7f924e596..1bd64849a 100644 --- a/cryptol-remote-api/src/CryptolServer/LoadModule.hs +++ b/cryptol-remote-api/src/CryptolServer/LoadModule.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} module CryptolServer.LoadModule ( loadFile @@ -36,7 +37,7 @@ instance JSON.FromJSON LoadFileParams where \o -> LoadFileParams <$> o .: "file" -instance Doc.DescribedParams LoadFileParams where +instance Doc.DescribedMethod LoadFileParams () where parameterFieldDescription = [("file", Doc.Paragraph [Doc.Text "File path of the module to load."]) @@ -70,7 +71,7 @@ instance JSON.FromJSON LoadModuleParams where JSON.withObject "params for \"load module\"" $ \o -> LoadModuleParams . unJSONModName <$> o .: "module name" -instance Doc.DescribedParams LoadModuleParams where +instance Doc.DescribedMethod LoadModuleParams () where parameterFieldDescription = [("module name", Doc.Paragraph [Doc.Text "Name of module to load."]) diff --git a/cryptol-remote-api/src/CryptolServer/Names.hs b/cryptol-remote-api/src/CryptolServer/Names.hs index 1552d8c31..12b73e89c 100644 --- a/cryptol-remote-api/src/CryptolServer/Names.hs +++ b/cryptol-remote-api/src/CryptolServer/Names.hs @@ -1,6 +1,9 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} module CryptolServer.Names ( visibleNames , visibleNamesDescr @@ -12,6 +15,7 @@ import Data.Aeson ((.=)) import qualified Data.Map as Map import Data.Map (Map) import Data.Text (unpack) +import Data.Typeable (Proxy(..), typeRep) import Cryptol.Parser.Name (PName(..)) import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), focusedEnv) @@ -31,9 +35,22 @@ data VisibleNamesParams = VisibleNamesParams instance JSON.FromJSON VisibleNamesParams where parseJSON _ = pure VisibleNamesParams -instance Doc.DescribedParams VisibleNamesParams where +instance Doc.DescribedMethod VisibleNamesParams [NameInfo] where parameterFieldDescription = [] + resultFieldDescription = + [ ("name", + Doc.Paragraph [Doc.Text "A human-readable representation of the name"]) + , ("type string", + Doc.Paragraph [Doc.Text "A human-readable representation of the name's type schema"]) + , ("type", + Doc.Paragraph [ Doc.Text " A" + , Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol type" + ]) + , ("documentation", + Doc.Paragraph [Doc.Text "An optional field containing documentation string for the name, if it is documented"]) + ] + visibleNamesDescr :: Doc.Block visibleNamesDescr = Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) names."] diff --git a/cryptol-remote-api/src/CryptolServer/Options.hs b/cryptol-remote-api/src/CryptolServer/Options.hs index e9ee3fb99..fe0310cc4 100644 --- a/cryptol-remote-api/src/CryptolServer/Options.hs +++ b/cryptol-remote-api/src/CryptolServer/Options.hs @@ -1,8 +1,11 @@ {-# OPTIONS_GHC -fno-warn-type-defaults -Wno-missing-deriving-strategies #-} {-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UndecidableInstances #-} module CryptolServer.Options (Options(..), WithOptions(..)) where import qualified Argo.Doc as Doc @@ -73,8 +76,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 forall params result . Doc.DescribedMethod params result => Doc.DescribedMethod (WithOptions params) result where + parameterFieldDescription = Doc.parameterFieldDescription @params + resultFieldDescription = Doc.resultFieldDescription @params @result instance FromJSON a => FromJSON (WithOptions a) where parseJSON = withObject "parameters with options" $ diff --git a/cryptol-remote-api/src/CryptolServer/Sat.hs b/cryptol-remote-api/src/CryptolServer/Sat.hs index a4224762d..02d1f4119 100644 --- a/cryptol-remote-api/src/CryptolServer/Sat.hs +++ b/cryptol-remote-api/src/CryptolServer/Sat.hs @@ -1,4 +1,5 @@ {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE OverloadedStrings #-} @@ -168,7 +169,7 @@ instance FromJSON ProveSatParams where Right int -> pure (SomeSat int)) v) -instance Doc.DescribedParams ProveSatParams where +instance Doc.DescribedMethod ProveSatParams ProveSatResult where parameterFieldDescription = [("prover", Doc.Paragraph ([Doc.Text "The SMT solver to use to check for satisfiability. I.e., one of the following: "] @@ -195,3 +196,33 @@ instance Doc.DescribedParams ProveSatParams where ] ) ] + + resultFieldDescription = + [ ("result", + Doc.Paragraph [ Doc.Text "A string (one of " + , Doc.Literal "unsatisfiable", Doc.Text ", " + , Doc.Literal "invalid", Doc.Text ", or " + , Doc.Literal "satisfied" + , Doc.Text ") indicating the result of checking for validity, satisfiability, or safety." + ]) + , ("counterexample type", + Doc.Paragraph $ onlyIfResultIs "invalid" ++ + [ Doc.Text "This describes the variety of counterexample that was produced. This can be either " + , Doc.Literal "safety violation", Doc.Text " or ", Doc.Literal "predicate falsified", Doc.Text "." + ]) + , ("counterexample", + Doc.Paragraph $ onlyIfResultIs "invalid" ++ + [ Doc.Text "A list of objects where each object has an " + , Doc.Literal "expr", Doc.Text "field, indicating a counterexample expression, and a " + , Doc.Literal "type", Doc.Text "field, indicating the type of the expression." + ]) + , ("models", + Doc.Paragraph $ onlyIfResultIs "satisfied" ++ + [ Doc.Text "A list of list of objects where each object has an " + , Doc.Literal "expr", Doc.Text "field, indicating a expression in a model, and a " + , Doc.Literal "type", Doc.Text "field, indicating the type of the expression." + ]) + ] + where + onlyIfResultIs val = [ Doc.Text "Only used if the " , Doc.Literal "result" + , Doc.Text " is ", Doc.Literal val, Doc.Text "." ] diff --git a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs index b9207b82a..6477d836b 100644 --- a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs +++ b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs @@ -1,4 +1,6 @@ +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} module CryptolServer.TypeCheck ( checkType , checkTypeDescr @@ -9,6 +11,7 @@ import qualified Argo.Doc as Doc --import Control.Lens hiding ((.=)) import Data.Aeson as JSON +import Data.Typeable import Cryptol.ModuleSystem (checkExpr) @@ -39,8 +42,13 @@ instance JSON.FromJSON TypeCheckParams where JSON.withObject "params for \"check type\"" $ \o -> TypeCheckParams <$> o .: "expression" -instance Doc.DescribedParams TypeCheckParams where +instance Doc.DescribedMethod TypeCheckParams JSON.Value where parameterFieldDescription = [("expression", Doc.Paragraph [Doc.Text "Expression to type check."]) ] + + resultFieldDescription = + [("type schema", + Doc.Paragraph [Doc.Text "A ", Doc.Link (Doc.TypeDesc (typeRep (Proxy @JSONSchema))) "JSON Cryptol Type"]) + ] diff --git a/deps/argo b/deps/argo index 1040dc26d..c73371813 160000 --- a/deps/argo +++ b/deps/argo @@ -1 +1 @@ -Subproject commit 1040dc26d142f13ff8ed6617ff5212f476b78c45 +Subproject commit c733718138c10c70c6e690d4a2de83a7b07e6cc9 From 88c369a2715f0d0cdd7e294f4c11d9944a11cc6a Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 30 May 2021 10:55:01 -0400 Subject: [PATCH 2/2] Autogenerate cryptol-remote-api docs (and check them in CI) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Unfortunately, the autogenerated documentation (now located in `Cryptol.rst`) doesn't yet have all of the information contained within the hand-written documentation (now located in `old-Cryptol.rst`—see #1206. In pursuit of eventually fixing that issue, the CI now makes sure that any changes to the autogenerated documentation are checked in. --- .github/ci.sh | 4 + .github/workflows/ci.yml | 3 + cry | 7 + cryptol-remote-api/check_docs.sh | 14 + cryptol-remote-api/docs/.gitignore | 1 + cryptol-remote-api/docs/Cryptol.rst | 782 ++++++++++++++++-------- cryptol-remote-api/docs/old-Cryptol.rst | 353 +++++++++++ 7 files changed, 898 insertions(+), 266 deletions(-) create mode 100755 cryptol-remote-api/check_docs.sh create mode 100644 cryptol-remote-api/docs/old-Cryptol.rst diff --git a/.github/ci.sh b/.github/ci.sh index f48171fe4..418be5050 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -147,6 +147,10 @@ test_rpc() { ./cry rpc-test } +check_rpc_docs() { + ./cry rpc-docs +} + bundle_files() { doc=dist/share/doc/cryptol lib=dist/share/cryptol diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2e5ba3f74..ec1b2b146 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -129,6 +129,9 @@ jobs: - shell: bash run: .github/ci.sh test_rpc if: runner.os != 'Windows' + - shell: bash + run: .github/ci.sh check_rpc_docs + if: runner.os != 'Windows' - if: matrix.ghc == '8.8.4' uses: actions/upload-artifact@v2 diff --git a/cry b/cry index bba30b7f8..5566a0951 100755 --- a/cry +++ b/cry @@ -21,6 +21,7 @@ Available commands: test Run some tests (may take a while) quick-test Like "test" but run fewer tests by default rpc-test Run RPC server tests + rpc-docs Check that the RPC documentation is up-to-date exe-path Print the location of the local executable EOM } @@ -90,6 +91,12 @@ case $COMMAND in $DIR/cryptol-remote-api/run_rpc_tests.sh ;; + rpc-docs) + echo "Checking cryptol-remote-api docs (Cryptol.rst) are up-to-date with server" + DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" + $DIR/cryptol-remote-api/check_docs.sh + ;; + help) show_usage && exit 0 ;; diff --git a/cryptol-remote-api/check_docs.sh b/cryptol-remote-api/check_docs.sh new file mode 100755 index 000000000..d6ae3b1b7 --- /dev/null +++ b/cryptol-remote-api/check_docs.sh @@ -0,0 +1,14 @@ +#! /bin/bash + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" + +cd $DIR/docs + +export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-remote-api) +if [[ ! -x "$CRYPTOL_SERVER" ]]; then + echo "could not locate cryptol-remote-api executable - try executing with cabal v2-exec" + exit 1 +fi + +$CRYPTOL_SERVER doc > TEMP.rst +diff Cryptol.rst TEMP.rst diff --git a/cryptol-remote-api/docs/.gitignore b/cryptol-remote-api/docs/.gitignore index 69fa449dd..0b51bc8ed 100644 --- a/cryptol-remote-api/docs/.gitignore +++ b/cryptol-remote-api/docs/.gitignore @@ -1 +1,2 @@ _build/ +TEMP.rst diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index bcebebf0c..a59026bd1 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -1,353 +1,603 @@ -================== -Cryptol Evaluation +Cryptol RPC Server ================== -All methods in this section additionally propagate server state in the -manner described in the prior section. +Fundamental Protocol +-------------------- -These methods may return :ref:`a variety of Cryptol errors -`, with codes in the range of ``20000``-``29999``. +This application is a `JSON-RPC `_ server. Additionally, it maintains a persistent cache of application states and explicitly indicates the state in which each command is to be carried out. -Options -======= +Transport +~~~~~~~~~ -Many of the options that can be set using the ``:set`` command at the -Cryptol REPL can be provided as parameters to methods in this API. In -addition to the listed fields, every command accepts an optional -``options`` parameter. Its value should be an object, and may have -zero or more of the following fields: +The server supports three transport methods: - - ``call stacks``: A Boolean that determines whether to track call stacks. - - ``output``: An object that contains further parameters to control strings generated by Cryptol (these are visible in e.g. error messages, but do not affect the structured data returned in the API): - + ``ASCII``: A Boolean (default ``true``). - + ``base``: What base to display numbers in (default ``10``). - + ``prefix of infinite lengths``: How much of an infinite sequence to display (default ``5``. - + ``floating point base``: What base to display floating point numbers in (default ``10``). - + ``floating point format``: The output format used to display floating point numbers (accepts strings in the same format as the argument to ``:set fpFormat`` in the REPL). -Module Management -================= +``stdio`` + in which the server communicates over ``stdin`` and ``stdout`` + + -Changing Directories --------------------- +Socket + in which the server communicates over ``stdin`` and ``stdout`` + + -:Method name: - ``change directory`` -:Parameters: - - ``directory``: The new working directory, represented as a string. +HTTP + in which the server communicates over HTTP + + +In both ``stdio`` and socket mode, messages are delimited using `netstrings. `_ -Loading Modules ---------------- -:Method name: - ``load module`` -:Parameters: - - ``module name``: The name of the Cryptol module to be loaded. - -Loading Files -------------- - -:Method name: - ``load file`` -:Parameters: - - ``file``: The name of the Cryptol source file to be loaded. - -Module Context --------------- - -:Method name: - ``focused module`` -:Parameters: none -:Return fields: - - ``module``: The name of the focused module, which would be shown in the - prompt in the Cryptol REPL, or ``null`` if there is no such focused module. - - ``parameterized``: A Boolean value indicating whether the focused module is - parameterized. This field is only present when the module name is not - ``null``. - -Evaluation and Typechecking -=========================== - -Evaluating Expressions ----------------------- - -This method evaluates a Cryptol expression. The type of the expression -needs to be fully-determined and finite - that is, functions and -infinite streams are not supported, and neither is polymorphism. - -:Method name: - ``evaluate expression`` -:Parameters: - - ``expression``: The :ref:`JSON Cryptol expression ` to be evaluated -:Return fields: - - ``value``: A :ref:`JSON Cryptol expression ` that denotes the value - - ``type``: A :ref:`JSON Cryptol type ` that denotes the result type - - ``type string``: A human-readable representation of the result type - -Calling Functions ------------------ - -Note: this method may be removed in the future, because its abilities -have been subsumed by ``evaluate expression``. - -This method applies a Cryptol function to some arguments. The type of -the resulting expression needs to be fully-determined and finite - -that is, functions and infinite streams are not supported, and neither -is polymorphism. - -:Method name: - ``call`` -:Parameters: - - ``function``: The name of a Cryptol function that is currently in scope - - ``arguments``: A list of arguments to the function, encoded as JSON - Cryptol expressions -:Return fields: - - ``value``: A :ref:`JSON Cryptol expression ` that denotes the value - - ``type``: A :ref:`JSON Cryptol type ` that denotes the result type - - ``type string``: A human-readable representation of the result type - -Visible Names -------------- - -Return information about all names in scope. - -:Method name: - ``visible names`` -:Parameters: none -:Return value: - A list of name information objects. Each name information object has the following - fields: - - - ``name``: A human-readable representation of the name - - ``type string``: A human-readable representation of the name's type schema - - ``type``: A :ref:`JSON Cryptol type ` - - Some will additionally have the following field: - - - ``documentation``: The documentation string for the name, if it is documented - -Checking Types --------------- - -Check the type of an expression. - -:Method name: - ``check type`` -:Parameters: - - ``expression``: A :ref:`JSON Cryptol expression ` for which a type is desired. -:Return fields: - - ``type schema``: A :ref:`JSON Cryptol type ` - -SAT ---- - -This method is not yet ready for public consumption. +Application State +~~~~~~~~~~~~~~~~~ -Terms and Types -=============== +According to the JSON-RPC specification, the ``params`` field in a message object must be an array or object. In this protocol, it is always an object. While each message may specify its own arguments, every message has a parameter field named ``state``. + +When the first message is sent from the client to the server, the ``state`` parameter should be initialized to the JSON null value ``null``. Replies from the server may contain a new state that should be used in subsequent requests, so that state changes executed by the request are visible. Prior versions of this protocol represented the initial state as the empty array ``[]``, but this is now deprecated and will be removed. + +In particular, per JSON-RPC, non-error replies are always a JSON object that contains a ``result`` field. The result field always contains an ``answer`` field and a ``state`` field, as well as ``stdout`` and ``stderr``. + + +``answer`` + The value returned as a response to the request (the precise contents depend on which request was sent) + + -.. _cryptol-json-expression: +``state`` + The state, to be sent in subsequent requests. If the server did not modify its state in response to the command, then this state may be the same as the one sent by the client. + + + +``stdout`` and ``stderr`` + These fields contain the contents of the Unix ``stdout`` and ``stderr`` file descriptors. They are intended as a stopgap measure for clients who are still in the process of obtaining structured information from the libraries on which they depend, so that information is not completely lost to users. However, the server may or may not cache this information and resend it. Applications are encouraged to used structured data and send it deliberately as the answer. + + +The precise structure of states is considered an implementation detail that could change at any time. Please treat them as opaque tokens that may be saved and re-used within a given server process, but not created by the client directly. + + + +Summary +------- + +An RCP server for `Cryptol `_ that supports type checking and evaluation of Cryptol code via the methods documented below. + + +Terms and Types +--------------- +.. _Expression: JSON Cryptol Expressions ------------------------- +~~~~~~~~~~~~~~~~~~~~~~~~ In the API, Cryptol expressions can be represented by the following: + JSON Booleans Represent the corresponding Cryptol Booleans + + JSON Integers Cryptol integer literals, that can be used at a variety of types + + JSON Strings Cryptol concrete syntax + + JSON Objects - Objects can represent a variety of Cryptol expressions. The field - ``expression`` contains a tag that can be used to determine the - remaining fields. - + Objects can represent a variety of Cryptol expressions. The field ``expression`` contains a tag that can be used to determine the remaining fields. + + The tag values in objects can be: -``bits`` - The expression is a bitvector. Further fields are: - + ``encoding``: Either the string ``base64`` or ``hex``, for base-64 or hexadecimal - representations of the bitvector - + ``data``: A string containing the actual data - + ``width``: An integer: the bit-width of the represented bit vector +``bits`` + + * The expression is a bitvector. Further fields are: + + + + * ``encoding``: Either the string ``base64`` or ``hex``, for base-64 or hexadecimal representations of the bitvector + + + + * ``data``: A string containing the actual data + + + + * ``width``: An integer: the bit-width of the represented bit vector + + + ``record`` - The expression is a record. The field ``data`` is a JSON - object that maps record field names to :ref:`JSON Cryptol expressions `. + The expression is a record. The field ``data`` is a JSON object that maps record field names to :ref:`JSON Cryptol expressions `. + + ``sequence`` - The expression is a sequence. The field ``data`` contains a - JSON array of the elements of the sequence; each is a JSON Cryptol - expression. + The expression is a sequence. The field ``data``contains a JSON array of the elements of the sequence; each is a JSON Cryptol expression. + + ``tuple`` - The expression is a tuple. The field ``data`` contains a JSON - array of the elements of the tuple; each is a JSON Cryptol - expression. + The expression is a tuple. The field ``data``contains a JSON array of the elements of the tuple; each is a JSON Cryptol expression. + + ``unit`` The expression is the unit constructor, and there are no further fields. + + ``let`` - The expression is a ``where`` binding. The fields are: + + * The expression is a ``where``binding. The fields are: + + + + * + ``binders`` + + * A list of binders. Each binder is an object with two fields: + + + + * ``name``: A string that is the name to be bound, and + + + + * ``definition``A :ref:`JSON Cryptol expression `. + + + + + ``body`` + A :ref:`JSON Cryptol expression ` in which the bound names may be used. + + + + - ``binders`` - A list of binders. Each binder is an object with two fields: +``call`` + + * The expression is a function application. Further fields are: + + + + * ``function``: A :ref:`JSON Cryptol expression `. + + + + * ``arguments``: A JSON array of :ref:`JSON Cryptol expressions `. + + + - - ``name``: A string that is the name to be bound, and - - ``definition``: A :ref:`JSON Cryptol expression `. +``instantiate`` + + * The expression is a type application. Further fields are: + + + + * ``generic``: The polymorphic expression to be instantiated + + + + * ``arguments``: A JSON object in which keys are the names of type parameters and values are :ref:`JSON Cryptol types `. + + + - ``body`` - A :ref:`JSON Cryptol expression ` in which the bound names may be used. +``integer modulo`` + + * The expression is an integer with a modulus (the Cryptol ``Z`` type). Further fields are: + + + + * ``integer``: A JSON number, representing the integer + + + + * ``modulus``: A JSON number, representing the modulus + + + + +.. _JSONSchema: +JSON Cryptol Types +~~~~~~~~~~~~~~~~~~ -``call`` - The expression is a function application. Further fields are: +JSON representations of types are type schemas. A type schema has three fields: - - ``function``: A :ref:`JSON Cryptol expressions `. - - ``arguments``: A JSON array of :ref:`JSON Cryptol expressions `. -``instantiate`` - The expression is a type application. Further fields are: +``forall`` + Contains an array of objects. Each object has two fields: ``name`` is the name of a type variable, and ``kind`` is its kind. There are four kind formers: the string ``Type`` represents ordinary datatypes, the string ``Num`` is the kind of numbers, and ``Prop`` is the kind of propositions. Arrow kinds are represented by objects in which the field ``kind`` is the string ``arrow``, and the fields ``from`` and ``to`` are the kinds on the left and right side of the arrow, respectively. + + - - ``generic``: The polymorphic expression to be instantiated - - ``arguments``: A JSON object in which keys are the names of type parameters and values are :ref:`JSON Cryptol types `. +``propositions`` + A JSON array of the constraints in the type. + + -``integer modulo`` - The expression is an integer with a modulus (the Cryptol ``Z`` type). Further fields are: +``type`` + The type in which the variables from ``forall`` are in scope and the constraints in ``propositions`` are in effect. + + - - ``integer``: A JSON number, representing the integer - - ``modulus``: A JSON number, representing the modulus -.. _cryptol-json-type: +Methods +------- -JSON Cryptol Types ------------------- +check (command) +~~~~~~~~~~~~~~~ -JSON representations of types are type schemas. A type schema has -three fields: +Tests a property against random values to give quick feedback. -``forall`` +Parameter fields +++++++++++++++++ - Contains an array of objects. Each object has two fields: ``name`` - is the name of a type variable, and ``kind`` is its kind. There - are four kind formers: the string ``Type`` represents ordinary - datatypes, the string ``Num`` is the kind of numbers, and - ``Prop`` is the kind of propositions. Arrow kinds are represented - by objects in which the field ``kind`` is the string ``arrow``, - and the fields ``from`` and ``to`` are the kinds on the left and - right side of the arrow, respectively. -``propositions`` - A JSON array of the constraints in the type. +``expression`` + The predicate (i.e., function) to check; must be a monomorphic function with return type Bit. + + + +``number of tests`` + The number of random inputs to test the property with, or ``all`` to exhaustively check the property (defaults to ``100`` if not provided). If ``all`` is specified and the property's argument types are not sufficiently small, checking may take longer than you are willing to wait! + + + +Return fields ++++++++++++++ + + +``tests run`` + The number of tests that were successfully run. + + + +``tests possible`` + The maximum number of possible tests. + + + +``result`` + The overall test result, represented as one of three string values:``pass`` (all tests succeeded), ``fail`` (a test evaluated to ``False``), or``error`` (an exception was raised during evaluation). + + + +``arguments`` + Only returned if the ``result`` is ``fail`` or ``error``. An array of JSON objects indicating the arguments passed to the property which triggered the failure or error. Each object has an ``expr`` field, which is an individual argument expression, and a ``type`` field, which is the type of the argument expression. + + + +``error message`` + Only returned if the ``result`` is ``error``. A human-readable representation of the exception that was raised during evaluation. + + + + +clear state (notification) +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Clear a particular state from the Cryptol server (making room for subsequent/unrelated states). + +Parameter fields +++++++++++++++++ + + +``state to clear`` + The state to clear from the server to make room for other unrelated states. + + + +Return fields ++++++++++++++ + +No return fields + + + +clear all states (notification) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Clear all states from the Cryptol server (making room for subsequent/unrelated states). + +Parameter fields +++++++++++++++++ + +No parameters + + +Return fields ++++++++++++++ + +No return fields + + + +extend search path (command) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Extend the server's search path with the given paths. + +Parameter fields +++++++++++++++++ + + +``paths`` + The paths to add to the search path. + + + +Return fields ++++++++++++++ + +No return fields + + + +load module (command) +~~~~~~~~~~~~~~~~~~~~~ + +Load the specified module (by name). + +Parameter fields +++++++++++++++++ + + +``module name`` + Name of module to load. + + + +Return fields ++++++++++++++ + +No return fields + + + +load file (command) +~~~~~~~~~~~~~~~~~~~ + +Load the specified module (by file path). + +Parameter fields +++++++++++++++++ + + +``file`` + File path of the module to load. + + + +Return fields ++++++++++++++ + +No return fields + + + +focused module (command) +~~~~~~~~~~~~~~~~~~~~~~~~ + +The 'current' module. Used to decide how to print names, for example. + +Parameter fields +++++++++++++++++ + +No parameters + + +Return fields ++++++++++++++ + + +``module`` + The name of the focused module, which would be shown in the prompt in the Cryptol REPL, or ``null`` if there is no such focused module. + + + +``parameterized`` + A Boolean value indicating whether the focused module is parameterized. This field is only present when the module name is not ``null``. + + + + +evaluate expression (command) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Evaluate the Cryptol expression to a value. + +Parameter fields +++++++++++++++++ + + +``expression`` + The expression to evaluate. + + + +Return fields ++++++++++++++ + + +``value`` + A :ref:`JSON Cryptol expression ` that denotes the value + + ``type`` - The type in which the variables from ``forall`` are in scope and - the constraints in ``propositions`` are in effect. + A:ref:`JSON Cryptol type ` that denotes the result type + + + +``type string`` + A human-readable representation of the result type + + + -Concrete Types +call (command) ~~~~~~~~~~~~~~ -Types are represented as JSON objects. The ``type`` field contains one of the following tags (represented as JSON strings): +Evaluate the result of calling a Cryptol function on one or more parameters. -``variable`` - The type is a type variable. The remaining fields are ``name``, - which contains the variable's name, and ``kind``, which contains - its kind (represented as in the ``forall`` section). When providing - types to Cryptol, the ``kind`` field should be elided, and type synonyms - may be provided with arguments through an optional ``arguments`` field. +Parameter fields +++++++++++++++++ -``record`` - The type is a record type. The remaining field is ``fields``, - which contains a JSON object whose keys are the names of fields and - whose values are the fields' types. -``number`` - The type is a number. The field ``value`` contains the number - itself. +``function`` + The function being called. + + -``inf`` - The type is the infinite number. There are no further fields. +``arguments`` + The arguments the function is being applied to. + + -``Bit`` - The type is the bit type. There are no further fields. +Return fields ++++++++++++++ -``Integer`` - The type is the integer type. There are no further fields. -``Rational`` - The type is the rational number type. There are no further fields. +``value`` + A :ref:`JSON Cryptol expression ` that denotes the value + + -``Z`` - The type is integers modulo another value. The field ``modulus`` - contains the modulus, which is a type. +``type`` + A:ref:`JSON Cryptol type ` that denotes the result type + + -``bitvector`` - The type is a bitvector. The field ``width`` contains the number - of bits, which is a type. +``type string`` + A human-readable representation of the result type + + -``sequence`` - The type is a sequence. The field ``length`` contains the length - of the sequence (a type), and the field ``contents`` contains the - type of entries in the sequence. -``function`` - The type is a function type. The fields ``domain`` and ``range`` - contain the domain and range types. +visible names (command) +~~~~~~~~~~~~~~~~~~~~~~~ -``unit`` - The type is the unit type. There are no further fields. +List the currently visible (i.e., in scope) names. -``tuple`` - The type is a tuple. The field ``contents`` is a JSON array - containing the types of the projections from the tuple. +Parameter fields +++++++++++++++++ + +No parameters + + +Return fields ++++++++++++++ + + +``name`` + A human-readable representation of the name + + + +``type string`` + A human-readable representation of the name's type schema + + + +``type`` + A:ref:`JSON Cryptol type ` + + + +``documentation`` + An optional field containing documentation string for the name, if it is documented + + + + +check type (command) +~~~~~~~~~~~~~~~~~~~~ + +Check and return the type of the given expression. + +Parameter fields +++++++++++++++++ + + +``expression`` + Expression to type check. + + + +Return fields ++++++++++++++ + + +``type schema`` + A :ref:`JSON Cryptol Type ` + + + + +prove or satisfy (command) +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Find a value which satisfies the given predicate, or show that it is valid.(i.e., find a value which when passed as the argument produces true or show that for all possible arguments the predicate will produce true). + +Parameter fields +++++++++++++++++ + + +``prover`` + The SMT solver to use to check for satisfiability. I.e., one of the following: ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``, . + + + +``expression`` + The function to check for validity, satisfiability, or safety depending on the specified value for ``query type``. For validity and satisfiability checks, the function must be a predicate (i.e., monomorphic function with return type Bit). + + + +``result count`` + How many satisfying results to search for; either a positive integer or ``all``. Only affects satisfiability checks. + + -One of ``+``, ``-``, ``*``, ``/``, ``%``, ``^^``, ``width``, ``min``, ``max``, ``/^``, ``%^``, ``lengthFromThenTo`` - The type is an application of the indicated type function. The - arguments are contained in the ``arguments`` field, as a JSON - array. +``query type`` + Whether to attempt to prove the predicate is true for all possible inputs (``prove``), find some inputs which make the predicate true (``sat``), or prove a function is safe (``safe``). + + -Propositions -~~~~~~~~~~~~ +Return fields ++++++++++++++ -Propositions/constraints have the key ``prop``, mapped to one of the -following tags: -``==`` - Equality. The equated terms are in the ``left`` and ``right`` - fields. +``result`` + A string (one of ``unsatisfiable``, ``invalid``, or ``satisfied``) indicating the result of checking for validity, satisfiability, or safety. + + -``!=`` - Inequality. The disequated terms are in the ``left`` and - ``right`` fields. +``counterexample type`` + Only used if the ``result`` is ``invalid``.This describes the variety of counterexample that was produced. This can be either ``safety violation`` or ``predicate falsified``. + + -``>=`` - Greater than. The greater type is in the ``greater`` field and the - lesser type is in the ``lesser`` field. +``counterexample`` + Only used if the ``result`` is ``invalid``.A list of objects where each object has an ``expr``field, indicating a counterexample expression, and a ``type``field, indicating the type of the expression. + + -``fin`` - Finitude. The finite type is in the ``subject`` field. +``models`` + Only used if the ``result`` is ``satisfied``.A list of list of objects where each object has an ``expr``field, indicating a expression in a model, and a ``type``field, indicating the type of the expression. + + -``has`` - The selector is in the ``selector`` field, the type that has this - selector is in the ``type`` field, and the type expected for the - projection is in the ``is`` field. -``Arith``, ``Cmp``, ``SignedCmp``, ``Zero``, ``Logic`` - The type that has these operations defined is in the ``subject`` - field. -``Literal`` - The size is in the ``size`` field, and the type is in the - ``subject`` field. -``True`` - There are no further fields. -``And`` - The conjuncts are in the ``left`` and ``right`` fields. diff --git a/cryptol-remote-api/docs/old-Cryptol.rst b/cryptol-remote-api/docs/old-Cryptol.rst new file mode 100644 index 000000000..bcebebf0c --- /dev/null +++ b/cryptol-remote-api/docs/old-Cryptol.rst @@ -0,0 +1,353 @@ +================== +Cryptol Evaluation +================== + +All methods in this section additionally propagate server state in the +manner described in the prior section. + +These methods may return :ref:`a variety of Cryptol errors +`, with codes in the range of ``20000``-``29999``. + +Options +======= + +Many of the options that can be set using the ``:set`` command at the +Cryptol REPL can be provided as parameters to methods in this API. In +addition to the listed fields, every command accepts an optional +``options`` parameter. Its value should be an object, and may have +zero or more of the following fields: + + - ``call stacks``: A Boolean that determines whether to track call stacks. + - ``output``: An object that contains further parameters to control strings generated by Cryptol (these are visible in e.g. error messages, but do not affect the structured data returned in the API): + + ``ASCII``: A Boolean (default ``true``). + + ``base``: What base to display numbers in (default ``10``). + + ``prefix of infinite lengths``: How much of an infinite sequence to display (default ``5``. + + ``floating point base``: What base to display floating point numbers in (default ``10``). + + ``floating point format``: The output format used to display floating point numbers (accepts strings in the same format as the argument to ``:set fpFormat`` in the REPL). + +Module Management +================= + +Changing Directories +-------------------- + +:Method name: + ``change directory`` +:Parameters: + - ``directory``: The new working directory, represented as a string. + +Loading Modules +--------------- + +:Method name: + ``load module`` +:Parameters: + - ``module name``: The name of the Cryptol module to be loaded. + +Loading Files +------------- + +:Method name: + ``load file`` +:Parameters: + - ``file``: The name of the Cryptol source file to be loaded. + +Module Context +-------------- + +:Method name: + ``focused module`` +:Parameters: none +:Return fields: + - ``module``: The name of the focused module, which would be shown in the + prompt in the Cryptol REPL, or ``null`` if there is no such focused module. + - ``parameterized``: A Boolean value indicating whether the focused module is + parameterized. This field is only present when the module name is not + ``null``. + +Evaluation and Typechecking +=========================== + +Evaluating Expressions +---------------------- + +This method evaluates a Cryptol expression. The type of the expression +needs to be fully-determined and finite - that is, functions and +infinite streams are not supported, and neither is polymorphism. + +:Method name: + ``evaluate expression`` +:Parameters: + - ``expression``: The :ref:`JSON Cryptol expression ` to be evaluated +:Return fields: + - ``value``: A :ref:`JSON Cryptol expression ` that denotes the value + - ``type``: A :ref:`JSON Cryptol type ` that denotes the result type + - ``type string``: A human-readable representation of the result type + +Calling Functions +----------------- + +Note: this method may be removed in the future, because its abilities +have been subsumed by ``evaluate expression``. + +This method applies a Cryptol function to some arguments. The type of +the resulting expression needs to be fully-determined and finite - +that is, functions and infinite streams are not supported, and neither +is polymorphism. + +:Method name: + ``call`` +:Parameters: + - ``function``: The name of a Cryptol function that is currently in scope + - ``arguments``: A list of arguments to the function, encoded as JSON + Cryptol expressions +:Return fields: + - ``value``: A :ref:`JSON Cryptol expression ` that denotes the value + - ``type``: A :ref:`JSON Cryptol type ` that denotes the result type + - ``type string``: A human-readable representation of the result type + +Visible Names +------------- + +Return information about all names in scope. + +:Method name: + ``visible names`` +:Parameters: none +:Return value: + A list of name information objects. Each name information object has the following + fields: + + - ``name``: A human-readable representation of the name + - ``type string``: A human-readable representation of the name's type schema + - ``type``: A :ref:`JSON Cryptol type ` + + Some will additionally have the following field: + + - ``documentation``: The documentation string for the name, if it is documented + +Checking Types +-------------- + +Check the type of an expression. + +:Method name: + ``check type`` +:Parameters: + - ``expression``: A :ref:`JSON Cryptol expression ` for which a type is desired. +:Return fields: + - ``type schema``: A :ref:`JSON Cryptol type ` + +SAT +--- + +This method is not yet ready for public consumption. + +Terms and Types +=============== + +.. _cryptol-json-expression: + +JSON Cryptol Expressions +------------------------ + +In the API, Cryptol expressions can be represented by the following: + +JSON Booleans + Represent the corresponding Cryptol Booleans + +JSON Integers + Cryptol integer literals, that can be used at a variety of types + +JSON Strings + Cryptol concrete syntax + +JSON Objects + Objects can represent a variety of Cryptol expressions. The field + ``expression`` contains a tag that can be used to determine the + remaining fields. + +The tag values in objects can be: + +``bits`` + The expression is a bitvector. Further fields are: + + + ``encoding``: Either the string ``base64`` or ``hex``, for base-64 or hexadecimal + representations of the bitvector + + ``data``: A string containing the actual data + + ``width``: An integer: the bit-width of the represented bit vector + +``record`` + The expression is a record. The field ``data`` is a JSON + object that maps record field names to :ref:`JSON Cryptol expressions `. + +``sequence`` + The expression is a sequence. The field ``data`` contains a + JSON array of the elements of the sequence; each is a JSON Cryptol + expression. + +``tuple`` + The expression is a tuple. The field ``data`` contains a JSON + array of the elements of the tuple; each is a JSON Cryptol + expression. + +``unit`` + The expression is the unit constructor, and there are no further fields. + +``let`` + The expression is a ``where`` binding. The fields are: + + ``binders`` + A list of binders. Each binder is an object with two fields: + + - ``name``: A string that is the name to be bound, and + - ``definition``: A :ref:`JSON Cryptol expression `. + + ``body`` + A :ref:`JSON Cryptol expression ` in which the bound names may be used. + +``call`` + The expression is a function application. Further fields are: + + - ``function``: A :ref:`JSON Cryptol expressions `. + - ``arguments``: A JSON array of :ref:`JSON Cryptol expressions `. + +``instantiate`` + The expression is a type application. Further fields are: + + - ``generic``: The polymorphic expression to be instantiated + - ``arguments``: A JSON object in which keys are the names of type parameters and values are :ref:`JSON Cryptol types `. + +``integer modulo`` + The expression is an integer with a modulus (the Cryptol ``Z`` type). Further fields are: + + - ``integer``: A JSON number, representing the integer + - ``modulus``: A JSON number, representing the modulus + +.. _cryptol-json-type: + +JSON Cryptol Types +------------------ + +JSON representations of types are type schemas. A type schema has +three fields: + +``forall`` + + Contains an array of objects. Each object has two fields: ``name`` + is the name of a type variable, and ``kind`` is its kind. There + are four kind formers: the string ``Type`` represents ordinary + datatypes, the string ``Num`` is the kind of numbers, and + ``Prop`` is the kind of propositions. Arrow kinds are represented + by objects in which the field ``kind`` is the string ``arrow``, + and the fields ``from`` and ``to`` are the kinds on the left and + right side of the arrow, respectively. + +``propositions`` + A JSON array of the constraints in the type. + +``type`` + The type in which the variables from ``forall`` are in scope and + the constraints in ``propositions`` are in effect. + +Concrete Types +~~~~~~~~~~~~~~ + +Types are represented as JSON objects. The ``type`` field contains one of the following tags (represented as JSON strings): + +``variable`` + The type is a type variable. The remaining fields are ``name``, + which contains the variable's name, and ``kind``, which contains + its kind (represented as in the ``forall`` section). When providing + types to Cryptol, the ``kind`` field should be elided, and type synonyms + may be provided with arguments through an optional ``arguments`` field. + +``record`` + The type is a record type. The remaining field is ``fields``, + which contains a JSON object whose keys are the names of fields and + whose values are the fields' types. + +``number`` + The type is a number. The field ``value`` contains the number + itself. + +``inf`` + The type is the infinite number. There are no further fields. + +``Bit`` + The type is the bit type. There are no further fields. + +``Integer`` + The type is the integer type. There are no further fields. + +``Rational`` + The type is the rational number type. There are no further fields. + +``Z`` + The type is integers modulo another value. The field ``modulus`` + contains the modulus, which is a type. + +``bitvector`` + The type is a bitvector. The field ``width`` contains the number + of bits, which is a type. + +``sequence`` + The type is a sequence. The field ``length`` contains the length + of the sequence (a type), and the field ``contents`` contains the + type of entries in the sequence. + +``function`` + The type is a function type. The fields ``domain`` and ``range`` + contain the domain and range types. + +``unit`` + The type is the unit type. There are no further fields. + +``tuple`` + The type is a tuple. The field ``contents`` is a JSON array + containing the types of the projections from the tuple. + +One of ``+``, ``-``, ``*``, ``/``, ``%``, ``^^``, ``width``, ``min``, ``max``, ``/^``, ``%^``, ``lengthFromThenTo`` + The type is an application of the indicated type function. The + arguments are contained in the ``arguments`` field, as a JSON + array. + +Propositions +~~~~~~~~~~~~ + +Propositions/constraints have the key ``prop``, mapped to one of the +following tags: + +``==`` + Equality. The equated terms are in the ``left`` and ``right`` + fields. + +``!=`` + Inequality. The disequated terms are in the ``left`` and + ``right`` fields. + +``>=`` + Greater than. The greater type is in the ``greater`` field and the + lesser type is in the ``lesser`` field. + +``fin`` + Finitude. The finite type is in the ``subject`` field. + +``has`` + The selector is in the ``selector`` field, the type that has this + selector is in the ``type`` field, and the type expected for the + projection is in the ``is`` field. + +``Arith``, ``Cmp``, ``SignedCmp``, ``Zero``, ``Logic`` + The type that has these operations defined is in the ``subject`` + field. + +``Literal`` + The size is in the ``size`` field, and the type is in the + ``subject`` field. + +``True`` + There are no further fields. + +``And`` + The conjuncts are in the ``left`` and ``right`` fields.