{-# LANGUAGE AllowAmbiguousTypes #-}
module ZkFold.Symbolic.Cardano.UPLC.Term where
import Data.Maybe (fromJust)
import Data.Typeable (Typeable, cast, typeOf)
import Prelude
import ZkFold.Symbolic.Compiler (SymbolicData)
data Term name fun a where
Var :: name -> Term name fun a
LamAbs :: name -> Term name fun a -> Term name fun a
Apply :: Term name fun a -> Term name fun a -> Term name fun a
Force :: Term name fun a -> Term name fun a
Delay :: Term name fun a -> Term name fun a
Constant :: (Eq c, Typeable c, SymbolicData a c) => c -> Term name fun a
Builtin :: fun -> Term name fun a
Error :: Term name fun a
instance (Eq name, Eq fun) => Eq (Term name fun a) where
Var name
x == :: Term name fun a -> Term name fun a -> Bool
== Var name
y = name
x name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
y
LamAbs name
x Term name fun a
f == LamAbs name
y Term name fun a
g = name
x name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
y Bool -> Bool -> Bool
&& Term name fun a
f Term name fun a -> Term name fun a -> Bool
forall a. Eq a => a -> a -> Bool
== Term name fun a
g
Apply Term name fun a
f Term name fun a
x == Apply Term name fun a
g Term name fun a
y = Term name fun a
f Term name fun a -> Term name fun a -> Bool
forall a. Eq a => a -> a -> Bool
== Term name fun a
g Bool -> Bool -> Bool
&& Term name fun a
x Term name fun a -> Term name fun a -> Bool
forall a. Eq a => a -> a -> Bool
== Term name fun a
y
Force Term name fun a
x == Force Term name fun a
y = Term name fun a
x Term name fun a -> Term name fun a -> Bool
forall a. Eq a => a -> a -> Bool
== Term name fun a
y
Delay Term name fun a
x == Delay Term name fun a
y = Term name fun a
x Term name fun a -> Term name fun a -> Bool
forall a. Eq a => a -> a -> Bool
== Term name fun a
y
Constant c
x == Constant c
y
| c -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf c
x TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== c -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf c
y = c
x c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe c -> c
forall a. HasCallStack => Maybe a -> a
fromJust (c -> Maybe c
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast c
y)
| Bool
otherwise = Bool
False
Builtin fun
x == Builtin fun
y = fun
x fun -> fun -> Bool
forall a. Eq a => a -> a -> Bool
== fun
y
Term name fun a
Error == Term name fun a
Error = Bool
True
Term name fun a
_ == Term name fun a
_ = Bool
False