{-# LANGUAGE DerivingVia #-}
module ZkFold.Symbolic.Cardano.Types where

import           Prelude                            hiding (Bool, Eq, length, splitAt, (*), (+))

import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Data.Vector
import           ZkFold.Symbolic.Compiler
import           ZkFold.Symbolic.Data.Bool          (Bool)
import           ZkFold.Symbolic.Data.ByteString
import           ZkFold.Symbolic.Data.Eq            (Eq)
import           ZkFold.Symbolic.Data.Eq.Structural
import           ZkFold.Symbolic.Data.UInt
import           ZkFold.Symbolic.Data.UTCTime

newtype Transaction inputs rinputs outputs tokens datum a = Transaction
    ( Vector rinputs (Input tokens datum a)
    , (Vector inputs (Input tokens datum a)
    , (Vector outputs (Output tokens datum a)
    , (UTCTime a, UTCTime a)
    )))

deriving instance
    ( Arithmetic a
    , KnownNat inputs
    , KnownNat rinputs
    , KnownNat outputs
    , KnownNat tokens
    ) => SymbolicData a (Transaction inputs rinputs outputs tokens datum (ArithmeticCircuit a))

txInputs :: Transaction inputs rinputs outputs tokens datum a -> Vector inputs (Input tokens datum a)
txInputs :: forall {k} (inputs :: Natural) (rinputs :: Natural)
       (outputs :: Natural) (tokens :: Natural) (datum :: k) a.
Transaction inputs rinputs outputs tokens datum a
-> Vector inputs (Input tokens datum a)
txInputs (Transaction (Vector rinputs (Input tokens datum a)
_, (Vector inputs (Input tokens datum a)
is, (Vector outputs (Output tokens datum a), (UTCTime a, UTCTime a))
_))) = Vector inputs (Input tokens datum a)
is

txOutputs :: Transaction inputs rinputs outputs tokens datum a -> Vector outputs (Output tokens datum a)
txOutputs :: forall {k} (inputs :: Natural) (rinputs :: Natural)
       (outputs :: Natural) (tokens :: Natural) (datum :: k) a.
Transaction inputs rinputs outputs tokens datum a
-> Vector outputs (Output tokens datum a)
txOutputs (Transaction (Vector rinputs (Input tokens datum a)
_, (Vector inputs (Input tokens datum a)
_, (Vector outputs (Output tokens datum a)
os, (UTCTime a, UTCTime a)
_)))) = Vector outputs (Output tokens datum a)
os

newtype TxId a = TxId a

deriving instance Arithmetic a => SymbolicData a (TxId (ArithmeticCircuit a))

newtype Value n a = Value (Vector n (ByteString 224 a, (ByteString 256 a, UInt 64 a)))

deriving instance (Arithmetic a, KnownNat n) => SymbolicData a (Value n (ArithmeticCircuit a))

newtype Input tokens datum a = Input (OutputRef a, Output tokens datum a)

txiOutput :: Input tokens datum a -> Output tokens datum a
txiOutput :: forall {k} (tokens :: Natural) (datum :: k) a.
Input tokens datum a -> Output tokens datum a
txiOutput (Input (OutputRef a
_, Output tokens datum a
txo)) = Output tokens datum a
txo

txiDatumHash :: Input tokens datum a -> ByteString 256 a
txiDatumHash :: forall {k} (tokens :: Natural) (datum :: k) a.
Input tokens datum a -> ByteString 256 a
txiDatumHash (Input (OutputRef a
_, Output tokens datum a
txo))= Output tokens datum a -> ByteString 256 a
forall {k} (tokens :: Natural) (datum :: k) a.
Output tokens datum a -> ByteString 256 a
txoDatumHash Output tokens datum a
txo

deriving instance (Arithmetic a, KnownNat tokens) => SymbolicData a (Input tokens datum (ArithmeticCircuit a))

newtype Output tokens datum a = Output (Address a, (Value tokens a, ByteString 256 a))

txoAddress :: Output tokens datum a -> Address a
txoAddress :: forall {k} (tokens :: Natural) (datum :: k) a.
Output tokens datum a -> Address a
txoAddress (Output (Address a
addr, (Value tokens a, ByteString 256 a)
_)) = Address a
addr

txoDatumHash :: Output tokens datum a -> ByteString 256 a
txoDatumHash :: forall {k} (tokens :: Natural) (datum :: k) a.
Output tokens datum a -> ByteString 256 a
txoDatumHash (Output (Address a
_, (Value tokens a
_, ByteString 256 a
dh))) = ByteString 256 a
dh

deriving instance (Arithmetic a, KnownNat tokens) => SymbolicData a (Output tokens datum (ArithmeticCircuit a))

deriving via (Structural (Output tokens datum (ArithmeticCircuit a)))
         instance (Arithmetic a, KnownNat tokens) =>
         Eq (Bool (ArithmeticCircuit a)) (Output tokens datum (ArithmeticCircuit a))

newtype OutputRef a = OutputRef (TxId a, UInt 32 a)

deriving instance Arithmetic a => SymbolicData a (OutputRef (ArithmeticCircuit a))

newtype Address a = Address (ByteString 4 a, (ByteString 224 a, ByteString 224 a))

paymentCredential :: Address a -> ByteString 224 a
paymentCredential :: forall a. Address a -> ByteString 224 a
paymentCredential (Address (ByteString 4 a
_, (ByteString 224 a
pc, ByteString 224 a
_))) = ByteString 224 a
pc

deriving instance Arithmetic a => SymbolicData a (Address (ArithmeticCircuit a))

newtype DatumHash datum a = DatumHash a
    deriving (SymbolicData i)

newtype ScriptHash a = ScriptHash a
    deriving (SymbolicData i)