Copyright	Copyright (c) 2016 the Hakaru team
License	BSD3
Maintainer	wren@community.haskell.org
Stability	experimental
Portability	GHC-only
Safe Haskell	None
Language	Haskell2010

Language.Hakaru.Syntax.AST.Eq

Contents

Orphan instances

Description

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.

Synopsis

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')
jmEq_Transform :: Transform args a -> Transform args a' -> Maybe (TypeEq a a')
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 ()
split :: [a] -> [(a, [a])]
zipWithSetM :: MonadPlus m => (a -> a -> m ()) -> [a] -> [a] -> m ()
zipWithSetMF :: (MonadPlus m, Foldable f) => (a -> a -> m ()) -> f a -> f a -> m ()
alphaEq :: forall abt d. ABT Term abt => abt '[] d -> abt '[] d -> Bool

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') Source #

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_Transform :: Transform args a -> Transform args a' -> Maybe (TypeEq a a') Source #

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

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

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

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

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

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

try_bool :: Bool -> ReaderT Varmap Maybe () Source #

split :: [a] -> [(a, [a])] Source #

zipWithSetM :: MonadPlus m => (a -> a -> m ()) -> [a] -> [a] -> m () Source #

zipWithSetMF :: (MonadPlus m, Foldable f) => (a -> a -> m ()) -> f a -> f a -> m () Source #

alphaEq :: forall abt d. ABT Term abt => abt '[] d -> abt '[] d -> Bool Source #

Orphan instances

(ABT Term abt, JmEq2 abt) => JmEq1 (Term abt :: Hakaru -> Type) Source #
Instance details Methods jmEq1 :: forall (i :: k) (j :: k). Term abt i -> Term abt j -> Maybe (TypeEq i j) Source #
(ABT Term abt, JmEq2 abt) => Eq1 (Term abt :: Hakaru -> Type) Source #
Instance details Methods eq1 :: forall (i :: k). Term abt i -> Term abt i -> Bool Source #
(Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type), JmEq1 (syn (TrivialABT syn)), Foldable21 syn) => JmEq1 (TrivialABT syn xs :: k -> Type) Source #
Instance details Methods jmEq1 :: forall (i :: k0) (j :: k0). TrivialABT syn xs i -> TrivialABT syn xs j -> Maybe (TypeEq i j) Source #
(Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type), Foldable21 syn, JmEq1 (syn (TrivialABT syn))) => Eq1 (TrivialABT syn xs :: k -> Type) Source #
Instance details Methods eq1 :: forall (i :: k0). TrivialABT syn xs i -> TrivialABT syn xs i -> Bool Source #
(Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type), JmEq1 (syn (TrivialABT syn)), Foldable21 syn) => JmEq2 (TrivialABT syn :: [k] -> k -> Type) Source #
Instance details Methods jmEq2 :: forall (i1 :: k1) (j1 :: k2) (i2 :: k1) (j2 :: k2). TrivialABT syn i1 j1 -> TrivialABT syn i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2) Source #
(Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type), Foldable21 syn, JmEq1 (syn (TrivialABT syn))) => Eq2 (TrivialABT syn :: [k] -> k -> Type) Source #
Instance details Methods eq2 :: forall (i :: k1) (j :: k2). TrivialABT syn i j -> TrivialABT syn i j -> Bool Source #
JmEq2 abt => JmEq1 (SArgs abt :: [([Hakaru], Hakaru)] -> Type) Source #
Instance details Methods jmEq1 :: forall (i :: k) (j :: k). SArgs abt i -> SArgs abt j -> Maybe (TypeEq i j) Source #
(ABT Term abt, JmEq2 abt) => Eq (Term abt a) Source #
Instance details Methods (==) :: Term abt a -> Term abt a -> Bool # (/=) :: Term abt a -> Term abt a -> Bool #
(Show1 (Sing :: k -> Type), JmEq1 (Sing :: k -> Type), Foldable21 syn, JmEq1 (syn (TrivialABT syn))) => Eq (TrivialABT syn xs a) Source #
Instance details Methods (==) :: TrivialABT syn xs a -> TrivialABT syn xs a -> Bool # (/=) :: TrivialABT syn xs a -> TrivialABT syn xs a -> Bool #