From fc6801590f399d3511aba80b808f5446d63b010f Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Wed, 28 Feb 2024 20:58:32 -0800
Subject: [PATCH] checkpoint before removing index

---
 src/Lib/TT.idr | 110 +++++++++++++++++++++++++++++++------------------
 1 file changed, 71 insertions(+), 39 deletions(-)

diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index 532ef57..e3a6b7e 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -1,3 +1,8 @@
+-- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q
+-- or drop the indices for now.
+
+-- The Control.App requires a patched idris. :(
+
 module Lib.TT
 -- For SourcePos
 import Lib.Parser.Impl
@@ -9,6 +14,7 @@ Name : Type
 Name = String
 
 -- Trying to do well-scoped here, so the indices are proven.
+-- RIP out the indices
 
 public export
 data Icit = Implicit | Explicit
@@ -57,7 +63,15 @@ public export
 -- IS/TypeTheory.idr is calling this a Kripke function space
 -- Yaffle, IS/TypeTheory use a function here.
 -- Kovacs, Idris use Env and Tm
-Closure n = (l : Nat) -> Val (l + n) -> Val (l + n)
+
+-- in cctt kovacs refers to this as defunctionalization vs HOAS
+-- https://github.com/AndrasKovacs/cctt/blob/main/README.md#defunctionalization
+
+
+-- Yaffle is vars -> vars here
+
+
+Closure n = Val (S n) -> Val n
 
 public export
 data Val : Nat -> Type where
@@ -69,44 +83,58 @@ data Val : Nat -> Type where
   VPi : Name -> Icit -> Lazy (Val n) -> Closure n -> Val n
   VU : Val n
 
-||| Env k n holds the evaluation environment.
-||| k is the number of levels and n is the size
-||| of the environment. 
+||| LocalEnv free vars
 public export
-Env : Nat -> Nat -> Type
-Env k n = Vect n (Val k)
+LocalEnv : Nat -> Nat -> Type 
+LocalEnv k n = Vect k (Val n)
+
+public export
+Env : Nat -> Type
+Env n = Vect n (Val n)
 
 export
-eval : Env k n -> Tm n -> Val k
+eval : LocalEnv k n -> Env n -> Tm (n + k) -> Val n
 
-export
-vapp : Val k -> Val k -> Val k
-vapp (VLam _ icit t) u = t 0 u
-vapp t u = VApp t u
-
--- thinEnv : (l : Nat) -> Env k n -> Env (l + k) n
-
-thinVal : {e : Nat} -> Val k -> Val (e + k)
-thinVal (VVar x) = VVar (shift _ x)
+thinVal : Val k -> Val (S k)
+thinVal (VVar x) = VVar (shift 1 x)
 thinVal (VRef str) = VRef str
 thinVal (VApp x y) = VApp (thinVal x) (thinVal y)
-thinVal (VLam str icit f) = VLam str icit 
-      (\g, v => rewrite plusAssociative g e k in f (g + e) (rewrite sym $ plusAssociative g e k in v))
-thinVal (VPi str icit x f) = VPi str icit (thinVal {e} x) 
-      (\g, v => rewrite plusAssociative g e k in f (g + e) (rewrite sym $ plusAssociative g e k in v))
+thinVal (VLam str icit f) = VLam str icit (believe_me f) -- FIXME
+thinVal (VPi str icit x f) = VPi str icit (thinVal x) (believe_me f)
 thinVal VU = VU
 
-bind : (e : Nat) -> Val (plus e k) -> Env k n -> Env (e + k) (S n)
-bind e v env = v :: map thinVal env
 
-eval env (Ref x) = VRef x
-eval env (Bnd n) = index n env
-eval env (Lam x icit t) = VLam x icit (\e, u => eval (bind e u env) t)-- (MkClosure env t) 
-eval env (App t u) = vapp (eval env t) (eval env u)
-eval env U = VU
-eval env (Pi x icit a b) = VPi x icit (eval env a) (\e, u => eval (bind e u env) b)
+export
+vapp : Val n -> Val n -> Val n
+vapp (VLam _ icit t) u = t (thinVal u)
+vapp t u = VApp t u
+
+-- thinVal : {e : Nat} -> Val k -> Val (e + k)
+-- thinVal (VVar x) = VVar (shift _ x)
+-- thinVal (VRef str) = VRef str
+-- thinVal (VApp x y) = VApp (thinVal x) (thinVal y)
+-- thinVal (VLam str icit f) = VLam str icit 
+--       (\g, v => rewrite plusAssociative g e k in f (g + e) (rewrite sym $ plusAssociative g e k in v))
+-- thinVal (VPi str icit x f) = VPi str icit (thinVal {e} x) 
+--       (\g, v => rewrite plusAssociative g e k in f (g + e) (rewrite sym $ plusAssociative g e k in v))
+-- thinVal VU = VU
+
+
+
+bind :  Val n -> Env n -> Env (S n)
+bind v env = thinVal v :: map thinVal env
+
+-- so here we have LocalEnv free vars in Yaffle
+
+eval locs env (Ref x) = VRef x
+eval locs env (App t u) = vapp (eval locs env t) (eval locs env u)
+eval locs env U = VU
+-- yaffle breaks out binder
+eval locs env (Lam x icit t) = VLam x icit (\u => (u :: locs) env (rewrite sym $ plusSuccRightSucc n k in t))
+eval locs env (Pi x icit a b) = VPi x icit (eval locs env a) (\u => eval (u :: locs) env (rewrite sym $ plusSuccRightSucc n k in b))
 -- This one we need to make 
-eval env (Let x icit ty t u) = eval (eval env t :: env) u
+eval locs env (Let x icit ty t u) = eval (eval locs env t :: locs) env (rewrite sym $ plusSuccRightSucc n k in u)
+eval locs env (Bnd i) = index i ?hole -- env
 
 vfresh : (l : Nat) -> Val (S l)
 vfresh l = VVar last
@@ -116,14 +144,15 @@ quote : (k : Nat) -> Val k -> Tm k
 quote l (VVar k) = Bnd (complement k) -- level to index
 quote l (VApp t u) = App (quote l t) (quote l u)
 -- so this one is calling the kripke on [x] and a fresh var
-quote l (VLam x icit t) = Lam x icit (quote (S l) (t 1 (vfresh l)))
-quote l (VPi x icit a b) = Pi x icit (quote l a) (quote (S l) (b 1 $ vfresh l))
+quote l (VLam x icit t) = Lam x icit (quote (S l) (believe_me $ t (vfresh l))) -- that one is too big
+quote l (VPi x icit a b) = Pi x icit (quote l a) (quote (S l) (believe_me $ b $ vfresh l))
 quote l VU = U
 quote _ (VRef n) = Ref n
 
+-- vars -> vars -> vars in yaffle
 export
-nf : {n : Nat} -> Env 0 n -> Tm n -> Tm 0
-nf env t = quote 0 (eval env t)
+nf : {n : Nat} -> Env n -> Tm n -> Tm n
+nf env t = quote n (eval [] env (rewrite plusZeroRightNeutral n in t))
 
 public export
 conv : (lvl : Nat) -> Val n -> Val n -> Bool
@@ -142,22 +171,25 @@ record Context (n : Nat)  where
   constructor MkCtx
   
   -- These are values, they'll be the length of the environment
-  env : Env n n -- Vect n (Val f)
+  env : Env n -- Vect n (Val f)
 
   -- fine for now, consider a map later
   types : Vect n (String, Val n)
   pos : SourcePos
 
+-- data Env : (tm : SnocList Name -> Type) -> SnocList Name -> Type where
 
+-- Kovacs Small-TT has locals and globals, lets do that.  
+-- Still need to sort out the indices - one or two on env?
 
 ||| add a binding to environment
-extend : Context n n -> String -> Val n -> Context (S n) (S n)
+extend : { n : Nat} -> Context n -> String -> Val n -> Context (S n)
 extend (MkCtx env types pos) name ty with (length env)
   _ | l = 
     
-    let types' = (name,ty) :: (map $ mapSnd thinVal) types in
-    let l' : Fin (S n) := ?hole in
-    MkCtx (VVar l' :: map thinVal env) types' pos
+    let types' = Data.Vect.(::) (name, thinVal ty)   (map (map thinVal) types) in
+    let l' : Fin (S n) := last in
+    MkCtx {n=S n} (VVar l' :: map thinVal env) types' pos
     -- ?hole_0 --  { env  := (Val (length env.(Context env types pos)) :: (Context env types pos).env), types := (n, ty) :: (Context env types pos).types  } (Context env types pos)
 
 
@@ -177,7 +209,7 @@ extend (MkCtx env types pos) name ty with (length env)
 --   types : Types n   -- name lookup, prettyprint
 --   bds : Vect n BD  -- meta creation
 --   lvl : Nat -- This is n, do we need it?
---   -- Kovacs and Weirich use a position node
+--   -- Kovacs and Weirich use a position node, Idris has FC
 --   pos : SourcePos
 
 -- %name Ctx ctx