Generics.MRSOP.Examples.SimpTH

Uses a more involved example to test some of the functionalities of generics-mrsop.

Simple IMPerative Language:

data Stmt var

Constructors

SAssign var (Exp var)

SIf (Exp var) (Stmt var) (Stmt var)

SSeq (Stmt var) (Stmt var)

SReturn (Exp var)

SDecl (Decl var)

SSkip

Instances

HasDatatypeInfo Kon Singl FamStmtString CodesStmtString

Methods

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

Show var => Show (Stmt var)

Methods

showsPrec :: Int -> Stmt var -> ShowS

show :: Stmt var -> String

showList :: [Stmt var] -> ShowS

data Decl var

Constructors

DVar var

DFun var var (Stmt var)

Instances

HasDatatypeInfo Kon Singl FamStmtString CodesStmtString

Methods

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

Show var => Show (Decl var)

Methods

showsPrec :: Int -> Decl var -> ShowS

show :: Decl var -> String

showList :: [Decl var] -> ShowS

data Exp var

Constructors

EVar var

ECall var (Exp var)

EAdd (Exp var) (Exp var)

ESub (Exp var) (Exp var)

ELit Int

Instances

HasDatatypeInfo Kon Singl FamStmtString CodesStmtString

Methods

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

Show var => Show (Exp var)

Methods

showsPrec :: Int -> Exp var -> ShowS

show :: Exp var -> String

showList :: [Exp var] -> ShowS

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 DeclStringDFun_ :: kon KString -> kon KString -> phi Z -> View kon phi (Lkup (S (S Z)) CodesStmtString)

pattern DeclStringDVar_ :: kon KString -> View kon phi (Lkup (S (S Z)) CodesStmtString)

pattern ExpStringELit_ :: kon KInt -> View kon phi (Lkup (S Z) CodesStmtString)

pattern ExpStringESub_ :: phi (S Z) -> phi (S Z) -> View kon phi (Lkup (S Z) CodesStmtString)

pattern ExpStringEAdd_ :: phi (S Z) -> phi (S Z) -> View kon phi (Lkup (S Z) CodesStmtString)

pattern ExpStringECall_ :: kon KString -> phi (S Z) -> View kon phi (Lkup (S Z) CodesStmtString)

pattern ExpStringEVar_ :: kon KString -> View kon phi (Lkup (S Z) CodesStmtString)

pattern StmtStringSSkip_ :: View kon phi (Lkup Z CodesStmtString)

pattern StmtStringSDecl_ :: phi (S (S Z)) -> View kon phi (Lkup Z CodesStmtString)

pattern StmtStringSReturn_ :: phi (S Z) -> View kon phi (Lkup Z CodesStmtString)

pattern StmtStringSSeq_ :: phi Z -> phi Z -> View kon phi (Lkup Z CodesStmtString)

pattern StmtStringSIf_ :: phi (S Z) -> phi Z -> phi Z -> View kon phi (Lkup Z CodesStmtString)

pattern StmtStringSAssign_ :: kon KString -> phi (S Z) -> View kon phi (Lkup Z CodesStmtString)

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]

type FIX = Fix Singl CodesStmtString

Alpha Equality Functionality

alphaEqD :: Decl String -> Decl String -> Bool

test1 :: String -> String -> String -> Decl String

test2 :: String -> String -> String -> Decl String

test3 :: String -> String -> String -> Decl String

Zipper test

(>>>) :: (a -> b) -> (b -> c) -> a -> c infixr 4

test4 :: Int -> Decl String

test5 :: Maybe (Decl String)

Orphan instances

Family Kon Singl FamStmtString CodesStmtString

Methods

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

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