[Haskell-cafe] Simple GADT parser for the eval example
Dimitrios Vytiniotis
dimitriv at cis.upenn.edu
Mon Oct 30 20:19:18 EST 2006
Just noticed Joost Visser's message but since I
had (essentially a very similar) response I thought I might
send it off as well ... It includes the conditional cases.
Regards,
-d
{-# OPTIONS_GHC -fglasgow-exts #-}
module Main where
data Term a where
Lit :: Int -> Term Int
Inc :: Term Int -> Term Int
IsZ :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
Pair :: Term a -> Term b -> Term (a,b)
Fst :: Term (a,b) -> Term a
Snd :: Term (a,b) -> Term b
data Expr = ELit Int
| EInc Expr
| EIsZ Expr
| EPair Expr Expr
| EIf Expr Expr Expr
| EFst Expr
| ESnd Expr
deriving (Read,Show)
-- Give a GADT for representation types
data R a where
Rint :: R Int
Rbool :: R Bool
Rpair :: R a -> R b -> R (a,b)
-- Give an existential type with a type representation
data TermEx where
MkTerm :: R a -> Term a -> TermEx
-- we use Weirich's higher-order type-safe cast to avoid deep traversals
-- one can replace the type_cast with a more simple traversal-based
-- version.
data CL c a d = CL (c (d,a))
data CR c a d = CR (c (a,d))
type_cast :: forall a b c. R a -> R b -> c a -> c b
type_cast Rint Rint x = x
type_cast Rbool Rbool x = x
type_cast (Rpair (ra::(R a0)) (rb::(R b0)))
(Rpair (ra'::(R a0')) (rb'::(R b0'))) x =
let g = (type_cast ra ra' :: ( (CL c b0) a0 -> (CL c b0) a0' ))
h = (type_cast rb rb' :: ( (CR c a0') b0 -> (CR c a0') b0'))
in case (g (CL x)) of
CL x' -> case (h (CR x')) of
CR y' -> y'
type_cast _ _ _ = error "cannot cast!"
-- give only the cases for Eif and Elit, the others are similar
my_read :: Expr -> TermEx
my_read (ELit i) = MkTerm Rint (Lit i);
my_read (EIf p t e) =
case (my_read p) of
MkTerm rb b ->
case rb of
Rbool ->
case (my_read t) of
MkTerm r1 t1 ->
case (my_read e) of
MkTerm r2 t2 ->
MkTerm r2 (If b (type_cast r1 r2 t1) t2)
_ -> error "conditional not boolean!"
More information about the Haskell-Cafe
mailing list