GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-07 08:19:12 +03:00
Code Issues Projects Releases Wiki Activity

add pretty-printing to some server replies

Browse Source
This commit is contained in:
Adam C. Foltzer 2015-07-10 18:19:30 -07:00
parent 89b4567b93
commit d7cf61f8e0
1 changed files with 9 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
cryptol-server/Main.hs
View File

@ -29,6 +29,7 @@ import Cryptol.REPL.Command
import Cryptol.REPL.Monad import Cryptol.REPL.Monad
import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.ModuleSystem as M import qualified Cryptol.ModuleSystem as M
import Cryptol.Utils.PP
import Cryptol.Aeson () import Cryptol.Aeson ()
@ -75,13 +76,13 @@ instance FromJSON FunHandle where
data RResult data RResult
= RRValue E.Value = RRValue E.Value
| RRFunValue FunHandle T.Type | RRFunValue FunHandle T.Type
| RRType T.Schema | RRType T.Schema String -- pretty-printed type
| RRDecls M.IfaceDecls | RRDecls M.IfaceDecls
| RRCheck String | RRCheck String
| RRExhaust String | RRExhaust String
| RRSat String | RRSat String
| RRProve String | RRProve String
| RRInteractiveError REPLException | RRInteractiveError REPLException String -- pretty-printed exception
| RRUnknownCmd Text | RRUnknownCmd Text
| RRBadMessage BS.ByteString String | RRBadMessage BS.ByteString String
| RROk | RROk
@ -92,8 +93,8 @@ instance ToJSON RResult where
[ "tag" .= "value", "value" .= v ] [ "tag" .= "value", "value" .= v ]
RRFunValue fh t -> object RRFunValue fh t -> object
[ "tag" .= "funValue", "handle" .= fh, "type" .= t ] [ "tag" .= "funValue", "handle" .= fh, "type" .= t ]
RRType s -> object RRType s pps -> object
[ "tag" .= "type", "value" .= s ] [ "tag" .= "type", "value" .= s, "pp" .= pps ]
RRDecls ifds -> object RRDecls ifds -> object
[ "tag" .= "decls", "decls" .= ifds ] [ "tag" .= "decls", "decls" .= ifds ]
RRCheck out -> object RRCheck out -> object
@ -104,8 +105,8 @@ instance ToJSON RResult where
[ "tag" .= "sat", "out" .= out ] [ "tag" .= "sat", "out" .= out ]
RRProve out -> object RRProve out -> object
[ "tag" .= "prove", "out" .= out ] [ "tag" .= "prove", "out" .= out ]
RRInteractiveError err -> object RRInteractiveError err pps -> object
[ "tag" .= "interactiveError", "error" .= err ] [ "tag" .= "interactiveError", "error" .= err, "pp" .= pps ]
RRUnknownCmd txt -> object RRUnknownCmd txt -> object
[ "tag" .= "unknownCommand", "command" .= txt ] [ "tag" .= "unknownCommand", "command" .= txt ]
RRBadMessage msg err -> object RRBadMessage msg err -> object
@ -193,7 +194,7 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
#endif #endif
loadPrelude loadPrelude
funHandles <- io $ newIORef (Map.empty, minBound :: FunHandle) funHandles <- io $ newIORef (Map.empty, minBound :: FunHandle)
let handle err = reply rep (RRInteractiveError err) let handle err = reply rep (RRInteractiveError err (show (pp err)))
loop = do loop = do
msg <- io $ receive rep msg <- io $ receive rep
io $ putStrLn "[cryptol-worker] received message:" io $ putStrLn "[cryptol-worker] received message:"
@ -222,7 +223,7 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
RCTypeOf txt -> do RCTypeOf txt -> do
expr <- replParseExpr (T.unpack txt) expr <- replParseExpr (T.unpack txt)
(_expr, _def, sch) <- replCheckExpr expr (_expr, _def, sch) <- replCheckExpr expr
reply rep (RRType sch) reply rep (RRType sch (show (pp sch)))
RCSetOpt key val -> do RCSetOpt key val -> do
setOptionCmd (T.unpack key ++ "=" ++ T.unpack val) setOptionCmd (T.unpack key ++ "=" ++ T.unpack val)
reply rep RROk reply rep RROk