{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}

module ZkFold.Symbolic.Cardano.UPLC.Builtins where

import           Data.Typeable                     (Proxy (..), Typeable)
import           Prelude                           (($))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Symbolic.Cardano.UPLC.Type
import           ZkFold.Symbolic.Compiler          (Arithmetic, ArithmeticCircuit, SomeArithmetizable (..))

-- TODO: Add the actual builtins available on-chain in Plutus V3

-- | A class for built-in functions in Plutus.
class PlutusBuiltinFunction a fun where
    builtinFunctionType :: fun -> SomeType a
    builtinFunctionRep  :: fun -> SomeArithmetizable a

data BuiltinFunctions =
      AddField
    | MulField

-- TODO: use shortcuts to make these definitions more readable
instance forall a . (Arithmetic a, Typeable a) => PlutusBuiltinFunction a BuiltinFunctions where
    builtinFunctionType :: BuiltinFunctions -> SomeType a
builtinFunctionType BuiltinFunctions
AddField =
          SomeType a -> SomeType a -> SomeType a
forall a. SomeType a -> SomeType a -> SomeType a
SomeFunction (SomeSymbolic a -> SomeType a
forall a. SomeSymbolic a -> SomeType a
SomeSym (SomeSymbolic a -> SomeType a) -> SomeSymbolic a -> SomeType a
forall a b. (a -> b) -> a -> b
$ Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a t.
(Typeable t, SymbolicData a t) =>
Proxy t -> SomeSymbolic a
SomeData (Proxy (ArithmeticCircuit a) -> SomeSymbolic a)
-> Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(ArithmeticCircuit a))
        (SomeType a -> SomeType a) -> SomeType a -> SomeType a
forall a b. (a -> b) -> a -> b
$ SomeType a -> SomeType a -> SomeType a
forall a. SomeType a -> SomeType a -> SomeType a
SomeFunction (SomeSymbolic a -> SomeType a
forall a. SomeSymbolic a -> SomeType a
SomeSym (SomeSymbolic a -> SomeType a) -> SomeSymbolic a -> SomeType a
forall a b. (a -> b) -> a -> b
$ Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a t.
(Typeable t, SymbolicData a t) =>
Proxy t -> SomeSymbolic a
SomeData (Proxy (ArithmeticCircuit a) -> SomeSymbolic a)
-> Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(ArithmeticCircuit a))
        (SomeType a -> SomeType a) -> SomeType a -> SomeType a
forall a b. (a -> b) -> a -> b
$ SomeSymbolic a -> SomeType a
forall a. SomeSymbolic a -> SomeType a
SomeSym (SomeSymbolic a -> SomeType a) -> SomeSymbolic a -> SomeType a
forall a b. (a -> b) -> a -> b
$ Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a t.
(Typeable t, SymbolicData a t) =>
Proxy t -> SomeSymbolic a
SomeData (Proxy (ArithmeticCircuit a) -> SomeSymbolic a)
-> Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(ArithmeticCircuit a)
    builtinFunctionType BuiltinFunctions
MulField =
        SomeType a -> SomeType a -> SomeType a
forall a. SomeType a -> SomeType a -> SomeType a
SomeFunction (SomeSymbolic a -> SomeType a
forall a. SomeSymbolic a -> SomeType a
SomeSym (SomeSymbolic a -> SomeType a) -> SomeSymbolic a -> SomeType a
forall a b. (a -> b) -> a -> b
$ Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a t.
(Typeable t, SymbolicData a t) =>
Proxy t -> SomeSymbolic a
SomeData (Proxy (ArithmeticCircuit a) -> SomeSymbolic a)
-> Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(ArithmeticCircuit a))
        (SomeType a -> SomeType a) -> SomeType a -> SomeType a
forall a b. (a -> b) -> a -> b
$ SomeType a -> SomeType a -> SomeType a
forall a. SomeType a -> SomeType a -> SomeType a
SomeFunction (SomeSymbolic a -> SomeType a
forall a. SomeSymbolic a -> SomeType a
SomeSym (SomeSymbolic a -> SomeType a) -> SomeSymbolic a -> SomeType a
forall a b. (a -> b) -> a -> b
$ Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a t.
(Typeable t, SymbolicData a t) =>
Proxy t -> SomeSymbolic a
SomeData (Proxy (ArithmeticCircuit a) -> SomeSymbolic a)
-> Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(ArithmeticCircuit a))
        (SomeType a -> SomeType a) -> SomeType a -> SomeType a
forall a b. (a -> b) -> a -> b
$ SomeSymbolic a -> SomeType a
forall a. SomeSymbolic a -> SomeType a
SomeSym (SomeSymbolic a -> SomeType a) -> SomeSymbolic a -> SomeType a
forall a b. (a -> b) -> a -> b
$ Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a t.
(Typeable t, SymbolicData a t) =>
Proxy t -> SomeSymbolic a
SomeData (Proxy (ArithmeticCircuit a) -> SomeSymbolic a)
-> Proxy (ArithmeticCircuit a) -> SomeSymbolic a
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(ArithmeticCircuit a)

    builtinFunctionRep :: BuiltinFunctions -> SomeArithmetizable a
builtinFunctionRep BuiltinFunctions
AddField = (ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a)
-> SomeArithmetizable a
forall t a.
(Typeable t, Arithmetizable a t) =>
t -> SomeArithmetizable a
SomeArithmetizable ((ArithmeticCircuit a
  -> ArithmeticCircuit a -> ArithmeticCircuit a)
 -> SomeArithmetizable a)
-> (ArithmeticCircuit a
    -> ArithmeticCircuit a -> ArithmeticCircuit a)
-> SomeArithmetizable a
forall a b. (a -> b) -> a -> b
$ \(ArithmeticCircuit a
x :: ArithmeticCircuit a) (ArithmeticCircuit a
y :: ArithmeticCircuit a) -> ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveSemigroup a => a -> a -> a
+ ArithmeticCircuit a
y
    builtinFunctionRep BuiltinFunctions
MulField = (ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a)
-> SomeArithmetizable a
forall t a.
(Typeable t, Arithmetizable a t) =>
t -> SomeArithmetizable a
SomeArithmetizable ((ArithmeticCircuit a
  -> ArithmeticCircuit a -> ArithmeticCircuit a)
 -> SomeArithmetizable a)
-> (ArithmeticCircuit a
    -> ArithmeticCircuit a -> ArithmeticCircuit a)
-> SomeArithmetizable a
forall a b. (a -> b) -> a -> b
$ \(ArithmeticCircuit a
x :: ArithmeticCircuit a) (ArithmeticCircuit a
y :: ArithmeticCircuit a) -> ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. MultiplicativeSemigroup a => a -> a -> a
* ArithmeticCircuit a
y