{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.Ord
  ( IsOrdering (..)
  , Ordering
  , Ord (..)
  , GOrd (..)
  ) where

import           Control.DeepSeq                  (NFData)
import           Data.Foldable                    (fold, toList)
import           Data.Function                    (on)
import           Data.List                        (concatMap, reverse, zipWith)
import           Data.Traversable                 (traverse)
import           GHC.Generics
import           Prelude                          (Monoid, Semigroup, Show, fmap, map, type (~), ($), (.), (<$>), (<>))
import qualified Prelude

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.Package
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Combinators (expansion)
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.Eq
import           ZkFold.Symbolic.MonadCircuit     (newAssigned)

class Monoid ordering => IsOrdering ordering where
  lt, eq, gt :: ordering

instance IsOrdering Prelude.Ordering where
  lt :: Ordering
lt = Ordering
Prelude.LT
  eq :: Ordering
eq = Ordering
Prelude.EQ
  gt :: Ordering
gt = Ordering
Prelude.GT

class
  ( Eq a
  , IsOrdering (OrderingOf a)
  ) => Ord a where

  type OrderingOf a
  type OrderingOf a = GOrderingOf (Rep a)

  ordering :: a -> a -> a -> OrderingOf a -> a
  default ordering
    :: (Generic a, GOrd (Rep a), OrderingOf a ~ GOrderingOf (Rep a))
    => a -> a -> a -> OrderingOf a -> a
  ordering a
ltCase a
eqCase a
gtCase OrderingOf a
o =
    Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any
-> Rep a Any -> Rep a Any -> GOrderingOf (Rep a) -> Rep a Any
forall x.
Rep a x -> Rep a x -> Rep a x -> GOrderingOf (Rep a) -> Rep a x
forall {k} (u :: k -> Type) (x :: k).
GOrd u =>
u x -> u x -> u x -> GOrderingOf u -> u x
gordering (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
ltCase) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
eqCase) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
gtCase) GOrderingOf (Rep a)
OrderingOf a
o)

  compare :: a -> a -> OrderingOf a
  default compare
    :: (Generic a, GOrd (Rep a), OrderingOf a ~ GOrderingOf (Rep a))
    => a -> a -> OrderingOf a
  compare a
x a
y = Rep a Any -> Rep a Any -> GOrderingOf (Rep a)
forall x. Rep a x -> Rep a x -> GOrderingOf (Rep a)
forall {k} (u :: k -> Type) (x :: k).
GOrd u =>
u x -> u x -> GOrderingOf u
gcompare (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
y)

  (<), (<=), (>), (>=) :: a -> a -> BooleanOf a
  infix 4 <
  infix 4 <=
  infix 4 >
  infix 4 >=
  default (<)
    :: (Ord (BooleanOf a), OrderingOf (BooleanOf a) ~ OrderingOf a)
    => a -> a -> BooleanOf a
  a
x < a
y = BooleanOf a
-> BooleanOf a
-> BooleanOf a
-> OrderingOf (BooleanOf a)
-> BooleanOf a
forall a. Ord a => a -> a -> a -> OrderingOf a -> a
ordering BooleanOf a
forall b. BoolType b => b
true BooleanOf a
forall b. BoolType b => b
false BooleanOf a
forall b. BoolType b => b
false (a -> a -> OrderingOf a
forall a. Ord a => a -> a -> OrderingOf a
compare a
x a
y)
  default (<=)
    :: (Ord (BooleanOf a), OrderingOf (BooleanOf a) ~ OrderingOf a)
    => a -> a -> BooleanOf a
  a
x <= a
y = BooleanOf a
-> BooleanOf a
-> BooleanOf a
-> OrderingOf (BooleanOf a)
-> BooleanOf a
forall a. Ord a => a -> a -> a -> OrderingOf a -> a
ordering BooleanOf a
forall b. BoolType b => b
true BooleanOf a
forall b. BoolType b => b
true BooleanOf a
forall b. BoolType b => b
false (a -> a -> OrderingOf a
forall a. Ord a => a -> a -> OrderingOf a
compare a
x a
y)
  default (>)
    :: (Ord (BooleanOf a), OrderingOf (BooleanOf a) ~ OrderingOf a)
    => a -> a -> BooleanOf a
  a
x > a
y = BooleanOf a
-> BooleanOf a
-> BooleanOf a
-> OrderingOf (BooleanOf a)
-> BooleanOf a
forall a. Ord a => a -> a -> a -> OrderingOf a -> a
ordering BooleanOf a
forall b. BoolType b => b
false BooleanOf a
forall b. BoolType b => b
false BooleanOf a
forall b. BoolType b => b
true (a -> a -> OrderingOf a
forall a. Ord a => a -> a -> OrderingOf a
compare a
x a
y)
  default (>=)
    :: (Ord (BooleanOf a), OrderingOf (BooleanOf a) ~ OrderingOf a)
    => a -> a -> BooleanOf a
  a
x >= a
y = BooleanOf a
-> BooleanOf a
-> BooleanOf a
-> OrderingOf (BooleanOf a)
-> BooleanOf a
forall a. Ord a => a -> a -> a -> OrderingOf a -> a
ordering BooleanOf a
forall b. BoolType b => b
false BooleanOf a
forall b. BoolType b => b
true BooleanOf a
forall b. BoolType b => b
true (a -> a -> OrderingOf a
forall a. Ord a => a -> a -> OrderingOf a
compare a
x a
y)
  max, min :: a -> a -> a
  max a
x a
y = a -> a -> a -> OrderingOf a -> a
forall a. Ord a => a -> a -> a -> OrderingOf a -> a
ordering a
y a
x a
x (a -> a -> OrderingOf a
forall a. Ord a => a -> a -> OrderingOf a
compare a
x a
y)
  min a
x a
y = a -> a -> a -> OrderingOf a -> a
forall a. Ord a => a -> a -> a -> OrderingOf a -> a
ordering a
x a
x a
y (a -> a -> OrderingOf a
forall a. Ord a => a -> a -> OrderingOf a
compare a
x a
y)

instance Ord Natural where
  type OrderingOf Natural = Prelude.Ordering
  ordering :: Natural -> Natural -> Natural -> OrderingOf Natural -> Natural
ordering Natural
x Natural
y Natural
z = \case
    Ordering
OrderingOf Natural
Prelude.LT -> Natural
x; Ordering
OrderingOf Natural
Prelude.EQ -> Natural
y; Ordering
OrderingOf Natural
Prelude.GT -> Natural
z
  compare :: Natural -> Natural -> OrderingOf Natural
compare = Natural -> Natural -> Ordering
Natural -> Natural -> OrderingOf Natural
forall a. Ord a => a -> a -> Ordering
Prelude.compare
  > :: Natural -> Natural -> BooleanOf Natural
(>) = Natural -> Natural -> Bool
Natural -> Natural -> BooleanOf Natural
forall a. Ord a => a -> a -> Bool
(Prelude.>)
  >= :: Natural -> Natural -> BooleanOf Natural
(>=) = Natural -> Natural -> Bool
Natural -> Natural -> BooleanOf Natural
forall a. Ord a => a -> a -> Bool
(Prelude.>=)
  < :: Natural -> Natural -> BooleanOf Natural
(<) = Natural -> Natural -> Bool
Natural -> Natural -> BooleanOf Natural
forall a. Ord a => a -> a -> Bool
(Prelude.<)
  <= :: Natural -> Natural -> BooleanOf Natural
(<=) = Natural -> Natural -> Bool
Natural -> Natural -> BooleanOf Natural
forall a. Ord a => a -> a -> Bool
(Prelude.<=)
  min :: Natural -> Natural -> Natural
min = Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
Prelude.min
  max :: Natural -> Natural -> Natural
max = Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
Prelude.max
instance Ord Prelude.Bool where
  type OrderingOf Prelude.Bool = Prelude.Ordering
  ordering :: Bool -> Bool -> Bool -> OrderingOf Bool -> Bool
ordering Bool
x Bool
y Bool
z = \case
    Ordering
OrderingOf Bool
Prelude.LT -> Bool
x; Ordering
OrderingOf Bool
Prelude.EQ -> Bool
y; Ordering
OrderingOf Bool
Prelude.GT -> Bool
z
  compare :: Bool -> Bool -> OrderingOf Bool
compare = Bool -> Bool -> Ordering
Bool -> Bool -> OrderingOf Bool
forall a. Ord a => a -> a -> Ordering
Prelude.compare
  > :: Bool -> Bool -> BooleanOf Bool
(>) = Bool -> Bool -> Bool
Bool -> Bool -> BooleanOf Bool
forall a. Ord a => a -> a -> Bool
(Prelude.>)
  >= :: Bool -> Bool -> BooleanOf Bool
(>=) = Bool -> Bool -> Bool
Bool -> Bool -> BooleanOf Bool
forall a. Ord a => a -> a -> Bool
(Prelude.>=)
  < :: Bool -> Bool -> BooleanOf Bool
(<) = Bool -> Bool -> Bool
Bool -> Bool -> BooleanOf Bool
forall a. Ord a => a -> a -> Bool
(Prelude.<)
  <= :: Bool -> Bool -> BooleanOf Bool
(<=) = Bool -> Bool -> Bool
Bool -> Bool -> BooleanOf Bool
forall a. Ord a => a -> a -> Bool
(Prelude.<=)
  min :: Bool -> Bool -> Bool
min = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
Prelude.min
  max :: Bool -> Bool -> Bool
max = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
Prelude.max
instance Ord Prelude.String where
  type OrderingOf Prelude.String = Prelude.Ordering
  ordering :: String -> String -> String -> OrderingOf String -> String
ordering String
x String
y String
z = \case
    Ordering
OrderingOf String
Prelude.LT -> String
x; Ordering
OrderingOf String
Prelude.EQ -> String
y; Ordering
OrderingOf String
Prelude.GT -> String
z
  compare :: String -> String -> OrderingOf String
compare = String -> String -> Ordering
String -> String -> OrderingOf String
forall a. Ord a => a -> a -> Ordering
Prelude.compare
  > :: String -> String -> BooleanOf String
(>) = String -> String -> Bool
String -> String -> BooleanOf String
forall a. Ord a => a -> a -> Bool
(Prelude.>)
  >= :: String -> String -> BooleanOf String
(>=) = String -> String -> Bool
String -> String -> BooleanOf String
forall a. Ord a => a -> a -> Bool
(Prelude.>=)
  < :: String -> String -> BooleanOf String
(<) = String -> String -> Bool
String -> String -> BooleanOf String
forall a. Ord a => a -> a -> Bool
(Prelude.<)
  <= :: String -> String -> BooleanOf String
(<=) = String -> String -> Bool
String -> String -> BooleanOf String
forall a. Ord a => a -> a -> Bool
(Prelude.<=)
  min :: String -> String -> String
min = String -> String -> String
forall a. Ord a => a -> a -> a
Prelude.min
  max :: String -> String -> String
max = String -> String -> String
forall a. Ord a => a -> a -> a
Prelude.max
instance KnownNat n => Ord (Zp n) where
  type OrderingOf (Zp n) = Prelude.Ordering
  ordering :: Zp n -> Zp n -> Zp n -> OrderingOf (Zp n) -> Zp n
ordering Zp n
x Zp n
y Zp n
z = \case
    Ordering
OrderingOf (Zp n)
Prelude.LT -> Zp n
x; Ordering
OrderingOf (Zp n)
Prelude.EQ -> Zp n
y; Ordering
OrderingOf (Zp n)
Prelude.GT -> Zp n
z
  compare :: Zp n -> Zp n -> OrderingOf (Zp n)
compare = Zp n -> Zp n -> Ordering
Zp n -> Zp n -> OrderingOf (Zp n)
forall a. Ord a => a -> a -> Ordering
Prelude.compare
  > :: Zp n -> Zp n -> BooleanOf (Zp n)
(>) = Zp n -> Zp n -> Bool
Zp n -> Zp n -> BooleanOf (Zp n)
forall a. Ord a => a -> a -> Bool
(Prelude.>)
  >= :: Zp n -> Zp n -> BooleanOf (Zp n)
(>=) = Zp n -> Zp n -> Bool
Zp n -> Zp n -> BooleanOf (Zp n)
forall a. Ord a => a -> a -> Bool
(Prelude.>=)
  < :: Zp n -> Zp n -> BooleanOf (Zp n)
(<) = Zp n -> Zp n -> Bool
Zp n -> Zp n -> BooleanOf (Zp n)
forall a. Ord a => a -> a -> Bool
(Prelude.<)
  <= :: Zp n -> Zp n -> BooleanOf (Zp n)
(<=) = Zp n -> Zp n -> Bool
Zp n -> Zp n -> BooleanOf (Zp n)
forall a. Ord a => a -> a -> Bool
(Prelude.<=)
  min :: Zp n -> Zp n -> Zp n
min = Zp n -> Zp n -> Zp n
forall a. Ord a => a -> a -> a
Prelude.min
  max :: Zp n -> Zp n -> Zp n
max = Zp n -> Zp n -> Zp n
forall a. Ord a => a -> a -> a
Prelude.max

newtype Ordering c = Ordering (c Par1)
  deriving ((forall x. Ordering c -> Rep (Ordering c) x)
-> (forall x. Rep (Ordering c) x -> Ordering c)
-> Generic (Ordering c)
forall x. Rep (Ordering c) x -> Ordering c
forall x. Ordering c -> Rep (Ordering c) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (c :: (Type -> Type) -> Type) x.
Rep (Ordering c) x -> Ordering c
forall (c :: (Type -> Type) -> Type) x.
Ordering c -> Rep (Ordering c) x
$cfrom :: forall (c :: (Type -> Type) -> Type) x.
Ordering c -> Rep (Ordering c) x
from :: forall x. Ordering c -> Rep (Ordering c) x
$cto :: forall (c :: (Type -> Type) -> Type) x.
Rep (Ordering c) x -> Ordering c
to :: forall x. Rep (Ordering c) x -> Ordering c
Generic)
deriving instance NFData (c Par1) => NFData (Ordering c)
deriving instance Show (c Par1) => Show (Ordering c)
deriving newtype instance Symbolic c => Conditional (Bool c) (Ordering c)
deriving newtype instance Symbolic c => Eq (Ordering c)
instance Symbolic c => SymbolicData (Ordering c)
instance Symbolic c => Semigroup (Ordering c) where
  Ordering c Par1
o1 <> :: Ordering c -> Ordering c -> Ordering c
<> Ordering c Par1
o2 = c Par1 -> Ordering c
forall (c :: (Type -> Type) -> Type). c Par1 -> Ordering c
Ordering (c Par1 -> Ordering c) -> c Par1 -> Ordering c
forall a b. (a -> b) -> a -> b
$ c Par1
-> c Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f -> c g -> CircuitFun '[f, g] h c -> c h
fromCircuit2F c Par1
o1 c Par1
o2 ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1, Par1] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$
    \(Par1 i
v1) (Par1 i
v2) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
      ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
x -> let x1 :: x
x1 = i -> x
x i
v1; x2 :: x
x2 = i -> x
x i
v2 in x
x1 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* x
x1 x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (x
x1 x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
x2) x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
x2)
instance Symbolic c => Monoid (Ordering c) where
  mempty :: Ordering c
mempty = Ordering c
forall ordering. IsOrdering ordering => ordering
eq
instance Symbolic c => IsOrdering (Ordering c) where
  lt :: Ordering c
lt = c Par1 -> Ordering c
forall (c :: (Type -> Type) -> Type). c Par1 -> Ordering c
Ordering (c Par1 -> Ordering c) -> c Par1 -> Ordering c
forall a b. (a -> b) -> a -> b
$ Par1 (BaseField c) -> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 (BaseField c -> BaseField c
forall a. AdditiveGroup a => a -> a
negate BaseField c
forall a. MultiplicativeMonoid a => a
one))
  eq :: Ordering c
eq = c Par1 -> Ordering c
forall (c :: (Type -> Type) -> Type). c Par1 -> Ordering c
Ordering (c Par1 -> Ordering c) -> c Par1 -> Ordering c
forall a b. (a -> b) -> a -> b
$ Par1 (BaseField c) -> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 BaseField c
forall a. AdditiveMonoid a => a
zero)
  gt :: Ordering c
gt = c Par1 -> Ordering c
forall (c :: (Type -> Type) -> Type). c Par1 -> Ordering c
Ordering (c Par1 -> Ordering c) -> c Par1 -> Ordering c
forall a b. (a -> b) -> a -> b
$ Par1 (BaseField c) -> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (BaseField c -> Par1 (BaseField c)
forall p. p -> Par1 p
Par1 BaseField c
forall a. MultiplicativeMonoid a => a
one)

instance (Symbolic c, LayoutFunctor f) => Ord (c f) where
  type OrderingOf (c f) = Ordering c
  ordering :: c f -> c f -> c f -> OrderingOf (c f) -> c f
ordering c f
x c f
y c f
z OrderingOf (c f)
o = c f -> c f -> BooleanOf (Ordering c) -> c f
forall b a. Conditional b a => a -> a -> b -> a
bool (c f -> c f -> BooleanOf (Ordering c) -> c f
forall b a. Conditional b a => a -> a -> b -> a
bool c f
x c f
y (Ordering c
OrderingOf (c f)
o Ordering c -> Ordering c -> BooleanOf (Ordering c)
forall a. Eq a => a -> a -> BooleanOf a
== Ordering c
forall ordering. IsOrdering ordering => ordering
eq)) c f
z (Ordering c
OrderingOf (c f)
o Ordering c -> Ordering c -> BooleanOf (Ordering c)
forall a. Eq a => a -> a -> BooleanOf a
== Ordering c
forall ordering. IsOrdering ordering => ordering
gt)
  compare :: c f -> c f -> OrderingOf (c f)
compare = c [] -> c [] -> Ordering c
forall (c :: (Type -> Type) -> Type).
Symbolic c =>
c [] -> c [] -> Ordering c
bitwiseCompare (c [] -> c [] -> Ordering c)
-> (c f -> c []) -> c f -> c f -> Ordering c
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` c f -> c []
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, LayoutFunctor f) =>
c f -> c []
getBitsBE

bitwiseCompare :: forall c . Symbolic c => c [] -> c [] -> Ordering c
bitwiseCompare :: forall (c :: (Type -> Type) -> Type).
Symbolic c =>
c [] -> c [] -> Ordering c
bitwiseCompare c []
x c []
y = [Ordering c] -> Ordering c
forall m. Monoid m => [m] -> m
forall (t :: Type -> Type) m. (Foldable t, Monoid m) => t m -> m
fold (((c Par1 -> c Par1 -> Ordering c)
-> [c Par1] -> [c Par1] -> [Ordering c]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Bool c -> Bool c -> Ordering c
Bool c -> Bool c -> OrderingOf (Bool c)
forall a. Ord a => a -> a -> OrderingOf a
compare (Bool c -> Bool c -> Ordering c)
-> (c Par1 -> Bool c) -> c Par1 -> c Par1 -> Ordering c
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` c Par1 -> Bool c
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool) ([c Par1] -> [c Par1] -> [Ordering c])
-> (c [] -> [c Par1]) -> c [] -> c [] -> [Ordering c]
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` c [] -> [c Par1]
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Package c, Functor f) =>
c f -> f (c Par1)
unpacked) c []
x c []
y)

getBitsBE :: forall c f . (Symbolic c, LayoutFunctor f) => c f -> c []
-- ^ @getBitsBE x@ returns a list of circuits computing bits of @x@, eldest to
-- youngest.
getBitsBE :: forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, LayoutFunctor f) =>
c f -> c []
getBitsBE c f
x = c f
-> (f (BaseField c) -> [BaseField c])
-> CircuitFun '[f] [] c
-> c []
forall (c :: (Type -> Type) -> Type) a (f :: Type -> Type)
       (g :: Type -> Type).
(Symbolic c, BaseField c ~ a) =>
c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g
symbolicF c f
x
    ((BaseField c -> [BaseField c]) -> f (BaseField c) -> [BaseField c]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap ([BaseField c] -> [BaseField c]
forall a. [a] -> [a]
reverse ([BaseField c] -> [BaseField c])
-> (BaseField c -> [BaseField c]) -> BaseField c -> [BaseField c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> [BaseField c] -> [BaseField c]
forall a. AdditiveMonoid a => Natural -> [a] -> [a]
padBits Natural
n ([BaseField c] -> [BaseField c])
-> (BaseField c -> [BaseField c]) -> BaseField c -> [BaseField c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> BaseField c) -> [Natural] -> [BaseField c]
forall a b. (a -> b) -> [a] -> [b]
map Natural -> BaseField c
forall a b. FromConstant a b => a -> b
fromConstant ([Natural] -> [BaseField c])
-> (BaseField c -> [Natural]) -> BaseField c -> [BaseField c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> [Natural]
Natural -> Bits Natural
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion (Natural -> [Natural])
-> (BaseField c -> Natural) -> BaseField c -> [Natural]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseField c -> Natural
BaseField c -> Const (BaseField c)
forall a. ToConstant a => a -> Const a
toConstant))
    (([[i]] -> [i]) -> m [[i]] -> m [i]
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (([i] -> [i]) -> [[i]] -> [i]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap [i] -> [i]
forall a. [a] -> [a]
reverse) (m [[i]] -> m [i]) -> (f i -> m [[i]]) -> f i -> m [i]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (i -> m [i]) -> [i] -> m [[i]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Natural -> i -> m [i]
forall i a w (m :: Type -> Type).
(MonadCircuit i a w m, Arithmetic a) =>
Natural -> i -> m [i]
expansion Natural
n) ([i] -> m [[i]]) -> (f i -> [i]) -> f i -> m [[i]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f i -> [i]
forall a. f a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList)
  where n :: Natural
n = forall a. KnownNat (NumberOfBits a) => Natural
numberOfBits @(BaseField c)

instance Symbolic c => Ord (Bool c) where
  type OrderingOf (Bool c) = Ordering c
  ordering :: Bool c -> Bool c -> Bool c -> OrderingOf (Bool c) -> Bool c
ordering Bool c
x Bool c
y Bool c
z OrderingOf (Bool c)
o = Bool c -> Bool c -> BooleanOf (Ordering c) -> Bool c
forall b a. Conditional b a => a -> a -> b -> a
bool (Bool c -> Bool c -> BooleanOf (Ordering c) -> Bool c
forall b a. Conditional b a => a -> a -> b -> a
bool Bool c
x Bool c
y (Ordering c
OrderingOf (Bool c)
o Ordering c -> Ordering c -> BooleanOf (Ordering c)
forall a. Eq a => a -> a -> BooleanOf a
== Ordering c
forall ordering. IsOrdering ordering => ordering
eq)) Bool c
z (Ordering c
OrderingOf (Bool c)
o Ordering c -> Ordering c -> BooleanOf (Ordering c)
forall a. Eq a => a -> a -> BooleanOf a
== Ordering c
forall ordering. IsOrdering ordering => ordering
gt)
  compare :: Bool c -> Bool c -> OrderingOf (Bool c)
compare (Bool c Par1
b1) (Bool c Par1
b2) = c Par1 -> Ordering c
forall (c :: (Type -> Type) -> Type). c Par1 -> Ordering c
Ordering (c Par1 -> Ordering c) -> c Par1 -> Ordering c
forall a b. (a -> b) -> a -> b
$ c Par1
-> c Par1
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type).
Symbolic c =>
c f -> c g -> CircuitFun '[f, g] h c -> c h
fromCircuit2F c Par1
b1 c Par1
b2 ((forall {i} {m :: Type -> Type}.
  (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
  FunBody '[Par1, Par1] Par1 i m)
 -> c Par1)
-> (forall {i} {m :: Type -> Type}.
    (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) =>
    FunBody '[Par1, Par1] Par1 i m)
-> c Par1
forall a b. (a -> b) -> a -> b
$
    \(Par1 i
v1) (Par1 i
v2) -> (i -> Par1 i) -> m i -> m (Par1 i)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap i -> Par1 i
forall p. p -> Par1 p
Par1 (m i -> m (Par1 i)) -> m i -> m (Par1 i)
forall a b. (a -> b) -> a -> b
$
      ClosedPoly i (BaseField c) -> m i
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
ClosedPoly var a -> m var
newAssigned (ClosedPoly i (BaseField c) -> m i)
-> ClosedPoly i (BaseField c) -> m i
forall a b. (a -> b) -> a -> b
$ \i -> x
x -> let x1 :: x
x1 = i -> x
x i
v1; x2 :: x
x2 = i -> x
x i
v2 in x
x1 x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
x2

deriving newtype instance Symbolic c => Ord (Ordering c)

class
  ( GEq u
  , IsOrdering (GOrderingOf u)
  ) => GOrd u where
  type GOrderingOf u
  gordering :: u x -> u x -> u x -> GOrderingOf u -> u x
  gcompare :: u x -> u x -> GOrderingOf u

instance
  ( GOrd u
  , GOrd v
  , GBooleanOf u ~ GBooleanOf v
  , GOrderingOf u ~ GOrderingOf v
  ) => GOrd (u :*: v) where
  type GOrderingOf (u :*: v) = GOrderingOf u
  gordering :: forall (x :: k).
(:*:) u v x
-> (:*:) u v x
-> (:*:) u v x
-> GOrderingOf (u :*: v)
-> (:*:) u v x
gordering (u x
lt0 :*: v x
lt1) (u x
eq0 :*: v x
eq1) (u x
gt0 :*: v x
gt1) GOrderingOf (u :*: v)
o =
    u x -> u x -> u x -> GOrderingOf u -> u x
forall (x :: k). u x -> u x -> u x -> GOrderingOf u -> u x
forall {k} (u :: k -> Type) (x :: k).
GOrd u =>
u x -> u x -> u x -> GOrderingOf u -> u x
gordering u x
lt0 u x
eq0 u x
gt0 GOrderingOf u
GOrderingOf (u :*: v)
o u x -> v x -> (:*:) u v x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: v x -> v x -> v x -> GOrderingOf v -> v x
forall (x :: k). v x -> v x -> v x -> GOrderingOf v -> v x
forall {k} (u :: k -> Type) (x :: k).
GOrd u =>
u x -> u x -> u x -> GOrderingOf u -> u x
gordering v x
lt1 v x
eq1 v x
gt1 GOrderingOf v
GOrderingOf (u :*: v)
o
  gcompare :: forall (x :: k).
(:*:) u v x -> (:*:) u v x -> GOrderingOf (u :*: v)
gcompare (u x
x0 :*: v x
x1) (u x
y0 :*: v x
y1) = u x -> u x -> GOrderingOf u
forall (x :: k). u x -> u x -> GOrderingOf u
forall {k} (u :: k -> Type) (x :: k).
GOrd u =>
u x -> u x -> GOrderingOf u
gcompare u x
x0 u x
y0 GOrderingOf v -> GOrderingOf v -> GOrderingOf v
forall a. Semigroup a => a -> a -> a
<> v x -> v x -> GOrderingOf v
forall (x :: k). v x -> v x -> GOrderingOf v
forall {k} (u :: k -> Type) (x :: k).
GOrd u =>
u x -> u x -> GOrderingOf u
gcompare v x
x1 v x
y1

instance GOrd v => GOrd (M1 i c v) where
  type GOrderingOf (M1 i c v) = GOrderingOf v
  gordering :: forall (x :: k).
M1 i c v x
-> M1 i c v x -> M1 i c v x -> GOrderingOf (M1 i c v) -> M1 i c v x
gordering (M1 v x
ltCase) (M1 v x
eqCase) (M1 v x
gtCase) GOrderingOf (M1 i c v)
o =
    v x -> M1 i c v x
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (v x -> v x -> v x -> GOrderingOf v -> v x
forall (x :: k). v x -> v x -> v x -> GOrderingOf v -> v x
forall {k} (u :: k -> Type) (x :: k).
GOrd u =>
u x -> u x -> u x -> GOrderingOf u -> u x
gordering v x
ltCase v x
eqCase v x
gtCase GOrderingOf v
GOrderingOf (M1 i c v)
o)
  gcompare :: forall (x :: k). M1 i c v x -> M1 i c v x -> GOrderingOf (M1 i c v)
gcompare (M1 v x
x) (M1 v x
y) = v x -> v x -> GOrderingOf v
forall (x :: k). v x -> v x -> GOrderingOf v
forall {k} (u :: k -> Type) (x :: k).
GOrd u =>
u x -> u x -> GOrderingOf u
gcompare v x
x v x
y

instance Ord x => GOrd (Rec0 x) where
  type GOrderingOf (Rec0 x) = OrderingOf x
  gordering :: forall (x :: k).
Rec0 x x
-> Rec0 x x -> Rec0 x x -> GOrderingOf (Rec0 x) -> Rec0 x x
gordering (K1 x
ltCase) (K1 x
eqCase) (K1 x
gtCase) GOrderingOf (Rec0 x)
o =
    x -> K1 R x x
forall k i c (p :: k). c -> K1 i c p
K1 (x -> x -> x -> OrderingOf x -> x
forall a. Ord a => a -> a -> a -> OrderingOf a -> a
ordering x
ltCase x
eqCase x
gtCase GOrderingOf (Rec0 x)
OrderingOf x
o)
  gcompare :: forall (x :: k). Rec0 x x -> Rec0 x x -> GOrderingOf (Rec0 x)
gcompare (K1 x
x) (K1 x
y) = x -> x -> OrderingOf x
forall a. Ord a => a -> a -> OrderingOf a
compare x
x x
y