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

Safe HaskellNone
LanguageHaskell2010

Generics.MRSOP.Examples.LambdaAlphaEqTH

Contents

Description

Provide a generic alpha equality decider for the lambda calculus.

Synopsis

Documentation

data Term Source #

Standard Lambda Calculus.

Constructors

Var String 
Abs String Term 
App Term Term 

type FamTerm = '[Term] Source #

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

pattern Pat0Var :: PoA Singl (El FamTerm) '[K KString] -> NS (PoA Singl (El FamTerm)) '['[K KString], '[K KString, I Z], '[I Z, I Z]] Source #

pattern Pat0Abs :: PoA Singl (El FamTerm) '[K KString, I Z] -> NS (PoA Singl (El FamTerm)) '['[K KString], '[K KString, I Z], '[I Z, I Z]] Source #

pattern Pat0App :: PoA Singl (El FamTerm) '[I Z, I Z] -> NS (PoA Singl (El FamTerm)) '['[K KString], '[K KString, I Z], '[I Z, I Z]] Source #

pattern IdxTerm :: forall (a :: Nat). () => (~#) Nat 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.

Minimal complete definition

onNewScope, addRule, (=~=)

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 MonadAlphaEq

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

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

pattern Var_ :: forall kon (a :: kon -> *) (b :: Nat -> *) (c :: [[Atom kon]]). () => forall (n :: Nat) (x :: [Atom kon]) (xs :: [[Atom kon]]) (x1 :: Atom kon) (xs1 :: [Atom kon]) (k :: kon). ((~#) [[Atom kon]] [[Atom kon]] c ((:) [Atom kon] x xs), (~#) Nat Nat n Z, (~#) [Atom kon] [Atom kon] (Lkup [Atom kon] n c) ((:) (Atom kon) x1 xs1), (~#) (Atom kon) (Atom kon) x1 (K kon k), (~#) [Atom kon] [Atom kon] xs1 ([] (Atom kon))) => a k -> View kon a b c Source #

pattern Abs_ :: forall kon (a :: kon -> *) (b :: Nat -> *) (c :: [[Atom kon]]). () => forall (n :: Nat) (xs :: [[Atom kon]]) (n1 :: Nat) (x :: [Atom kon]) (x1 :: [Atom kon]) (xs1 :: [[Atom kon]]) (x2 :: Atom kon) (xs2 :: [Atom kon]) (k :: kon) (x3 :: Atom kon) (xs3 :: [Atom kon]) (k1 :: Nat). ((~#) [[Atom kon]] [[Atom kon]] c ((:) [Atom kon] x xs), (~#) Nat Nat n (S n1), (~#) [[Atom kon]] [[Atom kon]] xs ((:) [Atom kon] x1 xs1), (~#) Nat Nat n1 Z, (~#) [Atom kon] [Atom kon] (Lkup [Atom kon] n c) ((:) (Atom kon) x2 xs2), (~#) (Atom kon) (Atom kon) x2 (K kon k), (~#) [Atom kon] [Atom kon] xs2 ((:) (Atom kon) x3 xs3), (~#) (Atom kon) (Atom kon) x3 (I kon k1), IsNat k1, (~#) [Atom kon] [Atom kon] xs3 ([] (Atom kon))) => a k -> b k1 -> View kon a b c Source #

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

Decides whether or not two terms are alpha equivalent.

Tests

Orphan instances