diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal index c4a6ea4d3..a3a00447b 100644 --- a/liquid-fixpoint.cabal +++ b/liquid-fixpoint.cabal @@ -127,8 +127,7 @@ library autogen-modules: Paths_liquid_fixpoint hs-source-dirs: src ghc-options: -W -Wno-missing-methods -Wmissing-signatures - build-depends: aeson - , ansi-terminal + build-depends: ansi-terminal , array , async , attoparsec @@ -145,6 +144,7 @@ library , filepath , hashable , intern + , json , lens-family , megaparsec >= 7.0.0 && < 10 , mtl diff --git a/src/Language/Fixpoint/Horn/Types.hs b/src/Language/Fixpoint/Horn/Types.hs index 400e44014..b8a83d5cb 100644 --- a/src/Language/Fixpoint/Horn/Types.hs +++ b/src/Language/Fixpoint/Horn/Types.hs @@ -39,14 +39,13 @@ import Data.Generics (Data) import Data.Typeable (Typeable) import GHC.Generics (Generic) import Control.DeepSeq ( NFData ) -import qualified Data.Text as T import Data.Maybe (fromMaybe) import qualified Data.List as L import qualified Language.Fixpoint.Misc as Misc import qualified Language.Fixpoint.Types as F import qualified Text.PrettyPrint.HughesPJ.Compat as P import qualified Data.HashMap.Strict as M -import Data.Aeson +import Text.JSON ------------------------------------------------------------------------------- -- | @HVar@ is a Horn variable @@ -226,9 +225,10 @@ instance F.PPrint Tag where pprintPrec _ _ NoTag = mempty pprintPrec _ _ (Tag s) = P.ptext s -instance ToJSON Tag where - toJSON NoTag = Null - toJSON (Tag s) = String (T.pack s) +instance JSON Tag where + showJSON NoTag = JSNull + showJSON (Tag s) = JSString (toJSString s) + readJSON _ = error "readJSON @Tag is undefined" instance F.PPrint (Query a) where pprintPrec k t q = P.vcat $ L.intersperse " " diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs index c2b43660d..90e43aaf8 100644 --- a/src/Language/Fixpoint/Solver.hs +++ b/src/Language/Fixpoint/Solver.hs @@ -29,9 +29,6 @@ module Language.Fixpoint.Solver ( import Control.Concurrent (setNumCapabilities) import qualified Data.HashMap.Strict as HashMap import qualified Data.Store as S -import Data.Aeson (ToJSON, encode) -import qualified Data.Text.Lazy.IO as LT -import qualified Data.Text.Lazy.Encoding as LT import System.Exit (ExitCode (..)) import System.Console.CmdArgs.Verbosity (whenNormal, whenLoud) import Text.PrettyPrint.HughesPJ (render) @@ -61,6 +58,7 @@ import Language.Fixpoint.Solver.Instantiate (instantiate) import Control.DeepSeq import qualified Data.ByteString as B import Data.Maybe (catMaybes) +import Text.JSON (JSON, encode) --------------------------------------------------------------------------- -- | Solve an .fq file ---------------------------------------------------- @@ -76,15 +74,15 @@ solveFQ cfg = do file = srcFile cfg --------------------------------------------------------------------------- -resultExitCode :: (Fixpoint a, NFData a, ToJSON a) => Config -> Result a +resultExitCode :: (Fixpoint a, NFData a, JSON a) => Config -> Result a -> IO ExitCode --------------------------------------------------------------------------- resultExitCode cfg r = do whenNormal $ colorStrLn (colorResult stat) (statStr $!! stat) - when (json cfg) $ LT.putStrLn jStr + when (json cfg) $ putStrLn jStr return (eCode r) where - jStr = LT.decodeUtf8 . encode $ r + jStr = encode r stat = resStatus $!! r eCode = resultExit . resStatus statStr = render . resultDoc diff --git a/src/Language/Fixpoint/Solver/Stats.hs b/src/Language/Fixpoint/Solver/Stats.hs index f1e433542..37fde55e3 100644 --- a/src/Language/Fixpoint/Solver/Stats.hs +++ b/src/Language/Fixpoint/Solver/Stats.hs @@ -12,7 +12,7 @@ import GHC.Generics import Text.PrettyPrint.HughesPJ (text) import qualified Data.Store as S import qualified Language.Fixpoint.Types.PrettyPrint as F -import Data.Aeson +import Text.JSON data Stats = Stats { numCstr :: !Int -- ^ # Horn Constraints @@ -43,11 +43,7 @@ instance Semigroup Stats where , numVald = numVald s1 + numVald s2 } -instance ToJSON Stats where - toJSON = genericToJSON defaultOptions - toEncoding = genericToEncoding defaultOptions - -instance FromJSON Stats +instance JSON Stats instance Monoid Stats where mempty = Stats 0 0 0 0 0 diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs index 94d0bc908..291b8e0eb 100644 --- a/src/Language/Fixpoint/Types/Constraints.hs +++ b/src/Language/Fixpoint/Types/Constraints.hs @@ -91,7 +91,6 @@ module Language.Fixpoint.Types.Constraints ( import qualified Data.Store as S import Data.Generics (Data) -import Data.Aeson hiding (Result) import qualified Data.Set as Set import Data.Typeable (Typeable) import Data.Hashable @@ -119,6 +118,7 @@ import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S import qualified Data.ByteString as B import qualified Data.Binary as B +import qualified Text.JSON -------------------------------------------------------------------------------- -- | Constraints --------------------------------------------------------------- @@ -282,9 +282,9 @@ data Result a = Result deriving (Generic, Show, Functor) - -instance ToJSON a => ToJSON (Result a) where - toJSON = toJSON . resStatus +instance Text.JSON.JSON a => Text.JSON.JSON (Result a) where + showJSON = Text.JSON.showJSON . resStatus + readJSON = error "readJSON @(Result a) is undefined" instance Semigroup (Result a) where r1 <> r2 = Result stat soln nonCutsSoln gsoln diff --git a/src/Language/Fixpoint/Types/Errors.hs b/src/Language/Fixpoint/Types/Errors.hs index 3b0806a00..bae0f2c67 100644 --- a/src/Language/Fixpoint/Types/Errors.hs +++ b/src/Language/Fixpoint/Types/Errors.hs @@ -55,7 +55,6 @@ module Language.Fixpoint.Types.Errors ( import System.Exit (ExitCode (..)) import Control.Exception import Data.Serialize (Serialize (..)) -import Data.Aeson hiding (Error, Result) import Data.Generics (Data) import Data.Typeable import Control.DeepSeq @@ -73,6 +72,7 @@ import Data.Function (on) -- import Debug.Trace import qualified Text.PrettyPrint.Annotated.HughesPJ as Ann +import qualified Text.JSON deriving instance Generic (Ann.AnnotDetails a) instance Serialize a => Serialize (Ann.AnnotDetails a) @@ -201,9 +201,7 @@ instance Monoid (FixResult a) where -- fmap f (Unsafe s xs) = Unsafe s (f <$> xs) -- fmap _ (Safe stats) = Safe stats -instance (ToJSON a) => ToJSON (FixResult a) where - toJSON = genericToJSON defaultOptions - toEncoding = genericToEncoding defaultOptions +instance Text.JSON.JSON a => Text.JSON.JSON (FixResult a) resultDoc :: (Fixpoint a) => FixResult a -> Doc resultDoc (Safe stats) = text "Safe (" <+> text (show $ Solver.checked stats) <+> " constraints checked)"