From c7fb1d5cd3e33cc0605f850722345c3dd7ef0ca8 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Tue, 26 Jul 2022 23:07:13 +0200
Subject: [PATCH] definition system, repl

---
 README.md              |   6 +-
 makefile               |   2 +
 pi.ipkg                |   1 -
 src/Core/Check.idr     |  46 +++++---
 src/Core/Convert.idr   | 150 +++++++++++++------------
 src/Core/Misc.idr      |  61 +++++++---
 src/Core/Normalize.idr |  21 +++-
 src/Core/Term.idr      |   8 ++
 src/Core/Tests.idr     | 155 --------------------------
 src/Main.idr           |  94 +++++++++++++---
 src/Parser/Parse.idr   | 245 ++++++++++++++++++++---------------------
 src/Parser/Tests.idr   |  89 ---------------
 tests/id1.pi           |   3 +
 tests/id2.pi           |   3 +
 14 files changed, 384 insertions(+), 500 deletions(-)
 delete mode 100644 src/Core/Tests.idr
 delete mode 100644 src/Parser/Tests.idr
 create mode 100644 tests/id1.pi
 create mode 100644 tests/id2.pi

diff --git a/README.md b/README.md
index e44ac82..b6bb6d9 100644
--- a/README.md
+++ b/README.md
@@ -22,12 +22,12 @@ A dependently typed system
 
 # TODO
 
-* Repl
-  * Defs
-
 * Performence optimisation
+  * Parsing !!! (this is like 90% of the time currently lmao)
   * Memoize normalisation and conversion somehow?
 
+* Repl
+
 * Universes
 
 * Implicit arguments
diff --git a/makefile b/makefile
index 0b15bd4..0281e1e 100644
--- a/makefile
+++ b/makefile
@@ -1,6 +1,8 @@
 .PHONY: all run
 all:
 	idris2 --build pi.ipkg
+clean:
+	idris2 --clean pi.ipkg
 run:
 	./build/exec/pi
 test:
diff --git a/pi.ipkg b/pi.ipkg
index 10a86ec..5d64b60 100644
--- a/pi.ipkg
+++ b/pi.ipkg
@@ -5,7 +5,6 @@ modules = Core.Check
         , Core.Misc
         , Core.Normalize
         , Core.Term
-        , Core.Tests
         , Core.Value
         , Parser.Parse
 
diff --git a/src/Core/Check.idr b/src/Core/Check.idr
index d2218be..b355644 100644
--- a/src/Core/Check.idr
+++ b/src/Core/Check.idr
@@ -5,6 +5,8 @@ import Control.Monad.Either
 import Control.Monad.Identity
 import Data.Vect
 import Data.Fin
+import Data.IOArray
+import Data.IORef
 
 import Core.Term
 import Core.Value
@@ -12,21 +14,27 @@ import Core.Normalize
 import Core.Misc
 import Core.Convert
 
-
 %default total
-
+ 
 -- extend environment, used to ensure environment is always in normal form
-extV : Ctx n -> Value -> PI (Ctx (S n))
+extV : {auto deftrs    : RefA DTR Value}
+       -> {auto frst   : Ref NST Nat}
+       -> Ctx n -> Value -> PI (Ctx (S n))
 extV ctx val = whnf val >>= pure . (`Data.Vect.(::)` ctx)
 
 -- to extend, closure env, term
-extT : Ctx m -> Ctx n -> Term n -> PI (Ctx (S m))
+extT : {auto deftrs    : RefA DTR Value}
+       -> {auto frst   : Ref NST Nat}
+       -> Ctx m -> Ctx n -> Term n -> PI (Ctx (S m))
 extT ctx env = extV ctx . VClos env
 
 mutual
   public export
   -- terms types expected term
-  check : Ctx n -> Ctx n -> Value -> Term n -> PI Bool
+  check : {auto deftrs    : RefA DTR Value}
+          -> {auto deftys : RefA DTY Value}
+          -> {auto frst   : Ref NST Nat}
+          -> Ctx n -> Ctx n -> Value -> Term n -> PI Bool
   check trs tys xpt' tr = do
     xpt <- whnf xpt'
     case tr of
@@ -49,7 +57,11 @@ mutual
       _       => convert xpt =<< infer trs tys tr
 
   -- terms types term
-  infer : Ctx n -> Ctx n -> Term n -> PI Value
+  public export
+  infer : {auto deftrs    : RefA DTR Value}
+          -> {auto deftys : RefA DTY Value}
+          -> {auto frst   : Ref NST Nat}
+          -> Ctx n -> Ctx n -> Term n -> PI Value
   infer trs tys TType      = pure VType
   infer trs tys TTop       = pure VType
   infer trs tys TBot       = pure VType
@@ -57,14 +69,19 @@ mutual
   infer trs tys TStar      = pure VTop
   infer trs tys TZero      = pure VNat
   infer trs tys (TVar i)   = pure (index i tys)
+  infer trs tys (TDef i)   = do
+    res <- getArr DTY i
+    case res of
+         Just x  => pure x
+         Nothing => oops "TDef type lookup"
   infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
-                              \case
-                                 VClos env (TPi a b) => do
-                                   guardS ("app x:\n" ++ show !(whnf (VClos env a))) =<< check trs tys (VClos env a) x
-                                   tr <- whnf (VClos trs x)
-                                   pure (VClos (tr :: env) b)
+    \case
+       VClos env (TPi a b) => do
+         guardS ("app x:\n" ++ show !(whnf (VClos env a))) =<< check trs tys (VClos env a) x
+         tr <- whnf (VClos trs x)
+         pure (VClos (tr :: env) b)
 
-                                 _ => oops "expected infer pi"
+       _ => oops "expected infer pi"
 
   infer trs tys (TPi a b) = do
     v <- VGen <$> fresh
@@ -141,6 +158,9 @@ mutual
   infer trs tys x          = oops ("cannot infer type " ++ show x)
 
 public export
-typecheck : Term 0 -> Term 0 -> Either String (Bool, List String)
+typecheck : {auto deftrs    : RefA DTR Value}
+            -> {auto deftys : RefA DTY Value}
+            -> {auto frst   : Ref NST Nat}
+            -> Term 0 -> Term 0 -> IO (Either String Bool)
 typecheck tr ty = resolve $ (&&) <$> check [] [] VType ty 
                                  <*> delay <$> check [] [] (VClos [] ty) tr
diff --git a/src/Core/Convert.idr b/src/Core/Convert.idr
index 0713d25..4187f19 100644
--- a/src/Core/Convert.idr
+++ b/src/Core/Convert.idr
@@ -11,102 +11,100 @@ import Control.Monad.Either
 
 import Data.Nat
 import Data.Vect
+import Data.IOArray
+import Data.IORef
 
 %default total
 
 public export
-convert : Value -> Value -> PI Bool
+convert : {auto deftrs    : RefA DTR Value}
+          -> {auto frst   : Ref NST Nat} 
+          -> Value -> Value -> PI Bool
 convert u1 u2 = do
   u1' <- whnf u1
   u2' <- whnf u2
-  logS ("checking equality of terms '" ++ show u1  ++ "' and '" ++ show u2  ++ "'.")
-  logS ("with value representations '" ++ show u1' ++ "' and '" ++ show u2' ++ "'.")
-  assert_total $ -- :(
-    case (u1', u2') of
-      (VType, VType) => pure True
-      (VTop, VTop)   => pure True
-      (VStar, VStar) => pure True
-      (VBot, VBot)   => pure True
-      (VNat, VNat)   => pure True
+  assert_total $ case (u1', u2') of
+    (VType, VType) => pure True
+    (VTop, VTop)   => pure True
+    (VStar, VStar) => pure True
+    (VBot, VBot)   => pure True
+    (VNat, VNat)   => pure True
 
-      (VGen k1, VGen k2) => pure (k1 == k2)
+    (VGen k1, VGen k2) => pure (k1 == k2)
 
-      (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2
+    (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2
 
-      (VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do
-        v <- VGen <$> fresh
-        convert (VClos (v :: env1) sc1) (VClos (v :: env2) sc2)
+    (VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do
+      v <- VGen <$> fresh
+      convert (VClos (v :: env1) sc1) (VClos (v :: env2) sc2)
 
-      (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do
-        v <- VGen <$> fresh
-        guardS (show a1 ++ " | " ++ show a2) =<< convert (VClos env1 a1) (VClos env2 a2)
-        convert (VClos (v :: env1) b1) (VClos (v :: env2) b2)
+    (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do
+      v <- VGen <$> fresh
+      (&&) <$> convert (VClos env1 a1) (VClos env2 a2)
+           <*> delay <$> convert (VClos (v :: env1) b1) (VClos (v :: env2) b2)
 
-      (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do
-        termGuard env1 env2 a1 a2
-        termConv  env1 env2 b1 b2
+    (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do
+      termGuard env1 env2 a1 a2
+      termConv  env1 env2 b1 b2
 
-      (VClos env1 (TPair a1 b1), VClos env2 (TPair a2 b2)) => do
-        termGuard env1 env2 a1 a2
-        termConv  env1 env2 b1 b2
+    (VClos env1 (TPair a1 b1), VClos env2 (TPair a2 b2)) => do
+      termGuard env1 env2 a1 a2
+      termConv  env1 env2 b1 b2
 
-      (VClos env1 (TId ty1 a1 b1), VClos env2 (TId ty2 a2 b2)) => do
-        termGuard env1 env2 ty1 ty2
-        termGuard env1 env2 a1 a2
-        termConv  env1 env2 b1 b2
-        
-      (VClos env1 (TRefl ty1 tr1), VClos env2 (TRefl ty2 tr2)) => do
-        termGuard env1 env2 ty1 ty2
-        termConv  env1 env2 tr1 tr2
+    (VClos env1 (TId ty1 a1 b1), VClos env2 (TId ty2 a2 b2)) => do
+      termGuard env1 env2 ty1 ty2
+      termGuard env1 env2 a1 a2
+      termConv  env1 env2 b1 b2
+      
+    (VClos env1 (TRefl ty1 tr1), VClos env2 (TRefl ty2 tr2)) => do
+      termGuard env1 env2 ty1 ty2
+      termConv  env1 env2 tr1 tr2
 
-      (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do
-        termGuard env1 env2 c1 c2
-        termGuard env1 env2 z1 z2
-        termConv  env1 env2 s1 s2
+    (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do
+      termGuard env1 env2 c1 c2
+      termGuard env1 env2 z1 z2
+      termConv  env1 env2 s1 s2
 
-      (VClos _ TZero, VClos _ TZero) => pure True
+    (VClos _ TZero, VClos _ TZero) => pure True
 
-      (VClos env1 (TSuc n1), VClos env2 (TSuc n2)) => do
-        termConv env1 env2 n1 n2
+    (VClos env1 (TSuc n1), VClos env2 (TSuc n2)) => do
+      termConv env1 env2 n1 n2
 
-      (VClos env1 (TJ ty1 a1 b1 c1 d1), VClos env2 (TJ ty2 a2 b2 c2 d2)) => do
-        termGuard env1 env2 ty1 ty2
-        termGuard env1 env2 a1  a2
-        termGuard env1 env2 b1  b2
-        termGuard env1 env2 c1  c2
-        termConv  env1 env2 d1  d2
+    (VClos env1 (TJ ty1 a1 b1 c1 d1), VClos env2 (TJ ty2 a2 b2 c2 d2)) => do
+      termGuard env1 env2 ty1 ty2
+      termGuard env1 env2 a1  a2
+      termGuard env1 env2 b1  b2
+      termGuard env1 env2 c1  c2
+      termConv  env1 env2 d1  d2
 
-      (VClos env1 (TSigInd a1 b1 c1 f1), VClos env2 (TSigInd a2 b2 c2 f2)) => do
-        termGuard env1 env2 a1 a2
-        termGuard env1 env2 b1 b2
-        termGuard env1 env2 c1 c2
-        termConv  env1 env2 f1 f2
+    (VClos env1 (TSigInd a1 b1 c1 f1), VClos env2 (TSigInd a2 b2 c2 f2)) => do
+      termGuard env1 env2 a1 a2
+      termGuard env1 env2 b1 b2
+      termGuard env1 env2 c1 c2
+      termConv  env1 env2 f1 f2
 
-      (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2
+    (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2
 
-      (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
-        termGuard env1 env2 c1 c2
-        termConv  env1 env2 st1 st2
+    (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
+      termGuard env1 env2 c1 c2
+      termConv  env1 env2 st1 st2
 
-      -- η rules
-      -- fresh cannot appear in vsc, so this is fine
-      (vsc, VClos env (TLam (TApp sc (TVar 0)))) => do
-        v <- VGen <$> fresh
-        convert vsc (VClos (v :: env) sc)
-      (VClos env (TLam (TApp sc (TVar 0))), vsc) => do
-        v <- VGen <$> fresh
-        convert vsc (VClos (v :: env) sc)
+    -- η rules
+    -- fresh cannot appear in vsc, so this is fine
+    (vsc, VClos env (TLam (TApp sc (TVar 0)))) => do
+      v <- VGen <$> fresh
+      convert vsc (VClos (v :: env) sc)
+    (VClos env (TLam (TApp sc (TVar 0))), vsc) => do
+      v <- VGen <$> fresh
+      convert vsc (VClos (v :: env) sc)
 
-      -- VApp
-      --     (VApp v1 v2 , VClos env (TApp t1 t2)) => (&&) <$> convert v1 (VClos env t1) <*> delay <$> convert v1 (VClos env t1)
-      --  (VClos env (TApp t1 t2), VApp v1 v2) => (&&) <$> convert v1 (VClos env t1) <*> delay <$> convert v1 (VClos env t1)
-
-      (v1, v2) => oops ("cannot convert \n" ++ show v1 ++ "\n\n" ++ show v2)
-  where
-    termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool
-    termConv env1 env2 a1 a2 = do
-      a1' <- eval env1 a1
-      a2' <- eval env2 a2
-      convert a1' a2'
-    termGuard : Ctx n -> Ctx m -> Term n -> Term m -> PI ()
-    termGuard env1 env2 a1 a2 = guardS "termGuard" =<< termConv env1 env2 a1 a2
+    (v1, v2) => oops ("cannot convert \n" ++ show v1 ++ "\n\n" ++ show v2)
+where
+  termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool
+  termConv env1 env2 a1 a2 = do
+    a1' <- eval env1 a1
+    a2' <- eval env2 a2
+    convert a1' a2'
+  termGuard : Ctx n -> Ctx m -> Term n -> Term m -> PI ()
+  termGuard env1 env2 a1 a2 = termConv env1 env2 a1 a2 >>=
+    guardS ("cannot convert \n" ++ show a1 ++ "\n\n" ++ show a2)
diff --git a/src/Core/Misc.idr b/src/Core/Misc.idr
index dfdac45..9dcb371 100644
--- a/src/Core/Misc.idr
+++ b/src/Core/Misc.idr
@@ -6,6 +6,8 @@ import Control.Monad.Either
 
 import Data.Nat
 import Data.Vect
+import Data.IORef
+import Data.IOArray
 
 %default total
 
@@ -19,13 +21,46 @@ Name = String
 
 public export
 PI : Type -> Type
-PI = EitherT String (RWS () (List String) Nat)
+PI = EitherT String IO
 
 public export
-resolve : PI a -> Either String (a, List String)
-resolve a = case runRWS (runEitherT a) () 0 of
-                 (Left e, _) => Left e
-                 (Right r, _, s) => Right (r, s)
+data NST : Type where
+public export
+data DTY : Type where
+public export
+data DTR : Type where
+
+public export
+data RefP : Type -> Type -> Type where
+  MkRefP : (label : Type) -> a -> RefP label a
+
+public export
+RefA : Type -> Type -> Type
+RefA label a = RefP label (IOArray a)
+
+public export
+Ref : Type -> Type -> Type
+Ref label a = RefP label (IORef a)
+
+public export
+getRef : HasIO io => (label : Type) -> {auto ref : Ref label a} -> io a
+getRef _ {ref = MkRefP _ ref} = readIORef ref
+
+public export
+putRef : HasIO io => (label : Type) -> {auto ref : Ref label a} -> a -> io ()
+putRef _ {ref = MkRefP _ ref} = writeIORef ref
+
+public export
+getArr : HasIO io => (label : Type) -> {auto ref : RefA label a} -> Int -> io (Maybe a)
+getArr _ {ref = MkRefP _ ref} = readArray ref
+
+public export
+putArr : HasIO io => (label : Type) -> {auto ref : RefA label a} -> Int -> a -> io Bool
+putArr _ {ref = MkRefP _ ref} = writeArray ref
+
+public export
+resolve : PI a -> IO (Either String a)
+resolve a = runEitherT a
 
 public export
 oops : String -> PI a
@@ -36,19 +71,9 @@ guardS : String -> Bool -> PI ()
 guardS str True  = pure ()
 guardS str False = oops str
 
-
 public export
-fresh : PI Nat
+fresh : {auto frst : Ref NST Nat} -> PI Nat
 fresh = do
-  i <- get
-  put (S i)
+  i <- getRef NST
+  putRef NST (S i)
   pure i
-
-public export
-logS : String -> PI ()
-logS = tell . (`Prelude.(::)` [])
-
-public export
-headM : Vect n a -> Maybe a
-headM [] = Nothing
-headM (x :: _) = Just x
diff --git a/src/Core/Normalize.idr b/src/Core/Normalize.idr
index 9066146..4d866fd 100644
--- a/src/Core/Normalize.idr
+++ b/src/Core/Normalize.idr
@@ -10,12 +10,16 @@ import Control.Monad.Either
 
 import Data.Nat
 import Data.Vect
+import Data.IOArray
+import Data.IORef
 
 %default total
 
 mutual
   public export
-  app : Value -> Value -> PI Value
+  app : {auto deftrs    : RefA DTR Value}
+        -> {auto frst   : Ref  NST Nat}
+        -> Value -> Value -> PI Value
   app (VClos env (TLam sc))       x = eval (x :: env) sc
 
   app (VClos env (TTopInd c st)) VTop = eval env st
@@ -36,8 +40,15 @@ mutual
   app f x = pure (VApp f x)
 
   public export
-  eval : Ctx n -> Term n -> PI Value
-  eval env (TVar i)   = pure (index i env)
+  eval : {auto deftrs : RefA DTR Value}
+         -> {auto frst   : Ref NST Nat} 
+         -> Ctx n -> Term n -> PI Value
+  eval env (TVar i)    = pure (index i env)
+  eval env (TDef i)    = do
+    res <- getArr DTR i
+    case res of
+         Just x  => pure x
+         Nothing => oops "TDef term lookup"
   eval env TType       = pure VType
   eval env TTop        = pure VTop
   eval env TStar       = pure VStar
@@ -55,7 +66,9 @@ mutual
   eval env tr         = pure (VClos env tr)
 
   public export
-  whnf : Value -> PI Value
+  whnf : {auto deftrs    : RefA DTR Value}
+         -> {auto frst   : Ref  NST Nat} 
+         -> Value -> PI Value
   whnf (VClos env tr) = eval env tr
   whnf (VApp f x) = do
     f' <- whnf f
diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index d5528fd..8cab18a 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -9,6 +9,9 @@ import Core.Misc
 {-
   The type of terms is indexed by the size of the environment in which
   they are valid, that is, it is impossible to construct an ill-scoped term.
+
+  Defs are used for performance reasons and are not implemented in a type safe manner.
+  if a def is not in scope the checker will scream at you.
 -}
 public export
 data Term : (_ : Index) -> Type where
@@ -40,8 +43,11 @@ data Term : (_ : Index) -> Type where
   TPi     : Term n -> Term (S n) -> Term n       -- Pi type            (∏ _ : A . B _ )
 
   TApp    : Term n -> Term n -> Term n           -- Appliction
+
   TVar    : Fin n  -> Term n                     -- Variable
 
+  TDef    : Int    -> Term n                     -- Def Variable
+
 infixl 3 `TApp`
 
 public export
@@ -76,6 +82,7 @@ Show (Term n) where
 
   show (TApp f x)      = "(" ++ show f ++ ") TApp (" ++ show x ++ ")"
   show (TVar i)        = "Var " ++ show i
+  show (TDef i)        = "Def " ++ show i
 
 public export
 weakTr : Term n -> Term (S n)
@@ -105,6 +112,7 @@ weakTr = go 0
     go n (TVar i)          = if weaken i < n
                                 then TVar (weaken i)
                                 else TVar (FS i)
+    go n (TDef i)          = TDef i
 
 public export
 weakTr2 : Term n -> Term (2+n)
diff --git a/src/Core/Tests.idr b/src/Core/Tests.idr
deleted file mode 100644
index 1ff9b3b..0000000
--- a/src/Core/Tests.idr
+++ /dev/null
@@ -1,155 +0,0 @@
-module Core.Tests
-
-import Core.Term
-import Core.Check
-import Core.Convert
-import Core.Misc
-import Core.Normalize
-import Core.Value
-
-import Control.Monad.RWS
-import Control.Monad.Identity
-import Control.Monad.Either
-
-import Data.Fin
-
-%default total
-
-{- λA. λx. x : ∏ (A : Type) → A → A -}
-test_id : Either String (Bool, List String)
-test_id = typecheck (TLam (TLam (TVar 0)))
-                    (TPi TType (TPi (TVar 0) (TVar 1)))
-
-{- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -}
-test_app : Either String (Bool, List String)
-test_app = typecheck (TLam (TLam (TLam (TLam (TVar 1 `TApp` TVar 0)))))
-                     (TPi TType 
-                          (TPi (TPi (TVar 0) TType)
-                               (TPi (TPi (TVar 1) (TVar 1 `TApp` TVar 0)) 
-                                    (TPi (TVar 2) (TVar 2 `TApp` TVar 0)))))
-
-{- λ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 (TVar 1 `TApp` TVar 0)))
-      y <- eval ctx0 (TLam (TLam (TLam (TVar 2 `TApp` TVar 0) `TApp` TVar 0)))
-      convert x y
-
-addition : Term 0
-addition = TNatInd (TLam (TPi TNat TNat)) 
-                   (TLam (TVar 0)) 
-                   (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TVar 1 `TApp` TVar 0)))))
-
-additionty : Term 0
-additionty = TPi TNat (TPi TNat TNat)
-
-additionty_test : Either String (Bool, List String)
-additionty_test = typecheck additionty TType
-
-addition_test : Either String (Bool, List String)
-addition_test = typecheck addition additionty
-
-{- 2 + 1 = 3 -}
-addition_compute_test : Either String (Bool, List String)
-addition_compute_test = resolve action
-  where
-    action : PI Bool
-    action = do
-      x <- eval ctx0 (addition `TApp` TSuc (TSuc TZero) `TApp` TSuc TZero)
-      y <- eval ctx0 (TSuc (TSuc (TSuc TZero)))
-      convert x y
-
-multi : Term 0
-multi = TNatInd (TLam (TPi TNat TNat)) 
-                (TLam TZero)
-                (TLam {-n-} (TLam {-n*-} (TLam {-m-} (weakTr3 addition `TApp` TVar 0 `TApp` (TVar 1 `TApp` TVar 0)))))
-
-multity : Term 0
-multity = TPi TNat (TPi TNat TNat)
-
-multity_test : Either String (Bool, List String)
-multity_test = typecheck multity TType
-
-multi_test : Either String (Bool, List String)
-multi_test = typecheck multi multity
-
-{- 2 * 3 = 6 -}
-multi_compute_test : Either String (Bool, List String)
-multi_compute_test = resolve action
-  where
-    action : PI Bool
-    action = do
-      x <- eval ctx0 (multi `TApp` TSuc (TSuc TZero) `TApp` TSuc (TSuc (TSuc TZero)))
-      y <- eval ctx0 (TSuc (TSuc (TSuc (TSuc (TSuc (TSuc TZero))))))
-      convert x y
-
--- no, not that kind
-unit_test : Either String (Bool, List String)
-unit_test = typecheck TStar TTop
-
-absurd_test : Either String (Bool, List String)
-absurd_test = typecheck (TLam (TBotInd (TLam (TVar 1)))) (TPi TType (TPi TBot (TVar 1)))
-
-pr1ty : Term 0
-pr1ty = TPi TType {- A : Type -}
-            (TPi (TPi (TVar 0) TType) {- B : A → Type -}
-                 (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
-                      (TVar 2)))
-
-pr1 : Term 0
-pr1 = TLam {- A : Type -} 
-           (TLam {- B : A → Type -}
-                 (TSigInd (TVar 1) (TVar 0) (TLam {-ΣAB-} (TVar 2)) (TLam (TLam (TVar 1)))))
-
-pr1ty_test : Either String (Bool, List String)
-pr1ty_test = typecheck pr1ty TType
-
-pr1_test : Either String (Bool, List String)
-pr1_test = typecheck pr1 pr1ty
-
-pr2ty : Term 0
-pr2ty = TPi TType {- A : Type -}
-            (TPi (TPi (TVar 0) TType) {- B : A → Type -}
-                 (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
-                      (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0))))
-
-pr2 : Term 0
-pr2 = TLam {- A : Type -} 
-           (TLam {- B : A → Type -}
-                 (TSigInd (TVar 1)
-                          (TVar 0)
-                          (TLam {-ΣAB-}
-                                (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0)))
-                          (TLam (TLam (TVar 0)))))
-
-pr2ty_test : Either String (Bool, List String)
-pr2ty_test = typecheck pr2ty TType
-
-pr2_test : Either String (Bool, List String)
-pr2_test = typecheck pr2 pr2ty
-
-pr2ty_let : Term 0
-pr2ty_let = TLet pr1ty pr1 {- pr1 : pr1ty -}
-                 (TPi TType {- A : Type -}
-                      (TPi (TPi (TVar 0) TType) {- B : A → Type -}
-                           (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
-                                (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0)))))
-
-pr2_let : Term 0
-pr2_let = TLet pr1ty pr1 {- pr1 : pr1ty -}
-               (TLam {- A : Type -} 
-                     (TLam {- B : A → Type -}
-                           (TSigInd (TVar 1)
-                                    (TVar 0)
-                                    (TLam {-ΣAB-}
-                                          (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0)))
-                                    (TLam (TLam (TVar 0))))))
-
-pr2ty_let_test : Either String (Bool, List String)
-pr2ty_let_test = typecheck pr2ty_let TType
-
-pr2_let_test : Either String (Bool, List String)
-pr2_let_test = typecheck pr2_let pr2ty_let
diff --git a/src/Main.idr b/src/Main.idr
index 2d77fa4..9607846 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -2,22 +2,59 @@ module Main
 
 import Core.Check
 import Core.Term
+import Core.Value
+import Core.Normalize
+import Core.Misc
 import Parser.Parse
 
+import Control.Monad.Either
 import Data.Vect
 import Data.String
+import Data.IORef
+import Data.IOArray
 import System
 import System.File
 
-unwrap : {a : Type} -> Show a => Either a b -> IO b
-unwrap {a = a} = \case 
+smartPrint : {a : Type} -> Show a => a -> IO ()
+smartPrint {a = String} = putStrLn
+smartPrint {a = _}      = printLn
+
+isTrue : String -> Bool -> IO ()
+isTrue _   True  = pure ()
+isTrue str False = putStrLn str >> exitFailure
+
+unwrapCC : {a : Type} -> Show a => IO b -> Either a b -> IO b
+unwrapCC {a = a} iob = \case 
                  Left e  => do
-                   case a of
-                        String => putStrLn e
-                        _      => printLn e
-                   exitFailure
+                   smartPrint e
+                   iob
                  Right s => pure s
 
+unwrap : {a : Type} -> Show a => Either a b -> IO b
+unwrap = unwrapCC exitFailure
+
+createNST : IO (Ref NST Nat)
+createNST = do
+  nstIoRef <- newIORef 0
+  pure (MkRefP NST nstIoRef)
+
+createDTX : (label : Type) -> Int -> IO (RefA label Value)
+createDTX label n = do
+  arr <- newArray n
+  pure (MkRefP label arr)
+
+typeCheck : {auto deftrs    : RefA DTR Value}
+            -> {auto deftys : RefA DTY Value}
+            -> {auto frst   : Ref  NST Nat}
+            -> Int -> List (Term 0, Term 0) -> IO ()
+typeCheck i []                 = pure ()
+typeCheck i ((ty, tr) :: defs) = do
+  vty <- unwrap =<< resolve (eval [] ty)
+  vtr <- unwrap =<< resolve (eval [] tr)
+  isTrue "putArr DTY" =<< putArr DTY i vty
+  isTrue "putArr DTR" =<< putArr DTR i vtr
+  typeCheck (i+1) defs
+
 replRead : IO String
 replRead = do
   line <- getLine
@@ -27,19 +64,40 @@ replRead = do
                ":exit" => exitSuccess
                _       => pure line
 
-repl : (n : Nat) -> Vect n String ->  IO ()
-repl n env = do
+repl : {auto deftrs    : RefA DTR Value}
+       -> {auto deftys : RefA DTY Value}
+       -> {auto frst   : Ref  NST Nat}
+       -> List String -> IO a
+repl strs = do
   line <- replRead
-  printLn =<< unwrap (parseEnv n env line)
-  repl n env
+  term <- unwrapCC (repl strs) (parseEnv strs line)
+  type <- unwrapCC (repl strs) =<< resolve (whnf =<< infer [] [] term)
+  val  <- unwrapCC (repl strs) =<< resolve (whnf =<< eval  [] term)
+  putStr "inferred type: "
+  printLn type
+  putStr "weak head normal form: "
+  printLn val
+  repl strs
 
 main : IO ()
 main = getArgs >>= \case
-          (_ :: x :: _) => do
-            putStr (x ++ ": ")
-            res <- readFile x >>= unwrap >>= unwrap . parsetoplevel
-                              >>= unwrap . (`typecheck` TTop)
-            if fst res
-               then putStrLn ("Success !")
-               else unwrap   (Left res)
-          _             => repl 0 []
+          (_ :: x :: xs) => do
+            putStrLn (x ++ ": ")
+            putStr "Parsing: "
+            (strs, res) <- readFile x >>= unwrap >>= unwrap . toplevel
+            putStrLn " OK!"
+            let rlen = cast (length res)
+            nst <- createNST
+            dtr <- createDTX DTR rlen
+            dty <- createDTX DTY rlen
+            putStr "Typechecking: "
+            typeCheck 0 res
+            putStrLn "OK!"
+            case xs of
+                 ("repl" :: _) => repl strs
+                 _             => exitSuccess
+          _ => do
+            nst <- createNST
+            dtr <- createDTX DTR 0
+            dty <- createDTX DTY 0
+            repl []
diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr
index b3aeed9..de717a5 100644
--- a/src/Parser/Parse.idr
+++ b/src/Parser/Parse.idr
@@ -211,40 +211,40 @@ lexPi str =
 {- Basic idea, parsing has a list of the identifiers to convert to -}
 {- de bruijn indecies, and a Nat to keep track of context size -}
 mutual
-  expr : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  expr n env = tpi n env
-           <|> tsigma n env
-           <|> tarr n env
-           <|> (do 
-             e <- expr1 n env
-             tapp n env e <|> pure e)
+  expr : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  expr defs n env = tpi defs n env
+                <|> tsigma defs n env
+                <|> tarr defs n env
+                <|> (do 
+                  e <- expr1 defs n env
+                  tapp defs n env e <|> pure e)
 
 
-  expr1 : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  expr1 n env = ttopind n env
-            <|> tbotind n env
-            <|> tsuc n env
-            <|> tnatind n env
-            <|> tsigind n env
-            <|> tid n env
-            <|> trefl n env
-            <|> tj n env
-            <|> (do
-              t <- term n env
-              tapp n env t <|> pure t)
+  expr1 : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  expr1 defs n env = ttopind defs n env
+                 <|> tbotind defs n env
+                 <|> tsuc defs n env
+                 <|> tnatind defs n env
+                 <|> tsigind defs n env
+                 <|> tid defs n env
+                 <|> trefl defs n env
+                 <|> tj defs n env
+                 <|> (do
+                   t <- term defs n env
+                   tapp defs n env t <|> pure t)
 
-  term : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  term n env = ttype
-           <|> ttop
-           <|> tstar
-           <|> tbot
-           <|> tnat
-           <|> tnum
-           <|> tpair n env
-           <|> tlet n env
-           <|> tlam n env
-           <|> tvar n env
-           <|> paren n env
+  term : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  term defs n env = ttype
+                <|> ttop
+                <|> tstar
+                <|> tbot
+                <|> tnat
+                <|> tnum
+                <|> tpair defs n env
+                <|> tlet defs n env
+                <|> tlam defs n env
+                <|> tvar defs n env
+                <|> paren defs n env
 
   ttype : Grammar () PiToken True (Term n)
   ttype = match PTType >> pure TType
@@ -255,22 +255,22 @@ mutual
   tstar : Grammar () PiToken True (Term n)
   tstar = match PTStar >> pure TStar
 
-  ttopind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  ttopind n env = do
+  ttopind : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  ttopind defs n env = do
     match PTTopInd
     commit
-    c  <- term n env
-    st <- term n env
+    c  <- term defs n env
+    st <- term defs n env
     pure (TTopInd c st)
 
   tbot : Grammar () PiToken True (Term n)
   tbot = match PTBot >> pure TBot
 
-  tbotind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tbotind n env = do
+  tbotind : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tbotind defs n env = do
     match PTBotInd
     commit
-    c <- term n env
+    c <- term defs n env
     pure (TBotInd c)
 
   tnat : Grammar () PiToken True (Term n)
@@ -285,162 +285,161 @@ mutual
       conv 0     = TZero
       conv (S n) = TSuc (conv n)
 
-  tsuc : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tsuc n env = do
+  tsuc : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tsuc defs n env = do
     match PTSuc
     commit
-    TSuc <$> term n env
+    TSuc <$> term defs n env
 
-  tnatind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tnatind n env = do
+  tnatind : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tnatind defs n env = do
     match PTNatInd
     commit
-    c <- term n env
-    z <- term n env
-    s <- term n env
+    c <- term defs n env
+    z <- term defs n env
+    s <- term defs n env
     pure (TNatInd c z s)
 
-  tsigma : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tsigma n env = do
+  tsigma : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tsigma defs n env = do
     match PTSigma
     commit
     match PTLParen
     arg <- match PTIdentifier
     match PTColon
-    a <- expr n env
+    a <- expr defs n env
     match PTRParen
-    b <- expr (S n) (arg :: env)
+    b <- expr defs (S n) (arg :: env)
     pure (TSigma a (TLam b))
 
-  tpair : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tpair n env = do
+  tpair : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tpair defs n env = do
     match PTLParen
-    x <- expr n env
+    x <- expr defs n env
     match PTComma
     commit
-    y <- expr n env
+    y <- expr defs n env
     match PTRParen
     pure (TPair x y)
 
-  tsigind : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tsigind n env = do
+  tsigind : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tsigind defs n env = do
     match PTSigInd
     commit
-    a <- term n env
-    b <- term n env
-    c <- term n env
-    f <- term n env
+    a <- term defs n env
+    b <- term defs n env
+    c <- term defs n env
+    f <- term defs n env
     pure (TSigInd a b c f)
 
-  tid : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tid n env = do
+  tid : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tid defs n env = do
     match PTId
     commit
-    ty <- term n env
-    a  <- term n env
-    b  <- term n env
+    ty <- term defs n env
+    a  <- term defs n env
+    b  <- term defs n env
     pure (TId ty a b)
 
-  trefl : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  trefl n env = do
+  trefl : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  trefl defs n env = do
     match PTRefl
     commit
-    ty <- term n env
-    tr <- term n env
+    ty <- term defs n env
+    tr <- term defs n env
     pure (TRefl ty tr)
 
-  tj : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tj n env = do
+  tj : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tj defs n env = do
     match PTJ
     commit
-    ty <- term n env
-    a  <- term n env
-    b  <- term n env
-    c  <- term n env
-    d  <- term n env
+    ty <- term defs n env
+    a  <- term defs n env
+    b  <- term defs n env
+    c  <- term defs n env
+    d  <- term defs n env
     pure (TJ ty a b c d)
 
-  tlet : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tlet n env = do
+  tlet : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tlet defs n env = do
     match PTLet
     commit
     arg <- match PTIdentifier
     match PTColon
-    ty <- expr n env
+    ty <- expr defs n env
     match PTDefEq
-    tr <- expr n env
+    tr <- expr defs n env
     match PTIn
-    tri <- expr (S n) (arg :: env)
+    tri <- expr defs (S n) (arg :: env)
     pure (TLet ty tr tri)
 
-  tlam : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tlam n env = do
+  tlam : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tlam defs n env = do
     match PTLambda
     commit
     arg <- match PTIdentifier
     match PTDot
-    e <- expr (S n) (arg :: env)
+    e <- expr defs (S n) (arg :: env)
     pure (TLam e)
 
-  tpi : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tpi n env = do
+  tpi : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tpi defs n env = do
     match PTPi
     commit
     match PTLParen
     arg <- match PTIdentifier
     match PTColon
-    a <- expr n env
+    a <- expr defs n env
     match PTRParen
-    b <- expr (S n) (arg :: env)
+    b <- expr defs (S n) (arg :: env)
     pure (TPi a b)
 
-  tarr : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tarr n env = do
-    l <- expr1 n env
+  tarr : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tarr defs n env = do
+    l <- expr1 defs n env
     match PTArrow
     commit
-    r <- expr (S n) ("" :: env)
+    r <- expr defs (S n) ("" :: env)
     pure (TPi l r)
 
-  tapp : (n : Nat) -> Vect n String -> Term n -> Grammar () PiToken True (Term n)
-  tapp n env e1 = do
-    e2 <- term n env
-    tapp1 n env (TApp e1 e2)
+  tapp : List String -> (n : Nat) -> Vect n String -> Term n -> Grammar () PiToken True (Term n)
+  tapp defs n env e1 = do
+    e2 <- term defs n env
+    tapp1 defs n env (TApp e1 e2)
 
-  tapp1 : (n : Nat) -> Vect n String -> Term n -> Grammar () PiToken False (Term n)
-  tapp1 n env e = tapp n env e <|> pure e
+  tapp1 : List String -> (n : Nat) -> Vect n String -> Term n -> Grammar () PiToken False (Term n)
+  tapp1 defs n env e = tapp defs n env e <|> pure e
 
-  tvar : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  tvar n env = do
+  tvar : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  tvar defs n env = do
     str <- match PTIdentifier
     commit
-    fromMaybe (fail ("'" ++ str ++ "' not in env")) (pure . TVar <$> findIndex (== str) env)
+    fromMaybe (fromMaybe (fail ("'" ++ str ++ "' not idefs n env"))
+                         (pure . TDef . cast . finToInteger <$> findIndex (== str) defs))
+              (pure . TVar <$> findIndex (== str) env)
 
-  paren : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-  paren n env = do
+  paren : List String -> (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
+  paren defs n env = do
     match PTLParen
     commit
-    e <- expr n env
+    e <- expr defs n env
     match PTRParen
     pure e
 
-definitions : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n)
-definitions n env = do
+definitions : List String -> Grammar () PiToken True (List String, List (Term 0, Term 0))
+definitions defs = do
     match PTLet
     commit
     arg <- match PTIdentifier
     match PTColon
-    ty <- expr n env
+    ty <- expr defs 0 []
     match PTDefEq
-    tr <- expr n env
-    next <- definitions (S n) (arg :: env) <|> pure TStar
-    pure (TLet ty tr next)
+    tr <- expr defs 0 []
+    next <- definitions (arg :: defs) <|> pure ([], [])
+    pure (arg :: fst next, (ty, tr) :: snd next)
 
-toplevel : Grammar () PiToken True (Term 0)
-toplevel = definitions 0 []
-
-parsePi : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) -> List (WithBounds PiToken) -> Either String (Term n)
-parsePi n env parseEntry toks =
+parsePi : List String -> Grammar () PiToken True a -> List (WithBounds PiToken) -> Either String a
+parsePi defs parseEntry toks =
   case parse parseEntry $ filter (not . ignored) toks of
     Right (l, []) => Right l
     Right (_, l) => Left ("contains tokens that were not consumed: " ++ show l)
@@ -452,20 +451,20 @@ parsePi n env parseEntry toks =
 
 
 public export
-parse : (n : Nat) -> Vect n String -> Grammar () PiToken True (Term n) -> String -> Either String (Term n)
-parse n env parseEntry x =
+parse : List String -> Grammar () PiToken True a -> String -> Either String a
+parse defs parseEntry x =
   case lexPi x of
-    Just toks => parsePi n env parseEntry toks
+    Just toks => parsePi defs parseEntry toks
     Nothing => Left "Failed to lex."
 
 public export
 parse0 : String -> Either String (Term 0)
-parse0 = parse 0 [] (expr 0 [])
+parse0 = parse [] (expr [] 0 [])
 
 public export
-parseEnv : (n : Nat) -> Vect n String -> String -> Either String (Term n)
-parseEnv n env = parse n env (expr n env)
+parseEnv : List String -> String -> Either String (Term 0)
+parseEnv defs = parse defs (expr defs 0 [])
 
 public export
-parsetoplevel : String -> Either String (Term 0)
-parsetoplevel = parse 0 [] (toplevel)
+toplevel : String -> Either String (List String, List (Term 0, Term 0))
+toplevel = parse [] (definitions [])
diff --git a/src/Parser/Tests.idr b/src/Parser/Tests.idr
deleted file mode 100644
index ffa4823..0000000
--- a/src/Parser/Tests.idr
+++ /dev/null
@@ -1,89 +0,0 @@
-module Parser.Tests
-
-import Core.Term
-import Core.Check
-import Core.Convert
-import Core.Misc
-import Core.Normalize
-import Core.Value
-
-import Control.Monad.RWS
-import Control.Monad.Identity
-import Control.Monad.Either
-
-import Data.Fin
-
-import Parser.Parse
-
-%default total
-
-convCheck : Term 0 -> Term 0 -> Either String (Bool, List String)
-convCheck a b = resolve action
-  where
-    action : PI Bool
-    action = do
-      x <- eval ctx0 a
-      y <- eval ctx0 b
-      convert x y
-
-{- λA. λx. x : ∏ (A : Type) → A → A -}
-test_id : Either String (Bool, List String)
-test_id = do
-  ty <- parse0 "Π ( A : Type ) A → A"
-  tr <- parse0 "λA.λx.x"
-  typecheck tr ty
-
-{- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -}
-test_app : Either String (Bool, List String)
-test_app = do
-  ty <- parse0 "Π (A : Type) Π (B : A → Type) Π (f : Π (x : A) B x) Π (x : A) B x"
-  tr <- parse0 "λA. λB. λf. λx. f x"
-  typecheck tr ty
-
-{- λf. f ≃ λf. λx. f x -}
-eta_test : Either String (Bool, List String)
-eta_test = do
-  a <- parse0 "λf. f"
-  b <- parse0 "λf. λx. f x"
-  convCheck a b
-
-additionty_test : Either String (Bool, List String)
-additionty_test = do
-  ty <- parse0 "ℕ → ℕ → ℕ"
-  typecheck ty TType
-
-addition_test : Either String (Bool, List String)
-addition_test = do
-  ty <- parse0 "ℕ → ℕ → ℕ"
-  tr <- parse0 "ℕ-ind (λ_. ℕ → ℕ) (λx.x) (λn.λnp.λm. suc (np m))"
-  typecheck tr ty
-
--- no, not that kind
-unit_test : Either String (Bool, List String)
-unit_test = do
-  ty <- parse0 "⊤"
-  tr <- parse0 "★"
-  typecheck tr ty
-
-absurd_test : Either String (Bool, List String)
-absurd_test = do
-  ty <- parse0 "Π(A : Type) ⊥ → A"
-  tr <- parse0 "λA. ⊥-ind (λ_. A)"
-  typecheck tr ty
-
-
-pr1_test : Either String (Bool, List String)
-pr1_test = do
-  tr <- parse0 $ "let pr1 : Π (A : Type) Π (B : A → Type) (Σ (a : A) B a) → A"
-                      ++ "≔ λA.λB. Σ-ind A B (λ_. A) (λa.λBa. a)"
-                      ++ "in ★"
-  typecheck tr TTop
-
-pr1_pr2_test : Either String (Bool, List String)
-pr1_pr2_test = do
-  tr <- parse0 $ "let pr1 : Π (A : Type) Π (B : A → Type) (Σ (a : A) B a) → A"
-                      ++ "≔ λA.λB. Σ-ind A B (λ_. A) (λa.λBa. a)"
-                      ++ "in let pr2 : Π (A : Type) Π (B : A → Type) Π (s : Σ (a : A) B a) B (pr1 A B s)"
-                      ++            "≔ λA.λB. Σ-ind A B (λs. B (pr1 A B s)) (λa.λBa. Ba)"
-                      ++            "in ★"
-  typecheck tr TTop
diff --git a/tests/id1.pi b/tests/id1.pi
new file mode 100644
index 0000000..ede76bf
--- /dev/null
+++ b/tests/id1.pi
@@ -0,0 +1,3 @@
+let transport : Π (A : Type) Π (f : A → Type) Π (x : A) Π (y : A)
+                Id A x y → f x → f y
+  ≔ λA.λf.λx.λy. J A x y (λa.λb.λ_. f a → f b) (λa.a)
diff --git a/tests/id2.pi b/tests/id2.pi
new file mode 100644
index 0000000..d6b25af
--- /dev/null
+++ b/tests/id2.pi
@@ -0,0 +1,3 @@
+let ap : Π (A : Type) Π (B : Type) Π (f : A → B)
+         Π (x : A) Π (y : A) Id A x y → Id B (f x) (f y)
+  ≔ λA.λB.λf.λx.λy. J A x y (λa.λb.λ_. Id B (f a) (f b)) (refl B (f x))