{-# 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.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 SysVar i
  = InVar (Rep i)
  | NewVar ByteString
  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 ByteString
b) = ByteString -> SysVar j
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar ByteString
b

deriving anyclass instance FromJSON (Rep i) => FromJSON (SysVar i)
deriving anyclass instance FromJSON (Rep i) => FromJSONKey (SysVar i)
deriving anyclass instance ToJSON (Rep i) => ToJSONKey (SysVar i)
deriving anyclass instance ToJSON (Rep i) => ToJSON (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)
deriving instance NFData (Rep i) => NFData (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 (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