{-# 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"
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