{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Data.Eq.Structural where

import           Data.Functor.Rep           (Representable)
import           Data.Proxy                 (Proxy (..))
import           Data.Traversable           (Traversable)
import           Prelude                    (type (~))

import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Eq

newtype Structural a = Structural a
-- ^ A newtype wrapper for easy definition of Eq instances.

instance
    ( SymbolicData x
    , Context x ~ c
    , Support x ~ Proxy c
    , Symbolic c
    , Representable (Layout x)
    , Traversable (Layout x)
    ) => Eq (Bool c) (Structural x) where

    Structural x
x == :: Structural x -> Structural x -> Bool c
== Structural x
y =
        let x' :: Context x (Layout x)
x' = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
x Proxy c
Support x
forall {k} (t :: k). Proxy t
Proxy
            y' :: Context x (Layout x)
y' = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
y Proxy c
Support x
forall {k} (t :: k). Proxy t
Proxy
         in c (Layout x)
Context x (Layout x)
x' c (Layout x) -> c (Layout x) -> Bool c
forall b a. Eq b a => a -> a -> b
== c (Layout x)
Context x (Layout x)
y'

    Structural x
x /= :: Structural x -> Structural x -> Bool c
/= Structural x
y =
        let x' :: Context x (Layout x)
x' = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
x Proxy c
Support x
forall {k} (t :: k). Proxy t
Proxy
            y' :: Context x (Layout x)
y' = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
y Proxy c
Support x
forall {k} (t :: k). Proxy t
Proxy
         in c (Layout x)
Context x (Layout x)
x' c (Layout x) -> c (Layout x) -> Bool c
forall b a. Eq b a => a -> a -> b
/= c (Layout x)
Context x (Layout x)
y'