From 36475d1fd99eca94bb829b859cf2a9e7cfa3668f Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Fri, 11 Jun 2021 08:52:34 -0700 Subject: [PATCH] chore: tweak rpc cryptol expr parser (#1215) * chore: tweak rpc cryptol expr parser * chore: update Cryptol server Expression docs --- cryptol-remote-api/cryptol-remote-api.cabal | 1 - cryptol-remote-api/docs/Cryptol.rst | 5 + cryptol-remote-api/python/cryptol/commands.py | 4 +- .../python/cryptol/cryptoltypes.py | 3 +- cryptol-remote-api/python/cryptol/opaque.py | 10 +- cryptol-remote-api/src/CryptolServer.hs | 49 +--- cryptol-remote-api/src/CryptolServer/Check.hs | 4 +- .../src/CryptolServer/Data/Expression.hs | 270 +++++++++--------- .../src/CryptolServer/Data/FreshName.hs | 42 --- .../src/CryptolServer/EvalExpr.hs | 7 +- .../src/CryptolServer/Exceptions.hs | 22 +- cryptol-remote-api/src/CryptolServer/Sat.hs | 3 +- .../src/CryptolServer/TypeCheck.hs | 3 +- 13 files changed, 161 insertions(+), 262 deletions(-) delete mode 100644 cryptol-remote-api/src/CryptolServer/Data/FreshName.hs diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index bf9c25d3..7ee65548 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -63,7 +63,6 @@ library CryptolServer.Check CryptolServer.ClearState CryptolServer.Data.Expression - CryptolServer.Data.FreshName CryptolServer.Data.Type CryptolServer.EvalExpr CryptolServer.ExtendSearchPath diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index a59026bd..ed903a0a 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -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 ~~~~~~~~~~~~~~~~~~ diff --git a/cryptol-remote-api/python/cryptol/commands.py b/cryptol-remote-api/python/cryptol/commands.py index f219bafc..67e0fbbc 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/cryptol-remote-api/python/cryptol/commands.py @@ -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: diff --git a/cryptol-remote-api/python/cryptol/cryptoltypes.py b/cryptol-remote-api/python/cryptol/cryptoltypes.py index 2a442345..82df00cd 100644 --- a/cryptol-remote-api/python/cryptol/cryptoltypes.py +++ b/cryptol-remote-api/python/cryptol/cryptoltypes.py @@ -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)) diff --git a/cryptol-remote-api/python/cryptol/opaque.py b/cryptol-remote-api/python/cryptol/opaque.py index 9933b8d5..4078203e 100644 --- a/cryptol-remote-api/python/cryptol/opaque.py +++ b/cryptol-remote-api/python/cryptol/opaque.py @@ -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) diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs index 5a00e9ed..f1731937 100644 --- a/cryptol-remote-api/src/CryptolServer.hs +++ b/cryptol-remote-api/src/CryptolServer.hs @@ -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 diff --git a/cryptol-remote-api/src/CryptolServer/Check.hs b/cryptol-remote-api/src/CryptolServer/Check.hs index c8cd223b..497399f5 100644 --- a/cryptol-remote-api/src/CryptolServer/Check.hs +++ b/cryptol-remote-api/src/CryptolServer/Check.hs @@ -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) diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index 3e46a7a7..f8e46596 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -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) diff --git a/cryptol-remote-api/src/CryptolServer/Data/FreshName.hs b/cryptol-remote-api/src/CryptolServer/Data/FreshName.hs deleted file mode 100644 index e2ff0913..00000000 --- a/cryptol-remote-api/src/CryptolServer/Data/FreshName.hs +++ /dev/null @@ -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 diff --git a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs index 68807e25..2f3c5199 100644 --- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs +++ b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs @@ -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 diff --git a/cryptol-remote-api/src/CryptolServer/Exceptions.hs b/cryptol-remote-api/src/CryptolServer/Exceptions.hs index 304107f6..8b46bbf1 100644 --- a/cryptol-remote-api/src/CryptolServer/Exceptions.hs +++ b/cryptol-remote-api/src/CryptolServer/Exceptions.hs @@ -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." diff --git a/cryptol-remote-api/src/CryptolServer/Sat.hs b/cryptol-remote-api/src/CryptolServer/Sat.hs index affd90db..db00f316 100644 --- a/cryptol-remote-api/src/CryptolServer/Sat.hs +++ b/cryptol-remote-api/src/CryptolServer/Sat.hs @@ -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) diff --git a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs index accfc120..29447bd4 100644 --- a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs +++ b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs @@ -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 =