STLC.idr

data Typ =
    IntTyp
  | BolTyp
  | FunTyp Typ Typ

toType : Typ -> Type
toType IntTyp       = Integer
toType BolTyp       = Bool
toType (FunTyp x y) = toType x -> toType y

dsl type
  pi = \ _ => FunTyp -- bug: if I write FunType it doesn't catch it here

data Variable : List Typ -> Typ -> Type where
  Zro : Variable (a :: g) a
  Suc : Variable g a -> Variable (b :: g) a

data Env : (Typ -> Type) -> List Typ -> Type where
  Nil  : Env f []
  (::) : f a -> Env f g -> Env f (a :: g)

get : Variable g a -> Env f g -> f a
get Zro     (y :: _)  = y
get (Suc x) (_ :: ys) = get x ys

data Trm : List Typ -> Typ -> Type where
  LitInt : Integer -> Trm g IntTyp -- I cannot write type Nat since
                                   -- I don't know how to re-purpose type constants

  Var : Variable g a -> Trm g a

  Abs : Trm (a :: g) b -> Trm g (type (a -> b))
  App : Trm g (type (a -> b)) -> Trm g a -> Trm g b

  Let : Trm g a -> Trm (a :: g) b -> Trm g b

  LitBol : Bool -> Trm g BolTyp
  Cnd : Trm g BolTyp -> Lazy (Trm g a) -> Lazy (Trm g a) -> Trm g a

fromInteger : Integer -> Trm g IntTyp
fromInteger = LitInt

evl : Env toType g -> Trm g a -> toType a
evl g (LitInt k)  = k
evl g (Var x)     = get x g
evl g (Abs n)     = \ y => evl (y :: g) n
evl g (App l m)   = (evl g l) (evl g m)
evl g (Let m n)   = evl g (App (Abs n) m)
evl g (LitBol k)  = k
evl g (Cnd l m n) = if evl g l then evl g m else evl g n

mkLet : TTName -> Trm g a -> Trm (a :: g) b -> Trm g b
mkLet _ = Let

mkLam : TTName -> Trm (a :: g) b -> Trm g (type (a -> b))
mkLam _ = Abs

dsl term
  lambda      = mkLam
  let         = mkLet
  variable    = Var
  index_first = Zro
  index_next  = Suc

syntax "IF" [l] "THEN" [m] "ELSE" [n] = Cnd l m n


-- Bug: below makes my system crash! It keeps eating up memory.
foo : Trm [] (type (IntTyp -> IntTyp -> IntTyp))
foo = term (\x, y => let z = 0
                     in z)
-- -}