From cae4368cd959d2dbffa2fb53b4886871915ba246 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Tue, 22 Apr 2025 20:30:29 -0700
Subject: [PATCH] misc cleanup

---
 newt/Prelude.newt        |  7 +------
 src/Lib/Compile.newt     |  1 -
 src/Lib/CompileExp.newt  | 11 +++--------
 src/Lib/Elab.newt        | 11 -----------
 src/Lib/LiftWhere.newt   |  2 +-
 src/Lib/Parser.newt      |  2 --
 src/Lib/Parser/Impl.newt |  1 -
 src/Lib/Syntax.newt      | 16 +++++++---------
 src/Lib/Types.newt       |  3 ---
 src/Main.newt            | 15 ++++++---------
 tests/Auto.newt          | 24 ------------------------
 tests/Auto2.newt         | 38 --------------------------------------
 tests/RUTest.newt.golden |  2 +-
 tests/TestCase.newt      |  2 --
 14 files changed, 19 insertions(+), 116 deletions(-)
 delete mode 100644 tests/Auto.newt
 delete mode 100644 tests/Auto2.newt

diff --git a/newt/Prelude.newt b/newt/Prelude.newt
index 834123c..4e19a22 100644
--- a/newt/Prelude.newt
+++ b/newt/Prelude.newt
@@ -189,8 +189,6 @@ instance Traversable List where
 traverse_ : ∀ t f a b. {{Traversable t}} {{Applicative f}} → (a → f b) → t a → f Unit
 traverse_ f xs = return (const MkUnit) <*> traverse f xs
 
--- FIXME - there is something subtly wrong in erasure here. t gets applied and there is no warning about it.
--- maybe we don't check the head of an application?
 for : {0 t : U → U} {0 f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {0 a : U} → {0 b : U} → t a → (a → f b) → f (t b)
 for stuff fun = traverse fun stuff
 
@@ -691,10 +689,7 @@ instance Eq Ordering where
   GT == GT = True
   _ == _ = False
 
--- FIXME There is a subtle issue here with shadowing if the file defines a GT in its own namespace
--- We end up chosing that an assigning to GT, which cause a lot of trouble.
--- Prelude.GT is not in scope, because we've depended on the other one.
-pfunc jsCompare uses (LT EQ GT) : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? Prelude_EQ : a < b ? Prelude_LT : Prelude_GT`
+pfunc jsCompare : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? "EQ" : a < b ? "LT" : "GT"`
 
 infixl 6 _<_ _<=_ _>_
 class Ord a where
diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt
index b75c64d..a975b18 100644
--- a/src/Lib/Compile.newt
+++ b/src/Lib/Compile.newt
@@ -51,7 +51,6 @@ data JSStmt : StKind -> U where
   JLet : (nm : String) -> JSStmt (Assign nm) -> JSStmt Plain  -- need somebody to assign
   JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm)
   -- TODO - switch to Int tags
-  -- FIXME add e to JAlt (or just drop it?)
   JCase : ∀ a. JSExp -> List JAlt -> JSStmt a
   -- throw can't be used
   JError : ∀ a. String -> JSStmt a
diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt
index 7f8eba2..764f5e9 100644
--- a/src/Lib/CompileExp.newt
+++ b/src/Lib/CompileExp.newt
@@ -58,8 +58,6 @@ lamArity : Tm -> Nat
 lamArity (Lam _ _ _ _ t) = S (lamArity t)
 lamArity _ = Z
 
-
-
 -- This is how much we want to curry at top level
 -- leading lambda Arity is used for function defs and metas
 -- TODO - figure out how this will work with erasure
@@ -75,16 +73,13 @@ arityForName fc nm = do
     (Just (PrimTCon arity)) => pure $ cast arity
     (Just (PrimFn t arity used)) => pure arity
 
-
 any : ∀ a. (a → Bool) → List a → Bool
 any f Nil = False
 any f (x :: xs) = if f x then True else any f xs
 
--- need to eta out extra args, fill in the rest of the apps
--- NOW - maybe eta here instead of Compile.newt, drop number on CApp
--- The problem would be deBruijn. We have to put the app under CLam
--- which would mess up all of the deBruijn (unless we push it out)
-
+-- apply an expression at an arity to a list of args
+-- CApp will specify any missing args, for eta conversion later
+-- and any extra args get individual CApp.
 apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp
 -- out of args, make one up (fix that last arg)
 apply t Nil acc (S k) =
diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt
index eb4be61..8168937 100644
--- a/src/Lib/Elab.newt
+++ b/src/Lib/Elab.newt
@@ -11,7 +11,6 @@ import Data.SortedMap
 import Lib.Eval
 import Lib.Util
 import Lib.TopContext
--- FIXME Def is shadowing...
 import Lib.Syntax
 import Lib.Types
 
@@ -682,8 +681,6 @@ findSplit (x :: xs) = findSplit xs
 
 -- we could pass into build case and use it for   (x /? y)
 
--- TODO, we may need to filter these against the type to rule out
--- impossible cases
 getConstructors : Context -> FC -> Val -> M (List (QName × Int × Tm))
 getConstructors ctx scfc (VRef fc nm _) = do
   names <- lookupTCon nm
@@ -731,13 +728,6 @@ substVal k v tm = go tm
     go (VMeta fc ix sp) = VMeta fc ix (map go sp)
     go (VRef fc nm sp) = VRef fc nm (map go sp)
     go tm = tm
-    -- FIXME - do I need a Val closure like idris?
-    -- or env in unify...
-    -- or quote back
-    -- go (VLam fc nm sc) = VLam fc nm sc
-    -- go (VCase x sc xs) = ?rhs_2
-    -- go (VU x) = ?rhs_7
-    -- go (VLit x y) = ?rhs_8
 
 -- need to turn k into a ground value
 
@@ -936,7 +926,6 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
         then case y of
           PatVar _ _ s => pure $ Just $ c :: (xs ++ acc)
           PatWild _ _ => pure $ Just $ c :: (xs ++ acc)
-          -- FIXME why don't we hit this (when user puts 'x' for Just 'x')
           PatLit fc lit => error fc "Literal \{show lit} in constructor split"
           PatCon fc icit nm ys as => if nm == dcName
             then case as of
diff --git a/src/Lib/LiftWhere.newt b/src/Lib/LiftWhere.newt
index 1d8aad5..cc160eb 100644
--- a/src/Lib/LiftWhere.newt
+++ b/src/Lib/LiftWhere.newt
@@ -39,7 +39,6 @@ liftWhereTm name env tm@(Case fc t alts) = do
 -- This is where the magic happens
 liftWhereTm name env (LetRec fc nm ty t u) = do
   let l = length env
-  -- FIXME we need a namespace and a name, these collide everywhere.
   qn <- getName name nm
   let env' = (Just (qn, S l) :: env)
   -- environment should subst this function (see next case)
@@ -51,6 +50,7 @@ liftWhereTm name env (LetRec fc nm ty t u) = do
   u' <- liftWhereTm qn env' u
   pure $ LetRec fc nm (Erased fc) (Erased fc) u'
   where
+    -- TODO might be nice if we could nest the names (Foo.go.go) for nested where
     getName : QName → String → M QName
     getName qn@(QN ns nm) ext = do
       let qn' = QN ns (nm ++ "." ++ ext)
diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt
index 3b0453b..b49b78d 100644
--- a/src/Lib/Parser.newt
+++ b/src/Lib/Parser.newt
@@ -1,7 +1,5 @@
 module Lib.Parser
 
--- NOW Still working on this.
-
 import Prelude
 import Lib.Common
 import Data.SortedMap
diff --git a/src/Lib/Parser/Impl.newt b/src/Lib/Parser/Impl.newt
index 42e428b..a775545 100644
--- a/src/Lib/Parser/Impl.newt
+++ b/src/Lib/Parser/Impl.newt
@@ -206,7 +206,6 @@ token' : Kind -> Parser String
 token' k = satisfy (\t => t.val.kind == k) "Expected a \{show k} token"
 
 keyword' : String -> Parser Unit
--- FIXME make this an appropriate whitelist
 keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected \{kw}"
 
 -- expect indented token of given kind
diff --git a/src/Lib/Syntax.newt b/src/Lib/Syntax.newt
index 9cd14ef..bc0a916 100644
--- a/src/Lib/Syntax.newt
+++ b/src/Lib/Syntax.newt
@@ -217,20 +217,18 @@ instance Pretty Literal where
   pretty (LInt i) = text $ show i
   pretty (LChar c) = text $ show c
 
-
-instance Pretty Pattern where
-  -- FIXME - wrap Implicit with {}
-  pretty (PatVar _ icit str) = text str
-  pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args)
-  pretty (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")"
-  pretty (PatWild _ icit) = text "_"
-  pretty (PatLit _ lit) = pretty lit
-
 wrap : Icit -> Doc -> Doc
 wrap Explicit x = text "(" ++ x ++ text ")"
 wrap Implicit x = text "{" ++ x ++ text "}"
 wrap Auto x = text "{{" ++ x ++ text "}}"
 
+instance Pretty Pattern where
+  pretty (PatVar _ Implicit str) = text str
+  pretty (PatVar _ icit str) = wrap icit $ text str
+  pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args)
+  pretty (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")"
+  pretty (PatWild _ icit) = text "_"
+  pretty (PatLit _ lit) = pretty lit
 
 instance Pretty Raw where
   pretty = asDoc 0
diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt
index 5e3844d..7c41260 100644
--- a/src/Lib/Types.newt
+++ b/src/Lib/Types.newt
@@ -188,7 +188,6 @@ pprint' p names (Pi _ "_" Explicit Many t u) =
   parens 0 p $ pprint' 1 names t <+> text "->" <+> pprint' 0 ("_" :: names) u
 pprint' p names (Pi _ nm Explicit rig t u) = parens 0 p $
   text "(" ++  text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t ++ text ")" <+> text "->" <+> pprint' 0 (nm :: names) u
--- FIXME - probably way wrong on the names here.  There is implicit binding going on
 pprint' p names (Case _ sc alts) = parens 0 p $ text "case" <+> pprint' 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (pprintAlt 0 names) alts)))
 pprint' p names (Lit _ lit) = text (show lit)
 pprint' p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> text ":=" <+> pprint' 0 names t <+> text "in" </> (nest 2 $ pprint' 0 (nm :: names) u)
@@ -355,8 +354,6 @@ record TopEntry where
   def : Def
   eflags : List EFlag
 
--- FIXME snoc
-
 instance Show TopEntry where
   show (MkEntry fc name type def flags) = "\{show name} : \{show type} := \{show def} \{show flags}"
 
diff --git a/src/Main.newt b/src/Main.newt
index 0d350b8..59c6d3b 100644
--- a/src/Main.newt
+++ b/src/Main.newt
@@ -179,8 +179,7 @@ processModule importFC base stk qn@(QN ns nm) = do
 
   (Nil) <- liftIO {M} $ readIORef top.errors
     | errors => do
-        for_ errors $ \err =>
-          putStrLn (showError src err)
+        traverse (putStrLn ∘ showError src) errors
         exitFailure "Compile failed"
   logMetas $ reverse $ listValues mc.metas
   pure src
@@ -190,7 +189,7 @@ processModule importFC base stk qn@(QN ns nm) = do
       (Left err) <- tryError $ processDecl ns decl | _ => pure MkUnit
       addError err
 
-
+-- unwind the module part of the path name
 baseDir : SnocList String -> SnocList String -> Either String String
 baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil)
 baseDir (dirs :< d) (ns :< n) = if d == n
@@ -201,17 +200,15 @@ baseDir Lin _ = Left "module path doesn't match directory"
 showErrors : String -> String -> M Unit
 showErrors fn src = do
   top <- getTop
+  -- TODO {M} needed to sort out scrutinee
   (Nil) <- liftIO {M} $ readIORef top.errors
     | errors => do
-        for_ errors $ \err =>
-          putStrLn (showError src err)
-        -- if err.file == fn
-        -- then putStrLn (showError src err)
-        -- else putStrLn (showError "" err)
+        traverse (putStrLn ∘ showError src) errors
         exitFailure "Compile failed"
   pure MkUnit
 
-
+-- processFile called on the top level file
+-- it sets up everything and then recurses into processModule
 processFile : String -> M Unit
 processFile fn = do
   putStrLn "*** Process \{fn}"
diff --git a/tests/Auto.newt b/tests/Auto.newt
deleted file mode 100644
index 0dc13f1..0000000
--- a/tests/Auto.newt
+++ /dev/null
@@ -1,24 +0,0 @@
-module Auto
-
-pfunc i2s : Int -> String := `(i) => ''+i`
-pfunc _++_ : String -> String -> String := `(a,b) => a + b`
-
-infixl 4 _++_
-
--- We need sugar and marking as class/instance on all of this
-
-data Show : U -> U where
-  MkShow : { A : U } -> ((show : A) -> String) -> Show A
-
--- FIXME - we'd like to inline this, so `show _ {{showInt}} a` ends up as `i2s a`
-show : {A : U} {{myshow : Show A}} -> A -> String
-show {_} {{MkShow foo}} a = foo a
-
-showInt : Show Int
-showInt = MkShow i2s
-
-ptype World
-pfunc log : {A : U} -> A -> World := `(_, a) => console.log(a)`
-
-main : Int -> World
-main _ = log ("answer: " ++ show 42)
diff --git a/tests/Auto2.newt b/tests/Auto2.newt
deleted file mode 100644
index 33b7392..0000000
--- a/tests/Auto2.newt
+++ /dev/null
@@ -1,38 +0,0 @@
-module Auto2
-
-ptype World
-pfunc log : {A : U} -> A -> World := `(_, a) => console.log(a)`
-
-
-pfunc i_plus : Int -> Int -> Int := `(x,y) => x + y`
-
-data Nat : U where
-  Z : Nat
-  S : Nat -> Nat
-
-plus : Nat -> Nat -> Nat
-plus Z x = x
-plus (S k) x = S (plus k x)
-
--- a type class
-data Add : U -> U where
-  MkAdd : {A : U} -> (A -> A -> A) -> Add A
-
-infixl 8 _+_
-_+_ : {A : U} -> {{myadd : Add A}} -> A -> A -> A
-_+_ {_} {{MkAdd adder}} x y = adder x y
-
--- Two instances
-addInt : Add Int
-addInt = MkAdd i_plus
-
-addNat : Add Nat
-addNat = MkAdd plus
-
--- sequencing hack
-infixl 2 _>>_
-_>>_ :  {a b : U} ->  a -> b -> b
-a >> b = b
-
-main : World -> World
-main _ = log (40 + 2) >> log (Z + Z)
diff --git a/tests/RUTest.newt.golden b/tests/RUTest.newt.golden
index 12decc1..aa47d0d 100644
--- a/tests/RUTest.newt.golden
+++ b/tests/RUTest.newt.golden
@@ -1,2 +1,2 @@
 0
-3
+0
diff --git a/tests/TestCase.newt b/tests/TestCase.newt
index 0506799..58f478d 100644
--- a/tests/TestCase.newt
+++ b/tests/TestCase.newt
@@ -60,8 +60,6 @@ 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