add test case for eta-equality

src/Tests.idr

@@ -2,7 +2,14 @@ module Tests
 
 import Term
 import Check
-import Check
+import Convert
+import Misc
+import Normalize
+import Value
+
+import Control.Monad.RWS
+import Control.Monad.Identity
+import Control.Monad.Either
 
 import Data.Nat
 
@@ -11,13 +18,25 @@ import Data.Nat
 a : {p, q : Nat} -> lt p q = True -> LT p q
 a {p} {q} eq = ltReflectsLT p q eq
 
-test1 : Either String (Bool, List String)
+{- λA. λx. x : ∏ (A : Type) → A → A -}
-test1 = typecheck (TLam (TLam (TVar 0 (a Refl))))
+test_id : Either String (Bool, List String)
+test_id = typecheck (TLam (TLam (TVar 0 (a Refl))))
                     (TPi TType (TPi (TVar 0 (a Refl)) (TVar 1 (a Refl))))
 
-test2 : Either String (Bool, List String)
+{- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -}
-test2 = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))))))
+test_app : Either String (Bool, List String)
+test_app = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))))))
                      (TPi TType 
                           (TPi (TPi (TVar 0 (a Refl)) TType)
                                (TPi (TPi (TVar 1 (a Refl)) (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))) 
                                     (TPi (TVar 2 (a Refl)) (TApp (TVar 2 (a Refl)) (TVar 0 (a Refl)))))))
+
+{- λf. λx. f x ≃ λf. λx. (λy. f y) x -}
+eta_test : Either String (Bool, List String)
+eta_test = resolve action
+  where
+    action : PI Bool
+    action = do
+      x <- eval ctx0 (TLam (TLam (TApp (TVar 1 (a Refl)) (TVar 0 (a Refl)))))
+      y <- eval ctx0 (TLam (TLam (TApp (TLam (TApp (TVar 2 (a Refl)) (TVar 0 (a Refl)))) (TVar 0 (a Refl)))))
+      convert x y

src/Value.idr

@@ -19,6 +19,10 @@ mutual
   Ctx : Index -> Type
   Ctx i = Vect i Value
 
+public export
+ctx0 : Ctx 0
+ctx0 = []
+
 public export
 Show Value where
   show VType       = "VType"