this is hard :(

src/Ctx.idr

@@ -9,10 +9,14 @@ import Data.Nat
 infixr 7 ::
 
 public export
-data Ctx : (Index -> Type) -> (_ : Index) -> Type where
+data Ctx : (Index -> Type) -> Index -> Type where
   Nil  : Ctx ty 0
-  (::) : ty n -> Ctx ty n -> Ctx ty (S n)
+  (::) : {n : _} -> ty n -> Ctx ty n -> Ctx ty (S n)
 
 public export
 data Closure : (Index -> Type) -> Type where
-  MkClosure : Ctx ty n -> ty n -> Closure ty
+  MkClosure : {n : _} -> Ctx ty n -> ty n -> Closure ty
+
+public export
+lookup : {m : _} -> (n : Nat) -> Ctx ty m -> LT n m -> ty (minus m n)
+lookup = ?wa

src/Normalize.idr

@@ -10,16 +10,37 @@ import Data.Nat
 %default total
 
 public export
-eval : List (Closure Term) -> Ctx Term n -> Term n -> PI NF
-eval stack ctx TType      = pure NType
-eval stack ctx (TVar n p) = pure NType
-
-eval stack ctx (TApp f x) = eval (MkClosure ctx x :: stack) ctx f
-eval _ _ _ = oops "eval"
+asTerm : NF -> Term 0
+asTerm NType = TType
+asTerm (NLam ty sc) = TLam (asTerm ty) sc
+asTerm (NPi  ty sc) = TPi  (asTerm ty) sc
 
 public export
-finalize : Term 0 -> PI NF
-finalize term = eval [] Nil term
+fromNF : NF -> Glue
+fromNF nf = MkGlue (asTerm nf) (const (pure nf))
 
--- idris can't see that there is no case for TVar itself
-finalize (TVar n p) = void (succNotLTEzero p)
+mutual
+  evalClosure : {n : Nat} -> Closure Term -> PI (Term n)
+  evalClosure (MkClosure ctx term) = eval [] ctx term >>= pure . weaken0 . asTerm
+
+  lookupLocal : (n : Nat) -> Ctx Term m -> LT n m -> PI NF
+  lookupLocal = ?how
+
+  public export
+  eval : {n : Nat} -> List (Closure Term) -> Ctx Term n -> Term n -> PI NF
+  eval stack env TType = pure NType
+
+  -- dirty
+  eval (thunk :: stack) env (TLam _ sc) = eval stack (!(assert_total (evalClosure thunk)) :: env) sc
+
+  eval stack env (TApp f x)   = eval (MkClosure env x :: stack) env x
+
+  eval stack env (TVar m p)   = lookupLocal m env p
+
+  eval stack env (TPi ty sc)  = ?idk
+
+  eval []    env (TLam ty sc) = ?what
+
+public export
+fromTerm : Term 0 -> Glue
+fromTerm term = MkGlue term (eval [] Nil)

src/Term.idr

@@ -54,3 +54,7 @@ weaken {p = S p} {q = S q} (LTESucc p1) (TVar r p2') =
   case p2' of 
     LTESucc p2 => TVar (minus (r + q) p)
       (LTESucc (lteTransp (minusLteMonotone (plusLteMonotoneRight q r p p2)) Refl (minusPlus p)))
+
+public export
+weaken0 : {n : _} -> Term 0 -> Term n
+weaken0 = weaken LTEZero

src/Value.idr

@@ -7,6 +7,18 @@ import Misc
 
 public export
 data NF : Type where
-  NType : NF                    -- Type of types
-  NLam  : NF    -> Term 1 -> NF -- Lambda abstraction
-  NPi   : NF    -> Term 1 -> NF -- Pi Type
+  NType : NF                 -- Type of types
+  NLam  : NF -> Term 1 -> NF -- Lambda abstraction
+  NPi   : NF -> Term 1 -> NF -- Pi Type
+
+public export
+data Glue : Type where
+  MkGlue : Term 0 -> (Term 0 -> PI NF) -> Glue
+
+public export
+getTerm : Glue -> Term 0
+getTerm (MkGlue term _) = term
+
+public export
+getNF : Glue -> PI NF
+getNF (MkGlue term f) = f term