Extending the code from Lecture 2, programming with Idris.

[Srdjan Stipic]

I am trying to extend the code from lecture 2,

programming with Idris (the code in at the end of the post).

I would like to do the following:

1. Create an environment with one integer variable.

  Something like this:

    envT: Env G

    envT = [Var TyInt 5]

  And use it like:

    testFac2 : Int

    testFac2 = interp envT fact 4

  I want that envT __not__ to influence the fact 4.

2. Create an environment with one integer variable

  and __lookup__ the variable:

    envT: Env G

    envT = [Var TyInt 5]

  And use it like:

   varT: Var TyInt

   varT = interp envT index -- where the index is the index in the envT

Please, can someone help me?

Thanks,

Srdjan

--- the code starts here

module Main

data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type

interpTy TyInt       = Int

interpTy TyBool      = Bool

interpTy (TyFun s t) = interpTy s -> interpTy t

using (G : Vect Ty n)

  data Env : Vect Ty n -> Type where

      Nil  : Env Nil

      (::) : interpTy a -> Env G -> Env (a :: G)

  data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

      stop : HasType fO (t :: G) t

      pop  : HasType k G t -> HasType (fS k) (u :: G) t

  lookup : HasType i G t -> Env G -> interpTy t

  lookup stop    (x :: xs) = x

  lookup (pop k) (x :: xs) = lookup k xs

------

  data Expr : Vect Ty n -> Ty -> Type where

      Var : HasType i G t -> Expr G t

      Val : (x : Int) -> Expr G TyInt

      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 -> Expr G a -> Expr G a -> Expr G a

  dsl expr

      lambda      = Lam

      variable    = Var

      index_first = stop

      index_next  = pop

------

  (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

  (<$>) = \f, a => App f a

  pure : Expr G a -> Expr G a

  pure = id

  syntax IF [x] THEN [t] ELSE [e] = If x t e

  (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool

  (==) = Op (==)

  (<) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool

  (<) = Op (<)

  instance Num (Expr G TyInt) where

    (+) x y = Op (+) x y

    (-) x y = Op (-) x y

    (*) x y = Op (*) x y

    abs x = IF x < 0 THEN (-x) ELSE x

    fromInteger = Val . fromInteger

  total 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

  eId : Expr G (TyFun TyInt TyInt)

  eId = expr (\x => x)

  eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))

  eTEST = expr (\x, y => y)

  eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

  eAdd = expr (\x, y => x + y)

  eDouble : Expr G (TyFun TyInt TyInt)

  eDouble = expr (\x => [| eAdd x x |])

  fact : Expr G (TyFun TyInt TyInt)

  fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)

testFac : Int

testFac = interp [] fact 4

unitTestFac : so (interp [] fact 4 == 24)

unitTestFac = oh

main : IO ()

main = do putStr "Enter a number: "

          n <- getLine

          putStrLn ("Answer: " ++ show (interp [] fact (cast n)))