From 349115d05547c0fdf1ed5f23d8d04fa2df0abff4 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 30 Sep 2023 06:40:54 -0700
Subject: [PATCH] Checkpoint some stuff so I can rollback the rest.

---
 src/Lib/Parser.idr    | 14 +++++++++
 src/Lib/TT.idr        | 73 ++++++++++++++++++++++++++++++++++++++-----
 src/Lib/Token.idr     |  3 +-
 src/Lib/Tokenizer.idr |  1 +
 4 files changed, 83 insertions(+), 8 deletions(-)

diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 820f59d..608b4ba 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -252,3 +252,17 @@ parseMod = do
   decls <- startBlock $ someSame $ parseDecl
   pure $ MkModule name [] decls
 
+
+public export
+data ReplCmd =
+    Def Decl
+  | Norm Raw -- or just name?
+  | Check Raw
+
+
+-- Eventually I'd like immediate actions in the file, like lean, but I
+-- also want to REPL to work and we can do that first.
+export parseRepl : Parser ReplCmd
+parseRepl = Def <$> parseDecl <|> Norm <$ keyword "#nf" <*> typeExpr
+  <|> Check <$ keyword "#check" <*> typeExpr
+  
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index 81f058b..532ef57 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -28,16 +28,23 @@ data Tm : Nat -> Type where
 %name Tm t, u, v
 
 -- TODO derive
+export 
+Eq Icit where
+  Implicit == Implicit = True
+  Explicit == Explicit = True
+  _ == _ = False
+
+||| Eq on Tm. We've got deBruijn indices, so I'm not comparing names
 export
 Eq (Tm n) where
   -- (Local x) == (Local y) = x == y
   (Bnd x) == (Bnd y) = x == y
   (Ref x) == (Ref y) = x == y
-  (Lam str icit t) == y = ?rhs_3
-  (App t u) == y = ?rhs_4
-  U == y = ?rhs_5
-  (Pi str icit t u) == y = ?rhs_6
-  (Let str icit t u v) == y = ?rhs_7
+  (Lam n icit t) == (Lam n' icit' t') = icit == icit' && t == t'
+  (App t u) == App t' u' = t == t' && u == u'
+  U == U = True
+  (Pi n icit t u) == (Pi n' icit' t' u') = icit == icit' && t == t' && u == u'
+  (Let n icit t u v) == (Let n' icit' t' u' v') = t == t' && u == u' && v == v'
   _ == _ = False
 
 -- public export
@@ -127,11 +134,47 @@ public export
 Types : Nat -> Type
 Types n = Vect n (Name, Lazy (Val n))
 
--- public export
+
+
+-- REVIEW indices
+public export
+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)
+
+  -- fine for now, consider a map later
+  types : Vect n (String, Val n)
+  pos : SourcePos
+
+
+
+||| add a binding to environment
+extend : Context n n -> String -> Val n -> Context (S n) (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
+    -- ?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)
+
+
+-- weirich has 'hints' to store the claims before the def is seen/checked
+-- saying it is unsafe. afterwards they are mixed into the context.
+-- idris essentially leaves holes, filled in later, for undefined claims
+-- Is it ok to leaving them in there (if they pass checkType) as long as
+-- we don't register the def if it fails checking?
+
+-- shoot, I have another of these in Check.idr
+
+
+-- -- public export
 -- record Ctx (n : Nat) where
 --   constructor MkCtx
 --   env : Env k n     -- for eval
---   types : Types n   -- name lookup, pp
+--   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
@@ -143,6 +186,22 @@ Types n = Vect n (Name, Lazy (Val n))
 -- emptyCtx : Ctx Z
 -- emptyCtx = MkCtx {k=0} [] [] [] 0 (0,0)
 
+-- find out how pi-forall treats binders
+-- Vars are unbound TName 
+
+-- ezoo
+-- Tm has Ix
+-- Val has Lvl
+
+-- by the time we hit ezoo 5/6, there is a Map string -> (Lvl, Type) for name lookup.
+
+-- smalltt
+
+
+-- idris
+
+
+
 -- public export
 -- bindCtx : Name -> Lazy (Val (zz + n))  -> Ctx n -> Ctx (S n)
 -- bindCtx x a (MkCtx env types bds l pos) =
diff --git a/src/Lib/Token.idr b/src/Lib/Token.idr
index 092421b..4687d9c 100644
--- a/src/Lib/Token.idr
+++ b/src/Lib/Token.idr
@@ -11,6 +11,7 @@ data Kind
   | Symbol
   | Space
   | Comment
+  | Pragma
   -- not doing Layout.idr
   | LBrace
   | Semi
@@ -30,7 +31,7 @@ Show Kind where
   show RBrace  = "RBrace"
   show Comment = "Comment"
   show EOI     = "EOI"
-
+  show Pragma  = "Pragma"
 export
 Eq Kind where
   Ident   == Ident = True
diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr
index 6bfd699..f0d97d0 100644
--- a/src/Lib/Tokenizer.idr
+++ b/src/Lib/Tokenizer.idr
@@ -26,6 +26,7 @@ rawTokens : Tokenizer (Token Kind)
 rawTokens
    =  match (alpha <+> many identMore) checkKW
   <|> match (some digit) (Tok Number)
+  <|> match (is '#' <+> many alpha) (Tok Pragma)
   <|> match (lineComment (exact "--")) (Tok Space)
   <|> match (some opChar) (\s => Tok Oper s)
   <|> match symbol (Tok Symbol)