{-# OPTIONS_GHC -fglasgow-exts #-}

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 

eval :: Term a -> a
eval (Lit i)    = i
eval (Inc t)    = eval t + 1
eval (IsZ t)    = eval t == 0
eval (If b t e) = if eval b then eval t else eval e
eval (Pair a b) = (eval a, eval b)
eval (Fst t)    = fst (eval t)
eval (Snd t)    = snd (eval t)

data Expr = ELit Int
          | EInc Expr
          | EIsZ Expr 
          | EPair Expr Expr
          | EIf Expr Expr Expr
          | EFst Expr
          | ESnd Expr
            deriving (Read,Show)

my_read' :: Expr -> Maybe DynTerm
my_read' (ELit a)    = return $ DynTerm Int (Lit a)
my_read' (EInc a)    = do
  DynTerm Int a' <- my_read' a
  return (DynTerm Int (Inc a'))
my_read' (EIsZ a)    = do
  DynTerm Int a' <- my_read' a
  return (DynTerm Bool (IsZ a'))
-- my_read' (EPair a b) = DynTerm $ Pair (my_read' a) (my_read' b)
-- my_read' (EIf p t e) = DynTerm $ If (my_read' p) (my_read' t) (my_read' e)
-- my_read' (EFst a)    = DynTerm $ Fst (my_read' a)
my_read' (ESnd a)    = do
  DynTerm (Prod x y) a' <- my_read' a 
  return (DynTerm y (Snd a'))

data DynTerm where
  DynTerm :: Type a -> Term a -> DynTerm
  
data Type a where
  Int :: Type Int
  Bool :: Type Bool
  Prod :: Type a -> Type b -> Type (a,b)
  
data Dynamic where
  Dyn :: Type a -> a -> Dynamic
  
test :: Expr -> Maybe Dynamic
test expr = do
  DynTerm t a <- my_read' expr
  return (Dyn t (eval a))
  
gshow :: Type a -> a -> String
gshow Int i = show i
gshow Bool b = show b
gshow (Prod a b) (x,y) = "("++gshow a x++","++gshow b y++")" 

instance Show Dynamic where
  show (Dyn t x) = gshow t x