| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Generics.MRSOP.Examples.LambdaAlphaEqTH
Description
Provide a generic alpha equality decider for the lambda calculus.
Synopsis
- data Term
- type FamTerm = '[Term]
- type CodesTerm = '['['[K KString], '[K KString, I Z], '[I Z, I Z]]]
- pattern App_ :: phi Z -> phi Z -> View kon phi (Lkup Z CodesTerm)
- pattern Abs_ :: kon KString -> phi Z -> View kon phi (Lkup Z CodesTerm)
- pattern Var_ :: kon KString -> View kon phi (Lkup Z CodesTerm)
- pattern IdxTerm :: forall (a :: Nat). () => a ~# Z => SNat a
- tyInfo_0 :: [Char]
- class Monad m => MonadAlphaEq m where
- onHead :: (a -> a) -> [a] -> [a]
- onScope :: String -> String -> [[(String, String)]] -> Bool
- runAlpha :: State [[(String, String)]] a -> a
- type FIX = Fix Singl CodesTerm
- alphaEq :: Term -> Term -> Bool
- t1 :: String -> String -> Term
- t2 :: String -> String -> String -> Char -> Term
Documentation
Standard Lambda Calculus.
Instances
| Family Singl FamTerm CodesTerm # | |
| HasDatatypeInfo Singl FamTerm CodesTerm # | |
Defined in Generics.MRSOP.Examples.LambdaAlphaEqTH Methods datatypeInfo :: Proxy FamTerm -> SNat ix -> DatatypeInfo (Lkup ix CodesTerm) # | |
The alpha-eq monad
We will use an abstract monad for keeping track of scopes and name equivalences
class Monad m => MonadAlphaEq m where #
Interface needed for deciding alpha equivalence.
Methods
onNewScope :: m a -> m a #
Runs a computation under a new scope.
addRule :: String -> String -> m () #
Registers a name equivalence under the current scope.
(=~=) :: String -> String -> m Bool #
Checks for a name equivalence under all scopes.
Instances
| MonadAlphaEq (State [[(String, String)]]) # | One of the simplest monads that implement |
onScope :: String -> String -> [[(String, String)]] -> Bool #
Given a list of scopes, which consist in a list of pairs each, checks whether or not two names are equivalent.