fresh names, move case stuff along a little

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"

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

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)

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)
+