Language.Hakaru.Syntax.AST.Eq

Warning: The following module is for testing purposes only. Using the JmEq1 instance for Term is inefficient and should not be done accidentally. To implement that (orphan) instance we also provide the following (orphan) instances:

SArgs      : JmEq1
Term       : JmEq1, Eq1, Eq
TrivialABT : JmEq2, JmEq1, Eq2, Eq1, Eq

TODO: because this is only for testing, everything else should move to the Tests directory.

Documentation

jmEq_S :: (ABT Term abt, JmEq2 abt) => SCon args a -> SArgs abt args -> SCon args' a' -> SArgs abt args' -> Maybe (TypeEq a a', TypeEq args args')

This function performs jmEq on a (:$) node of the AST. It's necessary to break it out like this since we can't just give a JmEq1 instance for SCon due to polymorphism issues (e.g., we can't just say that Lam_ is John Major equal to Lam_, since they may be at different types). However, once the SArgs associated with the SCon is given, that resolves the polymorphism.

jmEq_Branch :: (ABT Term abt, JmEq2 abt) => [(Branch a abt b, Branch a abt b')] -> Maybe (TypeEq b b')

all_jmEq2 :: (ABT Term abt, JmEq2 abt) => Seq (abt '[] a) -> Seq (abt '[] a) -> Maybe ()

jmEq_Tuple :: (ABT Term abt, JmEq2 abt) => ((abt '[] a, abt '[] b), (abt '[] a', abt '[] b')) -> Maybe (TypeEq a a', TypeEq b b')

type Varmap = Assocs (Variable :: Hakaru -> *)

void_jmEq1 :: Sing (a :: Hakaru) -> Sing (b :: Hakaru) -> ReaderT Varmap Maybe ()

void_varEq :: Variable (a :: Hakaru) -> Variable (b :: Hakaru) -> ReaderT Varmap Maybe ()

try_bool :: Bool -> ReaderT Varmap Maybe ()

alphaEq :: forall abt a. ABT Term abt => abt '[] a -> abt '[] a -> Bool

Orphan instances

(ABT Hakaru Term abt, JmEq2 Hakaru [Hakaru] abt) => JmEq1 Hakaru (Term abt)

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq (Term abt) i j)

(ABT Hakaru Term abt, JmEq2 Hakaru [Hakaru] abt) => Eq1 Hakaru (Term abt)

Methods

eq1 :: a i -> a i -> Bool

(Show1 k (Sing k), JmEq1 k (Sing k), JmEq1 k (syn (TrivialABT k syn)), Foldable21 k k [k] syn) => JmEq2 k [k] (TrivialABT k syn)

Methods

jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq (TrivialABT k syn) j1 j2)

(Show1 k (Sing k), JmEq1 k (Sing k), Foldable21 k k [k] syn, JmEq1 k (syn (TrivialABT k syn))) => Eq2 k [k] (TrivialABT k syn)

Methods

eq2 :: a i j -> a i j -> Bool

(Show1 k (Sing k), JmEq1 k (Sing k), JmEq1 k (syn (TrivialABT k syn)), Foldable21 k k [k] syn) => JmEq1 k (TrivialABT k syn xs)

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq (TrivialABT k syn xs) i j)

(Show1 k (Sing k), JmEq1 k (Sing k), Foldable21 k k [k] syn, JmEq1 k (syn (TrivialABT k syn))) => Eq1 k (TrivialABT k syn xs)

Methods

eq1 :: a i -> a i -> Bool

JmEq2 Hakaru [Hakaru] abt => JmEq1 [([Hakaru], Hakaru)] (SArgs abt)

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq (SArgs abt) i j)

(ABT Hakaru Term abt, JmEq2 Hakaru [Hakaru] abt) => Eq (Term abt a)

Methods

(==) :: Term abt a -> Term abt a -> Bool

(/=) :: Term abt a -> Term abt a -> Bool

(Show1 k (Sing k), JmEq1 k (Sing k), Foldable21 k k [k] syn, JmEq1 k (syn (TrivialABT k syn))) => Eq (TrivialABT k syn xs a)

Methods

(==) :: TrivialABT k syn xs a -> TrivialABT k syn xs a -> Bool

(/=) :: TrivialABT k syn xs a -> TrivialABT k syn xs a -> Bool