mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-08-17 01:41:09 +03:00
chore: tweak rpc cryptol expr parser (#1215)
* chore: tweak rpc cryptol expr parser * chore: update Cryptol server Expression docs
This commit is contained in:
Andrew Kent
GitHub
parent
eb829d89b2
commit
36475d1fd9
@ -63,7 +63,6 @@ library
|
||||
CryptolServer.Check
|
||||
CryptolServer.ClearState
|
||||
CryptolServer.Data.Expression
|
||||
CryptolServer.Data.FreshName
|
||||
CryptolServer.Data.Type
|
||||
CryptolServer.EvalExpr
|
||||
CryptolServer.ExtendSearchPath
|
||||
|
||||
@ -208,6 +208,11 @@ The tag values in objects can be:
|
||||
|
||||
|
||||
|
||||
``variable``
|
||||
The expression is a variable bound by the server. The field ``identifier`` contains the name of the variable.
|
||||
|
||||
|
||||
|
||||
.. _JSONSchema:
|
||||
JSON Cryptol Types
|
||||
~~~~~~~~~~~~~~~~~~
|
||||
|
||||
@ -50,8 +50,8 @@ def from_cryptol_arg(val : Any) -> Any:
|
||||
else:
|
||||
raise ValueError("Unknown encoding " + str(enc))
|
||||
return BV(size, n)
|
||||
elif tag == 'unique name':
|
||||
return OpaqueValue(int(val['unique']), str(val['identifier']))
|
||||
elif tag == 'variable':
|
||||
return OpaqueValue(str(val['identifier']))
|
||||
else:
|
||||
raise ValueError("Unknown expression tag " + tag)
|
||||
else:
|
||||
|
||||
@ -166,8 +166,7 @@ class CryptolType:
|
||||
'width': val.size(), # N.B. original length, not padded
|
||||
'data': val.hex()[2:]}
|
||||
elif isinstance(val, OpaqueValue):
|
||||
return {'expression': 'unique name',
|
||||
'unique': val.unique,
|
||||
return {'expression': 'variable',
|
||||
'identifier': val.identifier}
|
||||
else:
|
||||
raise TypeError("Unsupported value: " + str(val))
|
||||
|
||||
@ -7,24 +7,22 @@ class OpaqueValue():
|
||||
Note that as far as Python is concerned these values are only equal to
|
||||
themselves. If a richer notion of equality is required then the server should
|
||||
be consulted to compute the result."""
|
||||
unique : int
|
||||
identifier : str
|
||||
|
||||
def __init__(self, unique : int, identifier : str) -> None:
|
||||
self.unique = unique
|
||||
def __init__(self, identifier : str) -> None:
|
||||
self.identifier = identifier
|
||||
|
||||
def __str__(self) -> str:
|
||||
return self.identifier
|
||||
|
||||
def __repr__(self) -> str:
|
||||
return f"Opaque({self.unique!r}, {self.identifier!r})"
|
||||
return f"Opaque({self.identifier!r})"
|
||||
|
||||
def __eq__(self, other : Any) -> bool:
|
||||
if not isinstance(other, OpaqueValue):
|
||||
return False
|
||||
else:
|
||||
return self.unique == other.unique and self.identifier == other.identifier
|
||||
return self.identifier == other.identifier
|
||||
|
||||
def __hash__(self) -> int:
|
||||
return hash((self.unique, self.identifier))
|
||||
return hash(self.identifier)
|
||||
|
||||
@ -10,8 +10,6 @@ import Control.Monad.IO.Class
|
||||
import Control.Monad.Reader (ReaderT(ReaderT))
|
||||
import qualified Data.Aeson as JSON
|
||||
import Data.Containers.ListUtils (nubOrd)
|
||||
import Data.IntMap.Strict (IntMap)
|
||||
import qualified Data.IntMap.Strict as IntMap
|
||||
import Data.Text (Text)
|
||||
|
||||
import Cryptol.Eval (EvalOpts(..))
|
||||
@ -19,17 +17,15 @@ import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv(..), ModuleInput(..))
|
||||
import Cryptol.ModuleSystem.Env
|
||||
(getLoadedModules, lmFilePath, lmFingerprint,
|
||||
initialModuleEnv, ModulePath(..))
|
||||
import Cryptol.ModuleSystem.Name (Name, FreshM(..), nameUnique, nameIdent)
|
||||
import Cryptol.ModuleSystem.Name (FreshM(..))
|
||||
import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
|
||||
import Cryptol.Parser.AST (ModName, isInfixIdent)
|
||||
import Cryptol.Parser.AST (ModName)
|
||||
import Cryptol.TypeCheck( defaultSolverConfig )
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
|
||||
import qualified Argo
|
||||
import qualified Argo.Doc as Doc
|
||||
import CryptolServer.Data.FreshName
|
||||
import CryptolServer.Exceptions
|
||||
( cryptolError, invalidName)
|
||||
import CryptolServer.Exceptions ( cryptolError )
|
||||
import CryptolServer.Options
|
||||
( WithOptions(WithOptions), Options(Options, optEvalOpts) )
|
||||
|
||||
@ -127,7 +123,6 @@ data ServerState =
|
||||
ServerState { _loadedModule :: Maybe LoadedModule
|
||||
, _moduleEnv :: ModuleEnv
|
||||
, _tcSolver :: SMT.Solver
|
||||
, _freshNameEnv :: IntMap Name
|
||||
}
|
||||
|
||||
loadedModule :: Lens' ServerState (Maybe LoadedModule)
|
||||
@ -139,42 +134,12 @@ moduleEnv = lens _moduleEnv (\v n -> v { _moduleEnv = n })
|
||||
tcSolver :: Lens' ServerState SMT.Solver
|
||||
tcSolver = lens _tcSolver (\v n -> v { _tcSolver = n })
|
||||
|
||||
-- | Names generated when marshalling complex values to an RPC client;
|
||||
-- maps `nameUnique`s to `Name`s.
|
||||
freshNameEnv :: Lens' ServerState (IntMap Name)
|
||||
freshNameEnv = lens _freshNameEnv (\v n -> v { _freshNameEnv = n })
|
||||
|
||||
|
||||
-- | Take and remember the given name so it can later be recalled
|
||||
-- via it's `nameUnique` unique identifier. Return a `FreshName`
|
||||
-- which can be easily serialized/pretty-printed and marshalled
|
||||
-- across an RPC interface.
|
||||
registerName :: Name -> CryptolCommand FreshName
|
||||
registerName nm =
|
||||
if isInfixIdent (nameIdent nm)
|
||||
then raise $ invalidName nm
|
||||
else
|
||||
CryptolCommand $ const $ Argo.getState >>= \s ->
|
||||
let nmEnv = IntMap.insert (nameUnique nm) nm (view freshNameEnv s)
|
||||
in do Argo.setState (set freshNameEnv nmEnv s)
|
||||
pure $ unsafeToFreshName nm
|
||||
|
||||
-- | Return the underlying `Name` the given `FreshName` refers to. The
|
||||
-- `FreshName` should have previously been returned by `registerName` at some
|
||||
-- point, or else a JSON exception will be raised.
|
||||
resolveFreshName :: FreshName -> CryptolCommand (Maybe Name)
|
||||
resolveFreshName fnm =
|
||||
CryptolCommand $ const $ Argo.getState >>= \s ->
|
||||
case IntMap.lookup (freshNameUnique fnm) (view freshNameEnv s) of
|
||||
Nothing -> pure Nothing
|
||||
Just nm -> pure $ Just nm
|
||||
|
||||
|
||||
initialState :: IO ServerState
|
||||
initialState =
|
||||
do modEnv <- initialModuleEnv
|
||||
s <- SMT.startSolver (defaultSolverConfig (meSearchPath modEnv))
|
||||
pure (ServerState Nothing modEnv s IntMap.empty)
|
||||
pure (ServerState Nothing modEnv s)
|
||||
|
||||
extendSearchPath :: [FilePath] -> ServerState -> ServerState
|
||||
extendSearchPath paths =
|
||||
@ -190,12 +155,6 @@ instance FreshM CryptolCommand where
|
||||
CryptolCommand $ const (Argo.modifyState $ set moduleEnv mEnv')
|
||||
pure res
|
||||
|
||||
freshNameCount :: CryptolCommand Int
|
||||
freshNameCount = CryptolCommand $ const $ do
|
||||
fEnv <- view freshNameEnv <$> Argo.getState
|
||||
pure $ IntMap.size fEnv
|
||||
|
||||
|
||||
-- | Check that all of the modules loaded in the Cryptol environment
|
||||
-- currently have fingerprints that match those when they were loaded.
|
||||
validateServerState :: ServerState -> IO Bool
|
||||
|
||||
@ -41,7 +41,7 @@ import CryptolServer
|
||||
CryptolCommand )
|
||||
import CryptolServer.Exceptions (evalPolyErr)
|
||||
import CryptolServer.Data.Expression
|
||||
( readBack, getExpr, typecheckExpr, Expression)
|
||||
( readBack, getExpr, Expression)
|
||||
import CryptolServer.Data.Type ( JSONType(..) )
|
||||
import Cryptol.Utils.PP (pretty)
|
||||
|
||||
@ -54,7 +54,7 @@ checkDescr =
|
||||
check :: CheckParams -> CryptolCommand CheckResult
|
||||
check (CheckParams jsonExpr cMode) =
|
||||
do e <- getExpr jsonExpr
|
||||
(ty, schema) <- typecheckExpr e
|
||||
(_expr, ty, schema) <- liftModuleCmd (CM.checkExpr e)
|
||||
-- TODO? validEvalContext expr, ty, schema
|
||||
s <- getTCSolver
|
||||
perhapsDef <- liftIO (defaultReplExpr s ty schema)
|
||||
|
||||
@ -40,21 +40,19 @@ import Cryptol.Eval (evalSel)
|
||||
import Cryptol.Eval.Concrete (Value)
|
||||
import Cryptol.Eval.Type (TValue(..), tValTy)
|
||||
import Cryptol.Eval.Value (GenValue(..))
|
||||
import Cryptol.ModuleSystem
|
||||
(ModuleEnv, ModuleCmd, getPrimMap, evalDecls, renameType, checkExpr, focusedEnv)
|
||||
import Cryptol.ModuleSystem.Env (deNames,meDynEnv, mctxParams, mctxDecls, mctxNames)
|
||||
import Cryptol.ModuleSystem.Monad (runModuleM, interactive, getFocusedEnv)
|
||||
import Cryptol.ModuleSystem (ModuleCmd, getPrimMap, evalDecls, renameType)
|
||||
import Cryptol.ModuleSystem.Env (deNames,meDynEnv)
|
||||
import Cryptol.ModuleSystem.Monad (runModuleM, interactive)
|
||||
import qualified Cryptol.ModuleSystem.Base as Base
|
||||
import qualified Cryptol.ModuleSystem.Renamer as R
|
||||
import Cryptol.ModuleSystem.Name
|
||||
(Name, mkDeclared, NameSource( UserName ), liftSupply, nameIdent)
|
||||
import Cryptol.ModuleSystem.NamingEnv (singletonE, shadowing)
|
||||
import Cryptol.ModuleSystem.NamingEnv (singletonE, shadowing, namespaceMap)
|
||||
|
||||
import qualified Cryptol.Parser as CP
|
||||
import qualified Cryptol.Parser.AST as CP
|
||||
import Cryptol.Parser.Position (Located(..), emptyRange)
|
||||
import Cryptol.Parser.Selector
|
||||
import qualified Cryptol.TypeCheck as TC
|
||||
import qualified Cryptol.TypeCheck.AST as TC
|
||||
import Cryptol.Utils.Ident
|
||||
import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields)
|
||||
@ -63,7 +61,6 @@ import Argo
|
||||
import qualified Argo.Doc as Doc
|
||||
import CryptolServer
|
||||
import CryptolServer.Exceptions
|
||||
import CryptolServer.Data.FreshName
|
||||
import CryptolServer.Data.Type
|
||||
|
||||
data Encoding = Base64 | Hex
|
||||
@ -98,7 +95,10 @@ instance JSON.ToJSON LetBinding where
|
||||
-- | Cryptol expressions which can be serialized into JSON and sent
|
||||
-- to an RPC client.
|
||||
data Expression =
|
||||
Bit !Bool
|
||||
Variable !Text
|
||||
-- ^ Used when we need to send a result back to an RPC client which
|
||||
-- cannot be cleanly represented syntactically.
|
||||
| Bit !Bool
|
||||
| Unit
|
||||
| Num !Encoding !Text !Integer -- ^ data and bitwidth
|
||||
| Record !(HashMap Text Expression)
|
||||
@ -106,11 +106,9 @@ data Expression =
|
||||
| Tuple ![Expression]
|
||||
| Integer !Integer
|
||||
| IntegerModulo !Integer !Integer -- ^ value, modulus
|
||||
| UniqueName !FreshName
|
||||
-- ^ Essentially a Cryptol.ModuleSystem.Name's nameUnique and nameIdent.
|
||||
-- Used when we need to send a result back to an RPC client
|
||||
| Concrete !Text -- ^ Concrete Cryptol syntax as a string -- the Cryptol parser
|
||||
-- will establish it's meaning based on the current focus/context
|
||||
| Let ![LetBinding] !Expression
|
||||
| Application !Expression !(NonEmpty Expression)
|
||||
| TypeApplication !Expression !TypeArguments
|
||||
deriving (Eq, Show)
|
||||
@ -124,10 +122,11 @@ data ExpressionTag
|
||||
| TagSequence
|
||||
| TagTuple
|
||||
| TagUnit
|
||||
| TagLet
|
||||
| TagApp
|
||||
| TagTypeApp
|
||||
| TagIntMod
|
||||
| TagUniqueName
|
||||
| TagVariable
|
||||
|
||||
instance JSON.FromJSON ExpressionTag where
|
||||
parseJSON =
|
||||
@ -138,10 +137,11 @@ instance JSON.FromJSON ExpressionTag where
|
||||
"record" -> pure TagRecord
|
||||
"sequence" -> pure TagSequence
|
||||
"tuple" -> pure TagTuple
|
||||
"let" -> pure TagLet
|
||||
"call" -> pure TagApp
|
||||
"instantiate" -> pure TagTypeApp
|
||||
"integer modulo" -> pure TagIntMod
|
||||
"unique name" -> pure TagUniqueName
|
||||
"variable" -> pure TagVariable
|
||||
_ -> empty
|
||||
|
||||
instance JSON.ToJSON ExpressionTag where
|
||||
@ -150,10 +150,11 @@ instance JSON.ToJSON ExpressionTag where
|
||||
toJSON TagSequence = "sequence"
|
||||
toJSON TagTuple = "tuple"
|
||||
toJSON TagUnit = "unit"
|
||||
toJSON TagLet = "let"
|
||||
toJSON TagApp = "call"
|
||||
toJSON TagTypeApp = "instantiate"
|
||||
toJSON TagIntMod = "integer modulo"
|
||||
toJSON TagUniqueName = "unique name"
|
||||
toJSON TagVariable = "variable"
|
||||
|
||||
instance JSON.FromJSON TypeArguments where
|
||||
parseJSON =
|
||||
@ -200,16 +201,16 @@ instance JSON.FromJSON Expression where
|
||||
do contents <- o .: "data"
|
||||
flip (withArray "tuple") contents $
|
||||
\s -> Tuple . V.toList <$> traverse parseJSON s
|
||||
TagLet ->
|
||||
Let <$> o .: "binders" <*> o .: "body"
|
||||
TagApp ->
|
||||
Application <$> o .: "function" <*> o .: "arguments"
|
||||
TagTypeApp ->
|
||||
TypeApplication <$> o .: "generic" <*> o .: "arguments"
|
||||
TagIntMod ->
|
||||
IntegerModulo <$> o .: "integer" <*> o .: "modulus"
|
||||
TagUniqueName -> do
|
||||
contents <- o .: "unique"
|
||||
ident <- o .: "identifier"
|
||||
pure $ UniqueName $ unsafeFreshName contents ident
|
||||
TagVariable ->
|
||||
Variable <$> o .: "identifier"
|
||||
|
||||
instance ToJSON Encoding where
|
||||
toJSON Hex = String "hex"
|
||||
@ -245,15 +246,19 @@ instance JSON.ToJSON Expression where
|
||||
object [ "expression" .= TagTuple
|
||||
, "data" .= Array (V.fromList (map toJSON projs))
|
||||
]
|
||||
toJSON (Let binds body) =
|
||||
object [ "expression" .= TagLet
|
||||
, "binders" .= Array (V.fromList (map toJSON binds))
|
||||
, "body" .= toJSON body
|
||||
]
|
||||
toJSON (Application fun args) =
|
||||
object [ "expression" .= TagApp
|
||||
, "function" .= fun
|
||||
, "arguments" .= args
|
||||
]
|
||||
toJSON (UniqueName nm) =
|
||||
object [ "expression" .= TagUniqueName
|
||||
, "unique" .= toJSON (freshNameUnique nm)
|
||||
, "identifier" .= toJSON (freshNameText nm)
|
||||
toJSON (Variable nm) =
|
||||
object [ "expression" .= TagVariable
|
||||
, "identifier" .= toJSON nm
|
||||
]
|
||||
toJSON (TypeApplication _gen (TypeArguments _args)) =
|
||||
-- Presumably this is dead code, since values are what are sent back to
|
||||
@ -371,24 +376,28 @@ instance Doc.Described Expression where
|
||||
, Doc.Text ": A JSON number, representing the modulus"
|
||||
]
|
||||
])
|
||||
, (pure $ Doc.Literal "variable",
|
||||
Doc.Paragraph [ Doc.Text "The expression is a variable bound by the server. The field "
|
||||
, Doc.Literal "identifier"
|
||||
, Doc.Text " contains the name of the variable."
|
||||
])
|
||||
]
|
||||
]
|
||||
|
||||
|
||||
decode ::
|
||||
(Monad m) =>
|
||||
(forall a. JSONRPCException -> m a) ->
|
||||
(Argo.Method m, Monad m) =>
|
||||
Encoding ->
|
||||
Text ->
|
||||
m Integer
|
||||
decode raiseJSONErr Base64 txt =
|
||||
decode Base64 txt =
|
||||
let bytes = encodeUtf8 txt
|
||||
in
|
||||
case Base64.decode bytes of
|
||||
Left err -> raiseJSONErr (invalidBase64 bytes err)
|
||||
Left err -> Argo.raise (invalidBase64 bytes err)
|
||||
Right decoded -> pure $ bytesToInt decoded
|
||||
decode raiseJSONErr Hex txt =
|
||||
squish <$> traverse (hexDigit raiseJSONErr) (T.unpack txt)
|
||||
decode Hex txt =
|
||||
squish <$> traverse (hexDigit Argo.raise) (T.unpack txt)
|
||||
where
|
||||
squish = foldl (\acc i -> (acc * 16) + i) 0
|
||||
|
||||
@ -428,100 +437,98 @@ hexDigit raiseJSONErr =
|
||||
-- `Name` for the type in the current module environment.
|
||||
getTypeName ::
|
||||
(Monad m) =>
|
||||
m ModuleEnv ->
|
||||
R.NamingEnv ->
|
||||
(forall a. ModuleCmd a -> m a) ->
|
||||
Text ->
|
||||
m Name
|
||||
getTypeName getModEnv runModuleCmd ty = do
|
||||
nmEnv <- (mctxNames . focusedEnv) <$> getModEnv
|
||||
getTypeName nmEnv runModuleCmd ty =
|
||||
runModuleCmd $ renameType nmEnv (CP.UnQual (mkIdent ty))
|
||||
|
||||
getCryptolType ::
|
||||
(Monad m) =>
|
||||
m ModuleEnv ->
|
||||
R.NamingEnv ->
|
||||
(forall a. ModuleCmd a -> m a) ->
|
||||
JSONPType ->
|
||||
m (CP.Type Name)
|
||||
getCryptolType getModEnv runModuleCmd (JSONPType rawTy) = do
|
||||
nmEnv <- (mctxNames . focusedEnv) <$> getModEnv
|
||||
getCryptolType nmEnv runModuleCmd (JSONPType rawTy) =
|
||||
runModuleCmd $ \env -> runModuleM env $ interactive $
|
||||
Base.rename interactiveName nmEnv (R.rename rawTy)
|
||||
|
||||
getExpr :: Expression -> CryptolCommand (CP.Expr Name)
|
||||
getExpr = getCryptolExpr resolveFreshName
|
||||
getModuleEnv
|
||||
liftModuleCmd
|
||||
CryptolServer.raise
|
||||
getExpr :: Expression -> CryptolCommand (CP.Expr CP.PName)
|
||||
getExpr = CryptolCommand . const . getCryptolExpr
|
||||
|
||||
-- N.B., used in SAWServer as well, hence the more generic monad and
|
||||
-- parameterized monadic functions.
|
||||
getCryptolExpr :: forall m.
|
||||
(Monad m) =>
|
||||
(FreshName -> m (Maybe Name)) {- ^ How to resolve a FreshName in the server. -} ->
|
||||
m ModuleEnv {- ^ Getter for Cryptol ModuleEnv. -} ->
|
||||
(forall a. ModuleCmd a -> m a) {- ^ Runner for Cryptol ModuleCmd. -} ->
|
||||
(forall a. JSONRPCException -> m a) {- ^ JSONRPCException error raiser. -} ->
|
||||
Expression {- Syntactic expression to convert to Cryptol. -} ->
|
||||
m (CP.Expr Name)
|
||||
getCryptolExpr getName getModEnv runModuleCmd raiseJSONErr = go
|
||||
-- N.B., used in SAWServer as well, hence the more generic monad
|
||||
getCryptolExpr :: (Argo.Method m, Monad m) => Expression -> m (CP.Expr CP.PName)
|
||||
getCryptolExpr (Variable nm) =
|
||||
return $ CP.EVar $ CP.UnQual $ mkIdent nm
|
||||
getCryptolExpr Unit =
|
||||
return $
|
||||
CP.ETyped
|
||||
(CP.ETuple [])
|
||||
(CP.TTuple [])
|
||||
getCryptolExpr (Bit b) =
|
||||
return $
|
||||
CP.ETyped
|
||||
(CP.EVar (CP.UnQual (mkIdent $ if b then "True" else "False")))
|
||||
CP.TBit
|
||||
getCryptolExpr (Integer i) =
|
||||
return $
|
||||
CP.ETyped
|
||||
(CP.ELit (CP.ECNum i (CP.DecLit (pack (show i)))))
|
||||
(CP.TUser (CP.UnQual (mkIdent "Integer")) [])
|
||||
getCryptolExpr (IntegerModulo i n) =
|
||||
return $
|
||||
CP.ETyped
|
||||
(CP.ELit (CP.ECNum i (CP.DecLit (pack (show i)))))
|
||||
(CP.TUser (CP.UnQual (mkIdent "Z")) [CP.TNum n])
|
||||
getCryptolExpr (Num enc txt w) =
|
||||
do d <- decode enc txt
|
||||
return $ CP.ETyped
|
||||
(CP.ELit (CP.ECNum d (CP.DecLit txt)))
|
||||
(CP.TSeq (CP.TNum w) CP.TBit)
|
||||
getCryptolExpr (Record fields) =
|
||||
fmap (CP.ERecord . recordFromFields) $ for (HM.toList fields) $
|
||||
\(recName, spec) ->
|
||||
(mkIdent recName,) . (emptyRange,) <$> getCryptolExpr spec
|
||||
getCryptolExpr (Sequence elts) =
|
||||
CP.EList <$> traverse getCryptolExpr elts
|
||||
getCryptolExpr (Tuple projs) =
|
||||
CP.ETuple <$> traverse getCryptolExpr projs
|
||||
getCryptolExpr (Concrete syntax) =
|
||||
case CP.parseExpr syntax of
|
||||
Left err ->
|
||||
Argo.raise (cryptolParseErr syntax err)
|
||||
Right e -> pure e
|
||||
getCryptolExpr (Let binds body) =
|
||||
CP.EWhere <$> getCryptolExpr body <*> traverse mkBind binds
|
||||
where
|
||||
go (UniqueName fnm) = do
|
||||
mNm <- getName fnm
|
||||
case mNm of
|
||||
Nothing -> raiseJSONErr $ unknownFreshName fnm
|
||||
Just nm -> pure $ CP.EVar nm
|
||||
go Unit =
|
||||
return $
|
||||
CP.ETyped
|
||||
(CP.ETuple [])
|
||||
(CP.TTuple [])
|
||||
go (Bit b) =
|
||||
return $ CP.ETyped
|
||||
(if b
|
||||
then CP.ELit $ CP.ECNum 1 (CP.BinLit "1" 1)
|
||||
else CP.ELit $ CP.ECNum 0 (CP.BinLit "0" 0))
|
||||
CP.TBit
|
||||
go (Integer i) = do
|
||||
intTy <- getTypeName getModEnv runModuleCmd "Integer"
|
||||
pure $
|
||||
CP.ETyped
|
||||
(CP.ELit (CP.ECNum i (CP.DecLit (pack (show i)))))
|
||||
(CP.TUser intTy [])
|
||||
go (IntegerModulo i n) = do
|
||||
zTy <- getTypeName getModEnv runModuleCmd "Z"
|
||||
return $
|
||||
CP.ETyped
|
||||
(CP.ELit (CP.ECNum i (CP.DecLit (pack (show i)))))
|
||||
(CP.TUser zTy [CP.TNum n])
|
||||
go (Num enc txt w) = do
|
||||
d <- decode raiseJSONErr enc txt
|
||||
return $ CP.ETyped
|
||||
(CP.ELit (CP.ECNum d (CP.DecLit txt)))
|
||||
(CP.TSeq (CP.TNum w) CP.TBit)
|
||||
go (Record fields) =
|
||||
fmap (CP.ERecord . recordFromFields) $ for (HM.toList fields) $
|
||||
\(recName, spec) ->
|
||||
(mkIdent recName,) . (emptyRange,) <$> go spec
|
||||
go (Sequence elts) =
|
||||
CP.EList <$> traverse go elts
|
||||
go (Tuple projs) =
|
||||
CP.ETuple <$> traverse go projs
|
||||
go (Concrete syntax) =
|
||||
case CP.parseExpr syntax of
|
||||
Left err ->
|
||||
raiseJSONErr $ cryptolParseErr syntax err
|
||||
Right e -> do
|
||||
(expr, _ty, _schema) <- runModuleCmd (checkExpr e)
|
||||
pure expr
|
||||
go (Application fun (arg :| [])) =
|
||||
CP.EApp <$> go fun <*> go arg
|
||||
go (Application fun (arg1 :| (arg : args))) =
|
||||
go (Application (Application fun (arg1 :| [])) (arg :| args))
|
||||
go (TypeApplication gen (TypeArguments args)) =
|
||||
CP.EAppT <$> go gen <*> (mapM inst (Map.toList args))
|
||||
inst (n, t) = do
|
||||
t' <- getCryptolType getModEnv runModuleCmd t
|
||||
pure $ CP.NamedInst (CP.Named (Located emptyRange n) t')
|
||||
mkBind (LetBinding x rhs) =
|
||||
CP.DBind .
|
||||
(\bindBody ->
|
||||
CP.Bind { CP.bName = fakeLoc (CP.UnQual (mkIdent x))
|
||||
, CP.bParams = []
|
||||
, CP.bDef = bindBody
|
||||
, CP.bSignature = Nothing
|
||||
, CP.bInfix = False
|
||||
, CP.bFixity = Nothing
|
||||
, CP.bPragmas = []
|
||||
, CP.bMono = True
|
||||
, CP.bDoc = Nothing
|
||||
, CP.bExport = CP.Public
|
||||
}) .
|
||||
fakeLoc .
|
||||
CP.DExpr <$>
|
||||
getCryptolExpr rhs
|
||||
|
||||
fakeLoc = Located emptyRange
|
||||
getCryptolExpr (Application fun (arg :| [])) =
|
||||
CP.EApp <$> getCryptolExpr fun <*> getCryptolExpr arg
|
||||
getCryptolExpr (Application fun (arg1 :| (arg : args))) =
|
||||
getCryptolExpr (Application (Application fun (arg1 :| [])) (arg :| args))
|
||||
getCryptolExpr (TypeApplication gen (TypeArguments args)) =
|
||||
CP.EAppT <$> getCryptolExpr gen <*> pure (map inst (Map.toList args))
|
||||
where
|
||||
inst (n, t) = CP.NamedInst (CP.Named (Located emptyRange n) (unJSONPType t))
|
||||
|
||||
-- TODO add tests that this is big-endian
|
||||
-- | Interpret a ByteString as an Integer
|
||||
@ -577,7 +584,7 @@ readBack ty val =
|
||||
mName <- bindValToFreshName (varName ty) ty val
|
||||
case mName of
|
||||
Nothing -> pure Nothing
|
||||
Just name -> pure $ Just $ UniqueName name
|
||||
Just name -> pure $ Just $ Variable name
|
||||
where
|
||||
mismatchPanic :: CryptolCommand (Maybe Expression)
|
||||
mismatchPanic =
|
||||
@ -618,15 +625,14 @@ readBack ty val =
|
||||
-- the generated name will be of the form `CryptolServer'nameN` (where `N` is a
|
||||
-- natural number) and the `FreshName` that is returned can be serialized into an
|
||||
-- `Expression` and sent to an RPC client.
|
||||
bindValToFreshName :: Text -> TValue -> Concrete.Value -> CryptolCommand (Maybe FreshName)
|
||||
bindValToFreshName :: Text -> TValue -> Concrete.Value -> CryptolCommand (Maybe Text)
|
||||
bindValToFreshName nameBase ty val = do
|
||||
prims <- liftModuleCmd getPrimMap
|
||||
mb <- liftEval (Concrete.toExpr prims ty val)
|
||||
case mb of
|
||||
Nothing -> return Nothing
|
||||
Just expr -> do
|
||||
name <- genFreshName
|
||||
fName <- registerName name
|
||||
(txt, name) <- genFresh
|
||||
let schema = TC.Forall { TC.sVars = []
|
||||
, TC.sProps = []
|
||||
, TC.sType = tValTy ty
|
||||
@ -642,36 +648,28 @@ bindValToFreshName nameBase ty val = do
|
||||
liftModuleCmd (evalDecls [TC.NonRecursive decl])
|
||||
modifyModuleEnv $ \me ->
|
||||
let denv = meDynEnv me
|
||||
in me {meDynEnv = denv { deNames = singletonE (CP.UnQual (nameIdent name)) name
|
||||
`shadowing` deNames denv }}
|
||||
return $ Just fName
|
||||
in me {meDynEnv = denv { deNames = singletonE (CP.UnQual (mkIdent txt)) name `shadowing` deNames denv }}
|
||||
return $ Just txt
|
||||
where
|
||||
genFreshName :: CryptolCommand Name
|
||||
genFreshName = do
|
||||
cnt <- freshNameCount
|
||||
let ident = mkIdent $ "CryptolServer'" <> nameBase <> (T.pack $ show cnt)
|
||||
genFresh :: CryptolCommand (Text, Name)
|
||||
genFresh = do
|
||||
valNS <- (namespaceMap NSValue) . deNames . meDynEnv <$> getModuleEnv
|
||||
let txt = nextNewName valNS (Map.size valNS)
|
||||
ident = mkIdent txt
|
||||
mpath = TopModule interactiveName
|
||||
liftSupply (mkDeclared NSValue mpath UserName ident Nothing emptyRange)
|
||||
name <- liftSupply (mkDeclared NSValue mpath UserName ident Nothing emptyRange)
|
||||
pure (txt, name)
|
||||
where nextNewName :: Map CP.PName [Name] -> Int -> Text
|
||||
nextNewName ns n =
|
||||
let txt = "CryptolServer'" <> nameBase <> (T.pack $ show n)
|
||||
pname = CP.UnQual (mkIdent txt)
|
||||
in if Map.member pname ns
|
||||
then nextNewName ns (n + 1)
|
||||
else txt
|
||||
|
||||
|
||||
liftEval :: Eval a -> CryptolCommand a
|
||||
liftEval e = liftIO (runEval mempty e)
|
||||
|
||||
mkEApp :: CP.Expr Name -> [CP.Expr Name] -> CP.Expr Name
|
||||
mkEApp :: CP.Expr CP.PName -> [CP.Expr CP.PName] -> CP.Expr CP.PName
|
||||
mkEApp f args = foldl CP.EApp f args
|
||||
|
||||
|
||||
|
||||
-- | Typecheck a single expression, yielding a typechecked core expression and a type schema.
|
||||
typecheckExpr :: CP.Expr Name -> CryptolCommand (TC.Expr,TC.Schema)
|
||||
typecheckExpr e = liftModuleCmd $ \env -> runModuleM env $ interactive $ do
|
||||
fe <- getFocusedEnv
|
||||
let params = mctxParams fe
|
||||
decls = mctxDecls fe
|
||||
-- merge the dynamic and opened environments for typechecking
|
||||
prims <- Base.getPrimMap
|
||||
let act = Base.TCAction { Base.tcAction = TC.tcExpr
|
||||
, Base.tcLinter = Base.exprLinter
|
||||
, Base.tcPrims = prims }
|
||||
(te,s) <- Base.typecheck act e params decls
|
||||
return (te,s)
|
||||
|
||||
@ -1,42 +0,0 @@
|
||||
|
||||
module CryptolServer.Data.FreshName
|
||||
( FreshName
|
||||
, freshNameUnique
|
||||
, freshNameText
|
||||
, unsafeFreshName
|
||||
, unsafeToFreshName
|
||||
) where
|
||||
|
||||
|
||||
import Cryptol.ModuleSystem.Name (Name, nameUnique, nameIdent)
|
||||
import Cryptol.Parser.AST (identText)
|
||||
import Data.Text (Text)
|
||||
|
||||
-- | Minimal representative for fresh names generated by the server
|
||||
-- when marshalling complex values back to the user. The `Int`
|
||||
-- corresponds to the `nameUnique` of a `Name`, and the `Text`
|
||||
-- is the non-infix `Ident`'s textual representation.
|
||||
data FreshName = FreshName !Int !Text
|
||||
deriving (Eq, Show)
|
||||
|
||||
-- | Corresponds to the `nameUnique` field of a `Name`.
|
||||
freshNameUnique :: FreshName -> Int
|
||||
freshNameUnique (FreshName n _) = n
|
||||
|
||||
-- | Corresponds to the `nameIdent` field of a `Name` (except we know
|
||||
-- if is not infix, so we just store the `Text`).
|
||||
freshNameText :: FreshName -> Text
|
||||
freshNameText (FreshName _ txt) = txt
|
||||
|
||||
|
||||
-- | Get a `FreshName` which corresopnds to then given `Name`. N.B., this does
|
||||
-- _not_ register any names with the server or ensure the ident is not infix,
|
||||
-- and so should this function only be used by code which maintains
|
||||
-- these invariants.
|
||||
unsafeToFreshName :: Name -> FreshName
|
||||
unsafeToFreshName nm = FreshName (nameUnique nm) (identText (nameIdent nm))
|
||||
|
||||
-- | Creates a FreshName -- users should take care to ensure any generated
|
||||
-- `FreshName` has a mapping from `Int` to `FreshName` recorded in the server!
|
||||
unsafeFreshName :: Int -> Text -> FreshName
|
||||
unsafeFreshName n txt = FreshName n txt
|
||||
@ -15,8 +15,7 @@ import Data.Aeson as JSON
|
||||
import Data.Typeable (Proxy(..), typeRep)
|
||||
|
||||
|
||||
import Cryptol.ModuleSystem (evalExpr)
|
||||
import Cryptol.ModuleSystem.Name (Name)
|
||||
import Cryptol.ModuleSystem (evalExpr, checkExpr)
|
||||
import Cryptol.ModuleSystem.Env (deEnv,meDynEnv)
|
||||
import Cryptol.TypeCheck.Solve (defaultReplExpr)
|
||||
import Cryptol.TypeCheck.Subst (apSubst, listParamSubst)
|
||||
@ -40,9 +39,9 @@ evalExpression (EvalExprParams jsonExpr) =
|
||||
do e <- getExpr jsonExpr
|
||||
evalExpression' e
|
||||
|
||||
evalExpression' :: P.Expr Name -> CryptolCommand JSON.Value
|
||||
evalExpression' :: P.Expr P.PName -> CryptolCommand JSON.Value
|
||||
evalExpression' e = do
|
||||
(ty, schema) <- typecheckExpr e
|
||||
(_expr, ty, schema) <- liftModuleCmd (checkExpr e)
|
||||
-- TODO: see Cryptol REPL for how to check whether we
|
||||
-- can actually evaluate things, which we can't do in
|
||||
-- a parameterized module
|
||||
|
||||
@ -4,9 +4,7 @@ module CryptolServer.Exceptions
|
||||
, invalidBase64
|
||||
, invalidHex
|
||||
, invalidType
|
||||
, invalidName
|
||||
, unwantedDefaults
|
||||
, unknownFreshName
|
||||
, evalInParamMod
|
||||
, evalPolyErr
|
||||
, proverError
|
||||
@ -19,6 +17,7 @@ import qualified Data.Text as Text
|
||||
import qualified Data.Vector as Vector
|
||||
|
||||
import Cryptol.ModuleSystem (ModuleError(..), ModuleWarning(..))
|
||||
import Cryptol.ModuleSystem.Name as CM
|
||||
import Cryptol.Utils.PP (pretty, PP)
|
||||
|
||||
import Data.Aeson hiding (Encoding, Value, decode)
|
||||
@ -28,13 +27,10 @@ import Data.Text (Text)
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.HashMap.Strict as HashMap
|
||||
|
||||
import Cryptol.ModuleSystem.Name (Name, nameIdent)
|
||||
import Cryptol.Parser.AST (identText)
|
||||
import Cryptol.Parser
|
||||
import qualified Cryptol.TypeCheck.Type as TC
|
||||
|
||||
import Argo
|
||||
import CryptolServer.Data.FreshName
|
||||
import CryptolServer.Data.Type
|
||||
|
||||
cryptolError :: ModuleError -> [ModuleWarning] -> JSONRPCException
|
||||
@ -166,20 +162,6 @@ invalidType ty =
|
||||
20040 "Can't convert Cryptol data from this type to JSON"
|
||||
(Just (jsonTypeAndString ty))
|
||||
|
||||
invalidName :: Name -> JSONRPCException
|
||||
invalidName nm =
|
||||
makeJSONRPCException
|
||||
20041 "Internal error: invalid fresh name for a Cryptol server marshalled value."
|
||||
(Just (JSON.object ["name" .= (identText (nameIdent nm))]))
|
||||
|
||||
unknownFreshName :: FreshName -> JSONRPCException
|
||||
unknownFreshName nm =
|
||||
makeJSONRPCException
|
||||
20042 "Internal error: fresh name is not known in the server."
|
||||
(Just (JSON.object [ "unique" .= (freshNameUnique nm)
|
||||
, "ident" .= (freshNameText nm)
|
||||
]))
|
||||
|
||||
unwantedDefaults :: [(TC.TParam, TC.Type)] -> JSONRPCException
|
||||
unwantedDefaults defs =
|
||||
makeJSONRPCException
|
||||
@ -188,7 +170,7 @@ unwantedDefaults defs =
|
||||
[ jsonTypeAndString ty <> HashMap.fromList ["parameter" .= pretty param]
|
||||
| (param, ty) <- defs ] ]))
|
||||
|
||||
evalInParamMod :: [Cryptol.ModuleSystem.Name.Name] -> JSONRPCException
|
||||
evalInParamMod :: [CM.Name] -> JSONRPCException
|
||||
evalInParamMod mods =
|
||||
makeJSONRPCException
|
||||
20220 "Can't evaluate Cryptol in a parameterized module."
|
||||
|
||||
@ -23,6 +23,7 @@ import qualified Data.Text as T
|
||||
|
||||
import Cryptol.Eval.Concrete (Value)
|
||||
import Cryptol.Eval.Type (TValue, tValTy)
|
||||
import Cryptol.ModuleSystem (checkExpr)
|
||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv)
|
||||
import Cryptol.Symbolic ( ProverCommand(..), ProverResult(..), QueryType(..)
|
||||
, SatNum(..), CounterExampleType(..))
|
||||
@ -44,7 +45,7 @@ proveSatDescr =
|
||||
proveSat :: ProveSatParams -> CryptolCommand ProveSatResult
|
||||
proveSat (ProveSatParams queryType (Prover name) jsonExpr) =
|
||||
do e <- getExpr jsonExpr
|
||||
(ty, schema) <- typecheckExpr e
|
||||
(_expr, ty, schema) <- liftModuleCmd (checkExpr e)
|
||||
-- TODO validEvalContext expr, ty, schema
|
||||
me <- getModuleEnv
|
||||
let decls = deDecls (meDynEnv me)
|
||||
|
||||
@ -14,6 +14,7 @@ import Data.Aeson as JSON
|
||||
import Data.Typeable
|
||||
|
||||
|
||||
import Cryptol.ModuleSystem (checkExpr)
|
||||
import CryptolServer
|
||||
import CryptolServer.Data.Expression
|
||||
import CryptolServer.Data.Type
|
||||
@ -25,7 +26,7 @@ checkTypeDescr =
|
||||
checkType :: TypeCheckParams -> CryptolCommand JSON.Value
|
||||
checkType (TypeCheckParams e) = do
|
||||
e' <- getExpr e
|
||||
(_ty, schema) <- typecheckExpr e'
|
||||
(_expr, _ty, schema) <- liftModuleCmd (checkExpr e')
|
||||
return (JSON.object [ "type schema" .= JSONSchema schema ])
|
||||
|
||||
newtype TypeCheckParams =
|
||||
|
||||
Loading…
Reference in New Issue
Block a user