module WellTyped

import Data.Vect

data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt = Integer
interpTy TyBool = Bool
interpTy (TyFun x y) = interpTy x -> interpTy y

data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
  Stop : HasType FZ (t :: ctxt) t
  Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
%name HasType i

data Expr : Vect n Ty -> Ty -> Type where
  Var : HasType i ctxt t -> Expr ctxt t
  Val : (x : Integer) -> Expr ctxt TyInt
  Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
  App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
  Op  : (interpTy a -> interpTy b -> interpTy c) ->
        Expr ctxt a -> Expr ctxt b -> Expr ctxt c
  If  : Expr ctxt TyBool ->
        Lazy (Expr ctxt a) ->
        Lazy (Expr ctxt a) -> Expr ctxt a

data Env : Vect n Ty -> Type where
  Nil  : Env Nil
  (::) : interpTy a -> Env ctxt -> Env (a :: ctxt)

%name Env env

lookup : HasType i ctxt t -> Env ctxt -> interpTy t
lookup Stop (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs

interp : Env ctxt -> Expr ctxt t -> interpTy t
interp env (Var i)    = lookup i env
interp env (Val x)    = x
interp env (Lam x)    = \y => interp (y :: env) x
interp env (App x y)  = interp env x $ interp env y
interp env (Op f x y) = f (interp env x) (interp env y)
interp env (If x y z) = if interp env x then interp env y 
                                        else interp env z

add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

fact : Expr ctxt (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var Stop) (Val 0))
               (Val 1)
               (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
                       (Var Stop)))

main : IO ()
main = do putStr "Enter a number: "
          x <- getLine
          printLn (interp [] fact (cast x))