From 6abd97ee85cf9347d33d468ede285912dff6d2a8 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 9 Nov 2024 21:39:45 -0800
Subject: [PATCH] Improvements to grammar

---
 TODO.md                           |  4 +--
 playground/samples/Lists.newt     |  6 ++---
 playground/samples/Tour.newt      |  8 +++---
 playground/samples/Tree.newt      | 17 ++++++-------
 playground/samples/TypeClass.newt | 42 +++++++++++++++----------------
 src/Lib/Parser.idr                | 19 ++++++++------
 src/Main.idr                      |  4 +--
 tests/black/Tree.newt             | 18 ++++++-------
 tests/black/TypeClass.newt        | 42 +++++++++++++++----------------
 9 files changed, 80 insertions(+), 80 deletions(-)

diff --git a/TODO.md b/TODO.md
index 56eb4ef..8d5d4ac 100644
--- a/TODO.md
+++ b/TODO.md
@@ -2,10 +2,10 @@
 ## TODO
 
 - [x] forall / ∀ sugar
-- [ ] Bad module name error has FC 0,0 instead of the module or name
+- [x] Bad module name error has FC 0,0 instead of the module or name
 - [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this.
 - [ ] Remove context lambdas when printing solutions (show names from context)
-  - build list of names and strip λ, then call pprint with names
+  - maybe build list of names and strip λ, then call pprint with names
 - [ ] Check for shadowing when declaring dcon
 - [ ] Require infix decl before declaring names (helps find bugs)
 - [ ] sugar for typeclasses
diff --git a/playground/samples/Lists.newt b/playground/samples/Lists.newt
index ccd1b53..feacf8c 100644
--- a/playground/samples/Lists.newt
+++ b/playground/samples/Lists.newt
@@ -44,7 +44,7 @@ data _≡_ : ∀ A . A -> A -> U where
     Refl : ∀ A . {a : A} -> a ≡ a
 
 -- If a ≡ b then b ≡ a
-sym : {A : U} {a b : A} -> a ≡ b -> b ≡ a
+sym : {A} {a b : A} -> a ≡ b -> b ≡ a
 sym Refl = Refl
 
 -- if a ≡ b and b ≡ c then a ≡ c
@@ -52,11 +52,11 @@ trans : {A : U} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
 trans Refl x = x
 
 -- This lets us replace a with b inside an expression if a ≡ b
-replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace : ∀ A a b. (P : A -> U) -> a ≡ b -> P a -> P b
 replace p Refl x = x
 
 -- if a ≡ b then f a ≡ f b
-cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+cong : ∀ A B a b. (f : A -> B) -> a ≡ b -> f a ≡ f b
 
 -- if concatenate two lists, the length is the sum of the lengths
 -- of the original lists
diff --git a/playground/samples/Tour.newt b/playground/samples/Tour.newt
index d8ea502..67db0ca 100644
--- a/playground/samples/Tour.newt
+++ b/playground/samples/Tour.newt
@@ -20,7 +20,7 @@
 
 -/
 
--- One-line comments begin with two hypens
+-- One-line comments begin with two hyphens
 
 -- every file begins with a `module` declaration
 -- it must match the filename
@@ -150,16 +150,16 @@ data Monad : (U -> U) -> U where
             ({a b : U} -> m a -> (a -> m b) -> m b) ->
             Monad m
 
-pure : ∀ m . {{_ : Monad m}} -> {a : U} -> a -> m a
+pure : ∀ m. {{Monad m}} -> {a : U} -> a -> m a
 pure {{MkMonad p _}} a = p a
 
 -- we can declare multiple infix operators at once
 infixl 1 _>>=_ _>>_
 
-_>>=_ : ∀ m a b. {{_ : Monad m}} -> m a -> (a -> m b) -> m b
+_>>=_ : ∀ m a b. {{Monad m}} -> m a -> (a -> m b) -> m b
 _>>=_ {{MkMonad _ b}} ma amb = b ma amb
 
-_>>_ :  ∀ m a b. {{_ : Monad m}} -> m a -> m b -> m b
+_>>_ :  ∀ m a b. {{Monad m}} -> m a -> m b -> m b
 ma >> mb = ma >>= (λ _ => mb)
 
 -- That's our Monad typeclass, now let's make a List monad
diff --git a/playground/samples/Tree.newt b/playground/samples/Tree.newt
index 7d98c62..4104e22 100644
--- a/playground/samples/Tree.newt
+++ b/playground/samples/Tree.newt
@@ -16,8 +16,8 @@ data Void : U where
 infixl 4 _+_
 
 data _+_ : U -> U -> U where
-  inl : {A B : U} -> A -> A + B
-  inr : {A B : U} -> B -> A + B
+  inl : {A B} -> A -> A + B
+  inr : {A B} -> B -> A + B
 
 infix 4 _<=_
 
@@ -47,14 +47,14 @@ _ <<= Top = Unit
 _ <<= _ = Void
 
 data Intv : Bnd -> Bnd -> U where
-  intv : {l u : Bnd} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
+  intv : {l u} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
 
 data T23 : Bnd -> Bnd -> Nat -> U where
-  leaf : {l u : Bnd} {h : Nat} (lu : l <<= u) -> T23 l u Z
-  node2 : {l u : Bnd} {h : Nat} (x : _)
+  leaf : {l u} (lu : l <<= u) -> T23 l u Z
+  node2 : {l u h} (x : _)
     (tlx : T23 l (N x) h) (txu : T23 (N x) u h) ->
     T23 l u (S h)
-  node3 : {l u : Bnd} {h : Nat} (x y : _)
+  node3 : {l u h} (x y : _)
     (tlx : T23 l (N x) h) (txy : T23 (N x) (N y) h) (tyu : T23 (N y) u h) ->
     T23 l u (S h)
 
@@ -71,9 +71,8 @@ A * B = Sg A (\ _ => B)
 TooBig : Bnd -> Bnd -> Nat -> U
 TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
 
-insert : {h : Nat} {l u : Bnd} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
--- Agda is yellow here, needs h = x on each leaf
-insert (intv x lx xu) (leaf lu) = inl (x , (leaf {_} {_} {x} lx , leaf {_} {_} {x} xu))
+insert : {l u h} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
+insert (intv x lx xu) (leaf lu) = inl (x , (leaf lx , leaf xu))
 insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of
   -- u := N y is not solved at this time
   inl xy => case insert (intv {_} {N y} x lx xy) tly of
diff --git a/playground/samples/TypeClass.newt b/playground/samples/TypeClass.newt
index c3463f1..194fb2e 100644
--- a/playground/samples/TypeClass.newt
+++ b/playground/samples/TypeClass.newt
@@ -3,35 +3,35 @@ module TypeClass
 data Monad : (U -> U) -> U where
   MkMonad : { M : U -> U } ->
             (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
-            (pure : {A : U} -> A -> M A) ->
+            (pure : ∀ A. A -> M A) ->
             Monad M
 
 infixl 1 _>>=_ _>>_
-_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
-_>>=_ {a} {b} {m} {{MkMonad bind' _}}  ma amb = bind' {a} {b} ma amb
+_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
+_>>=_ {{MkMonad bind' _}}  ma amb = bind' ma amb
 
-_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
+_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
 ma >> mb = mb
 
-pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
-pure {_} {_} {{MkMonad _ pure'}} a = pure' a
+pure : ∀ m a. {{Monad m}} -> a -> m a
+pure {{MkMonad _ pure'}} a = pure' a
 
 data Either : U -> U -> U where
-  Left : {A B : U} -> A -> Either A B
-  Right : {A B : U} -> B -> Either A B
+  Left : ∀ A B. A -> Either A B
+  Right : ∀ A B. B -> Either A B
 
-bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C
+bindEither : ∀ A B C. (Either A B) -> (B -> Either A C) -> Either A C
 bindEither (Left a) amb = Left a
 bindEither (Right b) amb = amb b
 
-EitherMonad : {A : U} -> Monad (Either A)
+EitherMonad : ∀ A. Monad (Either A)
 EitherMonad = MkMonad {Either A} bindEither Right
 
 data Maybe : U -> U where
-  Just    : {A : U} -> A -> Maybe A
-  Nothing : {A : U} -> Maybe A
+  Just    : ∀ A. A -> Maybe A
+  Nothing : ∀ A. Maybe A
 
-bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
+bindMaybe : ∀ A B. Maybe A -> (A -> Maybe B) -> Maybe B
 bindMaybe Nothing amb = Nothing
 bindMaybe (Just a) amb = amb a
 
@@ -40,19 +40,19 @@ MaybeMonad = MkMonad bindMaybe Just
 
 infixr 7 _::_
 data List : U -> U where
-  Nil : {A : U} -> List A
-  _::_ : {A : U} -> A -> List A -> List A
+  Nil : ∀ A. List A
+  _::_ : ∀ A. A -> List A -> List A
 
 infixl 7 _++_
-_++_ : {A : U} -> List A -> List A -> List A
+_++_ : ∀ A. List A -> List A -> List A
 Nil ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
-bindList : {A B : U} -> List A -> (A -> List B) -> List B
+bindList : ∀ A B. List A -> (A -> List B) -> List B
 bindList Nil f = Nil
 bindList (x :: xs) f = f x ++ bindList xs f
 
-singleton : {A : U} -> A -> List A
+singleton : ∀ A. A -> List A
 singleton a = a :: Nil
 
 -- TODO need better error when the monad is not defined
@@ -61,7 +61,7 @@ ListMonad = MkMonad bindList singleton
 
 infixr 1 _,_
 data Pair : U -> U -> U where
-  _,_ : {A B : U} -> A -> B -> Pair A B
+  _,_ : ∀ A B. A -> B -> Pair A B
 
 ptype Int
 
@@ -69,7 +69,7 @@ test : Maybe Int
 test = pure 10
 
 foo : Int -> Maybe Int
-foo x = Just 42 >> Just x >>= (\ x => pure {_} {Maybe} 10)
+foo x = Just 42 >> Just x >>= (\ x => pure 10)
 
 bar : Int -> Maybe Int
 bar x = do
@@ -77,7 +77,7 @@ bar x = do
   z <- Just x
   pure z
 
-baz : {A B : U} -> List A -> List B -> List (Pair A B)
+baz : ∀ A B. List A -> List B -> List (Pair A B)
 baz xs ys = do
   x <- xs
   y <- ys
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index a858682..5fd87a6 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -233,20 +233,23 @@ ebind = do
 
 ibind : Parser (List (FC, String, Icit, Raw))
 ibind = do
+  -- I've gone back and forth on this, but I think {m a b} is more useful than {Nat}
   sym "{"
-  -- REVIEW - I have name required and type optional, which I think is the opposite of what I expect
-  names <- try (some (withPos varname) <* sym ":")
-  ty <- typeExpr
+  names <- (some (withPos varname))
+  ty <- optional (sym ":" *> typeExpr)
   sym "}"
-  pure $ map (\(pos,name) => (pos, name, Implicit, ty)) names
+  pure $ map (\(pos,name) => (pos, name, Implicit, fromMaybe (RImplicit pos) ty)) names
 
 abind : Parser (List (FC, String, Icit, Raw))
 abind = do
+  -- for this, however, it would be nice to allow {{Monad A}}
   sym "{{"
-  names <- try (some (withPos varname) <* sym ":")
+  name <- optional $ try (withPos varname <* sym ":")
   ty <- typeExpr
   sym "}}"
-  pure $ map (\(pos,name) => (pos, name, Auto, ty)) names
+  case name of
+    Just (pos,name) => pure [(pos, name, Auto, ty)]
+    Nothing => pure [(getFC ty, "_", Auto, ty)]
 
 arrow : Parser Unit
 arrow = sym "->" <|> sym "→"
@@ -371,8 +374,8 @@ parseDecl = parseMixfix <|> parsePType <|> parsePFunc <|> parseNorm <|> parseDat
 
 
 export
-parseModHeader : Parser String
-parseModHeader = sameLevel (keyword "module") >> uident
+parseModHeader : Parser (FC, String)
+parseModHeader = sameLevel (keyword "module") >> withPos uident
 
 export
 parseImports : Parser (List Import)
diff --git a/src/Main.idr b/src/Main.idr
index 7ad5c7b..1ae8fba 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -63,13 +63,13 @@ processModule base stk name = do
   let Right toks = tokenise src
     | Left err => fail (showError src err)
 
-  let Right (modName, ops, toks) := partialParse parseModHeader top.ops toks
+  let Right ((nameFC, modName), ops, toks) := partialParse parseModHeader top.ops toks
     | Left err => fail (showError src err)
 
 
   putStrLn "module \{modName}"
   let True = name == modName
-    | _ => fail "ERROR at (0, 0): module name \{show modName} doesn't match file name \{show fn}"
+    | _ => fail "ERROR at \{show nameFC}: module name \{show modName} doesn't match file name \{show fn}"
 
   let Right (imports, ops, toks) := partialParse parseImports ops toks
     | Left err => fail (showError src err)
diff --git a/tests/black/Tree.newt b/tests/black/Tree.newt
index 2594a8e..4104e22 100644
--- a/tests/black/Tree.newt
+++ b/tests/black/Tree.newt
@@ -16,8 +16,8 @@ data Void : U where
 infixl 4 _+_
 
 data _+_ : U -> U -> U where
-  inl : {A B : U} -> A -> A + B
-  inr : {A B : U} -> B -> A + B
+  inl : {A B} -> A -> A + B
+  inr : {A B} -> B -> A + B
 
 infix 4 _<=_
 
@@ -47,14 +47,14 @@ _ <<= Top = Unit
 _ <<= _ = Void
 
 data Intv : Bnd -> Bnd -> U where
-  intv : {l u : Bnd} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
+  intv : {l u} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
 
 data T23 : Bnd -> Bnd -> Nat -> U where
-  leaf : {l u : Bnd} {h : Nat} (lu : l <<= u) -> T23 l u Z
-  node2 : {l u : Bnd} {h : Nat} (x : _)
+  leaf : {l u} (lu : l <<= u) -> T23 l u Z
+  node2 : {l u h} (x : _)
     (tlx : T23 l (N x) h) (txu : T23 (N x) u h) ->
     T23 l u (S h)
-  node3 : {l u : Bnd} {h : Nat} (x y : _)
+  node3 : {l u h} (x y : _)
     (tlx : T23 l (N x) h) (txy : T23 (N x) (N y) h) (tyu : T23 (N y) u h) ->
     T23 l u (S h)
 
@@ -71,10 +71,8 @@ A * B = Sg A (\ _ => B)
 TooBig : Bnd -> Bnd -> Nat -> U
 TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
 
-insert : {h : Nat} {l u : Bnd} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
--- Agda is yellow here, needs h = x on each leaf
--- The second arg to the second _,_ is unsolved and pi-typed
-insert (intv x lx xu) (leaf lu) = inl (x , (leaf {_} {_} {x} lx , leaf {_} {_} {x} xu))
+insert : {l u h} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
+insert (intv x lx xu) (leaf lu) = inl (x , (leaf lx , leaf xu))
 insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of
   -- u := N y is not solved at this time
   inl xy => case insert (intv {_} {N y} x lx xy) tly of
diff --git a/tests/black/TypeClass.newt b/tests/black/TypeClass.newt
index c3463f1..194fb2e 100644
--- a/tests/black/TypeClass.newt
+++ b/tests/black/TypeClass.newt
@@ -3,35 +3,35 @@ module TypeClass
 data Monad : (U -> U) -> U where
   MkMonad : { M : U -> U } ->
             (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
-            (pure : {A : U} -> A -> M A) ->
+            (pure : ∀ A. A -> M A) ->
             Monad M
 
 infixl 1 _>>=_ _>>_
-_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
-_>>=_ {a} {b} {m} {{MkMonad bind' _}}  ma amb = bind' {a} {b} ma amb
+_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
+_>>=_ {{MkMonad bind' _}}  ma amb = bind' ma amb
 
-_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
+_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
 ma >> mb = mb
 
-pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
-pure {_} {_} {{MkMonad _ pure'}} a = pure' a
+pure : ∀ m a. {{Monad m}} -> a -> m a
+pure {{MkMonad _ pure'}} a = pure' a
 
 data Either : U -> U -> U where
-  Left : {A B : U} -> A -> Either A B
-  Right : {A B : U} -> B -> Either A B
+  Left : ∀ A B. A -> Either A B
+  Right : ∀ A B. B -> Either A B
 
-bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C
+bindEither : ∀ A B C. (Either A B) -> (B -> Either A C) -> Either A C
 bindEither (Left a) amb = Left a
 bindEither (Right b) amb = amb b
 
-EitherMonad : {A : U} -> Monad (Either A)
+EitherMonad : ∀ A. Monad (Either A)
 EitherMonad = MkMonad {Either A} bindEither Right
 
 data Maybe : U -> U where
-  Just    : {A : U} -> A -> Maybe A
-  Nothing : {A : U} -> Maybe A
+  Just    : ∀ A. A -> Maybe A
+  Nothing : ∀ A. Maybe A
 
-bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
+bindMaybe : ∀ A B. Maybe A -> (A -> Maybe B) -> Maybe B
 bindMaybe Nothing amb = Nothing
 bindMaybe (Just a) amb = amb a
 
@@ -40,19 +40,19 @@ MaybeMonad = MkMonad bindMaybe Just
 
 infixr 7 _::_
 data List : U -> U where
-  Nil : {A : U} -> List A
-  _::_ : {A : U} -> A -> List A -> List A
+  Nil : ∀ A. List A
+  _::_ : ∀ A. A -> List A -> List A
 
 infixl 7 _++_
-_++_ : {A : U} -> List A -> List A -> List A
+_++_ : ∀ A. List A -> List A -> List A
 Nil ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
-bindList : {A B : U} -> List A -> (A -> List B) -> List B
+bindList : ∀ A B. List A -> (A -> List B) -> List B
 bindList Nil f = Nil
 bindList (x :: xs) f = f x ++ bindList xs f
 
-singleton : {A : U} -> A -> List A
+singleton : ∀ A. A -> List A
 singleton a = a :: Nil
 
 -- TODO need better error when the monad is not defined
@@ -61,7 +61,7 @@ ListMonad = MkMonad bindList singleton
 
 infixr 1 _,_
 data Pair : U -> U -> U where
-  _,_ : {A B : U} -> A -> B -> Pair A B
+  _,_ : ∀ A B. A -> B -> Pair A B
 
 ptype Int
 
@@ -69,7 +69,7 @@ test : Maybe Int
 test = pure 10
 
 foo : Int -> Maybe Int
-foo x = Just 42 >> Just x >>= (\ x => pure {_} {Maybe} 10)
+foo x = Just 42 >> Just x >>= (\ x => pure 10)
 
 bar : Int -> Maybe Int
 bar x = do
@@ -77,7 +77,7 @@ bar x = do
   z <- Just x
   pure z
 
-baz : {A B : U} -> List A -> List B -> List (Pair A B)
+baz : ∀ A B. List A -> List B -> List (Pair A B)
 baz xs ys = do
   x <- xs
   y <- ys