{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module ZkFold.Symbolic.Cardano.UPLC where
import Data.Kind (Type)
import Data.Maybe (fromJust)
import Data.Typeable (Proxy (..), Typeable, cast)
import Prelude (Eq (..), error, otherwise, snd, ($))
import ZkFold.Symbolic.Cardano.UPLC.Builtins
import ZkFold.Symbolic.Cardano.UPLC.Inference
import ZkFold.Symbolic.Cardano.UPLC.Term
import ZkFold.Symbolic.Cardano.UPLC.Type
import ZkFold.Symbolic.Compiler (Arithmetic, Arithmetizable (..), SomeArithmetizable (..),
SymbolicData (..))
data ArgList name a where
ArgListEmpty :: ArgList name a
ArgListCons :: (Typeable t, SymbolicData a t) => (name, t) -> ArgList name a -> ArgList name a
class FromUPLC name fun a where
fromUPLC :: ArgList name a -> Term name fun a -> SomeArithmetizable a
instance forall name fun (a :: Type) . (Eq name, Typeable name, Typeable fun, Eq fun, PlutusBuiltinFunction a fun, Typeable a) => FromUPLC name fun a where
fromUPLC :: ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC ArgList name a
ArgListEmpty (Var name
_) = [Char] -> SomeArithmetizable a
forall a. HasCallStack => [Char] -> a
error [Char]
"fromUPLC: unknown variable"
fromUPLC (ArgListCons (name
x, t
t) ArgList name a
xs) (Var name
y)
| name
x name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
y = t -> SomeArithmetizable a
forall t a.
(Typeable t, Arithmetizable a t) =>
t -> SomeArithmetizable a
SomeArithmetizable t
t
| Bool
otherwise = forall name fun a.
FromUPLC name fun a =>
ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC @name @fun ArgList name a
xs (name -> Term name fun a
forall name fun a. name -> Term name fun a
Var name
y)
fromUPLC ArgList name a
args term :: Term name fun a
term@(LamAbs name
x Term name fun a
f) =
case (Term name fun a, SomeType a) -> SomeType a
forall a b. (a, b) -> b
snd ((Term name fun a, SomeType a) -> SomeType a)
-> (Term name fun a, SomeType a) -> SomeType a
forall a b. (a -> b) -> a -> b
$ forall name fun a.
(Eq name, Eq fun, PlutusBuiltinFunction a fun) =>
Term name fun a -> (Term name fun a, SomeType a)
inferTypes @name @fun Term name fun a
term of
SomeFunction SomeType a
t1 SomeType a
t2 ->
let t1' :: SomeType a
t1' = SomeType a -> SomeType a
forall a. SomeType a -> SomeType a
functionToData SomeType a
t1
t2' :: SomeType a
t2' = SomeType a -> SomeType a
forall a. SomeType a -> SomeType a
functionToData SomeType a
t2
in case (SomeType a
t1', SomeType a
t2') of
(SomeSym (SomeData (Proxy t
_ :: Proxy t1)), SomeSym (SomeArith (Proxy t
_ :: Proxy t2))) ->
(t -> t) -> SomeArithmetizable a
forall t a.
(Typeable t, Arithmetizable a t) =>
t -> SomeArithmetizable a
SomeArithmetizable ((t -> t) -> SomeArithmetizable a)
-> (t -> t) -> SomeArithmetizable a
forall a b. (a -> b) -> a -> b
$ \(t
arg :: t1) ->
case ArgList name a -> Term name fun a -> SomeArithmetizable a
forall name fun a.
FromUPLC name fun a =>
ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC ((name, t) -> ArgList name a -> ArgList name a
forall t a name.
(Typeable t, SymbolicData a t) =>
(name, t) -> ArgList name a -> ArgList name a
ArgListCons (name
x, t
arg) ArgList name a
args) Term name fun a
f of
SomeArithmetizable t
res -> Maybe t -> t
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe t -> t) -> Maybe t -> t
forall a b. (a -> b) -> a -> b
$ forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @_ @t2 t
res
(SomeSym (SomeData (Proxy t
_ :: Proxy t1)), SomeSym (SomeData (Proxy t
_ :: Proxy t2))) ->
(t -> t) -> SomeArithmetizable a
forall t a.
(Typeable t, Arithmetizable a t) =>
t -> SomeArithmetizable a
SomeArithmetizable ((t -> t) -> SomeArithmetizable a)
-> (t -> t) -> SomeArithmetizable a
forall a b. (a -> b) -> a -> b
$ \(t
arg :: t1) ->
case ArgList name a -> Term name fun a -> SomeArithmetizable a
forall name fun a.
FromUPLC name fun a =>
ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC ((name, t) -> ArgList name a -> ArgList name a
forall t a name.
(Typeable t, SymbolicData a t) =>
(name, t) -> ArgList name a -> ArgList name a
ArgListCons (name
x, t
arg) ArgList name a
args) Term name fun a
f of
SomeArithmetizable t
res -> Maybe t -> t
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe t -> t) -> Maybe t -> t
forall a b. (a -> b) -> a -> b
$ forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @_ @t2 t
res
(SomeType a, SomeType a)
_ -> [Char] -> SomeArithmetizable a
forall a. HasCallStack => [Char] -> a
error [Char]
"fromUPLC: LamAbs"
SomeType a
_ -> [Char] -> SomeArithmetizable a
forall a. HasCallStack => [Char] -> a
error [Char]
"fromUPLC: LamAbs"
fromUPLC ArgList name a
args (Apply Term name fun a
f Term name fun a
x) =
case (Term name fun a, SomeType a) -> SomeType a
forall a b. (a, b) -> b
snd ((Term name fun a, SomeType a) -> SomeType a)
-> (Term name fun a, SomeType a) -> SomeType a
forall a b. (a -> b) -> a -> b
$ forall name fun a.
(Eq name, Eq fun, PlutusBuiltinFunction a fun) =>
Term name fun a -> (Term name fun a, SomeType a)
inferTypes @name @fun Term name fun a
f of
SomeFunction SomeType a
t1 SomeType a
t2 ->
let t1' :: SomeType a
t1' = SomeType a -> SomeType a
forall a. SomeType a -> SomeType a
functionToData SomeType a
t1
t2' :: SomeType a
t2' = SomeType a -> SomeType a
forall a. SomeType a -> SomeType a
functionToData SomeType a
t2
in case (SomeType a
t1', SomeType a
t2', ArgList name a -> Term name fun a -> SomeArithmetizable a
forall name fun a.
FromUPLC name fun a =>
ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC ArgList name a
args Term name fun a
f, ArgList name a -> Term name fun a -> SomeArithmetizable a
forall name fun a.
FromUPLC name fun a =>
ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC ArgList name a
args Term name fun a
x) of
(SomeSym (SomeData (Proxy t
_ :: Proxy t1)), SomeSym (SomeArith (Proxy t
_ :: Proxy t2)), SomeArithmetizable t
f', SomeArithmetizable t
x') ->
t -> SomeArithmetizable a
forall t a.
(Typeable t, Arithmetizable a t) =>
t -> SomeArithmetizable a
SomeArithmetizable ((Maybe (t -> t) -> t -> t
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (t -> t) -> t -> t) -> Maybe (t -> t) -> t -> t
forall a b. (a -> b) -> a -> b
$ forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @_ @(t1 -> t2) t
f') (Maybe t -> t
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe t -> t) -> Maybe t -> t
forall a b. (a -> b) -> a -> b
$ forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @_ @t1 t
x') :: t2)
(SomeSym (SomeData (Proxy t
_ :: Proxy t1)), SomeSym (SomeData (Proxy t
_ :: Proxy t2)), SomeArithmetizable t
f', SomeArithmetizable t
x') ->
t -> SomeArithmetizable a
forall t a.
(Typeable t, Arithmetizable a t) =>
t -> SomeArithmetizable a
SomeArithmetizable ((Maybe (t -> t) -> t -> t
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (t -> t) -> t -> t) -> Maybe (t -> t) -> t -> t
forall a b. (a -> b) -> a -> b
$ forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @_ @(t1 -> t2) t
f') (Maybe t -> t
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe t -> t) -> Maybe t -> t
forall a b. (a -> b) -> a -> b
$ forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast @_ @t1 t
x') :: t2)
(SomeType a, SomeType a, SomeArithmetizable a,
SomeArithmetizable a)
_ -> [Char] -> SomeArithmetizable a
forall a. HasCallStack => [Char] -> a
error [Char]
"fromUPLC: Apply"
SomeType a
_ -> [Char] -> SomeArithmetizable a
forall a. HasCallStack => [Char] -> a
error [Char]
"fromUPLC: Apply"
fromUPLC ArgList name a
args (Force Term name fun a
t) = ArgList name a -> Term name fun a -> SomeArithmetizable a
forall name fun a.
FromUPLC name fun a =>
ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC ArgList name a
args Term name fun a
t
fromUPLC ArgList name a
args (Delay Term name fun a
t) = ArgList name a -> Term name fun a -> SomeArithmetizable a
forall name fun a.
FromUPLC name fun a =>
ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC ArgList name a
args Term name fun a
t
fromUPLC ArgList name a
_ (Constant c
c) = c -> SomeArithmetizable a
forall t a.
(Typeable t, Arithmetizable a t) =>
t -> SomeArithmetizable a
SomeArithmetizable c
c
fromUPLC ArgList name a
_ (Builtin fun
b) = fun -> SomeArithmetizable a
forall a fun.
PlutusBuiltinFunction a fun =>
fun -> SomeArithmetizable a
builtinFunctionRep fun
b
fromUPLC ArgList name a
_ Term name fun a
Error = [Char] -> SomeArithmetizable a
forall a. HasCallStack => [Char] -> a
error [Char]
"fromUPLC: Error"
instance forall name (a :: Type) . (Typeable name, Eq name, Eq BuiltinFunctions, Typeable a, Arithmetic a)
=> Arithmetizable a (Term name BuiltinFunctions a) where
arithmetize :: Term name BuiltinFunctions a
-> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
arithmetize Term name BuiltinFunctions a
term = case forall name fun a.
FromUPLC name fun a =>
ArgList name a -> Term name fun a -> SomeArithmetizable a
fromUPLC @name @_ @a ArgList name a
forall name a. ArgList name a
ArgListEmpty Term name BuiltinFunctions a
term of
SomeArithmetizable t
t -> t -> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
forall a x.
Arithmetizable a x =>
x -> [ArithmeticCircuit a] -> [ArithmeticCircuit a]
arithmetize t
t
inputSize :: Natural
inputSize = [Char] -> Natural
forall a. HasCallStack => [Char] -> a
error [Char]
"inputSize Term: not implemented"
outputSize :: Natural
outputSize = [Char] -> Natural
forall a. HasCallStack => [Char] -> a
error [Char]
"outputSize Term: not implemented"