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

module ZkFold.Symbolic.Cardano.UPLC.Type where

import           Data.Kind                (Type)
import           Data.Typeable            (Proxy (..), TypeRep, Typeable, typeOf)
import           Prelude

import           ZkFold.Symbolic.Compiler (Arithmetizable, SymbolicData)

data SomeType a where
    NoType         :: SomeType a
    AnyType        :: SomeType a
    AnyBuiltinType :: SomeType a
    SomeSym        :: SomeSymbolic a -> SomeType a
    SomeFunction   :: SomeType a -> SomeType a -> SomeType a

instance Eq (SomeType a) where
    SomeType a
NoType == :: SomeType a -> SomeType a -> Bool
== SomeType a
NoType                         = Bool
True
    SomeType a
AnyType == SomeType a
AnyType                       = Bool
True
    SomeType a
AnyBuiltinType == SomeType a
AnyBuiltinType         = Bool
True
    SomeSym SomeSymbolic a
x == SomeSym SomeSymbolic a
y                   = SomeSymbolic a
x SomeSymbolic a -> SomeSymbolic a -> Bool
forall a. Eq a => a -> a -> Bool
== SomeSymbolic a
y
    SomeFunction SomeType a
x1 SomeType a
x2 == SomeFunction SomeType a
y1 SomeType a
y2 = SomeType a
x1 SomeType a -> SomeType a -> Bool
forall a. Eq a => a -> a -> Bool
== SomeType a
y1 Bool -> Bool -> Bool
&& SomeType a
x2 SomeType a -> SomeType a -> Bool
forall a. Eq a => a -> a -> Bool
== SomeType a
y2
    SomeType a
_ == SomeType a
_                                   = Bool
False

instance Semigroup (SomeType a) where
    SomeType a
NoType <> :: SomeType a -> SomeType a -> SomeType a
<> SomeType a
t                              = SomeType a
t
    SomeType a
t <> SomeType a
NoType                              = SomeType a
t
    SomeType a
AnyType <> SomeType a
t                             = SomeType a
t
    SomeType a
t <> SomeType a
AnyType                             = SomeType a
t
    SomeType a
AnyBuiltinType <> SomeType a
t                      = SomeType a
t
    SomeType a
t <> SomeType a
AnyBuiltinType                      = SomeType a
t
    SomeSym SomeSymbolic a
t1 <> SomeSym SomeSymbolic a
t2                 = SomeSymbolic a -> SomeType a
forall a. SomeSymbolic a -> SomeType a
SomeSym (SomeSymbolic a
t1 SomeSymbolic a -> SomeSymbolic a -> SomeSymbolic a
forall a. Semigroup a => a -> a -> a
<> SomeSymbolic a
t2)
    SomeFunction SomeType a
t1 SomeType a
t2 <> SomeFunction SomeType a
t3 SomeType a
t4 = SomeType a -> SomeType a -> SomeType a
forall a. SomeType a -> SomeType a -> SomeType a
SomeFunction (SomeType a
t1 SomeType a -> SomeType a -> SomeType a
forall a. Semigroup a => a -> a -> a
<> SomeType a
t3) (SomeType a
t2 SomeType a -> SomeType a -> SomeType a
forall a. Semigroup a => a -> a -> a
<> SomeType a
t4)
    SomeType a
_ <> SomeType a
_                                   = [Char] -> SomeType a
forall a. HasCallStack => [Char] -> a
error [Char]
"Semigroup (SomeType a): constructor mismatch"

data SomeSymbolic a where
    SomeData  :: forall a (t :: Type) . (Typeable t, SymbolicData a t) => Proxy t -> SomeSymbolic a
    SomeArith :: forall a (t :: Type) . (Typeable t, Arithmetizable a t) => Proxy t -> SomeSymbolic a

getType :: SomeSymbolic a -> TypeRep
getType :: forall a. SomeSymbolic a -> TypeRep
getType (SomeData Proxy t
t)  = Proxy t -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Proxy t
t
getType (SomeArith Proxy t
t) = Proxy t -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Proxy t
t

instance Eq (SomeSymbolic a) where
    SomeSymbolic a
x == :: SomeSymbolic a -> SomeSymbolic a -> Bool
== SomeSymbolic a
y = SomeSymbolic a -> TypeRep
forall a. SomeSymbolic a -> TypeRep
getType SomeSymbolic a
x TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== SomeSymbolic a -> TypeRep
forall a. SomeSymbolic a -> TypeRep
getType SomeSymbolic a
y

instance Semigroup (SomeSymbolic a) where
    SomeData Proxy t
x <> :: SomeSymbolic a -> SomeSymbolic a -> SomeSymbolic a
<> SomeSymbolic a
y
      | Proxy t -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Proxy t
x TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== SomeSymbolic a -> TypeRep
forall a. SomeSymbolic a -> TypeRep
getType SomeSymbolic a
y = Proxy t -> SomeSymbolic a
forall a t.
(Typeable t, SymbolicData a t) =>
Proxy t -> SomeSymbolic a
SomeData Proxy t
x
      | Bool
otherwise = [Char] -> SomeSymbolic a
forall a. HasCallStack => [Char] -> a
error [Char]
"Semigroup (SomeSymbolic a): SomeData mismatch"
    SomeSymbolic a
x <> SomeData Proxy t
y
      | SomeSymbolic a -> TypeRep
forall a. SomeSymbolic a -> TypeRep
getType SomeSymbolic a
x TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy t -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Proxy t
y = Proxy t -> SomeSymbolic a
forall a t.
(Typeable t, SymbolicData a t) =>
Proxy t -> SomeSymbolic a
SomeData Proxy t
y
      | Bool
otherwise = [Char] -> SomeSymbolic a
forall a. HasCallStack => [Char] -> a
error [Char]
"Semigroup (SomeSymbolic a): SomeData mismatch"
    SomeArith Proxy t
x <> SomeArith Proxy t
y
      | Proxy t -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Proxy t
x TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy t -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Proxy t
y = Proxy t -> SomeSymbolic a
forall a t.
(Typeable t, Arithmetizable a t) =>
Proxy t -> SomeSymbolic a
SomeArith Proxy t
x
      | Bool
otherwise = [Char] -> SomeSymbolic a
forall a. HasCallStack => [Char] -> a
error [Char]
"Semigroup (SomeSymbolic a): SomeArith mismatch"

symToSym :: SomeSymbolic a -> SomeSymbolic a -> SomeSymbolic a
symToSym :: forall a. SomeSymbolic a -> SomeSymbolic a -> SomeSymbolic a
symToSym (SomeData (Proxy t
_ :: Proxy x)) (SomeData (Proxy t
_ :: Proxy y))  = Proxy (t -> t) -> SomeSymbolic a
forall a t.
(Typeable t, Arithmetizable a t) =>
Proxy t -> SomeSymbolic a
SomeArith (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(x -> y))
symToSym (SomeData (Proxy t
_ :: Proxy x)) (SomeArith (Proxy t
_ :: Proxy y)) = Proxy (t -> t) -> SomeSymbolic a
forall a t.
(Typeable t, Arithmetizable a t) =>
Proxy t -> SomeSymbolic a
SomeArith (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(x -> y))
symToSym (SomeArith Proxy t
_) SomeSymbolic a
_                                      = [Char] -> SomeSymbolic a
forall a. HasCallStack => [Char] -> a
error [Char]
"symToSym: cannot make a conversion"

-- TODO: add support for polymorphic types
functionToData :: SomeType a -> SomeType a
functionToData :: forall a. SomeType a -> SomeType a
functionToData (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 SomeSymbolic a
x, SomeSym SomeSymbolic a
y) -> SomeSymbolic a -> SomeType a
forall a. SomeSymbolic a -> SomeType a
SomeSym (SomeSymbolic a -> SomeSymbolic a -> SomeSymbolic a
forall a. SomeSymbolic a -> SomeSymbolic a -> SomeSymbolic a
symToSym SomeSymbolic a
x SomeSymbolic a
y)
        (SomeType a, SomeType a)
_                      -> [Char] -> SomeType a
forall a. HasCallStack => [Char] -> a
error [Char]
"functionToData: cannot make a conversion"
functionToData SomeType a
t = SomeType a
t