{-# 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 (..))
class PlutusBuiltinFunction a fun where
builtinFunctionType :: fun -> SomeType a
builtinFunctionRep :: fun -> SomeArithmetizable a
data BuiltinFunctions =
AddField
| MulField
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