{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}
import Generics.Instant
import Generics.Instant.TH
import Generics.Instant.Functions
--------------------------------------------------------------------------------
-- Generic enum
class GEnum a where
genum' :: [a]
instance GEnum U where
genum' = [U]
instance (GEnum a) => GEnum (Rec a) where
genum' = map Rec genum'
instance (GEnum a) => GEnum (Var a) where
genum' = map Var genum'
instance (GEnum a) => GEnum (CEq c p p a) where genum' = map C genum'
instance GEnum (CEq c p q a) where genum' = []
instance (GEnum f, GEnum g) => GEnum (f :+: g) where
genum' = map L genum' ||| map R genum'
instance (GEnum f, GEnum g) => GEnum (f :*: g) where
genum' = diag (map (\x -> map (\y -> x :*: y) genum') genum')
instance GEnum Int where
genum' = [0..9]
-- Dispatcher
genum :: (Representable a, GEnum (Rep a)) => [a]
genum = map to genum'
-- Utilities
infixr 5 |||
(|||) :: [a] -> [a] -> [a]
[] ||| ys = ys
(x:xs) ||| ys = x : ys ||| xs
diag :: [[a]] -> [a]
diag = concat . foldr skew [] . map (map (\x -> [x]))
skew :: [[a]] -> [[a]] -> [[a]]
skew [] ys = ys
skew (x:xs) ys = x : combine (++) xs ys
combine :: (a -> a -> a) -> [a] -> [a] -> [a]
combine _ xs [] = xs
combine _ [] ys = ys
combine f (x:xs) (y:ys) = f x y : combine f xs ys
-------------------------------------------------------------------------------
-- Simple Datatype
-------------------------------------------------------------------------------
-- Example datatype
data Exp = Const Int | Plus Exp Exp
data Const
data Plus
instance Constructor Const where conName _ = "Const"
instance Constructor Plus where conName _ = "Plus"
-- Representable instance
instance Representable Exp where
type Rep Exp = C Const (Var Int) :+: C Plus (Rec Exp :*: Rec Exp)
from (Const n) = L (C (Var n))
from (Plus e e') = R (C (Rec e :*: Rec e'))
to (L (C (Var n))) = Const n
to (R (C (Rec e :*: Rec e'))) = Plus e e'
exp1 = Plus (Const 1) (Const 2)
exp2 = Plus exp1 (Const 3)
instance GEq Exp where geq = geqDefault
testExp1 :: (Bool, Bool)
testExp1 = (geq exp2 exp2, geq exp1 exp2)
instance Empty Exp where empty' = empty
testExp2 :: Exp
testExp2 = empty
instance GShow Exp where gshow = gshowDefault
instance Show Exp where show = gshow -- convenience
testExp3 :: String
testExp3 = show exp2
{-
instance Update Exp where update' = update
instance MapOn Int where mapOn = (+1)
testExp4 :: Exp
testExp4 = update exp2
-}
-------------------------------------------------------------------------------
-- Mutually recursive datatypes
-------------------------------------------------------------------------------
data Decl = None | Seq Decl Decl | Assign String Expr
data Expr = V String | Lam String Expr | App Expr Expr | Let Decl Expr
-- Using TH
$(deriveAll ''Decl)
$(deriveAll ''Expr)
decls = Seq (Assign "x" (Lam "z" (V "z"))) (Assign "y" (V "x"))
expr = Let decls (App (V "x") (V "y"))
instance GShow Expr where gshow = gshowDefault
instance GShow Decl where gshow = gshowDefault
instance Show Expr where show = gshow -- convenience
instance Show Decl where show = gshow -- convenience
testAST1 :: String
testAST1 = show expr
instance Empty Expr where empty' = empty
instance Empty Decl where empty' = empty
testAST2 :: Expr
testAST2 = empty
testAST3 :: Decl
testAST3 = empty
instance GEq Expr where geq = geqDefault
instance GEq Decl where geq = geqDefault
testAST4 :: Bool
testAST4 = geq expr expr
{-
instance Update Decl where update' = update
instance Update Expr where update' = update
instance MapOn [Char] where mapOn _ = "a"
testAST5 :: Decl
testAST5 = update decls
testAST6 :: Expr
testAST6 = update expr
-}
-------------------------------------------------------------------------------
-- Equality constraints
-------------------------------------------------------------------------------
-- Example 1
-- G1 has one index
data G1 :: * -> * where
G11 :: Int -> G1 Int
G12 :: G1 Int -> G1 a
$(deriveAll ''G1)
-- Generic function instances
simplInstance ''GShow ''G1 'gshow 'gshowDefault
gadtInstance ''GEnum ''G1 'genum' 'genum
-- Testing
gshowG1 = gshow (G12 (G11 3))
genumG1 = gshow (take 100 $ genum :: [G1 Int])
-- Example 2: vectors
-- Vec has a parameter 'a' and an index 'n'
data Vec a :: * -> * where
Nil :: Vec a Ze
Cons :: a -> Vec a n -> Vec a (Su n)
deriveAll ''Vec
-- Generic function instances
-- These are not automatically generated because of the parameter `a`
-- The user needs to supply the instance context
instance (GShow a) => GShow (Vec a n) where gshow = gshowDefault
instance (GEnum a, GEnum (Vec a n)) => GEnum (Vec a (Su n)) where
genum' = genum
instance (GEnum a) => GEnum (Vec a Ze) where
genum' = genum
-- Testing
gshowVec = gshow (Cons 'p' Nil)
genumVec = gshow . take 10 $ (genum :: [Vec Int (Su (Su Ze))])
-- Example 3: terms
-- Term has one index
data Term :: * -> * where
Lit :: Int -> Term Int
IsZero :: Term Int -> Term Bool
Pair :: Term a -> Term b -> Term (a,b)
If :: Term Bool -> Term a -> Term a -> Term a
deriveAll ''Term
-- Generic function instances
simplInstance ''GShow ''Term 'gshow 'gshowDefault
gadtInstance ''GEnum ''Term 'genum' 'genum
-- Testing
gshowTerm = gshow (Pair (If (IsZero (Lit 1)) (Lit 2) (Lit 0)) (Lit 1))
genumTerm = gshow (take 10 (genum :: [Term (Bool,Int)]))
-- Example 4: Fin
data Fin n where
FZe :: Fin (Su n)
FSu :: Fin n -> Fin (Su n)
deriveAll ''Fin
simplInstance ''GShow ''Fin 'gshow 'gshowDefault
gadtInstance ''GEnum ''Fin 'genum' 'genum
-- We need to give this instance manually because the index Ze is never
-- used in the datatype definition
instance GEnum (Fin Ze) where genum' = []
gshowFin = gshow (FSu (FSu FZe))
genumFin = gshow (take 10 (genum :: [Fin (Su (Su Ze))]))