From 1fef9dcfc61b4fef04f2256280324cf066f164f9 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Tue, 13 Aug 2024 07:42:01 -0700
Subject: [PATCH] fresh names, move case stuff along a little

---
 README.md               | 17 ++++++++++-------
 newt/testcase.newt      | 15 +++++++++++++++
 src/Lib/Check.idr       |  7 ++++++-
 src/Lib/Compile.idr     | 30 ++++++++++++++++++++++++------
 src/Lib/ProcessDecl.idr |  4 ++++
 src/Lib/TT.idr          |  9 ++++++++-
 6 files changed, 67 insertions(+), 15 deletions(-)

diff --git a/README.md b/README.md
index 7e1ff5a..b217d95 100644
--- a/README.md
+++ b/README.md
@@ -7,25 +7,27 @@ Compiling to js including data.
 
 v1 of cases requires a constructor and vars, var, or default.
 
-
 ### Main
 
-- [ ] flag for debug?
+- [x] flag for debug?
 
 ### Data
 
 - [x] typecheck `plus`
-- [ ] don't leave extra "Axiom" entries for incomplete `data` (switch to a map or drop the order)
+- [x] don't leave extra "Axiom" entries for incomplete `data` (switch to a map or drop the order)
 - [ ] Check types when declaring data (collect telescope and check final type against type constructor)
 - [ ] Learn stuff like `n = S k` in case trees.
-  - Need test case
-  - If this is all var = tm, I could mutate the local env (Would it need to be `let` to be used in unification?)
+  - Need test case, but existing plus case fails unification if we try.
+  - I guess I need to let these pattern vars unify/match and learn equalities
+  - If this is all var = tm, I could mutate the local env, so var is now a let. (Would it need to be `let` to be used in unification?)
   - I could subst into something (environment / goal?)
   - I could carry around extra stuff for unification
   - With names, I could dump a `let` into the env
 - [ ] Handle default cases (non-constructor)
 - [ ] When we do impossible, take agda approach
 - [ ] test cases. Maybe from pi-forall
+- [ ] coverage checking
+- [ ] case tree builder
 
 ### Primitives
 
@@ -49,13 +51,13 @@ We need some erasure for runtime. The pi-forall notation isn't compatible with i
 
 Code generation is partially done.
 
-- [ ] Handle meta in compile
+- [ ] Handle meta in compile (inline solved metas?)
 - [ ] Default case (need to process list to cases and maybe default)
 - [ ] Arity for top level functions (and lambda for partial application)
      - I can do this here, but I'll have to wire in M, otherwise maybe a transform
        before this (we could pull out default case too)
 - [ ] Javascript operators / primitives
-- [ ] Don't do assign var to fresh var
+- [x] Don't do assign var to fresh var
 
 ### Parsing / Language
 
@@ -76,6 +78,7 @@ Code generation is partially done.
   - Look at smallTT rules
   - Can we not expand top level - expand in unification and matching pi types?
 - [ ] look into Lennart.newt issues
+- [ ] figure out how to add laziness (might have to be via the monad)
 
 So smalltt has TopVar with a Level. typechecking binders end up as top too.
 
diff --git a/newt/testcase.newt b/newt/testcase.newt
index 7a9eb89..a8f4362 100644
--- a/newt/testcase.newt
+++ b/newt/testcase.newt
@@ -52,6 +52,21 @@ not2 = \ v => case v of
   True => False
   x => True
 
+and : Bool -> Bool -> Bool
+and = \ x y => case x of
+  True => y
+  False => False
+
+-- FIXME - a case is evaluated here, and I don't know why.
+
+nand : Bool -> Bool -> Bool
+nand = \ x y => not (case x of
+    True => y
+    False => False)
+
+-- -- this should be an error.
+-- foo : Bool -> Bool
 
 data Void : U where
 
+
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 2cd5424..9acfb6f 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -238,8 +238,13 @@ checkAlt scty ctx ty (MkAlt ptm body) = do
     -- nameless variable
     go ctype [] ctx = do
       debug "*** end \{show ctype}"
+      -- FIXME FIXME - I think I should be unifying ctype against scty and learning stuff from it
+      -- like n = S k.
+      -- debug "Unifying constructor"
+      -- unifyCatch emptyFC ctx ctype scty
+      -- my first example has issues with Vect Z 0 =?=
+
       check ctx body ty
-      -- pure ctx -- this should be our constructor.
     -- This happens if we run out of runway (more args and no pi)
     -- go ctype tm ctx = error (getF "unhandled in checkAlt.go type: \{show ctype} term: \{show tm}"
     go ctype args ctx = error (argsFC args) "Extra args"
diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr
index 2ce929a..739049c 100644
--- a/src/Lib/Compile.idr
+++ b/src/Lib/Compile.idr
@@ -1,5 +1,6 @@
--- TODO fresh names
-
+-- TODO I think I'm missing the bit where a case might need to be assigned to a variable.
+-- TODO And then get primitives and a way to declare extern functions.  That may get us
+-- to utility
 module Lib.Compile
 
 import Lib.Types
@@ -41,7 +42,9 @@ data JSStmt : Kind -> Type where
 
 Cont e = JSExp -> JSStmt e
 
--- FIXME - add names to env so we can guarantee fresh names in the generated javascript.
+||| JSEnv contains `Var` for binders or `Dot` for destructured data. It
+||| used to translate binders
+JSEnv : Type
 JSEnv = List JSExp
 
 -- Stuff nm.h1, nm.h2, ... into environment
@@ -49,6 +52,21 @@ mkEnv : String -> Nat -> List JSExp -> List String -> List JSExp
 mkEnv nm k env [] = env
 mkEnv nm k env (x :: xs) = mkEnv nm (S k) (Dot (Var nm) "h\{show k}" :: env) xs
 
+envNames : Env -> List String
+
+-- If I was golfing, I'd be tempted to stick with deBruijn
+
+||| given a name, find a similar one that doesn't shadow in Env
+fresh : String -> JSEnv -> String
+fresh nm env = if free env nm then nm else go nm 1
+  where
+    free : JSEnv -> String -> Bool
+    free [] nm = True
+    free (Var n :: xs) nm = if n == nm then False else free xs nm
+    free (_ :: xs) nm = free xs nm
+
+    go : String -> Nat -> String
+    go nm k = let nm' = "\{nm}\{show k}" in if free env nm' then nm' else go nm (S k)
 
 -- This is inspired by A-normalization, look into the continuation monad
 -- There is an index on JSStmt, adopted from Stefan Hoeck's code.
@@ -61,11 +79,11 @@ termToJS env (CBnd k) f = case getAt k env of
   (Just e) => f e
   Nothing => ?bad_bounds
 termToJS env (CLam nm t) f =
-  let nm' = "\{nm}$\{show $ length env}"
+  let nm' = fresh nm env -- "\{nm}$\{show $ length env}"
       env' = (Var nm' :: env)
   in f $ JLam [nm'] (termToJS env' t JReturn)
 termToJS env (CFun nms t) f =
-  let nms' = map (\nm => "\{nm}$\{show $ length env}") nms
+  let nms' = map (\nm => fresh nm env) nms
       env' = foldl (\ e, nm => Var nm :: e) env nms'
   in f $ JLam nms' (termToJS env' t JReturn)
 termToJS env (CRef nm) f = f $ Var nm
@@ -85,7 +103,7 @@ termToJS env (CCase t alts) f =
   termToJS env t $ \case
     (Var nm) => (JCase (Dot (Var nm) "tag") (map (termToJSAlt nm) alts))
     t' =>
-      let nm = "sc$\{show $ length env}" in
+      let nm = fresh "sc" env in
         JSnoc (JConst nm t')
           (JCase (Dot (Var nm) "tag") (map (termToJSAlt nm) alts))
   where
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index f54cddb..4954a05 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -15,10 +15,14 @@ getArity (Pi x str icit t u) = S (getArity u)
 getArity _ = Z
 
 
+-- Can metas live in context for now?
+
 export
 processDecl : Decl -> M ()
 processDecl (TypeSig fc nm tm) = do
   top <- get
+  let Nothing := lookup nm top
+    | _ => error fc "\{show nm} is already defined"
   putStrLn "-----"
   putStrLn "TypeSig \{nm} \{show tm}"
   ty <- check (mkCtx top.metas) tm (VU fc)
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index 868bf9c..9d93ca3 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -106,6 +106,10 @@ lookup ctx nm = go ctx.types
 export
 eval : Env -> Mode -> Tm -> M Val
 
+-- REVIEW everything is evalutated whether it's needed or not
+-- It would be nice if the environment were lazy.
+-- e.g. case is getting evaluated when passed to a function because
+-- of dependencies in pi-types, even if the dependency isn't used
 public export
 ($$) : {auto mode : Mode} -> Closure -> Val -> M Val
 ($$) {mode} (MkClosure env tm) u = eval (u :: env) mode tm
@@ -153,7 +157,9 @@ eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkCl
 eval env mode (Bnd fc i) = case getAt i env of
   Just rval => pure rval
   Nothing => error' "Bad deBruin index \{show i}"
-eval env mode (Case{}) = ?todo
+
+-- We need a neutral and some code to run the case tree
+eval env mode tm@(Case{}) = ?todo_eval_case
 
 export
 quote : (lvl : Nat) -> Val -> M Tm
@@ -206,3 +212,4 @@ solveMeta ctx ix tm = do
     go (meta@(Solved k _) :: xs) lhs = if k == ix
       then error' "Meta \{show ix} already solved!"
       else go xs (lhs :< meta)
+