[Haskell-cafe] Simple GADT parser for the eval example

[Dimitrios Vytiniotis]

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!"