Get AOC day1 working

- Fixes to codegen for literal cases.
- Fix parsing of string literals
- Work around stack overflow in Prettier

.gitignore

@@ -5,3 +5,4 @@ build/
 *.log
 *.agda
 *.agdai
+*.js

aoc2023/Day1.newt

@@ -0,0 +1,94 @@
+module Day1
+
+import Lib
+ptype Int
+
+-- TODO fix import of fixity declarations
+infixr 4 _::_
+infixl 3 _<_
+infixl 4 _-_
+infixl 4 _+_
+infixl 5 _*_
+infixl 5 _/_
+infixr 0 _$_
+-- Code
+
+
+infixl 7 _._
+_._ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
+(f . g) x = f ( g x)
+
+
+digits1 : List Char -> List Int
+digits1 Nil = Nil
+digits1 (c :: cs) = let x = ord c in
+  case x < 58 of
+    True => case 48 < x of
+      True => x - 48 :: digits1 cs
+      False => digits1 cs
+    False => digits1 cs
+
+-- This happens with Char and not Nat, but why is Char working at all?
+-- I suspect it will fix if PatLit is implemented correctly
+
+tail : {a : U} -> List a -> List a
+tail Nil = Nil
+tail (x :: xs) = xs
+
+-- TODO I used @ patterns in Lean
+digits2 : List Char -> List Int
+digits2 xs = case xs of
+    ('o' :: 'n' :: 'e' :: _) => 1 :: digits2 (tail xs)
+    ('t' :: 'w' :: 'o' :: _) => 2 :: digits2 (tail xs)
+    ('t' :: 'h' :: 'r' :: 'e' :: 'e' :: _) => 3 :: digits2 (tail xs)
+    ('f' :: 'o' :: 'u' :: 'r' :: _) => 4 :: digits2 (tail xs)
+    ('f' :: 'i' :: 'v' :: 'e' :: _) => 5 :: digits2 (tail xs)
+    ('s' :: 'i' :: 'x' :: _) => 6 :: digits2 (tail xs)
+    ('s' :: 'e' :: 'v' :: 'e' :: 'n' :: _) => 7 :: digits2 (tail xs)
+    ('e' :: 'i' :: 'g' :: 'h' :: 't' :: _) => 8 :: digits2 (tail xs)
+    ('n' :: 'i' :: 'n' :: 'e' :: _) => 9 :: digits2 (tail xs)
+    (c :: cs) => let x = ord c in
+        case x < 58 of
+          True => case 48 < x of
+            True => x - 48 :: digits2 cs
+            False => digits2 cs
+          False => digits2 cs
+    Nil => Nil
+
+
+combine : List Int -> Int
+combine Nil = 0
+combine (x :: Nil) = x * 10 + x
+combine (x :: y :: Nil) = x * 10 + y
+combine (x :: y :: xs) = combine (x :: xs)
+
+part1 : String -> (String -> List Int) -> Int
+part1 text digits =
+  let lines = split (trim text) "\n" in
+  let nums = map combine $ map digits lines in
+  foldl _+_ 0 nums
+
+infixl 3 _>>_
+
+_>>_ : {A B : U} -> A -> B -> B
+a >> b = b
+
+
+runFile : String -> Dummy
+runFile fn =
+  let text = readFile fn in
+  log fn >>
+  log "part1" >>
+  log (part1 text (digits1 . unpack)) >>
+  log "part2" >>
+  log (part1 text (digits2 . unpack)) >>
+  log ""
+
+
+-- Argument is a hack to keep it from running at startup.  Need to add IO
+main : Int -> Dummy
+main _ =
+  runFile "aoc2023/day1/eg.txt" >>
+  runFile "aoc2023/day1/eg2.txt" >>
+  runFile "aoc2023/day1/input.txt"
+

aoc2023/Lib.newt

@@ -0,0 +1,133 @@
+module Lib
+
+-- Prelude
+
+data Bool : U where
+  True : Bool
+  False : Bool
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Maybe : U -> U where
+  Just : {a : U} -> a -> Maybe a
+  Nothing : {a : U} -> Maybe a
+
+data Either : U -> U -> U where
+  Left : {a b : U} -> a -> Either a b
+  Right : {a b : U} -> b -> Either a b
+
+
+infixr 4 _::_
+data List : U -> U where
+  Nil : {a : U} -> List a
+  _::_ : {a : U} -> a -> List a -> List a
+
+Cons : {a : U} -> a -> List a -> List a
+Cons x xs = x :: xs
+
+-- TODO where clauses
+reverse' : {A : U} -> List A -> List A -> List A
+reverse' Nil acc = acc
+reverse' (x :: xs) acc = reverse' xs (x :: acc)
+
+reverse : {A : U} -> List A -> List A
+reverse xs = reverse' xs Nil
+
+
+infixr 2 _,_
+
+data Pair : U -> U -> U where
+  _,_ : {a b : U} -> a -> b -> Pair a b
+
+infixr 0 _$_
+
+_$_ : {a b : U} -> (a -> b) -> a -> b
+f $ a = f a
+
+-- JS Bridge
+
+ptype Dummy
+
+
+ptype World
+data IO : U -> U where
+  MkIO : {a : U} -> (World -> Pair World a) -> IO a
+
+-- TODO unified Number for now
+ptype Int
+ptype String
+
+ptype Char
+
+ptype Array : U -> U
+
+pfunc arrayToList : {a : U} -> Array a -> List a := "
+(a, arr) => {
+  let rval = Nil(a)
+  for (let i = arr.length - 1; i >= 0; i--) {
+    rval = Cons(a, arr[i], rval)
+  }
+  return rval
+}
+"
+
+pfunc getArgs : List String := "arrayToList(String, process.argv)"
+-- Maybe integrate promises?
+
+
+pfunc ord : Char -> Int := "(c) => c.charCodeAt(0)"
+
+pfunc _<_ : Int -> Int -> Bool := "(x,y) => (x < y) ? True : False"
+pfunc _+_ : Int -> Int -> Int := "(x,y) => x + y"
+pfunc _-_ : Int -> Int -> Int := "(x,y) => x - y"
+pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y"
+pfunc _/_ : Int -> Int -> Int := "(x,y) => x / y"
+infixl 3 _<_
+infixl 4 _-_
+infixl 4 _+_
+infixl 5 _*_
+infixl 5 _/_
+
+
+-- Ideally we'd have newt write the arrows for us to keep things correct
+-- We'd still have difficulty with callbacks...
+pfunc fs : Dummy := "require('fs')"
+pfunc readFile : (fn : String) -> String := "(fn) => fs.readFileSync(fn, 'utf8')"
+pfunc log : {a : U} -> a -> Dummy := "(a, obj) => console.log(obj)"
+
+pfunc p_strHead : (s : String) -> Char := "(s) => s[0]"
+pfunc p_strTail : (s : String) -> String := "(s) => s[0]"
+
+pfunc trim : String -> String := "s => s.trim()"
+pfunc split : String -> String -> List String := "(s, by) => {
+  let parts = s.split(by)
+  let rval = Nil(String)
+  parts.reverse()
+  parts.forEach(p => { rval = _$3A$3A_(List(String), p, rval) })
+  return rval
+}"
+
+pfunc _++_ : String -> String -> String := "(a,b) => a + b"
+
+
+pfunc trace : {a : U} -> String -> a -> a := "(_, lab, a) => {
+  console.log(lab,a)
+  return a
+}"
+
+pfunc unpack : String -> List Char
+  := "(s) => {
+    let acc = Nil(Char)
+    for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc)
+    return acc
+}"
+
+foldl : {A B : U} -> (B -> A -> B) -> B -> List A -> B
+foldl f acc Nil = acc
+foldl f acc (x :: xs) = foldl f (f acc x) xs
+
+map : {A B : U} -> (A -> B) -> List A -> List B
+map f Nil = Nil
+map f (x :: xs) = f x :: map f xs

aoc2023/README.md

@@ -0,0 +1,2 @@
+
+Attempts to port AOC2023 solutions from Lean4 to see how usable newt is.

aoc2023/day1/eg.txt

@@ -0,0 +1,5 @@
+1abc2
+pqr3stu8vwx
+a1b2c3d4e5f
+treb7uchet
+

aoc2023/day1/eg2.txt

@@ -0,0 +1,7 @@
+two1nine
+eightwothree
+abcone2threexyz
+xtwone3four
+4nineeightseven2
+zoneight234
+7pqrstsixteen

src/Lib/Compile.idr

@@ -48,8 +48,16 @@ Cont e = JSExp -> JSStmt e
 
 ||| JSEnv contains `Var` for binders or `Dot` for destructured data. It
 ||| used to translate binders
-JSEnv : Type
+record JSEnv where
-JSEnv = List JSExp
+  constructor MkEnv
+  env : List JSExp
+  depth : Nat
+
+push : JSEnv -> JSExp -> JSEnv
+push env exp = { env $= (exp ::) } env
+
+empty : JSEnv
+empty = MkEnv [] Z
 
 litToJS : Literal -> JSExp
 litToJS (LString str) = LitString str
@@ -57,23 +65,24 @@ litToJS (LChar c) = LitString $ cast c
 litToJS (LInt i) = LitInt i
 
 -- Stuff nm.h1, nm.h2, ... into environment
-mkEnv : String -> Nat -> List JSExp -> List String -> List JSExp
+-- TODO consider JSExp instead of nm, so we can have $foo.h1 instead of assigning a sc.
+mkEnv : String -> Nat -> JSEnv -> List String -> JSEnv
 mkEnv nm k env [] = env
-mkEnv nm k env (x :: xs) = mkEnv nm (S k) (Dot (Var nm) "h\{show k}" :: env) xs
+mkEnv nm k env (x :: xs) = mkEnv nm (S k) (push env (Dot (Var nm) "h\{show k}")) xs
 
 envNames : Env -> List String
 
 ||| 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
+fresh nm env = if free env.env nm then nm else go nm 1
   where
-    free : JSEnv -> String -> Bool
+    free : List JSExp -> 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)
+    go nm k = let nm' = "\{nm}\{show k}" in if free env.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.
@@ -81,30 +90,28 @@ fresh nm env = if free env nm then nm else go nm 1
 -- Here we turn a Term into a statement (which may be a sequence of statements), there
 -- is a continuation, which turns the final JSExpr into a JSStmt, and the function returns
 -- a JSStmt, wrapping recursive calls in JSnoc if necessary.
-termToJS : List JSExp -> CExp -> Cont e -> JSStmt e
+termToJS : JSEnv -> CExp -> Cont e -> JSStmt e
-termToJS env (CBnd k) f = case getAt k env of
+termToJS env (CBnd k) f = case getAt k env.env of
   (Just e) => f e
   Nothing => ?bad_bounds
 termToJS env (CLam nm t) f =
   let nm' = fresh nm env -- "\{nm}$\{show $ length env}"
-      env' = (Var nm' :: env)
+      env' = push env (Var nm')
   in f $ JLam [nm'] (termToJS env' t JReturn)
 termToJS env (CFun nms t) f =
   let nms' = map (\nm => fresh nm env) nms
-      env' = foldl (\ e, nm => Var nm :: e) env nms'
+      env' = foldl (\ e, nm => push e (Var nm)) env nms'
   in f $ JLam nms' (termToJS env' t JReturn)
 termToJS env (CRef nm) f = f $ Var nm
 termToJS env (CMeta k) f = f $ LitString "META \{show k}"
-termToJS env (CLit (LString str)) f = f (LitString str)
+termToJS env (CLit lit) f = f (litToJS lit)
-termToJS env (CLit (LChar c)) f = f (LitString $ cast c)
-termToJS env (CLit (LInt i)) f = f (LitInt i)
 -- if it's a var, just use the original
-termToJS env (CLet nm (CBnd k) u) f = case getAt k env of
+termToJS env (CLet nm (CBnd k) u) f = case getAt k env.env of
-  Just e  => termToJS (e :: env) u f
+  Just e  => termToJS (push env e) u f
   Nothing => ?bad_bounds2
 termToJS env (CLet nm t u) f =
   let nm' = fresh nm env
-      env' = (Var nm' :: env)
+      env' = push env (Var nm')
   -- If it's a simple term, use const
   in case termToJS env t (JAssign nm') of
     (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f)
@@ -124,20 +131,24 @@ termToJS env (CCase t alts) f =
 
   termToJS env t $ \case
     (Var nm) => maybeCaseStmt env nm alts
-    t' =>
+    t' => do
-      let nm = fresh "sc" env in
+      -- TODO refactor nm to be a JSExp with Var{} or Dot{}
-        JSnoc (JConst nm t') (maybeCaseStmt (Var nm :: env) nm alts)
+      let nm = "sc$\{show env.depth}"
+      let env' = { depth $= S } env
+      JSnoc (JConst nm t') (maybeCaseStmt env' nm alts)
 
   where
-    termToJSAlt : List JSExp -> String -> CAlt -> JAlt
+    termToJSAlt : JSEnv -> String -> CAlt -> JAlt
     termToJSAlt env nm (CConAlt name args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f)
     -- intentionally reusing scrutinee name here
-    termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS (Var nm :: env) u f)
+    termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS  (env) u f)
-    termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS (Var nm :: env) u f)
+    termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS env u f)
 
-    maybeCaseStmt : List JSExp -> String -> List CAlt -> JSStmt e
+    maybeCaseStmt : JSEnv -> String -> List CAlt -> JSStmt e
     -- If there is a single alt, assume it matched
     maybeCaseStmt env nm [(CConAlt _ args u)] = (termToJS (mkEnv nm 0 env args) u f)
+    maybeCaseStmt env nm alts@(CLitAlt _ _  :: _) =
+        (JCase (Var nm) (map (termToJSAlt env nm) alts))
     maybeCaseStmt env nm alts =
           (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts))
 
@@ -233,7 +244,7 @@ entryToDoc (MkEntry name ty (Fn tm)) = do
   debug "compileFun \{pprint [] tm}"
   ct <- compileFun tm
   -- If ct has zero arity and is a compount expression, this fails..
-  let body@(JPlain {}) = termToJS [] ct JPlain
+  let body@(JPlain {}) = termToJS empty ct JPlain
     | js => error (getFC tm) "Not a plain expression: \{render 80 $ stmtToDoc js}"
   pure (text "const" <+> jsIdent name <+> text "=" <+/> stmtToDoc body)
 entryToDoc (MkEntry name type Axiom) = pure ""
@@ -243,7 +254,7 @@ entryToDoc (MkEntry name type PrimTCon) = pure $ dcon name (piArity type)
 entryToDoc (MkEntry name _ (PrimFn src)) = pure $ text "const" <+> jsIdent name <+> "=" <+> text src
 
 export
-compile : M Doc
+compile : M (List Doc)
 compile = do
   top <- get
-  pure $ stack $ !(traverse entryToDoc top.defs)
+  traverse entryToDoc top.defs

src/Lib/Elab.idr

@@ -680,7 +680,7 @@ buildLitCase ctx prob fc scnm scty lit = do
 
 buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt)
 buildLitCases ctx prob fc scnm scty = do
-  let lits = getLits scnm prob.clauses
+  let lits = nub $ getLits scnm prob.clauses
   alts <- traverse (buildLitCase ctx prob fc scnm scty) lits
   -- TODO build default case
   -- run getLits

src/Lib/Tokenizer.idr

@@ -44,6 +44,7 @@ unquote str = case unpack str of
     go : List Char -> List Char
     go [] = []
     go ['"'] = []
+    go ('\\' :: ('n' :: xs)) = '\n' :: go xs
     go ('\\' :: (x :: xs)) = x :: go xs
     go (x :: xs) = x :: go xs
 
@@ -55,7 +56,7 @@ rawTokens
   <|> match (is '#' <+> many alpha) (Tok Pragma)
   <|> match charLit (Tok Character)
   <|> match (exact "_" <+> (some opChar <|> exact ",") <+> exact "_") (Tok MixFix)
-  <|> match (quo <+> manyUntil quo ((esc any <+> any) <|> any) <+> opt quo) (Tok StringKind . unquote)
+  <|> match (quo <+> manyUntil quo (esc any <|> any) <+> quo) (Tok StringKind . unquote)
   <|> match (lineComment (exact "--")) (Tok Space)
   <|> match (blockComment (exact "/-") (exact "-/")) (Tok Space)
   <|> match (exact ",") (Tok Oper)

src/Lib/Types.idr

@@ -73,7 +73,6 @@ Show Literal where
 public export
 data CaseAlt : Type where
   CaseDefault : Tm -> CaseAlt
-  -- I've also seen a list of stuff that gets replaced
   CaseCons : (name : String) -> (args : List String) -> Tm ->  CaseAlt
   CaseLit : Literal -> Tm ->  CaseAlt
 
@@ -98,7 +97,6 @@ data Tm : Type where
   App : FC -> Tm -> Tm -> Tm
   U   : FC -> Tm
   Pi  : FC -> Name -> Icit -> Tm -> Tm -> Tm
-  -- REVIEW - do we want to just push it up like idris?
   Case : FC -> Tm -> List CaseAlt -> Tm
   -- need type?
   Let : FC -> Name -> Tm -> Tm -> Tm
@@ -173,7 +171,7 @@ pprint names tm = render 80 $ go names tm
     goAlt : List String -> CaseAlt -> Doc
 
     goAlt names (CaseDefault t) = "_" <+> "=>" <+> go ("_" :: names) t
-    goAlt names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+/> go (args ++ names) t
+    goAlt names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+/> go (reverse args ++ names) t
     goAlt names (CaseLit lit t) = text (show lit) <+> "=>" <+/> go names t
 
     go names (Bnd _ k) = case getAt k names of

src/Main.idr

@@ -38,15 +38,13 @@ dumpContext top = do
     go [] = pure ()
     go (x :: xs) = putStrLn "    \{show x}" >> go xs
 
-dumpSource : M ()
-dumpSource = do
-  doc <- compile
-  putStrLn $ render 90 doc
 
 writeSource : String -> M ()
 writeSource fn = do
-  doc <- compile
+  docs <- compile
-  let src = "#!/usr/bin/env node\n" ++ render 90 doc ++ "\nmain();"
+  let src = unlines $ ["#!/usr/bin/env node"]
+        ++ map (render 90) docs
+        ++ [ "main();" ]
   Right _ <- writeFile fn src
     | Left err => fail (show err)
   Right _ <- chmodRaw fn 493 | Left err => fail (show err)

tests/black/Prelude.newt

@@ -12,3 +12,13 @@ data Either : U -> U -> U where
   Left : {a b : U} -> a -> Either a b
   Right : {a b : U} -> b -> Either a b
 
+data List : U -> U where
+  Nil : {a : U} -> List a
+  Cons : {a : U} -> a -> List a -> List a
+
+-- Currently if I say _::_ = Cons, it gets curried
+
+infixr 4 _::_
+_::_ : {a : U} -> a -> List a -> List a
+_::_ x xs = Cons x xs
+