From 09671a0c1a836e8606a5f1b139855bb5c183a080 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Sun, 24 Apr 2022 14:30:21 +0200
Subject: [PATCH] this is hard :(

---
 src/Ctx.idr       | 10 +++++++---
 src/Normalize.idr | 41 +++++++++++++++++++++++++++++++----------
 src/Term.idr      |  4 ++++
 src/Value.idr     | 18 +++++++++++++++---
 4 files changed, 57 insertions(+), 16 deletions(-)

diff --git a/src/Ctx.idr b/src/Ctx.idr
index 1b6f10f..7c88cec 100644
--- a/src/Ctx.idr
+++ b/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
diff --git a/src/Normalize.idr b/src/Normalize.idr
index 3db568d..b4e1122 100644
--- a/src/Normalize.idr
+++ b/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)
diff --git a/src/Term.idr b/src/Term.idr
index f643c9c..ef79a66 100644
--- a/src/Term.idr
+++ b/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
diff --git a/src/Value.idr b/src/Value.idr
index 3f73276..9373bcf 100644
--- a/src/Value.idr
+++ b/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