From 5790d22dcc531f58a550448170177d23460294d3 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Wed, 11 May 2022 16:22:05 +0200
Subject: [PATCH] about to ruin stuff

---
 src/Ctx.idr       | 26 ++++++++++++++++++++++----
 src/Misc.idr      | 28 ++++++++++++++++++++++++++++
 src/Normalize.idr | 21 +++++++++++++++------
 src/Value.idr     |  1 +
 4 files changed, 66 insertions(+), 10 deletions(-)

diff --git a/src/Ctx.idr b/src/Ctx.idr
index 7c88cec..a782f78 100644
--- a/src/Ctx.idr
+++ b/src/Ctx.idr
@@ -13,10 +13,28 @@ data Ctx : (Index -> Type) -> Index -> Type where
   Nil  : Ctx ty 0
   (::) : {n : _} -> ty n -> Ctx ty n -> Ctx ty (S n)
 
+-- indexed by amount of free variables
 public export
-data Closure : (Index -> Type) -> Type where
-  MkClosure : {n : _} -> Ctx ty n -> ty n -> Closure ty
+data Closure : (Index -> Type) -> Index -> Type where
+  MkClosure : {n : _} -> Ctx ty n -> ty (m + n) -> Closure ty m
 
 public export
-lookup : {m : _} -> (n : Nat) -> Ctx ty m -> LT n m -> ty (minus m n)
-lookup = ?wa
+enclose : {n : _} -> ty n -> Closure ty n
+enclose {n = n} ty = MkClosure Nil (rewrite plusZeroRightNeutral n in ty)
+
+public export
+lookup : {m : _} -> (n : Nat) -> Ctx ty m -> LT n m -> ty (minus m (S n))
+lookup {m = S m} Z (x :: _) _       = rewrite minusZeroRight m in x
+lookup (S n) (_ :: ctx) (LTESucc p) = lookup n ctx p
+
+public export
+strengthen : Ctx ty (S n) -> Ctx ty n
+strengthen (_ :: ctx) = ctx
+
+public export
+strengthenTo : {n,m : _} -> Ctx ty m -> LTE n m -> Ctx ty n
+strengthenTo {n = Z} _ _ = Nil
+strengthenTo (x :: ctx) (LTESucc p)
+  = case lteSplit p of
+         Left Refl => x :: ctx
+         Right p2 => strengthenTo ctx p2
diff --git a/src/Misc.idr b/src/Misc.idr
index 9419ba0..ce0be6b 100644
--- a/src/Misc.idr
+++ b/src/Misc.idr
@@ -28,3 +28,31 @@ public export
 lteS : {n : _} -> LTE n (S n)
 lteS {n = Z}   = LTEZero
 lteS {n = S n} = LTESucc lteS
+
+public export
+lteSplit : {m : _} -> LTE n m -> Either (n = m) (LT n m)
+lteSplit {m = Z} LTEZero = Left Refl
+lteSplit {m = S m} LTEZero = Right (LTESucc LTEZero)
+lteSplit {m = S m} (LTESucc p) = case lteSplit p of
+                                      Left p2 => Left (cong S p2)
+                                      Right p2 => Right (LTESucc p2)
+
+public export
+minusLte : {m,n : _} -> LTE (minus n (S m)) n
+minusLte {n = Z} = LTEZero
+minusLte {n = S n} {m = Z} = rewrite minusZeroRight n in lteSuccRight reflexive
+minusLte {n = S n} {m = S m} = lteSuccRight (minusLte {n = n} {m = m})
+
+public export
+prevEq : (i, j : Nat) -> S i = S j -> i = j
+prevEq Z Z Refl = Refl
+prevEq (S i) (S _) Refl = Refl
+
+public export
+natEqDecid : (n, m : Nat) -> Either (Not (n = m)) (n = m) 
+natEqDecid Z Z        = Right Refl
+natEqDecid (S _) Z    = Left absurd
+natEqDecid Z (S _)    = Left absurd
+natEqDecid (S n) (S m) = case natEqDecid n m of
+                              Right p => Right (cong S p)
+                              Left  p => Left  (p . prevEq n m)
diff --git a/src/Normalize.idr b/src/Normalize.idr
index b4e1122..1d00053 100644
--- a/src/Normalize.idr
+++ b/src/Normalize.idr
@@ -9,6 +9,8 @@ import Data.Nat
 
 %default total
 
+-- There is some nasty assert_total here since I cannot solve the halting problem
+
 public export
 asTerm : NF -> Term 0
 asTerm NType = TType
@@ -19,15 +21,22 @@ public export
 fromNF : NF -> Glue
 fromNF nf = MkGlue (asTerm nf) (const (pure nf))
 
+substStep : {n,m : _} -> Term m -> LTE m n -> Term (S n) -> Term n
+substStep {m = m} tr p tr' = case tr' of -- case somehow needed for idris not to loop over metavariable
+                       TType        => TType
+                       (TLam ty sc) => TLam (substStep tr p ty) (substStep tr (lteSuccRight p) sc)
+                       (TPi  ty sc) => TPi  (substStep tr p ty) (substStep tr (lteSuccRight p) sc)
+                       (TApp f  x)  => TApp (substStep tr p f)  (substStep tr p x)  
+                       (TVar i  p)  => case natEqDecid m i of
+                                            Left  p => ?que1
+                                            Right p => ?que2
+
 mutual
-  evalClosure : {n : Nat} -> Closure Term -> PI (Term n)
+  evalClosure : {n : Nat} -> Closure Term 0 -> 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 : {n : Nat} -> List (Closure Term 0) -> Ctx Term n -> Term n -> PI NF
   eval stack env TType = pure NType
 
   -- dirty
@@ -35,7 +44,7 @@ mutual
 
   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 (TVar m p)   = assert_total $ eval stack (strengthenTo env minusLte) (lookup m env p)
 
   eval stack env (TPi ty sc)  = ?idk
 
diff --git a/src/Value.idr b/src/Value.idr
index 9373bcf..9a32f47 100644
--- a/src/Value.idr
+++ b/src/Value.idr
@@ -2,6 +2,7 @@ module Value
 
 import Term
 import Misc
+import Ctx
 
 %default total