content: -----------------------------------------------------------------------------
  -- |
  -- Module    : TestSuite.ADT.ADT
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Testing ADTs
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE FlexibleInstances   #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell     #-}
  {-# LANGUAGE TypeApplications    #-}
  
  {-# OPTIONS_GHC -Wall -Werror -Wno-unused-top-binds #-}
  
  module TestSuite.ADT.ADT(tests) where
  
  import Utils.SBVTestFramework
  import Data.SBV.Control
  import Data.SBV.Maybe
  
  data ADT  = AEmpty
            | ABool    Bool
            | AInteger Integer
            | AWord8   Word8
            | AWord16  Word16
            | AWord32  Word32
            | AWord64  Word64
            | AInt8    Int8
            | AInt16   Int16
            | AInt32   Int32
            | AInt64   Int64
            | AWord1   (WordN  1)
            | AWord5   (WordN  5)
            | AWord30  (WordN 30)
            | AInt1    (IntN   1)
            | AInt5    (IntN   5)
            | AInt30   (IntN  30)
            | AReal    AlgReal
            | AFloat   Float
            | ADouble  Double
            | AFP      (FloatingPoint 5 12)
            | AString  String
            | AList    [Integer]
            | ATuple   (Double, [(WordN 5, [Float])])
            | AMaybe   (Maybe (AlgReal, Float, (Either Integer Float, [Bool])))
            | AEither  (Either (Maybe Integer, Bool) [Integer])
            | APair    ADT ADT
            {-
            | KADT      String (Maybe [(String, [Kind])])
            | KChar
            | KSet  Kind
            | KArray  Kind Kind
            -}
            deriving Show
  
  mkSymbolic [''ADT]
  
  tests :: TestTree
  tests =
    testGroup "ADT" [
        goldenCapturedIO "adt00" $ checkWith t00
      , goldenCapturedIO "adt01" $ checkWith t01
      , goldenCapturedIO "adt02" $ checkWith t02
      , goldenCapturedIO "adt03" $ checkWith t03
      , goldenCapturedIO "adt04" t04
      , goldenCapturedIO "adt05" t05
      , goldenCapturedIO "adt06" t06
      ]
  
  checkWith :: Symbolic () -> FilePath -> IO ()
  checkWith props rf = runSMTWith z3{verbose=True, redirectVerbose = Just rf} $ do
          _ <- props
          query $ do cs <- checkSat
                     case cs of
                       Unsat  -> io $ appendFile rf "\nUNSAT"
                       DSat{} -> io $ appendFile rf "\nDSAT"
                       Sat{}  -> getModel         >>= \m -> io $ appendFile rf $ "\nMODEL: "   ++ show m ++ "\nDONE."
                       Unk    -> getUnknownReason >>= \r -> io $ appendFile rf $ "\nUNKNOWN: " ++ show r ++ "\nDONE."
  
  t00 :: Symbolic ()
  t00 = do a :: SADT <- free "e"
           constrain $ a ./== a
  
  t01 :: Symbolic ()
  t01 = do a :: SADT <- free "e"
           constrain $ a .=== literal (APair (AInt64 4) (AMaybe (Just (0, 12, (Left 3, [False, True])))))
  
  t02 :: Symbolic ()
  t02 = do a :: SADT <- free "e"
           constrain $ isAList a
  
  t03 :: Symbolic ()
  t03 = do a :: SADT <- free "e"
           constrain $ isAList a .&& isAFP a
  
  t04 :: FilePath -> IO ()
  t04 rf = do AllSatResult _ _ _ ms <- allSatWith z3{verbose=True, redirectVerbose = Just rf} t
              let sh m = appendFile rf $ "\nMODEL:" ++ show (SatResult m)
              mapM_ sh ms
    where t = do a :: SADT <- free "a"
                 constrain $ isAInteger a
                 constrain $ getAInteger_1 a .>= 0
                 constrain $ getAInteger_1 a .<= 5
  
  -- z3 is buggy on this. So we use cvc5. See: https://github.com/Z3Prover/z3/issues/7842
  t05 :: FilePath -> IO ()
  t05 rf = do AllSatResult _ _ _ ms <- allSatWith cvc5{verbose=True, redirectVerbose = Just rf, allSatMaxModelCount=Just 10} t
              let sh m = appendFile rf $ "\nMODEL:" ++ show (SatResult m)
              mapM_ sh ms
    where t = do a :: SADT <- free "a"
                 b :: SADT <- free "b"
                 constrain $ isAFloat a .&& getAFloat_1 a .== 4
                 constrain $ isAFloat b .&& fpIsNaN (getAFloat_1 b)
  
  t06 :: FilePath -> IO ()
  t06 rf = runSMTWith z3{verbose=True, redirectVerbose = Just rf} $ do
               a :: SADT <- free "a"
               constrain $ isAMaybe a
               constrain $ isJust (getAMaybe_1 a)
               query $ do cs <- checkSat
                          case cs of
                           Sat{} -> do v <- getValue a
                                       io $ do appendFile rf $ "\ngetValue: " ++ show v
                                               appendFile rf   "\nDONE\n"
                           _     -> error ("BAD RESULT: " ++ show cs)
  