mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-08-17 01:41:09 +03:00
Bump argo submodule to include docs for method results
This bumps the `argo` submodule to include commit
b9b3edd992
,
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.
This commit is contained in:
parent
33d7273346
commit
d7814a959b
@ -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 =
|
||||
|
@ -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 =
|
||||
|
@ -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 ()) ->
|
||||
|
@ -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"])
|
||||
]
|
||||
|
@ -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."
|
||||
])
|
||||
]
|
||||
|
@ -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
|
||||
|
@ -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 =
|
||||
|
@ -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."
|
||||
])
|
||||
]
|
||||
]
|
||||
|
@ -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"])
|
||||
]
|
||||
|
@ -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."])
|
||||
|
@ -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 "."
|
||||
])
|
||||
]
|
||||
|
@ -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."])
|
||||
|
@ -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."]
|
||||
|
@ -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" $
|
||||
|
@ -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 "." ]
|
||||
|
@ -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"])
|
||||
]
|
||||
|
2
deps/argo
vendored
2
deps/argo
vendored
@ -1 +1 @@
|
||||
Subproject commit 1040dc26d142f13ff8ed6617ff5212f476b78c45
|
||||
Subproject commit c733718138c10c70c6e690d4a2de83a7b07e6cc9
|
Loading…
Reference in New Issue
Block a user