Evaluation of expressions in Idris

expr.idr

data Expr : Type -> Type where
    Con  : Int -> Expr Int 
    Add  : Expr Int -> Expr Int -> Expr Int
    Mult : Expr Int -> Expr Int -> Expr Int
    IsZ  : Expr Int -> Expr Bool
    If   : Expr Bool -> Expr t -> Expr t -> Expr t
    And  : Expr Bool -> Expr Bool -> Expr Bool
    Or : Expr Bool -> Expr Bool -> Expr Bool
    Tuple : Expr t -> Expr s -> Expr (t,s)
    Fst : Expr(t,s) -> Expr t
    Snd : Expr(t,s) -> Expr s

unop : Show t => String -> t -> String
unop op e = op ++ "(" ++ show e ++ ")"

binop : (Show t, Show s) => String -> t -> s -> String
binop op e1 e2 = op ++ "(" ++ show e1 ++ "," ++ show e2 ++ ")"

implementation Show (Expr t) where
    show (Con i) = "Con " ++ show i
    show (Add e1 e2) = binop "Add" e1 e2
    show (Mult e1 e2) = binop "Mult" e1 e2
    show (IsZ e) = unop "IsZ" e
    show (If b e1 e2) = "If(" ++ show b ++ "," ++ show e1 ++ "," ++ show e2 ++ ")"
    show (And e1 e2) = binop "And" e1 e2
    show (Or e1 e2) = binop "Or" e1 e2
    show (Tuple e1 e2) = binop "Pair" e1 e2
    show (Fst e) = unop "Fst" e
    show (Snd e) = unop "Snd" e

--v1 = Add (IsZ $ Con 0) (Con 1) --Not allowed
v2 : Expr Int
v2 = Fst $ Tuple (Add (Con 42) (Con 1)) (Con 2) --All fine

eval : Expr t -> t
eval (Con i) = i
eval (Add e1 e2) = eval e1 + eval e2
eval (Mult e1 e2) = eval e1 * eval e2
eval (IsZ e) = eval e == 0
eval (If b e1 e2) = if eval b then eval e1 else eval e2
eval (And e1 e2) = eval e1 && eval e2
eval (Or e1 e2) = eval e1 || eval e2
eval (Tuple e1 e2) = (eval e1, eval e2)
eval (Fst e) = fst $ eval e
eval (Snd e) = snd $ eval e