Generics.MRSOP.Examples.SimpTH

Contents

• Simple IMPerative Language:
• Alpha Equality Functionality
  • Zipper test
• Orphan instances

Description

Synopsis

• data Stmt var
  • = SAssign var (Exp var)
  • | SIf (Exp var) (Stmt var) (Stmt var)
  • | SSeq (Stmt var) (Stmt var)
  • | SReturn (Exp var)
  • | SDecl (Decl var)
  • | SSkip
• data Decl var
  • = DVar var
  • | DFun var var (Stmt var)
• data Exp var
  • = EVar var
  • | ECall var (Exp var)
  • | EAdd (Exp var) (Exp var)
  • | ESub (Exp var) (Exp var)
  • | ELit Int
• type FamStmtString = '[Stmt String, Exp String, Decl String]
• type CodesStmtString = '['['[K KString, I (S Z)], '[I (S Z), I Z, I Z], '[I Z, I Z], '[I (S Z)], '[I (S (S Z))], '[]], '['[K KString], '[K KString, I (S Z)], '[I (S Z), I (S Z)], '[I (S Z), I (S Z)], '[K KInt]], '['[K KString], '[K KString, K KString, I Z]]]
• pattern Pat0SAssign :: PoA Singl (El FamStmtString) '[K KString, I (S Z)] -> NS (PoA Singl (El FamStmtString)) '['[K KString, I (S Z)], '[I (S Z), I Z, I Z], '[I Z, I Z], '[I (S Z)], '[I (S (S Z))], '[]]
• pattern Pat0SIf :: PoA Singl (El FamStmtString) '[I (S Z), I Z, I Z] -> NS (PoA Singl (El FamStmtString)) '['[K KString, I (S Z)], '[I (S Z), I Z, I Z], '[I Z, I Z], '[I (S Z)], '[I (S (S Z))], '[]]
• pattern Pat0SSeq :: PoA Singl (El FamStmtString) '[I Z, I Z] -> NS (PoA Singl (El FamStmtString)) '['[K KString, I (S Z)], '[I (S Z), I Z, I Z], '[I Z, I Z], '[I (S Z)], '[I (S (S Z))], '[]]
• pattern Pat0SReturn :: PoA Singl (El FamStmtString) '[I (S Z)] -> NS (PoA Singl (El FamStmtString)) '['[K KString, I (S Z)], '[I (S Z), I Z, I Z], '[I Z, I Z], '[I (S Z)], '[I (S (S Z))], '[]]
• pattern Pat0SDecl :: PoA Singl (El FamStmtString) '[I (S (S Z))] -> NS (PoA Singl (El FamStmtString)) '['[K KString, I (S Z)], '[I (S Z), I Z, I Z], '[I Z, I Z], '[I (S Z)], '[I (S (S Z))], '[]]
• pattern Pat0SSkip :: PoA Singl (El FamStmtString) '[] -> NS (PoA Singl (El FamStmtString)) '['[K KString, I (S Z)], '[I (S Z), I Z, I Z], '[I Z, I Z], '[I (S Z)], '[I (S (S Z))], '[]]
• pattern Pat1EVar :: PoA Singl (El FamStmtString) '[K KString] -> NS (PoA Singl (El FamStmtString)) '['[K KString], '[K KString, I (S Z)], '[I (S Z), I (S Z)], '[I (S Z), I (S Z)], '[K KInt]]
• pattern Pat1ECall :: PoA Singl (El FamStmtString) '[K KString, I (S Z)] -> NS (PoA Singl (El FamStmtString)) '['[K KString], '[K KString, I (S Z)], '[I (S Z), I (S Z)], '[I (S Z), I (S Z)], '[K KInt]]
• pattern Pat1EAdd :: PoA Singl (El FamStmtString) '[I (S Z), I (S Z)] -> NS (PoA Singl (El FamStmtString)) '['[K KString], '[K KString, I (S Z)], '[I (S Z), I (S Z)], '[I (S Z), I (S Z)], '[K KInt]]
• pattern Pat1ESub :: PoA Singl (El FamStmtString) '[I (S Z), I (S Z)] -> NS (PoA Singl (El FamStmtString)) '['[K KString], '[K KString, I (S Z)], '[I (S Z), I (S Z)], '[I (S Z), I (S Z)], '[K KInt]]
• pattern Pat1ELit :: PoA Singl (El FamStmtString) '[K KInt] -> NS (PoA Singl (El FamStmtString)) '['[K KString], '[K KString, I (S Z)], '[I (S Z), I (S Z)], '[I (S Z), I (S Z)], '[K KInt]]
• pattern Pat2DVar :: PoA Singl (El FamStmtString) '[K KString] -> NS (PoA Singl (El FamStmtString)) '['[K KString], '[K KString, K KString, I Z]]
• pattern Pat2DFun :: PoA Singl (El FamStmtString) '[K KString, K KString, I Z] -> NS (PoA Singl (El FamStmtString)) '['[K KString], '[K KString, K KString, I Z]]
• pattern IdxDeclString :: forall (a :: Nat). () => forall (n :: Nat) (n1 :: Nat). ((~#) Nat Nat a (S n), (~#) Nat Nat n (S n1), (~#) Nat Nat n1 Z) => SNat a
• pattern IdxExpString :: forall (a :: Nat). () => forall (n :: Nat). ((~#) Nat Nat a (S n), (~#) Nat Nat n Z) => SNat a
• pattern IdxStmtString :: forall (a :: Nat). () => (~#) Nat Nat a Z => SNat a
• tyInfo_2 :: [Char]
• tyInfo_1 :: [Char]
• tyInfo_0 :: [Char]
• pattern Decl_ :: forall (a :: Nat). () => forall (n :: Nat) (n1 :: Nat). ((~#) Nat Nat a (S n), (~#) Nat Nat n (S n1), (~#) Nat Nat n1 Z) => SNat a
• pattern Exp_ :: forall (a :: Nat). () => forall (n :: Nat). ((~#) Nat Nat a (S n), (~#) Nat Nat n Z) => SNat a
• pattern Stmt_ :: forall (a :: Nat). () => (~#) Nat Nat a Z => SNat a
• pattern SAssign_ :: 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) (x2 :: Atom kon) (xs2 :: [Atom kon]) (k1 :: Nat). ((~#) [[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) x2 xs2), (~#) (Atom kon) (Atom kon) x2 (I kon k1), IsNat k1, (~#) [Atom kon] [Atom kon] xs2 ([] (Atom kon))) => a k -> b k1 -> View kon a b c
• pattern DVar_ :: 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 DFun_ :: 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 :: kon) (x4 :: Atom kon) (xs4 :: [Atom kon]) (k2 :: 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 (K kon k1), (~#) [Atom kon] [Atom kon] xs3 ((:) (Atom kon) x4 xs4), (~#) (Atom kon) (Atom kon) x4 (I kon k2), IsNat k2, (~#) [Atom kon] [Atom kon] xs4 ([] (Atom kon))) => a k -> a k1 -> b k2 -> View kon a b c
• pattern EVar_ :: 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 ECall_ :: 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
• type FIX = Fix Singl CodesStmtString
• alphaEqD :: Decl String -> Decl String -> Bool
• test1 :: String -> String -> String -> Decl String
• test2 :: String -> String -> String -> Decl String
• test3 :: String -> String -> String -> Decl String
• (>>>) :: (a -> b) -> (b -> c) -> a -> c
• test4 :: Int -> Decl String
• test5 :: Maybe (Decl String)

Simple IMPerative Language:

Alpha Equality Functionality

Zipper test

Orphan instances