Day3 working

- Fix string and character encoding in output
- Fix autos not solving if another extends context

TODO.md

@@ -1,11 +1,14 @@
 
 ## TODO
 
+- [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
+- [ ] Fix string printing to be js instead of weird Idris strings
 - [ ] make $ special
   - Makes inference easier, cleaner output, and allows `foo $ \ x => ...`
   - remove hack from Elab.infer
 - [ ] Support @ on the LHS
 - [ ] records
+- [ ] `Inhabited (List a)` isn't solving if I have `instance ∀ a. Inhabited (List a)`
 - [ ] rework unify case tree
   - Idris needs help with the case tree to keep code size down, do it in stages, one dcon at a time.
 - [ ] Strategy to avoid three copies of `Prelude.newt` in this source tree

aoc2023/Day2.newt

@@ -12,14 +12,6 @@ data Game : U where
 -- Original had class and instance...
 -- Add, Sub, Mul, Neg
 
--- NB this is not lazy!
-infixl 5 _&&_
-
-_&&_ : Bool -> Bool -> Bool
-a && b = case a of
-  False => False
-  True => b
-
 max : Int -> Int -> Int
 max x y = case x < y of
   True => y

aoc2023/Day3.newt

@@ -0,0 +1,118 @@
+module Day3
+
+import Prelude
+import Node
+
+pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
+pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, '  ')`
+
+pfunc trace : ∀ a. String -> a -> a := `(_, msg, a) => { console.log(msg,debugStr(_,a)); return a }`
+
+maybe : ∀ a b. b → (a → b) → Maybe a → b
+maybe def f Nothing = def
+maybe def f (Just a) = f a
+
+-- was 'structure' I could make a `record` that destructures to this..
+data Number : U where
+  MkNumber : (start : Nat) -> (stop : Nat) → (value : Int) → Number
+
+isDigit : Char -> Bool
+isDigit '0' = True
+isDigit '1' = True
+isDigit '2' = True
+isDigit '3' = True
+isDigit '4' = True
+isDigit '5' = True
+isDigit '6' = True
+isDigit '7' = True
+isDigit '8' = True
+isDigit '9' = True
+isDigit _ = False
+
+numbers : List Char -> List Number
+numbers arr = go arr Z
+  where
+    go : List Char → Nat → List Number
+    go (c :: cs) start = if isDigit c
+      -- then let (front,back) = span isDigit (c :: cs) in ?
+      then case span isDigit (c :: cs) of
+        -- NOW FC on app is now broken, need the fc of the left
+          (front,back) => let stop = start + length front
+            in MkNumber start stop (stringToInt $ pack front) :: go back stop
+      else go cs (S start)
+    go Nil start = Nil
+
+
+range : ∀ a. Nat -> Nat -> List a -> List a
+range _ _ Nil = Nil
+range _ Z _ = Nil
+range Z (S k) (x :: xs) = x :: range Z k xs
+range (S n) (S m) (x :: xs) = range n m xs
+
+isPart : List (List Char) -> Nat -> Number -> Bool
+isPart rows row (MkNumber start end _) =
+  checkRow (pred row) || checkRow row || checkRow (S row)
+  where
+    isThing : Char -> Bool
+    isThing c = not (isDigit c || c == '.')
+
+    checkRow : Nat -> Bool
+    checkRow r = case getAt r rows of
+      Nothing => False
+      Just chars => case filter isThing (range (pred start) (S end) chars) of
+        Nil => False
+        _ => True
+
+getValue : Number -> Int
+getValue (MkNumber _ _ v) = v
+
+part1 : List (List Char) -> Int
+part1 rows =
+    foldl (\ acc num => acc + getValue num) 0 $
+      join $ map (partNums rows) $ enumerate rows
+  where
+    partNums : List (List Char) -> (Nat × List Char) -> List Number
+    partNums grid (r, cs) =
+      filter (isPart grid r) $ (numbers cs)
+
+gears : List (List Char) -> List Char -> Nat -> Int
+gears rows row y =
+    let a = numbers (getAt! (pred y) rows)
+        b = numbers (getAt! y rows)
+        c = numbers (getAt! (S y) rows)
+        all = a ++ b ++ c
+        cands = map fst $ filter (_==_ '*' ∘ snd) (enumerate row)
+    in foldl _+_ 0 $ map (check all) cands
+  where
+    ratio : List Int → Int
+    ratio (a :: b :: Nil) = a * b
+    ratio _ = 0
+
+    match : Nat → Number → Bool
+    match y (MkNumber start stop value) = pred start <= y && y < S stop
+
+    check : List Number → Nat →  Int
+    check nums y = ratio $ map getValue (filter (match y) nums)
+
+part2 : List (List Char) -> Int
+part2 rows =
+  foldl go 0 (enumerate rows)
+  where
+    go : Int → Nat × List Char → Int
+    go acc (y, row) = acc + gears rows row y
+
+-- 4361 / 467835
+-- 517021 / 81296995
+run : String -> IO Unit
+run fn = do
+  content <- readFile fn
+  let grid = (splitOn '\n' $ unpack $ trim content)
+  putStrLn fn
+  printLn (part1 grid)
+  printLn (part2 grid)
+
+main : IO Unit
+main = do
+  run "aoc2023/day3/eg.txt"
+  run "aoc2023/day3/input.txt"
+

aoc2023/Prelude.newt

@@ -0,0 +1,485 @@
+module Prelude
+
+id : ∀ a. a → a
+id x = x
+
+data Bool : U where
+  True False : Bool
+
+not : Bool → Bool
+not True = False
+not False = True
+
+-- In Idris, this is lazy in the second arg, we're not doing
+-- magic laziness for now, it's messy
+infixr 4 _||_
+_||_ : Bool → Bool → Bool
+True || _ = True
+False || b = b
+
+infixr 5 _&&_
+_&&_ : Bool → Bool → Bool
+False && b = False
+True && b = b
+
+infixl 6 _==_
+class Eq a where
+  _==_ : a → a → Bool
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+pred : Nat → Nat
+pred Z = Z
+pred (S k) = k
+
+instance Eq Nat where
+  Z == Z = True
+  S n == S m = n == m
+  x == y = False
+
+data Maybe : U -> U where
+  Just : ∀ a. a -> Maybe a
+  Nothing : ∀ a. Maybe a
+
+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
+
+infixr 7 _::_
+data List : U -> U where
+  Nil : ∀ A. List A
+  _::_ : ∀ A. A → List 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
+
+-- 'chips'
+infixr 6 _<>>_
+_<>>_ : ∀ a. SnocList a → List a → List a
+Lin <>> ys = ys
+(xs :< x) <>> ys = xs <>> x :: ys
+
+-- TODO this is special cased in some languages, maybe for easier
+-- inference? Figure out why.
+-- Currently very noisy in generated code (if nothing else, optimize it out?)
+infixr 0 _$_
+_$_ : ∀ a b. (a -> b) -> a -> b
+f $ a = f a
+
+infixr 8 _×_
+infixr 2 _,_
+data _×_ : U → U → U where
+  _,_ : ∀ A B. A → B → A × B
+
+fst : ∀ a b. a × b → a
+fst (a,b) = a
+
+snd : ∀ a b. a × b → b
+snd (a,b) = b
+
+infixl 6 _<_ _<=_
+class Ord a where
+  _<_ : a → a → Bool
+
+instance Ord Nat where
+  _ < Z = False
+  Z < S _ = True
+  S n < S m = n < m
+
+_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
+a <= b = a == b || a < b
+-- Monad
+
+class Monad (m : U → U) where
+  bind : {0 a b} → m a → (a → m b) → m b
+  pure : {0 a} → a → m a
+
+infixl 1 _>>=_ _>>_
+_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
+ma >>= amb = bind ma amb
+
+_>>_ :  {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
+ma >> mb = mb
+
+join : ∀ m. {{Monad m}} {0 a} → m (m a) → m a
+join mma = mma >>= id
+
+-- Equality
+
+infixl 1 _≡_
+data _≡_ : {A : U} -> A -> A -> U where
+  Refl :  {A : U} -> {a : A} -> a ≡ a
+
+replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace p Refl x = x
+
+cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+
+sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
+sym Refl = Refl
+
+-- Functor
+
+class Functor (m : U → U) where
+  map : {0 a b} → (a → b) → m a → m b
+
+infixr 4 _<$>_
+_<$>_ : {0 f} {{Functor f}} {0 a b} → (a → b) → f a → f b
+f <$> ma = map f ma
+
+instance Functor Maybe where
+  map f Nothing = Nothing
+  map f (Just a) = Just (f a)
+
+instance Functor List where
+  map f Nil = Nil
+  map f (x :: xs) = f x :: map f xs
+
+instance Functor SnocList where
+  map f Lin = Lin
+  map f (xs :< x) = map f xs :< f x
+
+-- TODO this probably should depend on / entail Functor
+infixl 3 _<*>_
+class Applicative (f : U → U) where
+  -- appIsFunctor : Functor f
+  return : {0 a} → a → f a
+  _<*>_ : {0 a b} -> f (a → b) → f a → f b
+
+infixr 2 _<|>_
+class Alternative (m : U → U) where
+  _<|>_ : {0 a} → m a → m a → m a
+
+instance Alternative Maybe where
+  Nothing <|> x = x
+  Just x <|> _ = Just x
+
+-- Semigroup
+
+infixl 8 _<+>_
+class Semigroup a where
+  _<+>_ : a → a → a
+
+infixl 7 _+_
+class Add a where
+  _+_ : a → a → a
+
+infixl 8 _*_
+class Mul a where
+  _*_ : a → a → a
+
+instance Add Nat where
+  Z + m = m
+  S n + m = S (n + m)
+
+instance Mul Nat where
+  Z * _ = Z
+  S n * m = m + n * m
+
+infixl 7 _-_
+class Sub a where
+  _-_ : a → a → a
+
+instance Sub Nat where
+  Z - m = Z
+  n - Z = n
+  S n - S m = n - m
+
+infixr 7 _++_
+class Concat a where
+  _++_ : a → a → a
+
+ptype String
+ptype Int
+ptype Char
+
+pfunc sconcat : String → String → String := `(x,y) => x + y`
+instance Concat String where
+  _++_ = sconcat
+
+
+pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? True : False`
+instance Eq Int where
+  a == b = jsEq a b
+
+instance Eq String where
+  a == b = jsEq a b
+
+instance Eq Char where
+  a == b = jsEq a b
+
+data Unit : U where
+  MkUnit : Unit
+
+ptype Array : U → U
+pfunc listToArray : {a : U} -> List a -> Array a := `
+(a, l) => {
+  let rval = []
+  while (l.tag !== 'Nil') {
+    rval.push(l.h1)
+    l = l.h2
+  }
+  return rval
+}
+`
+
+pfunc alen : {0 a : U} -> Array a -> Int := `(a,arr) => arr.length`
+pfunc aget : {0 a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
+pfunc aempty : {0 a : U} -> Unit -> Array a := `() => []`
+
+pfunc arrayToList uses (Nil _::_) : {0 a} → Array a → List a := `(a,arr) => {
+  let rval = Nil(a)
+  for (let i = arr.length - 1;i >= 0; i--) {
+    rval = _$3A$3A_(a, arr[i], rval)
+  }
+  return rval
+}`
+
+
+
+-- for now I'll run this in JS
+pfunc lines : String → List String := `(s) => arrayToList(s.split('\n'))`
+
+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 uses (Nil _::_) : String -> String -> List String := `(s, by) => {
+  let parts = s.split(by)
+  let rval = Nil(String)
+  parts.reverse()
+  parts.forEach(p => { rval = _$3A$3A_(undefined, p, rval) })
+  return rval
+}`
+
+pfunc slen : String -> Int := `s => s.length`
+pfunc sindex : String -> Int -> Char := `(s,i) => s[i]`
+
+-- TODO represent Nat as number at runtime
+pfunc natToInt : Nat -> Int := `(n) => {
+  let rval = 0
+  while (n.tag === 'S') {
+    n = n.h0
+    rval++
+  }
+  return rval
+}`
+
+pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')`
+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 : U} -> a -> World -> IORes a
+
+IO : U -> U
+IO a = World -> IORes a
+
+instance Monad IO where
+  bind ma mab = \ w => case ma w of
+    MkIORes a w => mab a w
+  pure a = \ w => MkIORes a w
+
+bindList : ∀ a b. List a → (a → List b) → List b
+
+instance ∀ a. Concat (List a) where
+  Nil ++ ys = ys
+  (x :: xs) ++ ys = x :: (xs ++ ys)
+
+instance Monad List where
+  pure a = a :: Nil
+  bind Nil amb = Nil
+  bind (x :: xs) amb = amb x ++ bind xs amb
+
+class HasIO (m : U -> U) where
+  liftIO : ∀ a. IO a → m a
+
+instance HasIO IO where
+  liftIO a = a
+
+pfunc debugLog uses (MkIORes MkUnit) : ∀ a. a -> IO Unit := `(_,s) => (w) => {
+  console.log(s)
+  return MkIORes(undefined,MkUnit,w)
+}`
+
+pfunc primPutStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
+  console.log(s)
+  return MkIORes(undefined,MkUnit,w)
+}`
+
+putStrLn : ∀ io. {{HasIO io}} -> String -> io Unit
+putStrLn s = liftIO (primPutStrLn s)
+
+pfunc showInt : Int -> String := `(i) => String(i)`
+
+class Show a where
+  show : a → String
+
+instance Show String where
+  show a = a
+
+instance Show Int where
+  show = showInt
+
+pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)`
+
+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
+}`
+
+pfunc pack : List Char → String := `(cs) => {
+  let rval = ''
+  while (cs.tag === '_::_') {
+    rval += cs.h1
+    cs = cs.h2
+  }
+
+  return rval
+}
+`
+
+pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => {
+  const go = (obj) => {
+    if (obj?.tag === '_::_') {
+      let stuff = listToArray(undefined,obj)
+      return '['+(stuff.map(go).join(', '))+']'
+    }
+    if (obj?.tag === 'S') {
+      return ''+natToInt(obj)
+    } else if (obj?.tag) {
+      let rval = '('+obj.tag
+      for(let i=0;;i++) {
+        let key = 'h'+i
+        if (!(key in obj)) break
+        rval += ' ' + go(obj[key])
+      }
+      return rval+')'
+    } else {
+      return JSON.stringify(obj)
+    }
+  }
+  return go(obj)
+}`
+
+pfunc stringToInt : String → Int := `(s) => {
+  let rval = Number(s)
+  if (isNaN(rval)) throw new Error(s + " is NaN")
+  return rval
+}`
+
+foldl : ∀ A B. (B -> A -> B) -> B -> List A -> B
+foldl f acc Nil = acc
+foldl f acc (x :: xs) = foldl f (f acc x) xs
+
+infixl 9 _∘_
+_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
+(f ∘ g) x = f (g x)
+
+
+pfunc addInt : Int → Int → Int := `(x,y) => x + y`
+pfunc mulInt : Int → Int → Int := `(x,y) => x * y`
+pfunc subInt : Int → Int → Int := `(x,y) => x - y`
+pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? True : False`
+
+instance Mul Int where
+  x * y = mulInt x y
+
+instance Add Int where
+  x + y = addInt x y
+
+instance Sub Int where
+  x - y = subInt x y
+
+instance Ord Int where
+  x < y = ltInt x y
+
+printLn : {m} {{HasIO m}} {a} {{Show a}} → a → m Unit
+printLn a = putStrLn (show a)
+
+-- opaque JSObject
+ptype JSObject
+
+reverse : ∀ a. List a → List a
+reverse {a} = go Nil
+  where
+    go : List a → List a → List a
+    go acc Nil = acc
+    go acc (x :: xs) = go (x :: acc) xs
+
+-- Like Idris1, but not idris2, we need {a} to put a in scope.
+span : ∀ a. (a -> Bool) -> List a -> List a × List a
+span {a} f xs = go xs Nil
+  where
+    go : List a -> List a -> List a × List a
+    go Nil left = (reverse left, Nil)
+    go (x :: xs) left = if f x
+      then go xs (x :: left)
+      else (reverse left, x :: xs)
+
+instance Show Nat where
+  show n = show (natToInt n)
+
+enumerate : ∀ a. List a → List (Nat × a)
+enumerate {a} xs = go Z xs
+  where
+    go : Nat → List a → List (Nat × a)
+    go k Nil = Nil
+    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
+
+drop : ∀ a. Nat -> List a -> List a
+drop _ Nil = Nil
+drop Z xs = xs
+drop (S k) (x :: xs) = drop k xs
+
+take : ∀ a. Nat -> List a -> List a
+take Z xs = Nil
+take _ Nil = Nil
+take (S k) (x :: xs) = x :: take k xs
+
+getAt : ∀ a. Nat → List a → Maybe a
+getAt _ Nil = Nothing
+getAt Z (x :: xs) = Just x
+getAt (S k) (x :: xs) = getAt k xs
+
+splitOn : ∀ a. {{Eq a}} → a → List a → List (List a)
+splitOn {a} v xs = go Nil xs
+  where
+    go : List a → List a → List (List a)
+    go acc Nil = reverse acc :: Nil
+    go acc (x :: xs) = if x == v
+      then reverse acc :: go Nil xs
+      else go (x :: acc) xs
+
+
+class Inhabited a where
+  default : a
+
+instance ∀ a. Inhabited (List a) where
+  default = Nil
+
+getAt! : ∀ a. {{Inhabited a}} → Nat → List a → a
+getAt! _ Nil = default
+getAt! Z (x :: xs) = x
+getAt! (S k) (x :: xs) = getAt! k xs

aoc2023/day3/eg.txt

@@ -0,0 +1,10 @@
+467..114..
+...*......
+..35..633.
+......#...
+617*......
+.....+.58.
+..592.....
+......755.
+...$.*....
+.664.598..

playground/samples/Day2.newt

@@ -17,14 +17,6 @@ data Game : U where
 -- Original had class and instance...
 -- Add, Sub, Mul, Neg
 
--- NB this is not lazy!
-infixl 5 _&&_
-
-_&&_ : Bool -> Bool -> Bool
-a && b = case a of
-  False => False
-  True => b
-
 max : Int -> Int -> Int
 max x y = case x < y of
   True => y

playground/samples/Prelude.newt

@@ -1,5 +1,7 @@
 module Prelude
 
+id : ∀ a. a → a
+id x = x
 
 data Bool : U where
   True False : Bool
@@ -15,6 +17,11 @@ _||_ : Bool → Bool → Bool
 True || _ = True
 False || b = b
 
+infixr 5 _&&_
+_&&_ : Bool → Bool → Bool
+False && b = False
+True && b = b
+
 infixl 6 _==_
 class Eq a where
   _==_ : a → a → Bool
@@ -23,6 +30,10 @@ data Nat : U where
   Z : Nat
   S : Nat -> Nat
 
+pred : Nat → Nat
+pred Z = Z
+pred (S k) = k
+
 instance Eq Nat where
   Z == Z = True
   S n == S m = n == m
@@ -73,7 +84,13 @@ infixr 2 _,_
 data _×_ : U → U → U where
   _,_ : ∀ A B. A → B → A × B
 
-infixl 6 _<_
+fst : ∀ a b. a × b → a
+fst (a,b) = a
+
+snd : ∀ a b. a × b → b
+snd (a,b) = b
+
+infixl 6 _<_ _<=_
 class Ord a where
   _<_ : a → a → Bool
 
@@ -82,6 +99,8 @@ instance Ord Nat where
   Z < S _ = True
   S n < S m = n < m
 
+_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
+a <= b = a == b || a < b
 -- Monad
 
 class Monad (m : U → U) where
@@ -95,6 +114,9 @@ ma >>= amb = bind ma amb
 _>>_ :  {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
 ma >> mb = mb
 
+join : ∀ m. {{Monad m}} {0 a} → m (m a) → m a
+join mma = mma >>= id
+
 -- Equality
 
 infixl 1 _≡_
@@ -167,7 +189,6 @@ instance Mul Nat where
   Z * _ = Z
   S n * m = m + n * m
 
-
 infixl 7 _-_
 class Sub a where
   _-_ : a → a → a
@@ -189,6 +210,17 @@ pfunc sconcat : String → String → String := `(x,y) => x + y`
 instance Concat String where
   _++_ = sconcat
 
+
+pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? True : False`
+instance Eq Int where
+  a == b = jsEq a b
+
+instance Eq String where
+  a == b = jsEq a b
+
+instance Eq Char where
+  a == b = jsEq a b
+
 data Unit : U where
   MkUnit : Unit
 
@@ -306,9 +338,6 @@ instance Show Int where
 
 pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)`
 
-infix 6 _<=_
-pfunc _<=_ uses (True False) : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False`
-
 pfunc unpack : String -> List Char
   := `(s) => {
     let acc = Nil(Char)
@@ -327,9 +356,15 @@ pfunc pack : List Char → String := `(cs) => {
 }
 `
 
-pfunc debugStr : ∀ a. a → String := `(_, obj) => {
+pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => {
   const go = (obj) => {
-    if (obj?.tag) {
+    if (obj?.tag === '_::_') {
+      let stuff = listToArray(undefined,obj)
+      return '['+(stuff.map(go).join(', '))+']'
+    }
+    if (obj?.tag === 'S') {
+      return ''+natToInt(obj)
+    } else if (obj?.tag) {
       let rval = '('+obj.tag
       for(let i=0;;i++) {
         let key = 'h'+i
@@ -398,3 +433,53 @@ span {a} f xs = go xs Nil
     go (x :: xs) left = if f x
       then go xs (x :: left)
       else (reverse left, x :: xs)
+
+instance Show Nat where
+  show n = show (natToInt n)
+
+enumerate : ∀ a. List a → List (Nat × a)
+enumerate {a} xs = go Z xs
+  where
+    go : Nat → List a → List (Nat × a)
+    go k Nil = Nil
+    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
+
+drop : ∀ a. Nat -> List a -> List a
+drop _ Nil = Nil
+drop Z xs = xs
+drop (S k) (x :: xs) = drop k xs
+
+take : ∀ a. Nat -> List a -> List a
+take Z xs = Nil
+take _ Nil = Nil
+take (S k) (x :: xs) = x :: take k xs
+
+getAt : ∀ a. Nat → List a → Maybe a
+getAt _ Nil = Nothing
+getAt Z (x :: xs) = Just x
+getAt (S k) (x :: xs) = getAt k xs
+
+splitOn : ∀ a. {{Eq a}} → a → List a → List (List a)
+splitOn {a} v xs = go Nil xs
+  where
+    go : List a → List a → List (List a)
+    go acc Nil = reverse acc :: Nil
+    go acc (x :: xs) = if x == v
+      then reverse acc :: go Nil xs
+      else go (x :: acc) xs
+
+
+class Inhabited a where
+  default : a
+
+instance ∀ a. Inhabited (List a) where
+  default = Nil
+
+getAt! : ∀ a. {{Inhabited a}} → Nat → List a → a
+getAt! _ Nil = default
+getAt! Z (x :: xs) = x
+getAt! (S k) (x :: xs) = getAt! k xs

src/Lib/Compile.idr

@@ -171,28 +171,45 @@ termToJS env (CCase t alts) f =
     maybeCaseStmt env nm alts =
           (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts))
 
+chars : List Char
+chars = unpack "0123456789ABCDEF"
+
+hexDigit : Nat -> Char
+hexDigit v = fromMaybe ' ' (getAt (mod v 16) chars)
+
+toHex : Nat -> List Char
+toHex 0 = []
+toHex v = snoc (toHex (div v 16)) (hexDigit v)
 
 -- FIXME escaping is wrong, e.g. \215 instead of \xd7
 jsString : String -> Doc
-jsString str = text (show str)
+jsString str = text $ pack $ encode (unpack str) [< '"']
+  where
+    encode : List Char -> SnocList Char -> List Char
+    encode [] acc = acc <>> ['"']
+    encode ('"' :: cs) acc = encode cs (acc :< '\\' :< '"')
+    encode ('\n' :: cs) acc = encode cs (acc :< '\\' :< 'n')
+    encode ('\\' :: cs) acc = encode cs (acc :< '\\' :< '\\')
+    encode (c :: cs) acc =
+      let v : Nat = cast c in
+      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 )
 
 keywords : List String
 keywords = [
   "var", "true", "false", "let", "case", "switch", "if", "then", "else", "String",
   "function", "void", "undefined", "null", "await", "async", "return", "const",
-  "Number"
+  "Number", "default"
 ]
 
 ||| escape identifiers for js
 jsIdent : String -> Doc
 jsIdent id = if elem id keywords then text ("$" ++ id) else text $ pack $ fix (unpack id)
   where
-    chars : List Char
-    chars = unpack "0123456789ABCDEF"
 
-    toHex : Nat -> List Char
-    toHex 0 = []
-    toHex v = snoc (toHex (div v 16)) (fromMaybe ' ' (getAt (mod v 16) chars))
 
     fix : List Char -> List Char
     fix [] = []

src/Lib/Parser.idr

@@ -61,7 +61,7 @@ charLit : Parser Raw
 charLit = do
   fc <- getPos
   v <- token Character
-  pure $ RLit fc (LChar $ assert_total $ strIndex v 1)
+  pure $ RLit fc (LChar $ assert_total $ strIndex v 0)
 
 lit : Parser Raw
 lit = intLit <|> stringLit <|> charLit

src/Lib/ProcessDecl.idr

@@ -93,8 +93,8 @@ makeSpine (S k) (Bound :: xs) = makeSpine k xs :< VVar emptyFC k [<]
 makeSpine 0 xs = ?fixme
 
 solveAutos : Nat -> List MetaEntry -> M ()
-solveAutos mlen [] = pure ()
+solveAutos mstart [] = pure ()
-solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
+solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
       debug "AUTO solving \{show k} : \{show ty}"
       -- we want the context here too.
       top <- get
@@ -103,7 +103,7 @@ solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
             xs => pure xs
         | res => do
           debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}"
-          solveAutos mlen es
+          solveAutos mstart es
         -- | res => error fc "FAILED to solve \{show ty}, matches: \{show $ map (pprint [] . fst) res}"
       writeIORef top.metas mc
       val <- eval ctx.env CBN tm
@@ -111,8 +111,9 @@ solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
       let sp = makeSpine ctx.lvl ctx.bds
       solve ctx.env k sp val
       mc <- readIORef top.metas
-      solveAutos mlen (take mlen mc.metas)
+      let mlen = length mc.metas `minus` mstart
-solveAutos mlen (_ :: es) = solveAutos mlen es
+      solveAutos mstart (take mlen mc.metas)
+solveAutos mstart (_ :: es) = solveAutos mstart es
 
 dumpEnv : Context -> M String
 dumpEnv ctx =
@@ -218,7 +219,7 @@ processDecl (Def fc nm clauses) = do
 
   mc <- readIORef top.metas
   let mlen = length mc.metas `minus` mstart
-  solveAutos mlen (take mlen mc.metas)
+  solveAutos mstart (take mlen mc.metas)
   -- TODO - make nf that expands all metas and drop zonk
   -- Day1.newt is a test case
   -- tm' <- nf [] tm

src/Lib/Token.idr

@@ -42,6 +42,7 @@ Show Kind where
   show Pragma  = "Pragma"
   show StringKind = "String"
   show JSLit = "JSLit"
+
 export
 Eq Kind where
   Ident   == Ident = True

src/Lib/Tokenizer.idr

@@ -47,6 +47,17 @@ unquote str = case unpack str of
     go ('\\' :: (x :: xs)) = x :: go xs
     go (x :: xs) = x :: go xs
 
+unquoteChar : String -> String
+unquoteChar str = pack $ case unpack str of
+  ('\'' :: xs) => go xs
+  imp => go imp -- shouldn't happen
+  where
+    go : List Char -> List Char
+    go [] = ['\''] -- shouldn't happen
+    go ('\\' :: ('n' :: xs)) = ['\n']
+    go ('\\' :: (x :: xs)) = [x]
+    go (x :: xs) = [x]
+
 opMiddle = pred (\c => not (isSpace c || c == '_'))
 
 btick = is '`'
@@ -61,6 +72,11 @@ trimJS str = case unpack str of
     go ['`'] = []
     go (x :: xs) = x :: go xs
 
+%hide charLit
+charLit : Lexer
+charLit = is '\'' <+> (is '\\' <+> any <|> any) <+> is '\''
+
+
 rawTokens : Tokenizer (Token Kind)
 rawTokens
   = match spaces (Tok Space)
@@ -75,7 +91,7 @@ rawTokens
   -- REVIEW - expect non-alpha after?
   <|> match (some digit) (Tok Number)
   -- for module names and maybe type constructors
-  <|> match (charLit) (Tok Character)
+  <|> match (charLit) (Tok Character . unquoteChar)
   <|> match (is '#' <+> many alpha) (Tok Pragma)
   <|> match (lineComment (exact "--")) (Tok Space)
   <|> match (blockComment (exact "/-") (exact "-/")) (Tok Space)

src/Main.idr

@@ -43,7 +43,7 @@ writeSource : String -> M ()
 writeSource fn = do
   docs <- compile
   let src = unlines $
-        [ "#!/usr/bin/env node"
+        [ "\"use strict\";"
         ,  "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })" ]
         ++ map (render 90) docs
         ++ [ "main();" ]