| 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.
The alpha-eq monad
We will use an abstract monad for keeping track of scopes and name equivalences
class Monad m => MonadAlphaEq m where Source #
Interface needed for deciding alpha equivalence.
Methods
onNewScope :: m a -> m a Source #
Runs a computation under a new scope.
addRule :: String -> String -> m () Source #
Registers a name equivalence under the current scope.
(=~=) :: String -> String -> m Bool Source #
Checks for a name equivalence under all scopes.
Instances
| MonadAlphaEq (State [[(String, String)]]) Source # | One of the simplest monads that implement |
onScope :: String -> String -> [[(String, String)]] -> Bool Source #
Given a list of scopes, which consist in a list of pairs each, checks whether or not two names are equivalent.