tests/Utils.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 module Utils where
   3
   4 import Data.ByteString.Builder qualified as BS
   5 import Control.Monad (Monad(..))
   6 import Data.Either (fromRight)
   7 import Data.Function ((&), (.))
   8 import Data.Functor ((<&>))
   9 import Data.List qualified as List
  10 import Data.Ord (Ord)
  11 import Data.String (String)
  12 import Data.Text qualified as Text
  13 import Logic
  14 import Logic.Theory.Arithmetic
  15 import Logic.Theory.Ord
  16 import Prelude (undefined)
  17 import System.FilePath (joinPath, pathSeparator, (<.>), (</>))
  18 import Test.Syd
  19 import Text.Show (Show (..))
  20 import System.FilePath qualified as Sys
  21
  22 assertStrictlyPositive :: Ord a => Zeroable a => a -> () ::: a / () > Zero
  23 assertStrictlyPositive i = unitName i / fromRight undefined (prove (unitName i > zero))
  24
  25 goldenPath ::
  26   Sys.FilePath ->
  27   TestDefM outers inner Sys.FilePath
  28 goldenPath msg = do
  29   descrPath <- getTestDescriptionPath
  30   let dirPath =
  31         List.reverse descrPath
  32           <&> Text.unpack . Text.replace (Text.pack ".") (Text.singleton pathSeparator)
  33           & joinPath
  34   return ("tests" </> dirPath </> msg <.> "golden")
  35
  36 goldenShow :: Show a => String -> a -> TestDefM outers () ()
  37 goldenShow msg a = do
  38   path <- goldenPath msg
  39   it msg do
  40     goldenPrettyShowInstance path a
  41
  42 goldenBuilder :: String -> BS.Builder -> TestDefM outers () ()
  43 goldenBuilder msg a = do
  44   path <- goldenPath msg
  45   it msg do
  46     pureGoldenByteStringBuilderFile path a
  47
  48 pattern (:=) :: a -> b -> (a, b)
  49 pattern (:=) x y = (x, y)
  50 infixr 0 :=