Skip to content

Instantly share code, notes, and snippets.

@lenaschoenburg
Created March 15, 2015 12:34
Show Gist options
  • Save lenaschoenburg/d7bc2f3fd335370be815 to your computer and use it in GitHub Desktop.
Save lenaschoenburg/d7bc2f3fd335370be815 to your computer and use it in GitHub Desktop.
Idris interpreter
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment