| 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
Description
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.
- 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_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
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_Branch :: (ABT Term abt, JmEq2 abt) => [(Branch a abt b, Branch a abt b')] -> Maybe (TypeEq b b') Source #
jmEq_Tuple :: (ABT Term abt, JmEq2 abt) => ((abt '[] a, abt '[] b), (abt '[] a', abt '[] b')) -> Maybe (TypeEq a a', TypeEq b b') Source #