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

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

import           Data.Functor                     ((<$>))
import           Data.Functor.Rep                 (pureRep)
import           GHC.Generics                     (Generic, Par1 (..))
import           Prelude                          (foldr, type (~), ($))
import qualified Prelude                          as Haskell

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.Eq

data Maybe context x = Maybe { forall (context :: (Type -> Type) -> Type) x.
Maybe context x -> Bool context
isJust :: Bool context, forall (context :: (Type -> Type) -> Type) x. Maybe context x -> x
fromJust :: 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
    , (forall x. Maybe context x -> Rep (Maybe context x) x)
-> (forall x. Rep (Maybe context x) x -> Maybe context x)
-> Generic (Maybe context x)
forall x. Rep (Maybe context x) x -> Maybe context x
forall x. Maybe context x -> Rep (Maybe context x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (context :: (Type -> Type) -> Type) x x.
Rep (Maybe context x) x -> Maybe context x
forall (context :: (Type -> Type) -> Type) x x.
Maybe context x -> Rep (Maybe context x) x
$cfrom :: forall (context :: (Type -> Type) -> Type) x x.
Maybe context x -> Rep (Maybe context x) x
from :: forall x. Maybe context x -> Rep (Maybe context x) x
$cto :: forall (context :: (Type -> Type) -> Type) x x.
Rep (Maybe context x) x -> Maybe context x
to :: forall x. Rep (Maybe context x) x -> Maybe context x
Generic
    )

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

instance (SymbolicOutput x, Context x ~ c) => SymbolicData (Maybe c x) where
instance (SymbolicOutput x, Context x ~ c, Conditional (Bool c) x) => Conditional (Bool c) (Maybe c x)
instance (SymbolicOutput x, Context x ~ c, Eq (Bool c) x) => Eq (Bool c) (Maybe c 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, Context x ~ c) =>
  Maybe c x
nothing :: forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ 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 (x -> Maybe c x) -> x -> Maybe c x
forall a b. (a -> b) -> a -> b
$ (Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
restore ((Support x -> (c (Layout x), Payload x (WitnessField c))) -> x)
-> (Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall a b. (a -> b) -> a -> b
$ (c (Layout x), Payload x (WitnessField c))
-> Support x -> (c (Layout x), Payload x (WitnessField c))
forall a b. a -> b -> a
Haskell.const (Layout x (BaseField c) -> c (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (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), WitnessField c -> Payload x (WitnessField c)
forall (f :: Type -> Type) a. Representable f => a -> f a
pureRep WitnessField c
forall a. AdditiveMonoid a => a
zero)

fromMaybe ::
  forall c x .
  Conditional (Bool c) x =>
  x -> Maybe c x -> x
fromMaybe :: forall (c :: (Type -> Type) -> Type) x.
Conditional (Bool c) x =>
x -> Maybe c x -> x
fromMaybe x
a (Maybe Bool c
j x
t) = x -> x -> Bool c -> x
forall b a. Conditional b a => a -> a -> b -> a
bool x
a x
t Bool c
j

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

maybe :: forall a b c .
    Conditional (Bool c) b =>
    b -> (a -> b) -> Maybe c a -> b
maybe :: forall a b (c :: (Type -> Type) -> Type).
Conditional (Bool c) b =>
b -> (a -> b) -> Maybe c a -> b
maybe b
d a -> b
h Maybe c a
m = b -> Maybe c b -> b
forall (c :: (Type -> Type) -> Type) x.
Conditional (Bool c) x =>
x -> Maybe c x -> x
fromMaybe b
d (a -> b
h (a -> b) -> Maybe c a -> Maybe c b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe c a
m)

find :: forall a c t .
    (SymbolicOutput a, Context a ~ c, Haskell.Foldable t, Conditional (Bool c) a) =>
    (a -> Bool c) -> t a -> Maybe c a
find :: forall a (c :: (Type -> Type) -> Type) (t :: Type -> Type).
(SymbolicOutput a, Context a ~ c, Foldable t,
 Conditional (Bool c) a) =>
(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, Context x ~ 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).
Conditional (Bool c) 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