{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var where

import           Control.Applicative             ()
import           Control.DeepSeq                 (NFData)
import           Data.Aeson                      (FromJSON, FromJSONKey, ToJSON, ToJSONKey)
import           Data.Binary                     (Binary)
import           Data.ByteString                 (ByteString)
import           Data.Functor.Rep                (Rep, Representable, index, tabulate)
import           GHC.Generics                    (Generic)
import           GHC.Show                        (Show)
import           Prelude                         (Eq, Ord)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Data.ByteString     ()

data NewVar
  = EqVar ByteString
  | FoldVar ByteString ByteString
  deriving
    ( (forall x. NewVar -> Rep NewVar x)
-> (forall x. Rep NewVar x -> NewVar) -> Generic NewVar
forall x. Rep NewVar x -> NewVar
forall x. NewVar -> Rep NewVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NewVar -> Rep NewVar x
from :: forall x. NewVar -> Rep NewVar x
$cto :: forall x. Rep NewVar x -> NewVar
to :: forall x. Rep NewVar x -> NewVar
Generic, Get NewVar
[NewVar] -> Put
NewVar -> Put
(NewVar -> Put) -> Get NewVar -> ([NewVar] -> Put) -> Binary NewVar
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
$cput :: NewVar -> Put
put :: NewVar -> Put
$cget :: Get NewVar
get :: Get NewVar
$cputList :: [NewVar] -> Put
putList :: [NewVar] -> Put
Binary, Value -> Parser [NewVar]
Value -> Parser NewVar
(Value -> Parser NewVar)
-> (Value -> Parser [NewVar]) -> FromJSON NewVar
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser NewVar
parseJSON :: Value -> Parser NewVar
$cparseJSONList :: Value -> Parser [NewVar]
parseJSONList :: Value -> Parser [NewVar]
FromJSON, FromJSONKeyFunction [NewVar]
FromJSONKeyFunction NewVar
FromJSONKeyFunction NewVar
-> FromJSONKeyFunction [NewVar] -> FromJSONKey NewVar
forall a.
FromJSONKeyFunction a -> FromJSONKeyFunction [a] -> FromJSONKey a
$cfromJSONKey :: FromJSONKeyFunction NewVar
fromJSONKey :: FromJSONKeyFunction NewVar
$cfromJSONKeyList :: FromJSONKeyFunction [NewVar]
fromJSONKeyList :: FromJSONKeyFunction [NewVar]
FromJSONKey, [NewVar] -> Value
[NewVar] -> Encoding
NewVar -> Value
NewVar -> Encoding
(NewVar -> Value)
-> (NewVar -> Encoding)
-> ([NewVar] -> Value)
-> ([NewVar] -> Encoding)
-> ToJSON NewVar
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
$ctoJSON :: NewVar -> Value
toJSON :: NewVar -> Value
$ctoEncoding :: NewVar -> Encoding
toEncoding :: NewVar -> Encoding
$ctoJSONList :: [NewVar] -> Value
toJSONList :: [NewVar] -> Value
$ctoEncodingList :: [NewVar] -> Encoding
toEncodingList :: [NewVar] -> Encoding
ToJSON, ToJSONKeyFunction [NewVar]
ToJSONKeyFunction NewVar
ToJSONKeyFunction NewVar
-> ToJSONKeyFunction [NewVar] -> ToJSONKey NewVar
forall a.
ToJSONKeyFunction a -> ToJSONKeyFunction [a] -> ToJSONKey a
$ctoJSONKey :: ToJSONKeyFunction NewVar
toJSONKey :: ToJSONKeyFunction NewVar
$ctoJSONKeyList :: ToJSONKeyFunction [NewVar]
toJSONKeyList :: ToJSONKeyFunction [NewVar]
ToJSONKey
    , Int -> NewVar -> ShowS
[NewVar] -> ShowS
NewVar -> String
(Int -> NewVar -> ShowS)
-> (NewVar -> String) -> ([NewVar] -> ShowS) -> Show NewVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NewVar -> ShowS
showsPrec :: Int -> NewVar -> ShowS
$cshow :: NewVar -> String
show :: NewVar -> String
$cshowList :: [NewVar] -> ShowS
showList :: [NewVar] -> ShowS
Show, NewVar -> NewVar -> Bool
(NewVar -> NewVar -> Bool)
-> (NewVar -> NewVar -> Bool) -> Eq NewVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NewVar -> NewVar -> Bool
== :: NewVar -> NewVar -> Bool
$c/= :: NewVar -> NewVar -> Bool
/= :: NewVar -> NewVar -> Bool
Eq, Eq NewVar
Eq NewVar =>
(NewVar -> NewVar -> Ordering)
-> (NewVar -> NewVar -> Bool)
-> (NewVar -> NewVar -> Bool)
-> (NewVar -> NewVar -> Bool)
-> (NewVar -> NewVar -> Bool)
-> (NewVar -> NewVar -> NewVar)
-> (NewVar -> NewVar -> NewVar)
-> Ord NewVar
NewVar -> NewVar -> Bool
NewVar -> NewVar -> Ordering
NewVar -> NewVar -> NewVar
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: NewVar -> NewVar -> Ordering
compare :: NewVar -> NewVar -> Ordering
$c< :: NewVar -> NewVar -> Bool
< :: NewVar -> NewVar -> Bool
$c<= :: NewVar -> NewVar -> Bool
<= :: NewVar -> NewVar -> Bool
$c> :: NewVar -> NewVar -> Bool
> :: NewVar -> NewVar -> Bool
$c>= :: NewVar -> NewVar -> Bool
>= :: NewVar -> NewVar -> Bool
$cmax :: NewVar -> NewVar -> NewVar
max :: NewVar -> NewVar -> NewVar
$cmin :: NewVar -> NewVar -> NewVar
min :: NewVar -> NewVar -> NewVar
Ord, NewVar -> ()
(NewVar -> ()) -> NFData NewVar
forall a. (a -> ()) -> NFData a
$crnf :: NewVar -> ()
rnf :: NewVar -> ()
NFData)

data SysVar i
  = InVar (Rep i)
  | NewVar NewVar
  deriving ((forall x. SysVar i -> Rep (SysVar i) x)
-> (forall x. Rep (SysVar i) x -> SysVar i) -> Generic (SysVar i)
forall x. Rep (SysVar i) x -> SysVar i
forall x. SysVar i -> Rep (SysVar i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (i :: Type -> Type) x. Rep (SysVar i) x -> SysVar i
forall (i :: Type -> Type) x. SysVar i -> Rep (SysVar i) x
$cfrom :: forall (i :: Type -> Type) x. SysVar i -> Rep (SysVar i) x
from :: forall x. SysVar i -> Rep (SysVar i) x
$cto :: forall (i :: Type -> Type) x. Rep (SysVar i) x -> SysVar i
to :: forall x. Rep (SysVar i) x -> SysVar i
Generic)

imapSysVar ::
  (Representable i, Representable j) =>
  (forall x. j x -> i x) -> SysVar i -> SysVar j
imapSysVar :: forall (i :: Type -> Type) (j :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> SysVar i -> SysVar j
imapSysVar forall x. j x -> i x
f (InVar Rep i
r)  = i (SysVar j) -> Rep i -> SysVar j
forall a. i a -> Rep i -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index (j (SysVar j) -> i (SysVar j)
forall x. j x -> i x
f ((Rep j -> SysVar j) -> j (SysVar j)
forall a. (Rep j -> a) -> j a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep j -> SysVar j
forall (i :: Type -> Type). Rep i -> SysVar i
InVar)) Rep i
r
imapSysVar forall x. j x -> i x
_ (NewVar NewVar
v) = NewVar -> SysVar j
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar NewVar
v

instance Binary (Rep i) => Binary (SysVar i)
instance NFData (Rep i) => NFData (SysVar i)
instance FromJSON (Rep i) => FromJSON (SysVar i)
instance FromJSON (Rep i) => FromJSONKey (SysVar i)
instance ToJSON (Rep i) => ToJSON (SysVar i)
instance ToJSON (Rep i) => ToJSONKey (SysVar i)
deriving stock instance Show (Rep i) => Show (SysVar i)
deriving stock instance Eq (Rep i) => Eq (SysVar i)
deriving stock instance Ord (Rep i) => Ord (SysVar i)

data Var a i
  = LinVar a (SysVar i) a
  | ConstVar a
  deriving (forall x. Var a i -> Rep (Var a i) x)
-> (forall x. Rep (Var a i) x -> Var a i) -> Generic (Var a i)
forall x. Rep (Var a i) x -> Var a i
forall x. Var a i -> Rep (Var a i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (i :: Type -> Type) x. Rep (Var a i) x -> Var a i
forall a (i :: Type -> Type) x. Var a i -> Rep (Var a i) x
$cfrom :: forall a (i :: Type -> Type) x. Var a i -> Rep (Var a i) x
from :: forall x. Var a i -> Rep (Var a i) x
$cto :: forall a (i :: Type -> Type) x. Rep (Var a i) x -> Var a i
to :: forall x. Rep (Var a i) x -> Var a i
Generic

toVar :: Semiring a => SysVar i -> Var a i
toVar :: forall a (i :: Type -> Type). Semiring a => SysVar i -> Var a i
toVar SysVar i
x = a -> SysVar i -> a -> Var a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> Var a i
LinVar a
forall a. MultiplicativeMonoid a => a
one SysVar i
x a
forall a. AdditiveMonoid a => a
zero

imapVar ::
  (Representable i, Representable j) =>
  (forall x. j x -> i x) -> Var a i -> Var a j
imapVar :: forall (i :: Type -> Type) (j :: Type -> Type) a.
(Representable i, Representable j) =>
(forall x. j x -> i x) -> Var a i -> Var a j
imapVar forall x. j x -> i x
f (LinVar a
k SysVar i
x a
b) = a -> SysVar j -> a -> Var a j
forall a (i :: Type -> Type). a -> SysVar i -> a -> Var a i
LinVar a
k ((forall x. j x -> i x) -> SysVar i -> SysVar j
forall (i :: Type -> Type) (j :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> SysVar i -> SysVar j
imapSysVar j x -> i x
forall x. j x -> i x
f SysVar i
x) a
b
imapVar forall x. j x -> i x
_ (ConstVar a
c)   = a -> Var a j
forall a (i :: Type -> Type). a -> Var a i
ConstVar a
c

deriving anyclass instance (Binary (Rep i), Binary a) => Binary (Var a i)
deriving anyclass instance (FromJSON (Rep i), FromJSON a) => FromJSON (Var a i)
deriving anyclass instance (FromJSON (Rep i), FromJSON a) => FromJSONKey (Var a i)
deriving anyclass instance (ToJSON (Rep i), ToJSON a) => ToJSONKey (Var a i)
deriving anyclass instance (ToJSON (Rep i), ToJSON a) => ToJSON (Var a i)
deriving stock instance (Show (Rep i), Show a) => Show (Var a i)
deriving stock instance (Eq (Rep i), Eq a) => Eq (Var a i)
deriving stock instance (Ord (Rep i), Ord a) => Ord (Var a i)
deriving instance (NFData (Rep i), NFData a) => NFData (Var a i)
instance FromConstant a (Var a i) where fromConstant :: a -> Var a i
fromConstant = a -> Var a i
forall a (i :: Type -> Type). a -> Var a i
ConstVar