sugar for data and other improvements

- parse types in let (everything but parser was there)
- add sugar for `data`
- move `joinBy` to prelude
- fix highlighting for char in vscode
- better errors for missing imports

TODO.md

@@ -3,6 +3,10 @@
 
 More comments in code! This is getting big enough that I need to re-find my bearings when fixing stuff.
 
+- [ ] tokenizer
+- [ ] string interpolation
+- [ ] pattern matching lambda
+  - I kept wanting this in AoC and use it a lot in the newt code
 - [ ] editor - indent newline on let with no in
   - I've seen this done in vi for Idris, but it seems non-trivial in vscode.
 - [x] Move on to next decl in case of error
@@ -47,8 +51,9 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [ ] **Translate newt to newt**
   - [x] Support @ on the LHS
   - [x] if / then / else sugar
-  - [ ] `data Foo = A | B` sugar
+  - [x] `data Foo = A | B` sugar
   - [x] records
+  - [ ] record sugar? (detailed above)
   - [x] where
   - [ ] add namespaces
   - [ ] magic nat?
@@ -58,7 +63,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [x] Strategy to avoid three copies of `Prelude.newt` in this source tree
 - [ ] `mapM` needs inference help when scrutinee (see Day2.newt)
   - Meta hasn't been solved yet. It's Normal, but maybe our delayed solving of Auto plays into it. Idris will peek at LHS of CaseAlts to guess the type if it doesn't have one.
-- [ ] Can't skip an auto. We need `{{_}}` to be auto or `%search` syntax.
+- [ ] Can't skip an auto. We need `{{_}}` to be auto or have a `%search` syntax.
 - [x] add filenames to FC
 - [ ] Add full ranges to FC
 - [x] maybe use backtick for javascript so we don't highlight strings as JS
@@ -74,9 +79,6 @@ More comments in code! This is getting big enough that I need to re-find my bear
   - maybe a file listing jobs, whether they are known broken, optional expected output, optional expected JS execution output.
 - [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine)
 - [x] Bad module name error has FC 0,0 instead of the module or name
-- [ ] ~~Remove context lambdas when printing solutions (show names from context)~~
-  - maybe build list of names and strip λ, then call pprint with names
-  - I've removed solution printing, so this is moot
 - [ ] Revisit substitution in case building
 - [x] Check for shadowing when declaring dcon
   - Handles the forward decl in `Zoo1.newt`, but we'll need different syntax if
@@ -131,7 +133,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [x] implicit patterns
 - [x] operators
 - [x] pair syntax (via comma operator)
-- [ ] `data` sugar: `data Maybe a = Nothing | Just a`
+- [x] `data` sugar: `data Maybe a = Nothing | Just a`
 - [x] matching on operators
   - [x] top level
   - [x] case statements

aoc2024/Day23.newt

@@ -65,11 +65,6 @@ bronKerbosch g rs (p :: ps) xs =
     best a Nothing = a
     best (Just a) (Just b) = if length a < length b then Just b else Just a
 
-joinBy : String → List String → String
-joinBy _ Nil = ""
-joinBy _ (x :: Nil) = x
-joinBy s (x :: y :: xs) = joinBy s ((x ++ s ++ y) :: xs)
-
 run : String -> IO Unit
 run fn = do
   putStrLn fn

aoc2024/Day24.newt

@@ -126,7 +126,6 @@ check : List Gate → List Int → String → Either (String × String) Unit
 check gates Nil carry = Right MkUnit
 check gates (bit :: bits) carry = do
   let xl = label 'x' bit
-  let yl = label 'x' bit
   let (Just a1) = matchIn xl And | _ => fail $ "no a1 " ++ show bit
   let (Just x1) = matchIn xl Xor | _ => fail $ "no x1 " ++ show bit
   -- just peel of the carry for bit0
@@ -174,11 +173,6 @@ trampoline gates acc = do
       putStrLn $ "SWAP " ++ a ++ " and " ++ b
       trampoline (map (swapPins a b) gates) (a :: b :: acc)
 
-joinBy : String → List String → String
-joinBy _ Nil = ""
-joinBy _ (x :: Nil) = x
-joinBy s (x :: y :: xs) = joinBy s ((x ++ s ++ y) :: xs)
-
 run : String -> IO Unit
 run fn = do
   putStrLn fn

newt-vscode/syntaxes/newt.tmLanguage.json

@@ -26,11 +26,14 @@
         { "include": "source.js" }
       ]
     },
+    {
+      "name": "string.newt",
+      "match": "'(.|\\\\.)'"
+    },
     {
       "name": "string.newt",
       "begin": "\"",
       "end": "\""
     }
-
   ]
 }

newt/Prelude.newt

@@ -6,8 +6,7 @@ id x = x
 the : (a : U) → a → a
 the _ a = a
 
-data Bool : U where
-  True False : Bool
+data Bool = True | False
 
 not : Bool → Bool
 not True = False
@@ -33,9 +32,7 @@ infixl 6 _/=_
 _/=_ : ∀ a. {{Eq a}} → a → a → Bool
 a /= b = not (a == b)
 
-data Nat : U where
-  Z : Nat
-  S : Nat -> Nat
+data Nat = Z | S Nat
 
 pred : Nat → Nat
 pred Z = Z
@@ -46,32 +43,25 @@ instance Eq Nat where
   S n == S m = n == m
   x == y = False
 
-data Maybe : U -> U where
-  Just : ∀ a. a -> Maybe a
-  Nothing : ∀ a. Maybe a
+
+data Maybe a = Just a | Nothing
 
 fromMaybe : ∀ a. a → Maybe a → a
 fromMaybe a Nothing = a
 fromMaybe _ (Just a) = a
 
-data Either : U -> U -> U where
-  Left : {0 a b : U} -> a -> Either a b
-  Right : {0 a b : U} -> b -> Either a b
+data Either a b = Left a | Right b
 
 infixr 7 _::_
-data List : U -> U where
-  Nil : ∀ A. List A
-  _::_ : ∀ A. A → List A → List A
+data List a = Nil | a :: List a
 
 length : ∀ a. List a → Nat
 length Nil = Z
 length (x :: xs) = S (length xs)
 
 
 infixl 7 _:<_
-data SnocList : U → U where
-  Lin : ∀ A. SnocList A
-  _:<_ : ∀ A. SnocList A → A → SnocList A
+data SnocList a = Lin | SnocList a :< a
 
 -- 'chips'
 infixr 6 _<>>_ _<><_
@@ -90,8 +80,7 @@ xs <>< (y :: ys) = (xs :< y) <>< ys
 
 infixr 8 _×_
 infixr 2 _,_
-data _×_ : U → U → U where
-  _,_ : ∀ A B. A → B → A × B
+data a × b = (a,b)
 
 fst : ∀ a b. a × b → a
 fst (a,b) = a
@@ -222,6 +211,8 @@ instance Mul Nat where
   Z * _ = Z
   S n * m = m + n * m
 
+pfunc mod : Int → Int → Int := `(a,b) => a % b`
+
 infixl 7 _-_
 class Sub a where
   _-_ : a → a → a
@@ -252,9 +243,7 @@ instance Eq String where
 instance Eq Char where
   a == b = jsEq a b
 
-
-data Unit : U where
-  MkUnit : Unit
+data Unit = MkUnit
 
 ptype Array : U → U
 pfunc listToArray : {a : U} -> List a -> Array a := `
@@ -324,8 +313,7 @@ pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))`
 -- I don't want to use an empty type because it would be a proof of void
 ptype World
 
-data IORes : U -> U where
-  MkIORes : ∀ a. a -> World -> IORes a
+data IORes a = MkIORes a World
 
 IO : U -> U
 IO a = World -> IORes a
@@ -761,3 +749,16 @@ instance ∀ a. {{Eq a}} → Eq (List a) where
 find : ∀ a. (a → Bool) → List a → Maybe a
 find f Nil = Nothing
 find f (x :: xs) = if f x then Just x else find f xs
+
+-- TODO this would be faster, but less pure as as primitive and
+-- fastConcat might be a good compromise
+joinBy : String → List String → String
+joinBy _ Nil = ""
+joinBy _ (x :: Nil) = x
+joinBy s (x :: y :: xs) = joinBy s ((x ++ s ++ y) :: xs)
+
+snoc : ∀ a. List a → a → List a
+snoc xs x = xs ++ (x :: Nil)
+
+instance ∀ a b. {{Show a}} {{Show b}} → Show (a × b) where
+  show (a,b) = "(" ++ show a ++ "," ++ show b ++ ")"

playground/src/monarch.ts

@@ -110,7 +110,8 @@ export let newtTokens: monaco.languages.IMonarchLanguage = {
           },
         },
       ],
-
+      // char literal, but I don't think there is a class for that.
+      [/'\\?.'/, "string"],
       [/\d+/, "number"],
 
       // strings
@@ -125,7 +126,7 @@ export let newtTokens: monaco.languages.IMonarchLanguage = {
     string: [
       [/[^\\"]+/, "string"],
       // [/@escapes/, "string.escape"],
-      [/\\./, "string.escape.invalid"],
+      // [/\\./, "string.escape.invalid"],
       [/"/, { token: "string.quote", bracket: "@close", next: "@pop" }],
     ],
     whitespace: [

port/Prettier.newt

@@ -14,7 +14,7 @@ import Prelude
 data Doc : U where
   Empty Line : Doc
   Text : String -> Doc
-  Nest : Nat -> Doc -> Doc
+  Nest : Int -> Doc -> Doc
   Seq : Doc -> Doc -> Doc
   Alt : Doc -> Doc -> Doc
 
@@ -24,7 +24,7 @@ data Doc : U where
 -- data Item = TEXT String | LINE Nat
 data Item : U where
   TEXT :  String -> Item
-  LINE : Nat -> Item
+  LINE : Int -> Item
 
 empty : Doc
 empty = Empty
@@ -43,13 +43,13 @@ group x = Alt (flatten x) x
 -- TODO - we can accumulate snoc and cat all at once
 layout : List Item -> SnocList String -> String
 layout Nil acc = fastConcat $ acc <>> Nil
-layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate k ' ')
+layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate (cast k) ' ')
 layout (TEXT str :: x) acc = layout x (acc :< str)
 
 -- Whether a documents first line fits.
-fits : Nat -> List Item -> Bool
+fits : Int -> List Item -> Bool
 fits 0 x = False
-fits w ((TEXT s) :: xs) = fits (w - length s) xs
+fits w ((TEXT s) :: xs) = fits (w - slen s) xs
 fits w _ = True
 
 -- vs Wadler, we're collecting the left side as a SnocList to prevent
@@ -58,21 +58,21 @@ fits w _ = True
 
 -- I've now added a `fit` boolean to indicate if we should cut when we hit the line length
 -- Wadler was relying on laziness to stop the first branch before LINE if necessary
-be : Bool -> SnocList Item -> Nat -> Nat -> List (Nat × Doc) -> Maybe (List Item)
+be : Bool -> SnocList Item -> Int -> Int -> List (Int × Doc) -> Maybe (List Item)
 be fit acc w k Nil = Just (acc <>> Nil)
 be fit acc w k ((i, Empty) :: xs) = be fit acc w k xs
 be fit acc w k ((i, Line) :: xs) = (be False (acc :< LINE i) w i xs)
 be fit acc w k ((i, (Text s)) :: xs) =
-  case not fit || (k + length s < w) of
-    True => (be fit (acc :< TEXT s) w (k + length s) xs)
+  case not fit || (k + slen s < w) of
+    True => (be fit (acc :< TEXT s) w (k + slen s) xs)
     False => Nothing
 be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i + j, x):: xs)
 be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs)
 be fit acc w k ((i, (Alt x y)) :: xs) =
   (_<>>_ acc) <$> (be True Lin w k ((i,x) :: xs) <|> be fit Lin w k ((i, y) :: xs))
 
-best : Nat -> Nat -> Doc -> List Item
-best w k x = fromMaybe Nil $ be False Lin w k ((Z,x) :: Nil)
+best : Int -> Int -> Doc -> List Item
+best w k x = fromMaybe Nil $ be False Lin w k ((0,x) :: Nil)
 
 -- interface Pretty a where
 --   pretty : a -> Doc
@@ -83,8 +83,8 @@ data Pretty : U -> U where
 pretty : {a} {{Pretty a}} → a → Doc
 pretty {{MkPretty p}} x = p x
 
-render : Nat -> Doc -> String
-render w x = layout (best w Z x) Lin
+render : Int -> Doc -> String
+render w x = layout (best w 0 x) Lin
 
 instance Semigroup Doc where
   x <+> y = Seq x (Seq (Text " ") y)
@@ -97,7 +97,7 @@ line = Line
 text : String -> Doc
 text = Text
 
-nest : Nat -> Doc -> Doc
+nest : Int -> Doc -> Doc
 nest = Nest
 
 instance Concat Doc where
@@ -123,7 +123,7 @@ stack = folddoc _</>_
 
 -- bracket x with l and r, indenting contents on new line
 bracket : String -> Doc -> String -> Doc
-bracket l x r = group (text l ++ nest (S (S Z)) (line ++ x) ++ line ++ text r)
+bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r)
 
 infixl 5 _<+/>_
 
@@ -138,7 +138,7 @@ fill Nil = Empty
 fill (x :: Nil) = x
 fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x </> fill (y :: xs))
 
--- separate with space
+-- separate with comma
 commaSep : List Doc -> Doc
 commaSep = folddoc (\a b => a ++ text "," <+/> b)
 

src/Lib/Common.idr

@@ -30,12 +30,6 @@ quoteString str = pack $ encode (unpack str) [< '"']
       let v : Nat = cast c in
       if v < 32 then encode cs (acc :< '\\' :< 'u' :< hexDigit (div v 4096) :< hexDigit (div v 256) :< hexDigit (div v 16) :< hexDigit v )
       else encode cs (acc :< c)
-      -- else if v < 128 then encode cs (acc :< c)
-      -- if v < 32 then encode cs (acc :< '\\' :< 'x' :< hexDigit (div v 16) :< hexDigit v )
-      -- else if v < 128 then encode cs (acc :< c)
-      -- -- TODO unicode
-      -- else if v < 256 then encode cs (acc :< '\\' :< 'x' :< hexDigit (div v 16) :< hexDigit v )
-      -- else encode cs (acc :< '\\' :< 'u' :< hexDigit (div v 4096) :< hexDigit (div v 256) :< hexDigit (div v 16) :< hexDigit v )
 
 public export
 data Json : Type where

src/Lib/Elab.idr

@@ -24,7 +24,6 @@ collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) =
   else (Def fc nm cl :: collectDecl rest)
 collectDecl (x :: xs) = x :: collectDecl xs
 
-
 -- renaming
 -- dom gamma ren
 data Pden = PR Nat Nat (List Nat)
@@ -724,7 +723,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
       Just cons <- rewriteConstraint sctynm vars cons [] | _ => pure Nothing
       pure $ Just $ MkClause fc cons pats expr
 
-
+export
 splitArgs : Raw -> List (Raw, Icit) -> (Raw, List (Raw, Icit))
 splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args)
 splitArgs tm args = (tm, args)