generics-mrsop-2.0.0: Generic Programming with Mutually Recursive Sums of Products.

Safe HaskellNone




Provide a generic alpha equality decider for the lambda calculus.



type FamTerm = '[Term] Source #

type CodesTerm = '['['[K KString], '[K KString, I Z], '[I Z, I Z]]] Source #

pattern App_ :: phi Z -> phi Z -> View kon phi (Lkup Z CodesTerm) Source #

pattern Abs_ :: kon KString -> phi Z -> View kon phi (Lkup Z CodesTerm) Source #

pattern Var_ :: kon KString -> View kon phi (Lkup Z CodesTerm) Source #

pattern IdxTerm :: forall (a :: Nat). () => a ~# Z => SNat a Source #

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.


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.

MonadAlphaEq (State [[(String, String)]]) Source #

One of the simplest monads that implement MonadAlphaEq

Instance details

Defined in Generics.MRSOP.Examples.LambdaAlphaEqTH

onHead :: (a -> a) -> [a] -> [a] Source #

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.

runAlpha :: State [[(String, String)]] a -> a Source #

Runs a computation.

Alpha equivalence for Lambda terms

alphaEq :: Term -> Term -> Bool Source #

Decides whether or not two terms are alpha equivalent.


Orphan instances

Family Singl FamTerm CodesTerm Source # 
Instance details