Lambda2.pi

module Lambda where

import Nat
import Fin
import Vec 

{- This version also requires that the object language be statically typed. 
   It eliminates all run-time errors from the expression. -}

lookup : [a:Type] -> [n:Nat] -> Fin n -> Vec a n -> a
lookup = \[a][n] f v. case f of 
   Zero [m] -> case v of 
           Cons [m'] x xs -> x 
   Succ [m] f' -> case v of 
              Cons [m'] x xs -> lookup [a][m] f' xs

data Ty : Type where
   TyFun of (Ty)(Ty)
   TyNat 

data List (a : Type) : Type where
   Nil 
   Cons of (a) (List a)

data VarRef (n : List Ty) (t : Ty) : Type where
   VZ of [ts : List Ty][n = Cons t ts]
   VS of [ts : List Ty][u : Ty](VarRef ts t)[n = Cons u ts]

-- a single variable in a context containing one variable

x : VarRef (Cons TyNat Nil) TyNat
x = VZ [Nil]

-- two variables in a context containing two vars

y1 : VarRef (Cons TyNat (Cons TyNat Nil)) TyNat
y1 = VZ [Cons TyNat Nil]

y2 : VarRef (Cons TyNat (Cons TyNat Nil)) TyNat
y2 = VS [Cons TyNat Nil][TyNat](VZ [Nil])


data Exp (n : List Ty) (t : Ty) : Type where
   Var of (VarRef n t)
   App of [t1:Ty] (Exp n (TyFun t1 t)) (Exp n t1)
   Lam of [t1: Ty][t2:Ty](Exp (Cons t1 n) t2) [t = TyFun t1 t2]
   Lit of (Nat)[t = TyNat]
   If0 of (Exp n TyNat)(Exp n t)(Exp n t)

data Env (val : Ty -> Type) (n : List Ty)  : Type where
   Nil  of [n = Nil]
   Cons of [t : Ty][ts : List Ty](val t)(Env val ts) [n = Cons t ts]

data Val (t : Ty) : Type where
   Clos of [n:List Ty][t1:Ty][t2:Ty] 
               (Env (\t. Val t) n) (Exp (Cons t1 n) t2)[t = TyFun t1 t2]
   VNat of (Nat)[t = TyNat]

env : List Ty -> Type
env = \u.  Env (\t. Val t) u

nth : [n : List Ty] -> [t:Ty] -> env n -> VarRef n t -> Val t
nth = \ [n][t] e var. case var of 
   VZ [ts]       -> case e of 
                      Cons [u][ts] v vs -> v
   VS [ts][u] v' -> case e of 
	              Cons [u][ts] v vs -> nth [ts][t] vs v'


interp : [n:List Ty] -> [t:Ty] -> env n -> Exp n t -> Val t
interp = \[n][t] rho exp. 
  case exp of 
    Var x          -> nth [n][t] rho x
    App [t1] e1 e2 -> 
      let v1 = interp [n][TyFun t1 t] rho e1 in
      let v2 = interp [n][t1]         rho e2 in 
      case v1 of
        Clos [m][t1'][t2'] rho' body -> 
          let rho'' = (Cons [t1][m] v2 rho' : env (Cons t1 m)) in 
          interp [Cons t1 m][t2'] rho'' body

    Lam [t1][t2] body -> Clos [n][t1][t2] rho body
    Lit i          -> VNat i
    If0 e1 e2 e3 -> case (interp [n][TyNat] rho e1) of 
        VNat x -> case x of 
          Zero     -> interp [n][t] rho e2
          (Succ y) -> interp [n][t] rho e3


t1 : interp [Nil][TyNat] Nil (App[TyNat] (Lam [TyNat][TyNat] (Var x)) (Lit 3)) = VNat 3
t1 = refl

-- t2 : interp [Nil][TyNat] Nil (App[TyNat] (Lam[TyNat][TyNat] (Var y1)) (Lit 2)) = TRUSTME
-- t2 = refl

-- t3 : interp [Nil][TyNat] Nil (App[TyNat] (Lit 1) (Lit 2)) = TRUSTME
-- t3 = refl