Idris interpreter

interpreter.idr

module Interpreter
import Data.Vect
import Data.Fin

data Ty = TyInt | TyBool | TyFun Ty Ty

interpretTy : Ty -> Type
interpretTy TyInt = Int
interpretTy TyBool = Bool
interpretTy (TyFun A T) = interpretTy A -> interpretTy T

using (Context:Vect n Ty)
  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type
    where 
      Stop : HasType FZ (t :: Context) t
      Pop  : HasType k Context t -> HasType (FS k) (u :: Context) t
  
  data Expression : Vect n Ty -> Ty -> Type 
    where
      Var : HasType i Context t -> Expression Context t 
      Val : (x : Int) -> Expression Context TyInt
      Lam : Expression (a :: Context) t -> Expression Context (TyFun a t)
      App : Expression Context (TyFun a t) -> Expression Context a -> Expression Context t
      Op  : (interpretTy a -> interpretTy b -> interpretTy c) ->
            Expression Context a -> Expression Context b -> Expression Context c
      If  : Expression Context TyBool ->
            Lazy (Expression Context a) ->
            Lazy (Expression Context a) -> Expression Context a 

  data Environment : Vect n Ty -> Type 
    where
      Nil : Environment Nil
      (::) : interpretTy a -> Environment Context -> Environment (a :: Context)

  lookup : (HasType i Context t) -> (Environment Context) -> (interpretTy t)
  lookup Stop (x :: xs) = x
  lookup (Pop k) (x :: xs)  = lookup k xs