Skip to content

Commit

Permalink
Replace aeson with json
Browse files Browse the repository at this point in the history
  • Loading branch information
facundominguez committed Dec 7, 2023
1 parent b6c3e11 commit 4ffa275
Show file tree
Hide file tree
Showing 6 changed files with 19 additions and 27 deletions.
4 changes: 2 additions & 2 deletions liquid-fixpoint.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -145,6 +144,7 @@ library
, filepath
, hashable
, intern
, json
, lens-family
, megaparsec >= 7.0.0 && < 10
, mtl
Expand Down
10 changes: 5 additions & 5 deletions src/Language/Fixpoint/Horn/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 " "
Expand Down
10 changes: 4 additions & 6 deletions src/Language/Fixpoint/Solver.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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 ----------------------------------------------------
Expand All @@ -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
Expand Down
8 changes: 2 additions & 6 deletions src/Language/Fixpoint/Solver/Stats.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/Language/Fixpoint/Types/Constraints.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 ---------------------------------------------------------------
Expand Down Expand Up @@ -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
Expand Down
6 changes: 2 additions & 4 deletions src/Language/Fixpoint/Types/Errors.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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)"
Expand Down

0 comments on commit 4ffa275

Please sign in to comment.