{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Algebra.TestUtils
  ( liftSNat,
    checkForTypeNat,
    module Algebra.Ring.Polynomial.Test,
    module Algebra.Ring.Polynomial.Monomial.Test,
    module Algebra.Field.Fraction.Test,
    module Algebra.Field.Finite.Test,
  )
where

import Algebra.Field.Finite.Test
import Algebra.Field.Fraction.Test
import Algebra.Field.Prime.Test ()
import Algebra.Internal
import Algebra.Ring.Ideal.Test ()
import Algebra.Ring.Polynomial.Monomial.Test
import Algebra.Ring.Polynomial.Test
import Numeric.Natural (Natural)
import Test.QuickCheck (Property, forAll)
import qualified Test.QuickCheck as QC
import Test.QuickCheck.Instances ()
import Prelude (($))

liftSNat :: (forall n. KnownNat (n :: Nat) => SNat n -> Property) -> Natural -> Property
liftSNat :: (forall (n :: Nat). KnownNat n => SNat n -> Property)
-> Natural -> Property
liftSNat forall (n :: Nat). KnownNat n => SNat n -> Property
f Natural
i =
  case Natural -> SomeSNat
toSomeSNat Natural
i of
    SomeSNat SNat n
sn -> SNat n -> (KnownNat n => Property) -> Property
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn ((KnownNat n => Property) -> Property)
-> (KnownNat n => Property) -> Property
forall a b. (a -> b) -> a -> b
$ SNat n -> Property
forall (n :: Nat). KnownNat n => SNat n -> Property
f SNat n
sn

checkForTypeNat :: [Natural] -> (forall n. KnownNat (n :: Nat) => SNat n -> Property) -> Property
checkForTypeNat :: [Natural]
-> (forall (n :: Nat). KnownNat n => SNat n -> Property)
-> Property
checkForTypeNat [Natural]
as forall (n :: Nat). KnownNat n => SNat n -> Property
test = Gen Natural -> (Natural -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([Natural] -> Gen Natural
forall a. [a] -> Gen a
QC.elements [Natural]
as) ((Natural -> Property) -> Property)
-> (Natural -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ (forall (n :: Nat). KnownNat n => SNat n -> Property)
-> Natural -> Property
liftSNat forall (n :: Nat). KnownNat n => SNat n -> Property
test