Generics.MRSOP.Examples.LambdaAlphaEqTH

Provide a generic alpha equality decider for the lambda calculus.

Documentation

data Term

Standard Lambda Calculus.

Constructors

Var String

Abs String Term

App Term Term

Instances

HasDatatypeInfo Kon Singl FamTerm CodesTerm

Methods

datatypeInfo :: Proxy [*] CodesTerm -> SNat ix -> DatatypeInfo Singl (Lkup [[Atom Singl]] ix codes)

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). () => (~#) Nat Nat a Z => SNat a

tyInfo_0 :: [Char]

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.

Minimal complete definition

onNewScope, addRule, (=~=)

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 MonadAlphaEq

Methods

onNewScope :: State [[(String, String)]] a -> State [[(String, String)]] a

addRule :: String -> String -> State [[(String, String)]] ()

(=~=) :: String -> String -> State [[(String, String)]] Bool

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

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.

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

Runs a computation.

Alpha equivalence for Lambda terms

type FIX = Fix Singl CodesTerm

alphaEq :: Term -> Term -> Bool

Decides whether or not two terms are alpha equivalent.

Tests

t1 :: String -> String -> Term

t2 :: String -> String -> String -> Char -> Term

Orphan instances

Family Kon Singl FamTerm CodesTerm

Methods

sfrom' :: SNat ix -> El CodesTerm ix -> Rep Singl FamTerm (El CodesTerm) (Lkup [[Atom Singl]] ix codes)

sto' :: SNat ix -> Rep Singl FamTerm (El CodesTerm) (Lkup [[Atom Singl]] ix codes) -> El CodesTerm ix