module Syntax where

type Name = String

data Term = Var  Name
          | Con  Constant
          | Lam  Name Type Term
          | App  Term Term
          | Cast Type Type Term
          deriving (Eq, Show)

data Type = Fun Name Type Type
          | Ref Name Base Term
          deriving (Eq, Show)

data Base = BInt | BBool
          deriving (Eq, Show)

data Constant = Ctrue
              | Cfalse
              | Cimpl
              | Cimplb Bool
              | Cnot
              | Cint   Integer
              | Cplus
              | Cplusn Integer
              | Cdiv 
              | Cdivn  Integer
              | Ceq
              | Ceqn   Integer
              | Cif    Type
              | Cfix   Type
              deriving (Eq, Show)