Interpreter.idr

module Interpreter

import Data.Fin
import Data.Vect

data Ty = TyInt 
        | TyBool 
        | TyStr
        | TyFun Ty Ty
        
interpTy : Ty -> Type
interpTy TyInt = Integer
interpTy TyBool = Bool
interpTy TyStr = String
interpTy (TyFun A T) = interpTy A -> interpTy T

interface InverpType (t : Type) where
  typ : Ty
  pf : interpTy typ = t

InverpType Integer where
  typ = TyInt
  pf = Refl

InverpType Bool where
  typ = TyBool
  pf = Refl

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

  data Expr : Vect n Ty -> Ty -> Type where
    Var : HasType i G t -> Expr G t
    Val : (cl : InverpType t) => (typ' : Ty) -> {eq : typ @{cl} = typ'} -> t -> Expr G typ'
    Lam : Expr (a :: G) t -> Expr G (TyFun a t)
    App : Expr G (TyFun a t) -> Expr G a -> Expr G t
    Op  : (interpTy a -> interpTy b -> interpTy c) ->
          Expr G a -> Expr G b -> Expr G c
    If  : Expr G TyBool ->
          Lazy (Expr G a) ->
          Lazy (Expr G a) -> Expr G a
  
  data Env : Vect n Ty -> Type where
      Nil  : Env Nil
      (::) : interpTy a -> Env G -> Env (a :: G)

  lookup : HasType i G t -> Env G -> interpTy t
  lookup Stop    (x :: xs) = x
  lookup (Pop k) (x :: xs) = lookup k xs
  
  interp : Env G -> Expr G t -> interpTy t
  interp env (Var i)     = lookup i env
  interp env (Val _ x)  ?= x
  interp env (Lam sc)    = \x => interp (x :: env) sc
  interp env (App f s)   = interp env f (interp env s)
  interp env (Op op x y) = op (interp env x) (interp env y)
  interp env (If x t e)  = if interp env x then interp env t
                                           else interp env e

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

  opeq : {G' : Vect n' Ty} -> Expr G' TyInt -> Expr G' TyInt -> Expr G' TyBool
  opeq = Op (==)

  opminus : {G' : Vect n' Ty} -> Expr G' TyInt -> Expr G' TyInt -> Expr G' TyInt
  opminus = Op (-)
  
  fact : Expr G (TyFun TyInt TyInt)
  fact = Lam (If (opeq (Var Stop) (Val _ {eq=Refl} 0))
                 (Val _ {eq=Refl} 1)
                 (Op (*) (App fact (opminus (Var Stop) (Val _ {eq=Refl} 1)))
                         (Var Stop)))
   
  -- upcase : Expr G (TyFun TyStr TyStr)
  -- upcase = Val (TyFun TyStr TyStr) toUpper