{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Shared oracle helpers for the @circuits-axioma*@ executables.
--
-- This library holds generic test machinery that is useful across multiple
-- executables: assertion printers, finite enumeration, and truth-table
-- helpers.  Nothing here depends on @circuits@.
module Circuit.Tools.Test
  ( -- * Assertions
    check,
    approx,

    -- * Finite enumeration
    enumFunctions,
    enumCartesian,
    allBoolFns,
    pairBoolFns,
    pairDoubleFns,
  )
where

import Control.Monad (replicateM)
import Data.Kind (Type)
import Data.Maybe (fromMaybe)
import Data.Proxy (Proxy (..))
import GHC.TypeNats (KnownNat, natVal)
import Prelude hiding (curry, id, uncurry, (.))

-- | Print PASS/FAIL for a named boolean assertion and return the result.
check :: String -> Bool -> IO Bool
check :: String -> Bool -> IO Bool
check String
name Bool
ok = do
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ (if Bool
ok then String
"PASS " else String
"FAIL ") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
  Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
ok

-- | Approximate equality for floating-point oracles.
approx :: Double -> Double -> Bool
approx :: Double -> Double -> Bool
approx Double
x Double
y = Double -> Double
forall a. Num a => a -> a
abs (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
y) Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
1e-9

-- | Enumerate all functions from a finite domain to a finite codomain.
enumFunctions :: (Eq a) => [a] -> [b] -> [a -> b]
enumFunctions :: forall a b. Eq a => [a] -> [b] -> [a -> b]
enumFunctions [] [b]
_ = [b -> a -> b
forall a b. a -> b -> a
const (String -> b
forall a. HasCallStack => String -> a
error String
"enumFunctions: empty domain")]
enumFunctions [a]
domain [b]
codomain = ([b] -> a -> b) -> [[b]] -> [a -> b]
forall a b. (a -> b) -> [a] -> [b]
map ([a] -> [b] -> a -> b
forall {a} {a}. Eq a => [a] -> [a] -> a -> a
listToFunction [a]
domain) (Int -> [b] -> [[b]]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
domain) [b]
codomain)
  where
    listToFunction :: [a] -> [a] -> a -> a
listToFunction [a]
dom [a]
vals a
x = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error String
"listToFunction: input not in domain") (a -> [(a, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
x ([a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
dom [a]
vals))

-- | Cartesian product of two lists.
enumCartesian :: [a] -> [b] -> [(a, b)]
enumCartesian :: forall a b. [a] -> [b] -> [(a, b)]
enumCartesian [a]
xs [b]
ys = [(a
x, b
y) | a
x <- [a]
xs, b
y <- [b]
ys]

-- | All functions from a finite bounded enumerable type to 'Bool'.
allBoolFns :: forall a. (Bounded a, Enum a) => [a -> Bool]
allBoolFns :: forall a. (Bounded a, Enum a) => [a -> Bool]
allBoolFns = ([Bool] -> a -> Bool) -> [[Bool]] -> [a -> Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\[Bool]
bits a
a -> [Bool]
bits [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! a -> Int
forall a. Enum a => a -> Int
fromEnum a
a) (Int -> [Bool] -> [[Bool]]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (a -> Int
forall a. Enum a => a -> Int
fromEnum (a
forall a. Bounded a => a
maxBound :: a) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Bool
False, Bool
True])

-- | All functions from a pair of finite bounded enumerable values to 'Bool'.
--
-- Pairs do not have an 'Enum' instance in current GHC, so we enumerate the
-- underlying values explicitly and index into the truth table.
pairBoolFns :: forall b. (Enum b) => [b] -> [(b, b) -> Bool]
pairBoolFns :: forall b. Enum b => [b] -> [(b, b) -> Bool]
pairBoolFns [b]
bs = ([Bool] -> (b, b) -> Bool) -> [[Bool]] -> [(b, b) -> Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\[Bool]
bits (b
b1, b
b2) -> [Bool]
bits [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! (b -> Int
forall a. Enum a => a -> Int
fromEnum b
b1 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ b -> Int
forall a. Enum a => a -> Int
fromEnum b
b2)) (Int -> [Bool] -> [[Bool]]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) [Bool
False, Bool
True])
  where
    n :: Int
n = [b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
bs

-- | Boolean-valued pair functions rendered as {0,1}-valued 'Double' functions.
pairDoubleFns :: (Enum b) => [b] -> [(b, b) -> Double]
pairDoubleFns :: forall b. Enum b => [b] -> [(b, b) -> Double]
pairDoubleFns [b]
bs = (((b, b) -> Bool) -> (b, b) -> Double)
-> [(b, b) -> Bool] -> [(b, b) -> Double]
forall a b. (a -> b) -> [a] -> [b]
map (\(b, b) -> Bool
k (b, b)
p -> if (b, b) -> Bool
k (b, b)
p then Double
1 else Double
0) ([b] -> [(b, b) -> Bool]
forall b. Enum b => [b] -> [(b, b) -> Bool]
pairBoolFns [b]
bs)