Skip to content

Commit 0d61ed1

Browse files
author
Adam C. Foltzer
committed
Merge branch 'feature/cryptol-server'
Brings the JSON over ZeroMQ server into the main line of development. It is disabled by default, but there is now a `server` flag in `cryptol.cabal` that in turn gets enabled if the `CRYPTOL_SERVER` environment variable is nonempty during `make`.
2 parents 6a7477b + 900e4ac commit 0d61ed1

File tree

11 files changed

+730
-136
lines changed

11 files changed

+730
-136
lines changed

‎Makefile

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ GIT_INFO_FILES := ${GIT_INFO_FILES} .git/packed-refs
110110
endif
111111

112112
CRYPTOL_SRC := \
113-
$(shell find src cryptol \
113+
$(shell find src cryptol cryptol-server \
114114
\( -name \*.hs -or -name \*.x -or -name \*.y \) \
115115
-and \( -not -name \*\#\* \) -print) \
116116
$(shell find lib -name \*.cry) \
@@ -119,6 +119,11 @@ CRYPTOL_SRC := \
119119
print-%:
120120
@echo $* = $($*)
121121

122+
# If CRYPTOL_SERVER is nonempty, build the cryptol-server executable
123+
ifneq (,${CRYPTOL_SERVER})
124+
SERVER_FLAG := -fserver
125+
endif
126+
122127
# We do things differently based on whether we have a PREFIX set by
123128
# the user. If we do, then we know the eventual path it'll wind up in
124129
# (useful for stuff like RPMs or Homebrew). If not, we try to be as
@@ -127,7 +132,8 @@ ifneq (,${PREFIX})
127132
PREFIX_ARG := --prefix=$(call adjust-path,${PREFIX_ABS})
128133
DESTDIR_ARG := --destdir=${PKG}
129134
CONFIGURE_ARGS := -f-relocatable -f-self-contained \
130-
--docdir=$(call adjust-path,${PREFIX}/${PREFIX_SHARE}/${PREFIX_DOC})
135+
--docdir=$(call adjust-path,${PREFIX}/${PREFIX_SHARE}/${PREFIX_DOC}) \
136+
${SERVER_FLAG}
131137
else
132138
# This is kind of weird: 1. Prefix argument must be absolute; Cabal
133139
# doesn't yet fully support relocatable packages. 2. We have to
@@ -136,7 +142,8 @@ else
136142
PREFIX_ARG := --prefix=$(call adjust-path,${ROOT_PATH})
137143
DESTDIR_ARG := --destdir=${PKG}
138144
CONFIGURE_ARGS := -f-self-contained \
139-
--docdir=$(call adjust-path,${PREFIX_SHARE}/${PREFIX_DOC})
145+
--docdir=$(call adjust-path,${PREFIX_SHARE}/${PREFIX_DOC}) \
146+
${SERVER_FLAG}
140147
endif
141148

142149
dist/setup-config: cryptol.cabal Makefile | ${CS_BIN}/alex ${CS_BIN}/happy

‎README.md

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,19 @@ be happy to incorporate your changes.
155155
The ICryptol notebook interface is now a
156156
[standalone project](https://github.com/GaloisInc/ICryptol).
157157

158+
### Cryptol Server and pycryptol (Experimental)
159+
160+
This package includes an executable in `/cryptol-server` that provides
161+
an interface to the Cryptol interpreter via JSON over
162+
ZeroMQ. Currently this is used to support the
163+
[`pycryptol`](http://pycryptol.readthedocs.org/en/latest/) library. It
164+
is part of this package because we intend to eventually make the
165+
console REPL a client of that server as well. The `cryptol-server`
166+
executable is included in any builds if the `CRYPTOL_SERVER`
167+
environment variable is non-empty when running `make`, for example:
168+
169+
CRYPTOL_SERVER=1 make dist
170+
158171
# Where to Look Next
159172

160173
The `docs` directory of the installation package contains an

‎cryptol-server/Cryptol/Aeson.hs

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
{-# LANGUAGE ExtendedDefaultRules #-}
2+
{-# LANGUAGE TemplateHaskell #-}
3+
{-# LANGUAGE LambdaCase #-}
4+
{-# LANGUAGE FlexibleInstances #-}
5+
{-# LANGUAGE RecordWildCards #-}
6+
{-# OPTIONS_GHC -Wall -fno-warn-orphans -fno-warn-type-defaults #-}
7+
-- | Orphan 'FromJSON' and 'ToJSON' instances for certain Cryptol
8+
-- types. Since these are meant to be consumed over a wire, they are
9+
-- mostly focused on base values and interfaces rather than a full
10+
-- serialization of internal ASTs and such.
11+
module Cryptol.Aeson where
12+
13+
import Control.Applicative
14+
import Control.Exception
15+
import Data.Aeson
16+
import Data.Aeson.TH
17+
import qualified Data.HashMap.Strict as HM
18+
import Data.List
19+
import qualified Data.Map as Map
20+
import Data.Map (Map)
21+
import Data.Text (Text)
22+
import qualified Data.Text as T
23+
24+
import qualified Cryptol.Eval.Error as E
25+
import qualified Cryptol.Eval.Value as E
26+
import qualified Cryptol.ModuleSystem as M
27+
import qualified Cryptol.ModuleSystem.Monad as M
28+
import qualified Cryptol.ModuleSystem.Renamer as M
29+
import Cryptol.ModuleSystem.Interface
30+
import Cryptol.ModuleSystem.Name
31+
import qualified Cryptol.Parser as P
32+
import qualified Cryptol.Parser.AST as P
33+
import qualified Cryptol.Parser.Lexer as P
34+
import qualified Cryptol.Parser.NoInclude as P
35+
import qualified Cryptol.Parser.NoPat as NoPat
36+
import qualified Cryptol.Parser.Position as P
37+
import Cryptol.REPL.Monad
38+
import qualified Cryptol.TypeCheck.AST as T
39+
import qualified Cryptol.TypeCheck.InferTypes as T
40+
import Cryptol.Utils.PP hiding (empty)
41+
42+
instance FromJSON a => FromJSON (Map QName a) where
43+
parseJSON = withObject "QName map" $ \o -> do
44+
let (ks, vs) = unzip (HM.toList o)
45+
ks' = map keyToQName ks
46+
vs' <- mapM parseJSON vs
47+
return (Map.fromList (zip ks' vs'))
48+
49+
instance ToJSON a => ToJSON (Map QName a) where
50+
toJSON m = Object (HM.fromList (zip ks' vs'))
51+
where (ks, vs) = unzip (Map.toList m)
52+
ks' = map keyFromQName ks
53+
vs' = map toJSON vs
54+
55+
-- | Assume that a 'QName' contains only an optional 'ModName' and a
56+
-- 'Name', rather than a 'NewName'. This should be safe for the
57+
-- purposes of this API where we're dealing with top-level names.
58+
keyToQName :: Text -> QName
59+
keyToQName str =
60+
case map T.unpack (T.split (== '.') str) of
61+
[] -> error "empty QName"
62+
[""] -> error "empty QName"
63+
[x] -> mkUnqual (Name x)
64+
xs -> mkQual (ModName (init xs)) (Name (last xs))
65+
66+
keyFromQName :: QName -> Text
67+
keyFromQName = \case
68+
QName Nothing (Name x) -> T.pack x
69+
QName (Just (ModName mn)) (Name x) ->
70+
T.pack (intercalate "." (mn ++ [x]))
71+
_ -> error "NewName unsupported in JSON"
72+
73+
instance ToJSON Doc where
74+
toJSON = String . T.pack . render
75+
76+
instance ToJSON E.Value where
77+
toJSON = \case
78+
E.VRecord fs -> object
79+
[ "record" .= fs ]
80+
E.VTuple vs -> object
81+
[ "tuple" .= vs ]
82+
E.VBit b -> object
83+
[ "bit" .= b ]
84+
E.VSeq isWord xs -> object
85+
[ "sequence" .= object [ "isWord" .= isWord, "elements" .= xs ] ]
86+
E.VWord w -> object
87+
[ "word" .= w ]
88+
E.VStream _ -> object
89+
[ "stream" .= object [ "@note" .= "streams not supported" ] ]
90+
E.VFun _ -> object
91+
[ "function" .= object [ "@note" .= "functions not supported" ] ]
92+
E.VPoly _ -> object
93+
[ "poly" .= object [ "@note" .= "polymorphic values not supported" ] ]
94+
95+
instance FromJSON E.Value where
96+
parseJSON = withObject "Value" $ \o ->
97+
E.VRecord <$> o .: "record"
98+
<|> E.VTuple <$> o .: "tuple"
99+
<|> E.VBit <$> o .: "bit"
100+
<|> do s <- o .: "sequence"
101+
E.VSeq <$> s .: "isWord" <*> s .: "elements"
102+
<|> E.VWord <$> o .: "word"
103+
<|> error ("unexpected JSON value: " ++ show o)
104+
105+
instance ToJSON P.Token where
106+
toJSON = toJSON . pp
107+
108+
instance ToJSON IOException where
109+
toJSON exn = object
110+
[ "IOException" .= show exn ]
111+
112+
instance ToJSON M.RenamerError where
113+
toJSON err = object
114+
[ "renamerError" .= pp err ]
115+
116+
instance ToJSON T.Error where
117+
toJSON err = object
118+
[ "inferError" .= pp err ]
119+
120+
instance ToJSON E.BV where
121+
toJSON = \case
122+
E.BV w v -> object
123+
[ "bitvector" .= object [ "width" .= w, "value" .= v ] ]
124+
125+
instance FromJSON E.BV where
126+
parseJSON = withObject "BV" $ \o -> do
127+
bv <- o .: "bitvector"
128+
E.BV <$> bv .: "width" <*> bv .: "value"
129+
130+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''REPLException)
131+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NameEnv)
132+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NameInfo)
133+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''E.EvalError)
134+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.ParseError)
135+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Position)
136+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Range)
137+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Located)
138+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.IncludeError)
139+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Schema)
140+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Type)
141+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.TParam)
142+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Prop)
143+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Named)
144+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Kind)
145+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NoPat.Error)
146+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''M.ModuleError)
147+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''M.ImportSource)
148+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Import)
149+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.ImportSpec)
150+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Type)
151+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TParam)
152+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Kind)
153+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TVar)
154+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TCon)
155+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.PC)
156+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TC)
157+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.UserTC)
158+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Schema)
159+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TFun)
160+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Selector)
161+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } { fieldLabelModifier = drop 1 } ''T.Fixity)
162+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Pragma)
163+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Assoc)
164+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''QName)
165+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''ModName)
166+
$(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Name)
167+
$(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Pass)
168+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''IfaceDecl)
169+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Newtype)
170+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TySyn)
171+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''IfaceDecls)
172+
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Iface)

0 commit comments

Comments
 (0)