diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index 7ee65548b..6b29e31db 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -42,6 +42,7 @@ common deps bytestring ^>= 0.10.8, containers >=0.6.0.1 && <0.7, cryptol >= 2.9.0, + directory, filepath ^>= 1.4, lens >= 4.17 && < 4.20, mtl ^>= 2.2, diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index ed903a0a3..0f29e5c63 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -559,7 +559,7 @@ 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``, . + The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``. @@ -578,27 +578,37 @@ Parameter fields +``hash consing`` + Whether or not to use hash consing of terms (if available).``true`` to enable or ``false`` to disable. + + + Return fields +++++++++++++ ``result`` - A string (one of ``unsatisfiable``, ``invalid``, or ``satisfied``) indicating the result of checking for validity, satisfiability, or safety. + Either a string indicating the result of checking for validity, satisfiability, or safety---i.e., one of ``unsatisfiable``, ``invalid``, or ``satisfied``---or the string literal ``offline`` indicating an offline solver option was selected and the contents of the SMT query will be returned instead of a SAT result. ``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``. + 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``. ``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. + 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. ``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. + 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. + + + +``query`` + Only used if the ``result`` is ``offline``. The raw textual contents of the requested SMT query which can inspected or manually given to an SMT solver. diff --git a/cryptol-remote-api/python/cryptol/commands.py b/cryptol-remote-api/python/cryptol/commands.py index 67e0fbbc7..888aee744 100644 --- a/cryptol-remote-api/python/cryptol/commands.py +++ b/cryptol-remote-api/python/cryptol/commands.py @@ -9,7 +9,7 @@ import argo_client.interaction as argo from argo_client.interaction import HasProtocolState -from . import solver +from .solver import Solver, OfflineSmtQuery from .bitvector import BV from .opaque import OpaqueValue @@ -167,12 +167,13 @@ class SmtQueryType(str, Enum): SAT = 'sat' class CryptolProveSat(argo.Command): - def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : solver.Solver, count : Optional[int]) -> None: + def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : Solver, count : Optional[int]) -> None: super(CryptolProveSat, self).__init__( 'prove or satisfy', {'query type': qtype, 'expression': expr, - 'prover': solver, + 'prover': solver.name(), + 'hash consing': "true" if solver.hash_consing() else "false", 'result count': 'all' if count is None else count}, connection ) @@ -193,19 +194,21 @@ def process_result(self, res : Any) -> Any: return [from_cryptol_arg(arg['expr']) for m in res['models'] for arg in m] + elif res['result'] == 'offline': + return OfflineSmtQuery(content=res['query']) else: raise ValueError("Unknown SMT result: " + str(res)) class CryptolProve(CryptolProveSat): - def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None: + def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None: super(CryptolProve, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1) class CryptolSat(CryptolProveSat): - def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver, count : int) -> None: + def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int) -> None: super(CryptolSat, self).__init__(connection, SmtQueryType.SAT, expr, solver, count) class CryptolSafe(CryptolProveSat): - def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None: + def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None: super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1) class CryptolNames(argo.Command): diff --git a/cryptol-remote-api/python/cryptol/solver.py b/cryptol-remote-api/python/cryptol/solver.py index b1c8bf988..cfdc293ab 100644 --- a/cryptol-remote-api/python/cryptol/solver.py +++ b/cryptol-remote-api/python/cryptol/solver.py @@ -1,7 +1,35 @@ """Cryptol solver-related definitions""" from typing import NewType -Solver = NewType('Solver', str) +from dataclasses import dataclass + +@dataclass +class OfflineSmtQuery(): + """An SMTLIB2 script -- produced when an `offline` prover is used.""" + content: str + +class Solver(): + """An SMT solver mode selectable for Cryptol. Compare with the `:set prover` options in + the Cryptol REPL.""" + __name: str + __hash_consing: bool + + def __init__(self, name:str, hash_consing:bool=True) -> None: + self.__name = name + self.__hash_consing = hash_consing + + def name(self) -> str: + """Returns a string describing the solver setup which Cryptol will recognize -- i.e., + see the options available via `:set prover = NAME`.""" + return self.__name + + def hash_consing(self) -> bool: + """Returns whether hash consing is enabled (if applicable).""" + return self.__hash_consing + + def without_hash_consing(self) -> 'Solver': + """Returns an identical solver but with hash consing disabled (if applicable).""" + return Solver(name=self.__name, hash_consing=False) # Cryptol-supported SMT configurations/solvers # (see Cryptol.Symbolic.SBV Haskell module) @@ -25,5 +53,5 @@ W4_YICES: Solver = Solver("w4-yices") W4_Z3: Solver = Solver("w4-z3") W4_BOOLECTOR: Solver = Solver("w4-boolector") -W4_MATHSAT: Solver = Solver("w4-offline") +W4_OFFLINE: Solver = Solver("w4-offline") W4_ABC: Solver = Solver("w4-any") diff --git a/cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py b/cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py index d154878a1..f6cdd6dd8 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py +++ b/cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py @@ -54,7 +54,7 @@ def test_low_level(self): # self.assertEqual(add(BV(8,1), BV(8,2)), BV(8,3)) # self.assertEqual(add(BV(8,255), BV(8,1)), BV(8,0)) - def test_sat(self): + def test_sat_and_prove(self): c = self.c # test a single sat model can be returned rootsOf9 = c.sat('isSqrtOf9').result() @@ -81,6 +81,13 @@ def test_sat(self): # check for a valid condition self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]').result()) + self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.Z3).result()) + self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3).result()) + self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3.without_hash_consing()).result()) + self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.SBV_Z3).result()) + self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.OFFLINE).result(), solver.OfflineSmtQuery) + self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.SBV_OFFLINE).result(), solver.OfflineSmtQuery) + self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.W4_OFFLINE).result(), solver.OfflineSmtQuery) def test_check(self): c = self.c @@ -146,6 +153,12 @@ def test_safe(self): res = c.safe("\\x -> x / (x:[8])").result() self.assertEqual(res, [BV(size=8, value=0)]) + res = c.safe("\\x -> x / (x:[8])", solver.Z3).result() + self.assertEqual(res, [BV(size=8, value=0)]) + + res = c.safe("\\x -> x / (x:[8])", solver.W4_Z3).result() + self.assertEqual(res, [BV(size=8, value=0)]) + def test_many_usages_one_connection(self): c = self.c diff --git a/cryptol-remote-api/src/CryptolServer/Sat.hs b/cryptol-remote-api/src/CryptolServer/Sat.hs index db00f316e..752a08533 100644 --- a/cryptol-remote-api/src/CryptolServer/Sat.hs +++ b/cryptol-remote-api/src/CryptolServer/Sat.hs @@ -14,9 +14,12 @@ module CryptolServer.Sat import qualified Argo.Doc as Doc import Control.Applicative import Control.Monad.IO.Class -import Data.Aeson ((.=), (.:), FromJSON, ToJSON) +import Data.Aeson ((.=), (.:), (.:?), (.!=), FromJSON, ToJSON) +import qualified Data.Aeson as Aeson +import qualified Data.Aeson.Types as Aeson import qualified Data.Aeson as JSON import Data.IORef +import qualified Data.List as List import Data.Scientific (floatingOrInteger) import Data.Text (Text) import qualified Data.Text as T @@ -25,9 +28,11 @@ import Cryptol.Eval.Concrete (Value) import Cryptol.Eval.Type (TValue, tValTy) import Cryptol.ModuleSystem (checkExpr) import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv) +import Cryptol.REPL.Command (withRWTempFile) import Cryptol.Symbolic ( ProverCommand(..), ProverResult(..), QueryType(..) , SatNum(..), CounterExampleType(..)) -import Cryptol.Symbolic.SBV (proverNames, satProve, setupProver) +import qualified Cryptol.Symbolic.SBV as SBV +import qualified Cryptol.Symbolic.What4 as W4 import Cryptol.TypeCheck.AST (Expr) import Cryptol.TypeCheck.Solve (defaultReplExpr) @@ -35,6 +40,8 @@ import CryptolServer import CryptolServer.Exceptions (evalPolyErr, proverError) import CryptolServer.Data.Expression import CryptolServer.Data.Type +import Data.Text.IO as TIO +import System.IO (hSeek,SeekMode(..)) proveSatDescr :: Doc.Block proveSatDescr = @@ -42,61 +49,134 @@ proveSatDescr = [ Doc.Text "Find a value which satisfies the given predicate, or show that it is valid." , Doc.Text "(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)."] + + proveSat :: ProveSatParams -> CryptolCommand ProveSatResult -proveSat (ProveSatParams queryType (Prover name) jsonExpr) = - do e <- getExpr jsonExpr - (_expr, ty, schema) <- liftModuleCmd (checkExpr e) - -- TODO validEvalContext expr, ty, schema - me <- getModuleEnv - let decls = deDecls (meDynEnv me) - s <- getTCSolver - - perhapsDef <- liftIO (defaultReplExpr s ty schema) - case perhapsDef of - Nothing -> - raise (evalPolyErr schema) - Just (_tys, checked) -> - do timing <- liftIO $ newIORef 0 - let cmd = - ProverCommand - { pcQueryType = queryType - , pcProverName = name - , pcVerbose = True -- verbose - , pcProverStats = timing - , pcExtraDecls = decls - , pcSmtFile = Nothing -- mfile - , pcExpr = checked - , pcSchema = schema - , pcValidate = False - , pcIgnoreSafety = False - } - sbvCfg <- liftIO (setupProver name) >>= \case - Left msg -> error msg - Right (_ws, sbvCfg) -> return sbvCfg - (_firstProver, res) <- liftModuleCmd $ satProve sbvCfg cmd - _stats <- liftIO (readIORef timing) - case res of - ProverError msg -> raise (proverError msg) - EmptyResult -> error "got empty result for online prover!" - CounterExample cexType es -> Invalid cexType <$> satResult es - ThmResult _ts -> pure Unsatisfiable - AllSatResult results -> - Satisfied <$> traverse satResult results +proveSat (ProveSatParams queryType (ProverName proverName) jsonExpr hConsing) = do + e <- getExpr jsonExpr + (_expr, ty, schema) <- liftModuleCmd (checkExpr e) + -- TODO validEvalContext expr, ty, schema + decls <- deDecls . meDynEnv <$> getModuleEnv + s <- getTCSolver + perhapsDef <- liftIO (defaultReplExpr s ty schema) + case perhapsDef of + Nothing -> raise (evalPolyErr schema) + Just (_tys, checked) -> do + timing <- liftIO $ newIORef 0 + let cmd = + ProverCommand + { pcQueryType = queryType + , pcProverName = proverName + , pcVerbose = True + , pcProverStats = timing + , pcExtraDecls = decls + , pcSmtFile = Nothing + , pcExpr = checked + , pcSchema = schema + , pcValidate = False + , pcIgnoreSafety = False + } + res <- if proverName `elem` ["offline","sbv-offline","w4-offline"] + then offlineProveSat proverName cmd hConsing + else onlineProveSat proverName cmd hConsing + _stats <- liftIO (readIORef timing) + pure res - where - satResult :: [(TValue, Expr, Value)] -> CryptolCommand [(JSONType, Expression)] - satResult es = traverse result es - result (t, _, v) = do - me <- readBack t v - case me of - Nothing -> error $ "type is not convertable: " ++ (show t) - Just e -> pure (JSONType mempty (tValTy t), e) +getProverConfig :: + -- | Prover name. + String -> + CryptolCommand (Either SBV.SBVProverConfig W4.W4ProverConfig) +getProverConfig proverName = + if proverName `elem` W4.proverNames then do + liftIO (W4.setupProver proverName) >>= \case + Left msg -> raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg + Right (_ws, w4Cfg) -> pure $ Right w4Cfg + else if proverName `elem` SBV.proverNames then do + liftIO (SBV.setupProver proverName) >>= \case + Left msg -> raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg + Right (_ws, sbvCfg) -> pure $ Left sbvCfg + else do + raise $ proverError + $ proverName ++ "is not a recognized solver;" + ++ " please choose one of the following instead: " + ++ (show $ W4.proverNames ++ SBV.proverNames) + + +offlineProveSat :: + -- | Prover name. + String -> + ProverCommand -> + -- | Whether hash consing is enabled. + Bool -> + CryptolCommand ProveSatResult +offlineProveSat proverName cmd hConsing = do + getProverConfig proverName >>= \case + Left sbvCfg -> do + result <- liftModuleCmd $ SBV.satProveOffline sbvCfg cmd + case result of + Left msg -> do + raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg + Right smtlib -> pure $ OfflineSMTQuery $ T.pack smtlib + Right w4Cfg -> do + smtlibRef <- liftIO $ newIORef ("" :: Text) + result <- liftModuleCmd $ + W4.satProveOffline w4Cfg hConsing False cmd $ \f -> do + withRWTempFile "smtOutput.tmp" $ \h -> do + f h + hSeek h AbsoluteSeek 0 + contents <- TIO.hGetContents h + writeIORef smtlibRef contents + case result of + Just errMsg -> raise $ proverError $ "encountered an error using " ++ proverName ++ " to generate a query: " ++ errMsg + Nothing -> do + smtlib <- liftIO $ readIORef smtlibRef + pure $ OfflineSMTQuery smtlib + + +onlineProveSat :: + -- | Prover name. + String -> + ProverCommand -> + -- | Type of expression sat is being called for. + Bool -> + CryptolCommand ProveSatResult +onlineProveSat proverName cmd hConsing = do + res <- + getProverConfig proverName >>= \case + Left sbvCfg -> do + (_firstProver, res) <- liftModuleCmd $ SBV.satProve sbvCfg cmd + _stats <- liftIO (readIORef (pcProverStats cmd)) + pure res + Right w4Cfg -> do + (_firstProver, res) <- + liftModuleCmd $ W4.satProve w4Cfg hConsing False {- warn uninterp fns -} cmd + _stats <- liftIO (readIORef (pcProverStats cmd)) + pure res + case res of + ProverError msg -> raise (proverError msg) + EmptyResult -> raise $ proverError "got empty result for online prover!" + CounterExample cexType es -> Invalid cexType <$> convertSatResult es + ThmResult _ts -> pure Unsatisfiable + AllSatResult results -> + Satisfied <$> traverse convertSatResult results + + where + convertSatResult :: [(TValue, Expr, Value)] -> CryptolCommand [(JSONType, Expression)] + convertSatResult es = traverse result es + where + result :: forall b. (TValue, b, Value) -> CryptolCommand (JSONType, Expression) + result (t, _, v) = do + me <- readBack t v + case me of + Nothing -> error $ "type is not convertable: " ++ (show t) + Just e -> pure (JSONType mempty (tValTy t), e) data ProveSatResult = Unsatisfiable | Invalid CounterExampleType [(JSONType, Expression)] | Satisfied [[(JSONType, Expression)]] + | OfflineSMTQuery Text instance ToJSON ProveSatResult where toJSON Unsatisfiable = JSON.object ["result" .= ("unsatisfiable" :: Text)] @@ -124,25 +204,25 @@ instance ToJSON ProveSatResult where | res <- xs ] ] + toJSON (OfflineSMTQuery smtlib) = + JSON.object [ "result" .= ("offline" :: Text) + , "query" .= smtlib + ] +newtype ProverName = ProverName String -newtype Prover = Prover String - -instance FromJSON Prover where - parseJSON = - JSON.withText "prover name" $ - \txt -> - let str = T.unpack txt - in if str `elem` proverNames - then return (Prover str) - else empty - +instance FromJSON ProverName where + parseJSON (Aeson.String name) = pure $ ProverName $ T.unpack name + parseJSON invalid = + Aeson.prependFailure "parsing prover name failed, " + (Aeson.typeMismatch "String" invalid) data ProveSatParams = ProveSatParams { queryType :: QueryType - , prover :: Prover + , prover :: ProverName , expression :: Expression + , w4HashConsing :: Bool } instance FromJSON ProveSatParams where @@ -153,7 +233,12 @@ instance FromJSON ProveSatParams where expression <- o .: "expression" numResults <- (o .: "result count" >>= num) queryType <- (o .: "query type" >>= getQueryType numResults) - pure ProveSatParams{queryType, prover, expression} + hConsing <- (o .:? "hash consing" >>= onOrOff) .!= True + pure $ ProveSatParams + { queryType = queryType, + prover = prover, + expression = expression, + w4HashConsing = hConsing} where getQueryType numResults = (JSON.withText "query" $ @@ -169,13 +254,25 @@ instance FromJSON ProveSatParams where case floatingOrInteger s of Left (_float :: Double) -> empty Right int -> pure (SomeSat int)) v) + onOrOff Nothing = pure Nothing + onOrOff (Just val) = + (JSON.withText "hash consing" + (\case + "on" -> pure $ Just True + "true" -> pure $ Just True + "yes" -> pure $ Just True + "off" -> pure $ Just False + "false" -> pure $ Just False + "no" -> pure $ Just False + _ -> empty) + val) 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: "] - ++ (concat (map (\p -> [Doc.Literal (T.pack p), Doc.Text ", "]) proverNames)) + ++ (List.intersperse (Doc.Text ", ") $ map (Doc.Literal . T.pack) $ W4.proverNames ++ SBV.proverNames) ++ [Doc.Text "."])) , ("expression", Doc.Paragraph [ Doc.Text "The function to check for validity, satisfiability, or safety" @@ -197,15 +294,22 @@ instance Doc.DescribedMethod ProveSatParams ProveSatResult where , Doc.Text ")." ] ) + , ("hash consing", + Doc.Paragraph [Doc.Text "Whether or not to use hash consing of terms (if available)." + , Doc.Literal "true", Doc.Text" to enable or ", Doc.Literal "false", Doc.Text " to disable."]) ] resultFieldDescription = [ ("result", - Doc.Paragraph [ Doc.Text "A string (one of " + Doc.Paragraph [ Doc.Text "Either a string indicating the result of checking for validity, satisfiability, or safety" + , Doc.Text "---i.e., 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." + , Doc.Literal "satisfied", Doc.Text "---" + , Doc.Text "or the string literal " + , Doc.Literal "offline" + , Doc.Text " indicating an offline solver option was selected and the contents of the SMT query will be" + , Doc.Text " returned instead of a SAT result." ]) , ("counterexample type", Doc.Paragraph $ onlyIfResultIs "invalid" ++ @@ -224,7 +328,12 @@ instance Doc.DescribedMethod ProveSatParams ProveSatResult where , 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." ]) + , ("query", + Doc.Paragraph $ onlyIfResultIs "offline" ++ + [ Doc.Text "The raw textual contents of the requested SMT query which can inspected or manually" + , Doc.Text " given to an SMT solver." + ]) ] where onlyIfResultIs val = [ Doc.Text "Only used if the " , Doc.Literal "result" - , Doc.Text " is ", Doc.Literal val, Doc.Text "." ] + , Doc.Text " is ", Doc.Literal val, Doc.Text ". " ] diff --git a/cryptol-remote-api/update_docs.sh b/cryptol-remote-api/update_docs.sh new file mode 100755 index 000000000..ef144f543 --- /dev/null +++ b/cryptol-remote-api/update_docs.sh @@ -0,0 +1,7 @@ +#! /bin/bash + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" + +pushd $DIR/docs +cabal run exe:cryptol-remote-api --verbose=0 -- doc > Cryptol.rst +popd diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 72754ea7a..8f9143640 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -46,6 +46,7 @@ module Cryptol.REPL.Command ( -- Misc utilities , handleCtrlC , sanitize + , withRWTempFile -- To support Notebook interface (might need to refactor) , replParse