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

-- Based on the November 2022 UPLC spec
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