{-# 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 (..))

-- TODO: we need to figure out what to do with error terms

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"