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

module ZkFold.Symbolic.Data.Maybe (
    Maybe, maybe, just, nothing, fromMaybe, isNothing, isJust, find
) where

import           Data.Function                    ((.))
import           Data.Functor.Rep                 (Representable, pureRep)
import           Data.Proxy                       (Proxy)
import           Data.Traversable                 (Traversable)
import           GHC.Generics                     (Par1 (..))
import           Prelude                          (foldr, type (~), ($))
import qualified Prelude                          as Haskell

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Control.HApplicative (HApplicative)
import           ZkFold.Base.Data.HFunctor        (HFunctor, hmap)
import qualified ZkFold.Base.Data.Vector          as V
import           ZkFold.Base.Data.Vector          (Vector)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Conditional

data Maybe context x = Maybe (Bool context) x
  deriving stock
    ( (forall a b. (a -> b) -> Maybe context a -> Maybe context b)
-> (forall a b. a -> Maybe context b -> Maybe context a)
-> Functor (Maybe context)
forall a b. a -> Maybe context b -> Maybe context a
forall a b. (a -> b) -> Maybe context a -> Maybe context b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (context :: (Type -> Type) -> Type) a b.
a -> Maybe context b -> Maybe context a
forall (context :: (Type -> Type) -> Type) a b.
(a -> b) -> Maybe context a -> Maybe context b
$cfmap :: forall (context :: (Type -> Type) -> Type) a b.
(a -> b) -> Maybe context a -> Maybe context b
fmap :: forall a b. (a -> b) -> Maybe context a -> Maybe context b
$c<$ :: forall (context :: (Type -> Type) -> Type) a b.
a -> Maybe context b -> Maybe context a
<$ :: forall a b. a -> Maybe context b -> Maybe context a
Haskell.Functor
    , (forall m. Monoid m => Maybe context m -> m)
-> (forall m a. Monoid m => (a -> m) -> Maybe context a -> m)
-> (forall m a. Monoid m => (a -> m) -> Maybe context a -> m)
-> (forall a b. (a -> b -> b) -> b -> Maybe context a -> b)
-> (forall a b. (a -> b -> b) -> b -> Maybe context a -> b)
-> (forall b a. (b -> a -> b) -> b -> Maybe context a -> b)
-> (forall b a. (b -> a -> b) -> b -> Maybe context a -> b)
-> (forall a. (a -> a -> a) -> Maybe context a -> a)
-> (forall a. (a -> a -> a) -> Maybe context a -> a)
-> (forall a. Maybe context a -> [a])
-> (forall a. Maybe context a -> Bool)
-> (forall a. Maybe context a -> Int)
-> (forall a. Eq a => a -> Maybe context a -> Bool)
-> (forall a. Ord a => Maybe context a -> a)
-> (forall a. Ord a => Maybe context a -> a)
-> (forall a. Num a => Maybe context a -> a)
-> (forall a. Num a => Maybe context a -> a)
-> Foldable (Maybe context)
forall a. Eq a => a -> Maybe context a -> Bool
forall a. Num a => Maybe context a -> a
forall a. Ord a => Maybe context a -> a
forall m. Monoid m => Maybe context m -> m
forall a. Maybe context a -> Bool
forall a. Maybe context a -> Int
forall a. Maybe context a -> [a]
forall a. (a -> a -> a) -> Maybe context a -> a
forall m a. Monoid m => (a -> m) -> Maybe context a -> m
forall b a. (b -> a -> b) -> b -> Maybe context a -> b
forall a b. (a -> b -> b) -> b -> Maybe context a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
forall (context :: (Type -> Type) -> Type) a.
Eq a =>
a -> Maybe context a -> Bool
forall (context :: (Type -> Type) -> Type) a.
Num a =>
Maybe context a -> a
forall (context :: (Type -> Type) -> Type) a.
Ord a =>
Maybe context a -> a
forall (context :: (Type -> Type) -> Type) m.
Monoid m =>
Maybe context m -> m
forall (context :: (Type -> Type) -> Type) a.
Maybe context a -> Bool
forall (context :: (Type -> Type) -> Type) a.
Maybe context a -> Int
forall (context :: (Type -> Type) -> Type) a.
Maybe context a -> [a]
forall (context :: (Type -> Type) -> Type) a.
(a -> a -> a) -> Maybe context a -> a
forall (context :: (Type -> Type) -> Type) m a.
Monoid m =>
(a -> m) -> Maybe context a -> m
forall (context :: (Type -> Type) -> Type) b a.
(b -> a -> b) -> b -> Maybe context a -> b
forall (context :: (Type -> Type) -> Type) a b.
(a -> b -> b) -> b -> Maybe context a -> b
$cfold :: forall (context :: (Type -> Type) -> Type) m.
Monoid m =>
Maybe context m -> m
fold :: forall m. Monoid m => Maybe context m -> m
$cfoldMap :: forall (context :: (Type -> Type) -> Type) m a.
Monoid m =>
(a -> m) -> Maybe context a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Maybe context a -> m
$cfoldMap' :: forall (context :: (Type -> Type) -> Type) m a.
Monoid m =>
(a -> m) -> Maybe context a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Maybe context a -> m
$cfoldr :: forall (context :: (Type -> Type) -> Type) a b.
(a -> b -> b) -> b -> Maybe context a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Maybe context a -> b
$cfoldr' :: forall (context :: (Type -> Type) -> Type) a b.
(a -> b -> b) -> b -> Maybe context a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Maybe context a -> b
$cfoldl :: forall (context :: (Type -> Type) -> Type) b a.
(b -> a -> b) -> b -> Maybe context a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Maybe context a -> b
$cfoldl' :: forall (context :: (Type -> Type) -> Type) b a.
(b -> a -> b) -> b -> Maybe context a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Maybe context a -> b
$cfoldr1 :: forall (context :: (Type -> Type) -> Type) a.
(a -> a -> a) -> Maybe context a -> a
foldr1 :: forall a. (a -> a -> a) -> Maybe context a -> a
$cfoldl1 :: forall (context :: (Type -> Type) -> Type) a.
(a -> a -> a) -> Maybe context a -> a
foldl1 :: forall a. (a -> a -> a) -> Maybe context a -> a
$ctoList :: forall (context :: (Type -> Type) -> Type) a.
Maybe context a -> [a]
toList :: forall a. Maybe context a -> [a]
$cnull :: forall (context :: (Type -> Type) -> Type) a.
Maybe context a -> Bool
null :: forall a. Maybe context a -> Bool
$clength :: forall (context :: (Type -> Type) -> Type) a.
Maybe context a -> Int
length :: forall a. Maybe context a -> Int
$celem :: forall (context :: (Type -> Type) -> Type) a.
Eq a =>
a -> Maybe context a -> Bool
elem :: forall a. Eq a => a -> Maybe context a -> Bool
$cmaximum :: forall (context :: (Type -> Type) -> Type) a.
Ord a =>
Maybe context a -> a
maximum :: forall a. Ord a => Maybe context a -> a
$cminimum :: forall (context :: (Type -> Type) -> Type) a.
Ord a =>
Maybe context a -> a
minimum :: forall a. Ord a => Maybe context a -> a
$csum :: forall (context :: (Type -> Type) -> Type) a.
Num a =>
Maybe context a -> a
sum :: forall a. Num a => Maybe context a -> a
$cproduct :: forall (context :: (Type -> Type) -> Type) a.
Num a =>
Maybe context a -> a
product :: forall a. Num a => Maybe context a -> a
Haskell.Foldable
    , Functor (Maybe context)
Foldable (Maybe context)
(Functor (Maybe context), Foldable (Maybe context)) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> Maybe context a -> f (Maybe context b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Maybe context (f a) -> f (Maybe context a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Maybe context a -> m (Maybe context b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Maybe context (m a) -> m (Maybe context a))
-> Traversable (Maybe context)
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
Maybe context (m a) -> m (Maybe context a)
forall (f :: Type -> Type) a.
Applicative f =>
Maybe context (f a) -> f (Maybe context a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Maybe context a -> m (Maybe context b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Maybe context a -> f (Maybe context b)
forall (context :: (Type -> Type) -> Type). Functor (Maybe context)
forall (context :: (Type -> Type) -> Type).
Foldable (Maybe context)
forall (context :: (Type -> Type) -> Type) (m :: Type -> Type) a.
Monad m =>
Maybe context (m a) -> m (Maybe context a)
forall (context :: (Type -> Type) -> Type) (f :: Type -> Type) a.
Applicative f =>
Maybe context (f a) -> f (Maybe context a)
forall (context :: (Type -> Type) -> Type) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Maybe context a -> m (Maybe context b)
forall (context :: (Type -> Type) -> Type) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Maybe context a -> f (Maybe context b)
$ctraverse :: forall (context :: (Type -> Type) -> Type) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Maybe context a -> f (Maybe context b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Maybe context a -> f (Maybe context b)
$csequenceA :: forall (context :: (Type -> Type) -> Type) (f :: Type -> Type) a.
Applicative f =>
Maybe context (f a) -> f (Maybe context a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Maybe context (f a) -> f (Maybe context a)
$cmapM :: forall (context :: (Type -> Type) -> Type) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Maybe context a -> m (Maybe context b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Maybe context a -> m (Maybe context b)
$csequence :: forall (context :: (Type -> Type) -> Type) (m :: Type -> Type) a.
Monad m =>
Maybe context (m a) -> m (Maybe context a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Maybe context (m a) -> m (Maybe context a)
Haskell.Traversable
    )

deriving stock instance (Haskell.Eq (context Par1), Haskell.Eq x) => Haskell.Eq (Maybe context x)

just :: Symbolic c => x -> Maybe c x
just :: forall (c :: (Type -> Type) -> Type) x.
Symbolic c =>
x -> Maybe c x
just = Bool c -> x -> Maybe c x
forall (context :: (Type -> Type) -> Type) x.
Bool context -> x -> Maybe context x
Maybe Bool c
forall b. BoolType b => b
true

nothing ::
  forall x c .
  (SymbolicData x, Representable (Layout x), Context x ~ c, Symbolic c) =>
  Maybe c x
nothing :: forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Representable (Layout x), Context x ~ c,
 Symbolic c) =>
Maybe c x
nothing = Bool c -> x -> Maybe c x
forall (context :: (Type -> Type) -> Type) x.
Bool context -> x -> Maybe context x
Maybe Bool c
forall b. BoolType b => b
false (let c :: c (Layout x)
c = forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed @c (Layout x (BaseField c) -> c (Layout x))
-> Layout x (BaseField c) -> c (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField c -> Layout x (BaseField c)
forall (f :: Type -> Type) a. Representable f => a -> f a
pureRep BaseField c
forall a. AdditiveMonoid a => a
zero in (Support x -> Context x (Layout x)) -> x
forall x.
SymbolicData x =>
(Support x -> Context x (Layout x)) -> x
restore (c (Layout x) -> Support x -> c (Layout x)
forall a b. a -> b -> a
Haskell.const c (Layout x)
c))

fromMaybe
    :: forall c x
    .  HFunctor c
    => Ring (c (Vector 1))
    => SymbolicData x
    => Context x ~ c
    => Layout x ~ Vector 1
    => x
    -> Maybe c x
    -> x
fromMaybe :: forall (c :: (Type -> Type) -> Type) x.
(HFunctor c, Ring (c (Vector 1)), SymbolicData x, Context x ~ c,
 Layout x ~ Vector 1) =>
x -> Maybe c x -> x
fromMaybe x
a (Maybe (Bool c Par1
h) x
t) = (Support x -> Context x (Layout x)) -> x
forall x.
SymbolicData x =>
(Support x -> Context x (Layout x)) -> x
restore ((Support x -> Context x (Layout x)) -> x)
-> (Support x -> Context x (Layout x)) -> x
forall a b. (a -> b) -> a -> b
$ \Support x
i ->
  let
    as :: Context x (Layout x)
as = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
a Support x
i
    ts :: Context x (Layout x)
ts = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
t Support x
i
  in
    (c (Vector 1)
Context x (Layout x)
ts c (Vector 1) -> c (Vector 1) -> c (Vector 1)
forall a. AdditiveGroup a => a -> a -> a
- c (Vector 1)
Context x (Layout x)
as) c (Vector 1) -> c (Vector 1) -> c (Vector 1)
forall a. MultiplicativeSemigroup a => a -> a -> a
* (forall a. Par1 a -> Vector 1 a) -> c Par1 -> c (Vector 1)
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a) -> c f -> c g
hmap (a -> Vector 1 a
forall a. a -> Vector 1 a
V.singleton (a -> Vector 1 a) -> (Par1 a -> a) -> Par1 a -> Vector 1 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 a -> a
forall p. Par1 p -> p
unPar1) c Par1
h c (Vector 1) -> c (Vector 1) -> c (Vector 1)
forall a. AdditiveSemigroup a => a -> a -> a
+ c (Vector 1)
Context x (Layout x)
as

isNothing :: Symbolic c => Maybe c x -> Bool c
isNothing :: forall (c :: (Type -> Type) -> Type) x.
Symbolic c =>
Maybe c x -> Bool c
isNothing (Maybe Bool c
h x
_) = Bool c -> Bool c
forall b. BoolType b => b -> b
not Bool c
h

isJust :: Maybe c x -> Bool c
isJust :: forall (c :: (Type -> Type) -> Type) x. Maybe c x -> Bool c
isJust (Maybe Bool c
h x
_) = Bool c
h

instance
    ( HApplicative c
    , SymbolicData x
    , Context x ~ c
    , Support x ~ Proxy c
    ) => SymbolicData (Maybe c x) where

    type Context (Maybe c x) = Context (Bool c, x)
    type Support (Maybe c x) = Support (Bool c, x)
    type Layout (Maybe c x) = Layout (Bool c, x)

    pieces :: Maybe c x
-> Support (Maybe c x) -> Context (Maybe c x) (Layout (Maybe c x))
pieces (Maybe Bool c
b x
t) = (Bool c, x)
-> Support (Bool c, x) -> Context (Bool c, x) (Layout (Bool c, x))
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces (Bool c
b, x
t)
    restore :: (Support (Maybe c x) -> Context (Maybe c x) (Layout (Maybe c x)))
-> Maybe c x
restore Support (Maybe c x) -> Context (Maybe c x) (Layout (Maybe c x))
f = let (Bool c
b, x
t) = (Support (Bool c, x) -> Context (Bool c, x) (Layout (Bool c, x)))
-> (Bool c, x)
forall x.
SymbolicData x =>
(Support x -> Context x (Layout x)) -> x
restore Support (Bool c, x) -> Context (Bool c, x) (Layout (Bool c, x))
Support (Maybe c x) -> Context (Maybe c x) (Layout (Maybe c x))
f in Bool c -> x -> Maybe c x
forall (context :: (Type -> Type) -> Type) x.
Bool context -> x -> Maybe context x
Maybe Bool c
b x
t

maybe :: forall a b c .
    (Symbolic c, SymbolicData b, Context b ~ c) =>
    (Representable (Layout b), Traversable (Layout b)) =>
    b -> (a -> b) -> Maybe c a -> b
maybe :: forall a b (c :: (Type -> Type) -> Type).
(Symbolic c, SymbolicData b, Context b ~ c,
 Representable (Layout b), Traversable (Layout b)) =>
b -> (a -> b) -> Maybe c a -> b
maybe b
d a -> b
h x :: Maybe c a
x@(Maybe Bool c
_ a
v) = forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) b
d (a -> b
h a
v) (Bool c -> b) -> Bool c -> b
forall a b. (a -> b) -> a -> b
$ Maybe c a -> Bool c
forall (c :: (Type -> Type) -> Type) x.
Symbolic c =>
Maybe c x -> Bool c
isNothing Maybe c a
x

find :: forall a c t .
    (Symbolic c, SymbolicData a, Context a ~ c, Support a ~ Proxy c) =>
    (Representable (Layout a), Traversable (Layout a)) =>
    Haskell.Foldable t =>
    (a -> Bool c) -> t a -> Maybe c a
find :: forall a (c :: (Type -> Type) -> Type) (t :: Type -> Type).
(Symbolic c, SymbolicData a, Context a ~ c, Support a ~ Proxy c,
 Representable (Layout a), Traversable (Layout a), Foldable t) =>
(a -> Bool c) -> t a -> Maybe c a
find a -> Bool c
p = let n :: Maybe (Context a) a
n = Maybe (Context a) a
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Representable (Layout x), Context x ~ c,
 Symbolic c) =>
Maybe c x
nothing in
    (a -> Maybe c a -> Maybe c a) -> Maybe c a -> t a -> Maybe c a
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
i Maybe c a
r -> forall a b (c :: (Type -> Type) -> Type).
(Symbolic c, SymbolicData b, Context b ~ c,
 Representable (Layout b), Traversable (Layout b)) =>
b -> (a -> b) -> Maybe c a -> b
maybe @a @_ @c (forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool c) Maybe c a
Maybe (Context a) a
n (a -> Maybe c a
forall (c :: (Type -> Type) -> Type) x.
Symbolic c =>
x -> Maybe c x
just a
i) (Bool c -> Maybe c a) -> Bool c -> Maybe c a
forall a b. (a -> b) -> a -> b
$ a -> Bool c
p a
i) (Maybe c a -> a -> Maybe c a
forall a b. a -> b -> a
Haskell.const Maybe c a
r) Maybe c a
r) Maybe c a
Maybe (Context a) a
n