{-# LANGUAGE UndecidableInstances #-}
module Utils where

import Data.ByteString.Builder qualified as BS
import Control.Monad (Monad(..))
import Data.Either (fromRight)
import Data.Function ((&), (.))
import Data.Functor ((<&>))
import Data.List qualified as List
import Data.Ord (Ord)
import Data.String (String)
import Data.Text qualified as Text
import Logic
import Logic.Theory.Arithmetic
import Logic.Theory.Ord
import Prelude (undefined)
import System.FilePath (joinPath, pathSeparator, (<.>), (</>))
import Test.Syd
import Text.Show (Show (..))
import System.FilePath qualified as Sys

assertStrictlyPositive :: Ord a => Zeroable a => a -> () ::: a / () > Zero
assertStrictlyPositive i = unitName i / fromRight undefined (prove (unitName i > zero))

goldenPath ::
  Sys.FilePath ->
  TestDefM outers inner Sys.FilePath
goldenPath msg = do
  descrPath <- getTestDescriptionPath
  let dirPath =
        List.reverse descrPath
          <&> Text.unpack . Text.replace (Text.pack ".") (Text.singleton pathSeparator)
          & joinPath
  return ("tests" </> dirPath </> msg <.> "golden")

goldenShow :: Show a => String -> a -> TestDefM outers () ()
goldenShow msg a = do
  path <- goldenPath msg
  it msg do
    goldenPrettyShowInstance path a

goldenBuilder :: String -> BS.Builder -> TestDefM outers () ()
goldenBuilder msg a = do
  path <- goldenPath msg
  it msg do
    pureGoldenByteStringBuilderFile path a

pattern (:=) :: a -> b -> (a, b)
pattern (:=) x y = (x, y)
infixr 0 :=