{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-}

module Algebra.Ring.Polynomial.Monomial.Test
  ( arbitraryMonomialOfSum,
    arbitraryMonomial,
  )
where

import Algebra.Internal
import Algebra.Ring.Polynomial.Monomial
  ( Monomial,
    OrderedMonomial (..),
  )
import qualified Data.Sized as SV
import Data.Type.Equality (gcastWith)
import Data.Type.Natural.Lemma.Arithmetic (succAndPlusOneL)
import Test.QuickCheck
  ( Arbitrary,
    Gen,
    arbitrary,
    arbitrarySizedBoundedIntegral,
    vectorOf,
  )
import qualified Test.QuickCheck as QC
import Test.SmallCheck.Series
  ( Serial,
    cons0,
    newtypeCons,
    series,
  )
import qualified Test.SmallCheck.Series as SC
import Prelude

instance (KnownNat n, Monad m) => Serial m (Monomial n) where
  series :: Series m (Monomial n)
series =
    case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n) of
      ZeroOrSucc n
IsZero -> Sized Vector 0 Int -> Series m (Sized Vector 0 Int)
forall a (m :: * -> *). a -> Series m a
cons0 Sized Vector 0 Int
forall (f :: * -> *) a. (Monoid (f a), Dom f a) => Sized f 0 a
SV.empty
      IsSucc SNat n1
n ->
        (n :~: (1 + n1))
-> ((n ~ (1 + n1)) => Series m (Monomial n))
-> Series m (Monomial n)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (SNat n1 -> Succ n1 :~: (1 + n1)
forall (n :: Nat). SNat n -> Succ n :~: (1 + n)
succAndPlusOneL SNat n1
n) (((n ~ (1 + n1)) => Series m (Monomial n))
 -> Series m (Monomial n))
-> ((n ~ (1 + n1)) => Series m (Monomial n))
-> Series m (Monomial n)
forall a b. (a -> b) -> a -> b
$
          SNat n1
-> (KnownNat n1 => Series m (Monomial n)) -> Series m (Monomial n)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
n ((KnownNat n1 => Series m (Monomial n)) -> Series m (Monomial n))
-> (KnownNat n1 => Series m (Monomial n)) -> Series m (Monomial n)
forall a b. (a -> b) -> a -> b
$ Int -> Sized Vector n1 Int -> Sized Vector (1 + n1) Int
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (1 + n) a
SV.cons (Int -> Sized Vector n1 Int -> Sized Vector (1 + n1) Int)
-> Series m Int
-> Series m (Sized Vector n1 Int -> Sized Vector (1 + n1) Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NonNegative Int -> Int
forall a. NonNegative a -> a
SC.getNonNegative (NonNegative Int -> Int)
-> Series m (NonNegative Int) -> Series m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Series m (NonNegative Int)
forall (m :: * -> *) a. Serial m a => Series m a
series) Series m (Sized Vector n1 Int -> Sized Vector (1 + n1) Int)
-> Series m (Sized Vector n1 Int)
-> Series m (Sized Vector (1 + n1) Int)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Series m (Sized Vector n1 Int)
forall (m :: * -> *) a. Serial m a => Series m a
series

instance (Monad m, Serial m (Monomial n)) => Serial m (OrderedMonomial ord n) where
  series :: Series m (OrderedMonomial ord n)
series = (Monomial n -> OrderedMonomial ord n)
-> Series m (OrderedMonomial ord n)
forall (m :: * -> *) a b. Serial m a => (a -> b) -> Series m b
newtypeCons Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial

arbitraryMonomialOfSum :: SNat n -> Int -> Gen (Monomial n)
arbitraryMonomialOfSum :: SNat n -> Int -> Gen (Monomial n)
arbitraryMonomialOfSum SNat n
n Int
k = SNat n -> (KnownNat n => Gen (Monomial n)) -> Gen (Monomial n)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => Gen (Monomial n)) -> Gen (Monomial n))
-> (KnownNat n => Gen (Monomial n)) -> Gen (Monomial n)
forall a b. (a -> b) -> a -> b
$
  case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc SNat n
n of
    ZeroOrSucc n
IsZero
      | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> [Sized Vector 0 Int] -> Gen (Sized Vector 0 Int)
forall a. [a] -> Gen a
QC.elements [Sized Vector 0 Int
forall (f :: * -> *) a. (Monoid (f a), Dom f a) => Sized f 0 a
SV.empty]
      | Bool
otherwise -> [Char] -> Gen (Monomial n)
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"
    IsSucc SNat n1
m -> SNat n1 -> (KnownNat n1 => Gen (Monomial n)) -> Gen (Monomial n)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
m ((KnownNat n1 => Gen (Monomial n)) -> Gen (Monomial n))
-> (KnownNat n1 => Gen (Monomial n)) -> Gen (Monomial n)
forall a b. (a -> b) -> a -> b
$ do
      Int
l <- [Int] -> Gen Int
forall a. [a] -> Gen a
QC.elements [Int
0 .. Int -> Int
forall a. Num a => a -> a
abs Int
k]
      (Int
l Int -> Sized Vector n1 Int -> Monomial n
forall (f :: * -> *) a (n :: Nat) (n1 :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, n ~ (1 + n1), KnownNat n1) =>
a -> Sized f n1 a -> Sized f n a
:<) (Sized Vector n1 Int -> Monomial n)
-> Gen (Sized Vector n1 Int) -> Gen (Monomial n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SNat n1 -> Int -> Gen (Sized Vector n1 Int)
forall (n :: Nat). SNat n -> Int -> Gen (Monomial n)
arbitraryMonomialOfSum SNat n1
m (Int -> Int
forall a. Num a => a -> a
abs Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
l)

-- * Instances for QuickCheck.

instance KnownNat n => Arbitrary (Monomial n) where
  arbitrary :: Gen (Monomial n)
arbitrary = Gen (Monomial n)
forall (n :: Nat). KnownNat n => Gen (Monomial n)
arbitraryMonomial

arbitraryMonomial :: forall n. KnownNat n => Gen (Monomial n)
arbitraryMonomial :: Gen (Monomial n)
arbitraryMonomial =
  SNat n -> [Int] -> Monomial n
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Sized f n a
SV.unsafeFromList SNat n
len ([Int] -> Monomial n) -> ([Int] -> [Int]) -> [Int] -> Monomial n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
forall a. Num a => a -> a
abs
    ([Int] -> Monomial n) -> Gen [Int] -> Gen (Monomial n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen Int -> Gen [Int]
forall a. Int -> Gen a -> Gen [a]
vectorOf (SNat n -> Int
forall (n :: Nat). SNat n -> Int
sNatToInt SNat n
len) Gen Int
forall a. (Bounded a, Integral a) => Gen a
arbitrarySizedBoundedIntegral
  where
    len :: SNat n
len = SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n

instance (KnownNat n) => Arbitrary (OrderedMonomial ord n) where
  arbitrary :: Gen (OrderedMonomial ord n)
arbitrary = Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial n -> OrderedMonomial ord n)
-> Gen (Monomial n) -> Gen (OrderedMonomial ord n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Monomial n)
forall a. Arbitrary a => Gen a
arbitrary