cleanup

src/Lib/Compile.newt

@@ -444,8 +444,6 @@ process name = do
   -- Maybe move this dance into liftWhere
   ref <- newIORef entries
   let foo = MkRef ref -- for the autos below
-  -- TODO, erasure needs to happen on Tm, but can be part of Tm -> CExp
-  -- if we move the liftWhere down.
   eraseEntries
   liftWhere
   entries <- readIORef ref

src/Lib/LiftWhere.newt

@@ -58,11 +58,6 @@ liftWhereTm name env (LetRec fc nm ty t u) = do
       let (Just _) = lookupMap qn' top | _ => pure qn'
       getName qn (ext ++ "'")
 
-    -- Hacky - CompileExp expects a pi type that matches arity
-    wrapPi : Nat → Tm → Tm
-    wrapPi Z tm = tm
-    wrapPi (S k) tm = Pi fc "_" Explicit Many (Erased fc) $ wrapPi k tm
-
     wrapLam : Nat → Tm → Tm
     wrapLam Z tm = tm
     -- REVIEW We've already erased, hopefully we don't need quantity

src/Lib/TCO.newt

@@ -32,8 +32,6 @@ tailNames (CConstr _ _ args) = Nil
 tailNames (CBnd _) = Nil
 tailNames (CFun _ tm) = tailNames tm
 tailNames (CLam _ _) = Nil
--- should not happen, FIXME
-tailNames (CAppRef t args n) = Nil
 tailNames (CApp t u) = Nil
 tailNames (CRef _) = Nil
 tailNames CErased = Nil

src/Prelude.newt

@@ -523,8 +523,11 @@ enumerate {a} xs = go Z xs
     go k (x :: xs) = (k,x) :: go (S k) xs
 
 filter : ∀ a. (a → Bool) → List a → List a
-filter pred Nil = Nil
-filter pred (x :: xs) = if pred x then x :: filter pred xs else filter pred xs
+filter {a} pred xs = go xs Lin
+  where
+    go : List a → SnocList a → List a
+    go Nil acc = acc <>> Nil
+    go (x :: xs) acc = if pred x then go xs (acc :< x) else go xs acc
 
 drop : ∀ a. Nat → List a → List a
 drop _ Nil = Nil