{-# 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