From a9c72d5a6d4bf2b91913b46248163b3360668a61 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 11 Apr 2024 19:57:02 -0700
Subject: [PATCH] drop HOAS, add Monad stack.

HOAS was dropped while fixing unrelated bug, but I think I'll keep it
out.
---
 Makefile                |  9 +++++++++
 eg/ex.newt              |  6 +++++-
 src/Lib/Check.idr       |  4 ++--
 src/Lib/Parser/Impl.idr |  4 ++--
 src/Lib/TT.idr          | 44 +++++++++++++++++++++--------------------
 src/Main.idr            | 28 +++++++++++++++-----------
 6 files changed, 58 insertions(+), 37 deletions(-)
 create mode 100644 Makefile

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..55ffbe5
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,9 @@
+SRCS=$(shell find src -name "*.idr")
+
+all: build/exec/newt
+
+build/exec/newt: ${SRCS}
+	idris2 --build newt.ipkg
+
+test: build/exec/newt
+	build/exec/newt
diff --git a/eg/ex.newt b/eg/ex.newt
index 22e3b93..de13ec0 100644
--- a/eg/ex.newt
+++ b/eg/ex.newt
@@ -3,5 +3,9 @@ module Foo
 
 id : (a : U) -> a -> a
 id = \ a => \ x => x
--- if I put foo here, it fails with 'extra toks'
+
+-- if I put foo here, it fails with 'extra toks' at "module"
 -- errors aren't cutting to the top
+-- I think we need the errors to be fatal if anything is consumed (since the nearest alt)
+
+foo
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 2c1dfef..24c7e78 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -21,7 +21,7 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m}
                       -- TODO icit
                       let var = VVar (length ctx.env)
                       let ctx' = extend ctx nm a
-                      tm' <- check ctx' tm (b var)
+                      tm' <- check ctx' tm (b $$ var)
                       pure $ Lam nm icit tm'
                       
                     other => throwError "Expected pi type \{show $ quote 0 ty}"
@@ -44,7 +44,7 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m}
     case tty of
       (VPi str icit' a b) => do
         u <- check ctx u a
-        pure (App t u, b (eval ctx.env t))
+        pure (App t u, b $$ eval ctx.env t)
       _ => throwError "Expected Pi type"    
   infer ctx RU = pure (U, VU) -- YOLO
   infer ctx (RPi nm icit ty ty2) = do
diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr
index 346fa39..d9968ab 100644
--- a/src/Lib/Parser/Impl.idr
+++ b/src/Lib/Parser/Impl.idr
@@ -31,7 +31,7 @@ showError src (E (line, col) msg) = "Err at \{show (line,col)} \{msg}\n" ++ go 0
       if l == line then
         "\{x}\n\{replicate (cast col) ' '}^\n"
       else if line - 3 < l then x ++ "\n" ++ go (l + 1) xs 
-      else ""
+      else go (l + 1) xs
 
 -- Result of a parse
 public export
@@ -68,7 +68,7 @@ parse : Parser a -> TokenList -> Either Error a
 parse pa toks = case runP pa toks False emptyPos of
   Fail fatal err toks com => Left err
   OK a [] _ => Right a
-  OK a ts _ => Left (error toks "Extra toks")
+  OK a ts _ => Left (error ts "Extra toks")
 
 -- I think I want to drop the typeclasses for v1
 
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index 99e9ace..f93f4a8 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -82,8 +82,7 @@ data Val : Type
 
 
 public export
-0 Closure : Type
-Closure = Val -> Val
+data Closure : Type
 
 public export
 data Val : Type where
@@ -102,44 +101,46 @@ Env = List Val
 export
 eval : Env -> Tm -> Val
 
+data Closure = MkClosure Env Tm
+
+public export
+($$) : Closure -> Val -> Val
+($$) (MkClosure env tm) u = eval (u :: env) tm
+
+infixl 8 $$ 
+
 export
 vapp : Val -> Val -> Val
-vapp (VLam _ icit t) u = t u
+vapp (VLam _ icit t) u = t $$ u
 vapp t u = VApp t u
 
 bind : Val -> Env -> Env
 bind v env = v :: env
 
--- so here we have LocalEnv free vars in Yaffle
-
 eval env (Ref x) = VRef x
 eval env (App t u) = vapp (eval env t) (eval env u)
 eval env U = VU
--- yaffle breaks out binder
-eval env (Lam x icit t) = VLam x icit (\u => eval (u :: env) t)
-eval env (Pi x icit a b) = VPi x icit (eval env a) (\u => eval (u :: env) b)
--- This one we need to make 
+eval env (Lam x icit t) = VLam x icit (MkClosure env t)
+eval env (Pi x icit a b) = VPi x icit (eval env a) (MkClosure env b)
 eval env (Let x icit ty t u) = eval (eval env t :: env) u
 eval env (Bnd i) = let Just rval = getAt i env | _ => ?out_of_index
                    in rval
 
-vfresh : Nat -> Val
-vfresh l = VVar l
-
 export
-quote : (k : Nat) -> Val -> Tm
-quote l (VVar k) = Bnd (S l `minus` k) -- level to index
+quote : (lvl : Nat) -> Val -> Tm
+quote l (VVar k) = Bnd ((l `minus` k) `minus` 1) -- 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 (vfresh l))) -- that one is too big
-quote l (VPi x icit a b) = Pi x icit (quote l a) (quote (S l) (b $ vfresh l))
+quote l (VLam x icit t) = Lam x icit (quote (S l) (t $$ VVar l)) -- that one is too big
+quote l (VPi x icit a b) = Pi x icit (quote l a) (quote (S l) (b $$ VVar l))
 quote l VU = U
 quote _ (VRef n) = Ref n
 
--- vars -> vars -> vars in yaffle
+-- how are we using this?  Can we assume completely closed?
+-- ezoo only seems to use it at [], but essentially does this:
 export
-nf : {n : Nat} -> Env -> Tm -> Tm
-nf env t = quote n (eval env t)
+nf : Env -> Tm -> Tm
+nf env t = quote (length env) (eval env t)
 
 public export
 conv : (lvl : Nat) -> Val -> Val -> Bool
@@ -160,8 +161,6 @@ record Context where
   -- lvl = length types
   pos : SourcePos            -- the last SourcePos that we saw
 
-
-
 export
 empty : Context
 empty = MkCtx [] [] (0,0)
@@ -178,6 +177,9 @@ extend : Context -> String -> Val -> Context
 extend (MkCtx env types pos) name ty =
     MkCtx (VVar (length env) :: env) ((name, ty) :: types) pos
 
+update : Context -> String -> Tm -> Context
+-- oof
+
 lookup : {0 m : Type -> Type} -> {auto _ : MonadError String m} ->
       Context -> String -> m Val
 lookup ctx nm = go ctx.types
diff --git a/src/Main.idr b/src/Main.idr
index acb059c..8c0e5cc 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -29,25 +29,31 @@ Main2.idr has an older App attempt without the code below. Retrofit.
 M : Type -> Type
 M = (StateT Context (EitherT String IO))
 
-processDecl : Context -> Decl -> M Context
-processDecl ctx (TypeSig nm tm)= do
+processDecl : Decl -> M ()
+processDecl (TypeSig nm tm) = do
+  ctx <- get
   putStrLn "TypeSig \{nm} \{show tm}"
   ty <- check ctx tm VU
   putStrLn "got \{show ty}"
   let vty = eval ctx.env ty
-  putStrLn "-- \{show $ quote 0 vty}   XXXXXXXXXX"
-  pure $ extend ctx nm vty
+  putStrLn "--- \{show $ quote 0 vty}" 
+  put $ extend ctx nm vty
 
-processDecl ctx (Def nm raw) = do
+processDecl (Def nm raw) = do
   putStrLn "def \{show nm}"
+  ctx <- get
   let Just ty = lookup nm ctx.types
-    | Nothing => printLn "skip def \{nm} without Decl" >> pure ctx
+    | Nothing => printLn "skip def \{nm} without Decl"
   putStrLn "check \{nm} = \{show raw} at \{show $ quote 0 ty}"
   Right tm <- pure $ the (Either String Tm) (check ctx raw ty)
-    | Left err => printLn err >> pure ctx
+    | Left err => printLn err
   putStrLn "got \{show tm}"
-  pure ctx
-processDecl ctx decl = putStrLn "skip \{show decl}" >> pure ctx
+  -- XXXXX here I need to update the environment
+  -- I may want to rework things to have a top environment with names,
+  -- then levels / indices for local stuff.
+  
+  
+processDecl decl = putStrLn "skip \{show decl}"
 
 processFile : String -> M ()
 processFile fn = do
@@ -59,8 +65,8 @@ processFile fn = do
     | Left y => putStrLn (showError src y)
   putStrLn $ pretty 80 $ pretty res
   printLn "process Decls"
-  ctx <- foldlM processDecl empty res.decls
-  putStrLn "done \{show ctx}"
+  traverse_ processDecl res.decls
+  putStrLn "done \{show !get}"
 
 main' : M ()
 main' = do