public
Created

Recovering sharing in a GADT

  • Download Gist
soreifygadt.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
{-# LANGUAGE GADTs, TypeFamilies, FlexibleInstances, RankNTypes #-}
import Data.Reify
import Control.Applicative
import Data.Map
 
data Ast e where
IntLit :: Int -> Ast Int
Add :: Ast Int -> Ast Int -> Ast Int
BoolLit :: Bool -> Ast Bool
IfThenElse :: Ast Bool -> Ast e -> Ast e -> Ast e
 
type Name = Unique
 
data Ast2 e s where
IntLit2 :: Int -> Ast2 Int s
Add2 :: Ast2 Int s -> Ast2 Int s -> Ast2 Int s
BoolLit2 :: Bool -> Ast2 Bool s
IfThenElse2 :: Ast2 Bool s -> Ast2 e s -> Ast2 e s -> Ast2 e s
Var :: Type e -> s -> Ast2 e s
data Type a where
Bool :: Type Bool
Int :: Type Int
 
data Refl a b where Refl :: Refl a a
 
typeEq :: Type a -> Type b -> Maybe (Refl a b)
typeEq Bool Bool = Just Refl
typeEq Int Int = Just Refl
typeEq _ _ = Nothing
 
getType :: Ast e -> Type e
getType (IntLit _) = Int
getType (Add _ _) = Int
getType (BoolLit _) = Bool
getType (IfThenElse _ _ e) = getType e
 
data WrappedAst s where
Wrap :: Type e -> Ast2 e s -> WrappedAst s
 
 
instance MuRef (Ast e) where
type DeRef (Ast e) = WrappedAst
mapDeRef f e = Wrap (getType e) <$> mapDeRef' f e
where
mapDeRef' :: Applicative f => (forall b. (MuRef b, WrappedAst ~ DeRef b) => b -> f u) -> Ast e -> f (Ast2 e u)
mapDeRef' f (IntLit i) = pure $ IntLit2 i
mapDeRef' f (Add a b) = Add2 <$> (Var Int <$> f a) <*> (Var Int <$> f b)
mapDeRef' f (BoolLit b) = pure $ BoolLit2 b
mapDeRef' f (IfThenElse b t e) = IfThenElse2 <$> (Var Bool <$> f b) <*> (Var (getType t) <$> f t) <*> (Var (getType e) <$> f e)
 
 
getVar :: Map Name (WrappedAst Name) -> Type e -> Name -> Maybe (Ast2 e Name)
getVar m t n = case m ! n of Wrap t' e -> (\Refl -> e) <$> typeEq t t'
 
 
conv :: Ast e -> IO (Map Name (WrappedAst Name), Maybe (Ast2 e Name))
conv e = do
Graph l n <- reifyGraph e
let m = fromList l
return (m, getVar m (getType e) n)
 
 
test = IfThenElse (IfThenElse true true true) (Add one one) one
where
one = IntLit 1
true = BoolLit True
 
 
instance Show (Type a) where
show Bool = "Bool"
show Int = "Int"
 
instance Show (WrappedAst Unique) where
show (Wrap t a) = "(" ++ show a ++ " :: " ++ show t ++ ")"
 
instance Show s => Show (Ast2 e s) where
show (IntLit2 i) = "(IntLit2 " ++ show i ++ ")"
show (Add2 l r) = "(Add " ++ show l ++ " " ++ show r ++ ")"
show (BoolLit2 b) = "(BoolLit2 " ++ show b ++ ")"
show (IfThenElse2 b t e) = "(IfThenElse2 " ++ show b ++ " " ++ show t ++ " " ++ show e ++ ")"
show (Var t n) = "(Var " ++ show t ++ " " ++ show n ++ ")"

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.