Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cryptol-remote-api: Allow building with aeson-2.0.* #1308

Merged
merged 1 commit into from
Nov 30, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion cryptol-remote-api/cryptol-remote-api.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ common deps
build-depends:
base >=4.11.1.0 && <4.15,
argo,
aeson >= 1.4.2 && < 2.0,
aeson >= 1.4.2 && < 2.1,
base64-bytestring >= 1.0,
bytestring ^>= 0.10.8,
containers >=0.6.0.1 && <0.7,
Expand Down Expand Up @@ -81,6 +81,9 @@ library
CryptolServer.Sat
CryptolServer.TypeCheck

other-modules:
CryptolServer.AesonCompat

executable cryptol-remote-api
import: deps, warnings, errors
main-is: Main.hs
Expand Down
68 changes: 68 additions & 0 deletions cryptol-remote-api/src/CryptolServer/AesonCompat.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
{-# LANGUAGE CPP #-}

-- | A compatibility shim for papering over the differences between
-- @aeson-2.0.*@ and pre-2.0.* versions of @aeson@.
--
-- TODO: When the ecosystem widely uses @aeson-2.0.0.0@ or later, remove this
-- module entirely.
module CryptolServer.AesonCompat where

import Data.HashMap.Strict (HashMap)
import Data.Text (Text)

#if MIN_VERSION_aeson(2,0,0)
import Data.Aeson.Key (Key)
import qualified Data.Aeson.Key as K
import Data.Aeson.KeyMap (KeyMap)
import qualified Data.Aeson.KeyMap as KM
#else
import qualified Data.HashMap.Strict as HM
#endif

#if MIN_VERSION_aeson(2,0,0)
type KeyCompat = Key

deleteKM :: Key -> KeyMap v -> KeyMap v
deleteKM = KM.delete

fromListKM :: [(Key, v)] -> KeyMap v
fromListKM = KM.fromList

keyFromText :: Text -> Key
keyFromText = K.fromText

keyToText :: Key -> Text
keyToText = K.toText

lookupKM :: Key -> KeyMap v -> Maybe v
lookupKM = KM.lookup

toHashMapTextKM :: KeyMap v -> HashMap Text v
toHashMapTextKM = KM.toHashMapText

toListKM :: KeyMap v -> [(Key, v)]
toListKM = KM.toList
#else
type KeyCompat = Text

deleteKM :: Text -> HashMap Text v -> HashMap Text v
deleteKM = HM.delete

fromListKM :: [(Text, v)] -> HashMap Text v
fromListKM = HM.fromList

keyFromText :: Text -> Text
keyFromText = id

keyToText :: Text -> Text
keyToText = id

lookupKM :: Text -> HashMap Text v -> Maybe v
lookupKM = HM.lookup

toHashMapTextKM :: HashMap Text v -> HashMap Text v
toHashMapTextKM = id

toListKM :: HashMap Text v -> [(Text, v)]
toListKM = HM.toList
#endif
3 changes: 2 additions & 1 deletion cryptol-remote-api/src/CryptolServer/Check.hs
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ import CryptolServer
liftModuleCmd,
CryptolMethod(raise),
CryptolCommand )
import CryptolServer.AesonCompat (KeyCompat)
import CryptolServer.Exceptions (evalPolyErr)
import CryptolServer.Data.Expression
( readBack, getExpr, Expression)
Expand Down Expand Up @@ -118,7 +119,7 @@ data CheckResult =
, checkTestsPossible :: Maybe Integer
}

convertServerTestResult :: ServerTestResult -> [(Text, JSON.Value)]
convertServerTestResult :: ServerTestResult -> [(KeyCompat, JSON.Value)]
convertServerTestResult Pass = ["result" .= ("pass" :: Text)]
convertServerTestResult (FailFalse args) =
[ "result" .= ("fail" :: Text)
Expand Down
9 changes: 5 additions & 4 deletions cryptol-remote-api/src/CryptolServer/Data/Expression.hs
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields)
import Argo
import qualified Argo.Doc as Doc
import CryptolServer
import CryptolServer.AesonCompat
import CryptolServer.Exceptions
import CryptolServer.Data.Type

Expand Down Expand Up @@ -160,9 +161,9 @@ instance JSON.FromJSON TypeArguments where
parseJSON =
withObject "type arguments" $ \o ->
TypeArguments . Map.fromList <$>
traverse elt (HM.toList o)
traverse elt (toListKM o)
where
elt (name, ty) = (mkIdent name,) <$> parseJSON ty
elt (name, ty) = (mkIdent (keyToText name),) <$> parseJSON ty

instance JSON.FromJSON Expression where
parseJSON v = bool v <|> integer v <|> concrete v <|> obj v
Expand Down Expand Up @@ -192,7 +193,7 @@ instance JSON.FromJSON Expression where
TagRecord ->
do fields <- o .: "data"
flip (withObject "record data") fields $
\fs -> Record <$> traverse parseJSON fs
\fs -> (Record . toHashMapTextKM) <$> traverse parseJSON fs
TagSequence ->
do contents <- o .: "data"
flip (withArray "sequence") contents $
Expand Down Expand Up @@ -234,7 +235,7 @@ instance JSON.ToJSON Expression where
]
toJSON (Record fields) =
object [ "expression" .= TagRecord
, "data" .= object [ fieldName .= toJSON val
, "data" .= object [ keyFromText fieldName .= toJSON val
| (fieldName, val) <- HM.toList fields
]
]
Expand Down
10 changes: 5 additions & 5 deletions cryptol-remote-api/src/CryptolServer/Data/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ import qualified Data.Aeson as JSON
import Data.Aeson ((.=), (.:), (.!=), (.:?))
import Data.Aeson.Types (Parser, typeMismatch)
import Data.Functor ((<&>))
import qualified Data.HashMap.Strict as HM
import qualified Data.Text as T

import qualified Cryptol.Parser.AST as C
Expand All @@ -27,6 +26,7 @@ import Cryptol.Utils.PP (pp)
import Cryptol.Utils.RecordMap (canonicalFields)

import qualified Argo.Doc as Doc
import CryptolServer.AesonCompat


newtype JSONSchema = JSONSchema Schema
Expand Down Expand Up @@ -219,7 +219,7 @@ instance JSON.ToJSON JSONType where
JSON.object
[ "type" .= T.pack "record"
, "fields" .=
JSON.object [ T.pack (show (pp f)) .= JSONType ns t'
JSON.object [ keyFromText (T.pack (show (pp f))) .= JSONType ns t'
| (f, t') <- canonicalFields fields
]
]
Expand All @@ -231,17 +231,17 @@ instance JSON.FromJSON JSONPType where
where
getType :: JSON.Value -> Parser (C.Type C.PName)
getType (JSON.Object o) =
case HM.lookup "type" o of
case lookupKM "type" o of
Just t -> asType t o
Nothing ->
case HM.lookup "prop" o of
case lookupKM "prop" o of
Just p -> asProp p o
Nothing -> fail "Expected type or prop key"
getType other = typeMismatch "object" other

asType "record" = \o -> C.TRecord <$> ((o .: "fields") >>= getFields)
where
getFields obj = recordFromFields <$> traverse (\(k, v) -> (mkIdent k,) . (emptyRange,) <$> getType v) (HM.toList obj)
getFields obj = recordFromFields <$> traverse (\(k, v) -> (mkIdent (keyToText k),) . (emptyRange,) <$> getType v) (toListKM obj)
asType "variable" = \o -> C.TUser <$> (name <$> o .: "name") <*> (map unJSONPType <$> (o .:? "arguments" .!= []))
asType "number" = \o -> C.TNum <$> (o .: "value")
asType "inf" = const $ pure $ C.TUser (name "inf") []
Expand Down
6 changes: 3 additions & 3 deletions cryptol-remote-api/src/CryptolServer/Exceptions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,12 @@ import Data.ByteString (ByteString)
import qualified Data.ByteString.Char8 as B8
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.HashMap.Strict as HashMap

import Cryptol.Parser
import qualified Cryptol.TypeCheck.Type as TC

import Argo
import CryptolServer.AesonCompat
import CryptolServer.Data.Type

cryptolError :: ModuleError -> [ModuleWarning] -> JSONRPCException
Expand Down Expand Up @@ -167,7 +167,7 @@ unwantedDefaults defs =
makeJSONRPCException
20210 "Execution would have required these defaults"
(Just (JSON.object ["defaults" .=
[ jsonTypeAndString ty <> HashMap.fromList ["parameter" .= pretty param]
[ jsonTypeAndString ty <> fromListKM ["parameter" .= pretty param]
| (param, ty) <- defs ] ]))

evalInParamMod :: [CM.Name] -> JSONRPCException
Expand Down Expand Up @@ -204,6 +204,6 @@ cryptolParseErr expr err =
-- human-readable string
jsonTypeAndString :: TC.Type -> JSON.Object
jsonTypeAndString ty =
HashMap.fromList
fromListKM
[ "type" .= JSONSchema (TC.Forall [] [] ty)
, "type string" .= pretty ty ]
7 changes: 4 additions & 3 deletions cryptol-remote-api/src/CryptolServer/Options.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,15 @@ import qualified Argo.Doc as Doc
import Data.Aeson hiding (Options)
import Data.Aeson.Types (Parser, typeMismatch)
import Data.Coerce
import qualified Data.HashMap.Strict as HM
import qualified Data.Text as T

import Cryptol.Eval(EvalOpts(..))
import Cryptol.REPL.Monad (parseFieldOrder, parsePPFloatFormat)
import Cryptol.Utils.Logger (quietLogger)
import Cryptol.Utils.PP (PPOpts(..), PPFloatFormat(..), PPFloatExp(..), FieldOrder(..), defaultPPOpts)

import CryptolServer.AesonCompat

data Options = Options { optCallStacks :: Bool, optEvalOpts :: EvalOpts }

newtype JSONEvalOpts = JSONEvalOpts { getEvalOpts :: EvalOpts }
Expand All @@ -40,7 +41,7 @@ newtypeField :: forall wrapped bare proxy.
(Coercible wrapped bare, FromJSON wrapped) =>
proxy wrapped bare ->
Object -> T.Text -> bare -> Parser bare
newtypeField _proxy o field def = unwrap (o .:! field) .!= def where
newtypeField _proxy o field def = unwrap (o .:! keyFromText field) .!= def where
unwrap :: Parser (Maybe wrapped) -> Parser (Maybe bare)
unwrap = coerce

Expand Down Expand Up @@ -85,7 +86,7 @@ instance FromJSON a => FromJSON (WithOptions a) where
\o ->
WithOptions <$>
o .:! "options" .!= defaultOpts <*>
parseJSON (Object (HM.delete "options" o))
parseJSON (Object (deleteKM "options" o))

defaultOpts :: Options
defaultOpts = Options False theEvalOpts
Expand Down