| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Generics.MRSOP.Examples.LambdaAlphaEqTH
Description
Provide a generic alpha equality decider for the lambda calculus.
- data Term
- type FamTerm = '[Term]
- type CodesTerm = '['['[K KString], '[K KString, I Z], '[I Z, I Z]]]
- pattern Pat0Var :: PoA Singl (El FamTerm) '[K KString] -> NS (PoA Singl (El FamTerm)) '['[K KString], '[K KString, I Z], '[I Z, I Z]]
- 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]]
- 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]]
- pattern IdxTerm :: forall (a :: Nat). () => (~#) Nat 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
- pattern Term_ :: forall (a :: Nat). () => (~#) Nat Nat a Z => SNat a
- 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
- 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
- alphaEq :: Term -> Term -> Bool
- t1 :: String -> String -> Term
- t2 :: String -> String -> String -> Char -> Term
Documentation
Standard Lambda Calculus.
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 #
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
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.
Alpha equivalence for Lambda terms
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 #