content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE MultiWayIf #-}
  {-# LANGUAGE LambdaCase #-}
  
  module SerializeTestUtils where
  
  import           Control.Monad ( when )
  import           Control.Monad.IO.Class ( MonadIO, liftIO )
  import           Hedgehog
  import           System.Directory
  import qualified What4.Expr.Builder as S
  import qualified What4.Interface as WI
  import qualified What4.Serialize.Normalize as WN
  
  import           Prelude
  
  
  debugFile :: FilePath
  debugFile = "what4serialize.log"
  
  debugReset :: IO ()
  debugReset = do e <- doesFileExist debugFile
                  when e $ removeFile debugFile
  
  debugOut, alwaysPrint :: MonadIO m => String -> m ()
  debugOut msg = liftIO $ do appendFile debugFile (msg <> "\n")
                             -- alwaysPrint  -- comment this out to disable printing
                             return ()
  alwaysPrint = liftIO . putStrLn
  
  
  showSymFn :: S.ExprSymFn t args ret -> String
  showSymFn fn = case S.symFnInfo fn of
    S.DefinedFnInfo _ expr _ -> (show $ WI.printSymExpr expr)
    _ -> ""
  
  symFnEqualityTest :: ( MonadIO m
                       , MonadTest m
                       , sym ~ S.ExprBuilder t st flgs
                       ) =>
                       sym
                    -> WI.SymFn sym args ret
                    -> WI.SymFn sym arts' ret'
                    -> m ()
  symFnEqualityTest sym fn1 fn2 = do
    (liftIO $ WN.testEquivSymFn sym fn1 fn2) >>= \case
      WN.ExprEquivalent -> success
      WN.ExprNormEquivalent -> success
      WN.ExprUnequal -> do
        debugOut $ "Resulting functions do not match:\n"
          ++ "fn1:\n" ++ (showSymFn fn1) ++ "\n"
          ++ "fn2:\n" ++ (showSymFn fn2)
        failure
  