{-# LANGUAGE DataKinds #-}
module ReWire.FiniteComp where

import ReWire
import ReWire.Finite
import qualified ReWire.Bits as B


--
-- Operations on Finites are actually operations on words
--

{-# INLINE (+) #-}
(+) :: KnownNat n => Finite n -> Finite n -> Finite n
Finite n
a + :: forall (n :: Nat). KnownNat n => Finite n -> Finite n -> Finite n
+ Finite n
b = W 128 -> Finite n
forall (n :: Nat) (m :: Nat). KnownNat n => W m -> Finite n
toFinite' (W 128 -> Finite n) -> W 128 -> Finite n
forall a b. (a -> b) -> a -> b
$ (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> W 128
forall (n :: Nat). KnownNat n => W n -> W n -> W n
B.+ Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b

{-# INLINE (-) #-}
(-) :: KnownNat n => Finite n -> Finite n -> Finite n
Finite n
a - :: forall (n :: Nat). KnownNat n => Finite n -> Finite n -> Finite n
- Finite n
b = W 128 -> Finite n
forall (n :: Nat) (m :: Nat). KnownNat n => W m -> Finite n
toFinite' (W 128 -> Finite n) -> W 128 -> Finite n
forall a b. (a -> b) -> a -> b
$ (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> W 128
forall (n :: Nat). KnownNat n => W n -> W n -> W n
B.- Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b

{-# INLINE (*) #-}
(*) :: KnownNat n => Finite n -> Finite n -> Finite n
Finite n
a * :: forall (n :: Nat). KnownNat n => Finite n -> Finite n -> Finite n
* Finite n
b = W 128 -> Finite n
forall (n :: Nat) (m :: Nat). KnownNat n => W m -> Finite n
toFinite' (W 128 -> Finite n) -> W 128 -> Finite n
forall a b. (a -> b) -> a -> b
$ (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> W 128
forall (n :: Nat). KnownNat n => W n -> W n -> W n
B.* Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b

{-# INLINE div #-}
div :: KnownNat n => Finite n -> Finite n -> Finite n
div :: forall (n :: Nat). KnownNat n => Finite n -> Finite n -> Finite n
div Finite n
a Finite n
b = W 128 -> Finite n
forall (n :: Nat) (m :: Nat). KnownNat n => W m -> Finite n
toFinite' (W 128 -> Finite n) -> W 128 -> Finite n
forall a b. (a -> b) -> a -> b
$ (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> W 128
forall (n :: Nat). KnownNat n => W n -> W n -> W n
B./ Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b

{-# INLINE mod #-}
mod :: KnownNat n => Finite n -> Finite n -> Finite n
mod :: forall (n :: Nat). KnownNat n => Finite n -> Finite n -> Finite n
mod Finite n
a Finite n
b = W 128 -> Finite n
forall (n :: Nat) (m :: Nat). KnownNat n => W m -> Finite n
toFinite' (W 128 -> Finite n) -> W 128 -> Finite n
forall a b. (a -> b) -> a -> b
$ (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> W 128
forall (n :: Nat). KnownNat n => W n -> W n -> W n
B.% Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b

{-# INLINE (==) #-}
(==) :: Finite n -> Finite n -> Bool
Finite n
a == :: forall (n :: Nat). Finite n -> Finite n -> Bool
== Finite n
b = (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> Bool
forall (n :: Nat). W n -> W n -> Bool
B.== (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b :: B.Lit)

{-# INLINE (<) #-}
(<) :: Finite n -> Finite n -> Bool
Finite n
a < :: forall (n :: Nat). Finite n -> Finite n -> Bool
< Finite n
b = (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> Bool
forall (n :: Nat). W n -> W n -> Bool
B.< (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b :: B.Lit)

{-# INLINE (<=) #-}
(<=) :: Finite n -> Finite n -> Bool
Finite n
a <= :: forall (n :: Nat). Finite n -> Finite n -> Bool
<= Finite n
b = (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> Bool
forall (n :: Nat). W n -> W n -> Bool
B.<= (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b :: B.Lit)

{-# INLINE (>) #-}
(>) :: Finite n -> Finite n -> Bool
Finite n
a > :: forall (n :: Nat). Finite n -> Finite n -> Bool
> Finite n
b = (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> Bool
forall (n :: Nat). W n -> W n -> Bool
B.> (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b :: B.Lit)

{-# INLINE (>=) #-}
(>=) :: Finite n -> Finite n -> Bool
Finite n
a >= :: forall (n :: Nat). Finite n -> Finite n -> Bool
>= Finite n
b = (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit) W 128 -> W 128 -> Bool
forall (n :: Nat). W n -> W n -> Bool
B.>= (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
b :: B.Lit)

{-# INLINE even #-}
even :: Finite n -> Bool
even :: forall (n :: Nat). Finite n -> Bool
even Finite n
a = W (1 + 127) -> Bool
forall (n :: Nat). W (1 + n) -> Bool
B.even (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit)

{-# INLINE odd #-}
odd :: Finite n -> Bool
odd :: forall (n :: Nat). Finite n -> Bool
odd Finite n
a = W (1 + 127) -> Bool
forall (n :: Nat). W (1 + n) -> Bool
B.odd (Finite n -> W 128
forall (m :: Nat) (n :: Nat). KnownNat m => Finite n -> W m
fromFinite Finite n
a :: B.Lit)