Day6 and let identifiers contain ?

TODO.md

@@ -1,6 +1,8 @@
 
 ## TODO
 
+- [ ] literals for double
+- [ ] default failing case for constructor matching
 - [ ] Add icit to Lam (see `check` for details)
 - [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
 - [x] deconstructing `let` (and do arrows)

aoc2023/Aoc.newt

@@ -0,0 +1,19 @@
+module Aoc
+
+import Prelude
+
+nums : String → List Int
+nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
+
+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

aoc2023/Day3.newt

@@ -2,6 +2,7 @@ module Day3
 
 import Prelude
 import Node
+import Aoc
 
 pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
 pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, '  ')`
@@ -15,18 +16,6 @@ maybe def f (Just a) = f a
 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

aoc2023/Day6.newt

@@ -0,0 +1,74 @@
+module Day6
+
+import Prelude
+import Node
+import Aoc
+
+Problem : U
+Problem = List (Int × Int)
+
+pNums : String → Either String (List Int)
+pNums line =
+  let (_ :: line :: Nil) = split line ": "
+    | _ => Left "expected two parts" in
+  Right $ nums line
+
+parse : String → Either String Problem
+parse content = do
+  let (a :: b :: Nil) = split (trim content) "\n"
+    | _ => Left "expected two lines"
+  times <- pNums a
+  dists <- pNums b
+  Right (zip times dists)
+
+part1 : Problem → Int
+part1 prob = go 1 prob
+  where
+    run : Int -> Int -> Int → Int → Int
+    run time dist t count =
+      let count = if dist < t * (time - t) then count + 1 else count in
+      if time == t then count
+      else run time dist (t + 1) count
+
+    go : Int → Problem → Int
+    go acc Nil = acc
+    go acc ((time,dist) :: prob) = go (acc * run time dist 0 0) prob
+
+part2 : Int × Int → IO Unit
+part2 (time,dist) = do
+  let t = intToDouble time
+  let d = intToDouble dist
+  let x = sqrtDouble (t * t - intToDouble 4 * d)
+  let start = (t - x) / intToDouble 2
+  let stop = (t + x) / intToDouble 2
+  let s = doubleToInt $ ceilDouble start
+  let e = doubleToInt $ ceilDouble stop
+  putStrLn $ "part2 " ++ show (e - s)
+
+parse2 : String → Either String (Int × Int)
+parse2 content =
+  let (a :: b :: Nil) = split (trim content) "\n"
+    | _ => Left "too many parts" in
+  let time = stringToInt $ pack $ filter isDigit $ unpack a
+      dist = stringToInt $ pack $ filter isDigit $ unpack b
+  in Right (time, dist)
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let (Right prob) = parse text | Left err => putStrLn err
+  putStrLn $ debugStr prob
+  putStrLn $ "part1 " ++ show (part1 prob)
+  let (Right prob) = parse2 text | Left err => putStrLn err
+  part2 prob
+  -- debugLog prob
+  -- part2 prob
+
+-- 288 / 71503
+-- 1413720 / 30565288
+
+main : IO Unit
+main = do
+  run "aoc2023/day6/eg.txt"
+  run "aoc2023/day6/input.txt"

aoc2023/Prelude.newt

@@ -187,10 +187,13 @@ infixl 7 _+_
 class Add a where
   _+_ : a → a → a
 
-infixl 8 _*_
+infixl 8 _*_ _/_
 class Mul a where
   _*_ : a → a → a
 
+class Div a where
+  _/_ : a → a → a
+
 instance Add Nat where
   Z + m = m
   S n + m = S (n + m)
@@ -535,3 +538,29 @@ elem v (x :: xs) = if v == x then True else elem v xs
 -- sum : ∀ a. {{Add a}} → List a → a
 -- sum xs = foldl _+_
 pfunc trace uses (debugStr) : ∀ a. String -> a -> a := `(_, msg, a) => { console.log(msg,debugStr(_,a)); return a }`
+
+mapMaybe : ∀ a b. (a → Maybe b) → List a → List b
+mapMaybe f Nil = Nil
+mapMaybe f (x :: xs) = case f x of
+  Just y => y :: mapMaybe f xs
+  Nothing => mapMaybe f xs
+
+zip : ∀ a b. List a → List b → List (a × b)
+zip (x :: xs) (y :: ys) = (x,y) :: zip xs ys
+zip _ _ = Nil
+
+-- TODO add double literals
+ptype Double
+pfunc intToDouble : Int → Double := `(x) => x`
+pfunc doubleToInt : Double → Int := `(x) => x`
+pfunc addDouble : Double → Double → Double := `(x,y) => x + y`
+pfunc subDouble : Double → Double → Double := `(x,y) => x - y`
+pfunc mulDouble : Double → Double → Double := `(x,y) => x * y`
+pfunc divDouble : Double → Double → Double := `(x,y) => x / y`
+pfunc sqrtDouble : Double → Double := `(x) => Math.sqrt(x)`
+pfunc ceilDouble : Double → Double := `(x) => Math.ceil(x)`
+
+instance Add Double where x + y = addDouble x y
+instance Sub Double where x - y = subDouble x y
+instance Mul Double where x * y = mulDouble x y
+instance Div Double where x / y = divDouble x y

aoc2023/day6/eg.txt

@@ -0,0 +1,2 @@
+Time:      7  15   30
+Distance:  9  40  200

playground/samples/Prelude.newt

@@ -187,10 +187,13 @@ infixl 7 _+_
 class Add a where
   _+_ : a → a → a
 
-infixl 8 _*_
+infixl 8 _*_ _/_
 class Mul a where
   _*_ : a → a → a
 
+class Div a where
+  _/_ : a → a → a
+
 instance Add Nat where
   Z + m = m
   S n + m = S (n + m)
@@ -535,3 +538,29 @@ elem v (x :: xs) = if v == x then True else elem v xs
 -- sum : ∀ a. {{Add a}} → List a → a
 -- sum xs = foldl _+_
 pfunc trace uses (debugStr) : ∀ a. String -> a -> a := `(_, msg, a) => { console.log(msg,debugStr(_,a)); return a }`
+
+mapMaybe : ∀ a b. (a → Maybe b) → List a → List b
+mapMaybe f Nil = Nil
+mapMaybe f (x :: xs) = case f x of
+  Just y => y :: mapMaybe f xs
+  Nothing => mapMaybe f xs
+
+zip : ∀ a b. List a → List b → List (a × b)
+zip (x :: xs) (y :: ys) = (x,y) :: zip xs ys
+zip _ _ = Nil
+
+-- TODO add double literals
+ptype Double
+pfunc intToDouble : Int → Double := `(x) => x`
+pfunc doubleToInt : Double → Int := `(x) => x`
+pfunc addDouble : Double → Double → Double := `(x,y) => x + y`
+pfunc subDouble : Double → Double → Double := `(x,y) => x - y`
+pfunc mulDouble : Double → Double → Double := `(x,y) => x * y`
+pfunc divDouble : Double → Double → Double := `(x,y) => x / y`
+pfunc sqrtDouble : Double → Double := `(x) => Math.sqrt(x)`
+pfunc ceilDouble : Double → Double := `(x) => Math.ceil(x)`
+
+instance Add Double where x + y = addDouble x y
+instance Sub Double where x - y = subDouble x y
+instance Mul Double where x * y = mulDouble x y
+instance Div Double where x / y = divDouble x y

port/Prelude.newt

@@ -1,5 +1,7 @@
 module Prelude
 
+id : ∀ a. a → a
+id x = x
 
 data Bool : U where
   True False : Bool
@@ -15,22 +17,35 @@ _||_ : 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
 
+infixl 6 _/=_
+_/=_ : ∀ a. {{Eq a}} → a → a → Bool
+a /= b = not (a == b)
+
 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 : U} -> a -> Maybe a
+  Just : ∀ a. a -> Maybe a
-  Nothing : {a : U} -> Maybe a
+  Nothing : ∀ a. Maybe a
 
 fromMaybe : ∀ a. a → Maybe a → a
 fromMaybe a Nothing = a
@@ -45,6 +60,10 @@ 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
@@ -57,19 +76,23 @@ _<>>_ : ∀ 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
+-- This is now handled by the parser, and LHS becomes `f a`.
--- inference? Figure out why.
+-- infixr 0 _$_
--- Currently very noisy in generated code (if nothing else, optimize it out?)
+-- _$_ : ∀ a b. (a -> b) -> a -> b
-infixr 0 _$_
+-- f $ a = f a
-_$_ : ∀ 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
 
-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
 
@@ -78,6 +101,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
@@ -91,6 +116,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 _≡_
@@ -133,6 +161,14 @@ class Applicative (f : U → U) where
   return : {0 a} → a → f a
   _<*>_ : {0 a b} -> f (a → b) → f a → f b
 
+class Traversable (t : U → U) where
+  traverse : {f : U → U} → {{appf : Applicative f}} → {a : U} → {b : U} → (a → f b) → t a → f (t b)
+
+instance Applicative Maybe where
+  return a = Just a
+  Nothing <*> _ = Nothing
+  Just f <*> fa = f <$> fa
+
 infixr 2 _<|>_
 class Alternative (m : U → U) where
   _<|>_ : {0 a} → m a → m a → m a
@@ -151,10 +187,13 @@ infixl 7 _+_
 class Add a where
   _+_ : a → a → a
 
-infixl 8 _*_
+infixl 8 _*_ _/_
 class Mul a where
   _*_ : a → a → a
 
+class Div a where
+  _/_ : a → a → a
+
 instance Add Nat where
   Z + m = m
   S n + m = S (n + m)
@@ -163,7 +202,6 @@ instance Mul Nat where
   Z * _ = Z
   S n * m = m + n * m
 
-
 infixl 7 _-_
 class Sub a where
   _-_ : a → a → a
@@ -181,17 +219,21 @@ ptype String
 ptype Int
 ptype Char
 
--- probably want to switch to Int or implement magic Nat
-pfunc length : String → Nat := `(s) => {
-  let rval = Z
-  for (let i = 0; i < s.length; s++) rval = S(rval)
-  return rval
-}`
-
 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
 
@@ -211,7 +253,7 @@ 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 : {0 a} → Array a → List a := `(a,arr) => {
+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)
@@ -228,11 +270,11 @@ 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) => {
+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_(List(String), p, rval) })
+  parts.forEach(p => { rval = _$3A$3A_(undefined, p, rval) })
   return rval
 }`
 
@@ -266,12 +308,43 @@ instance Monad IO where
     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
+
+
+
+-- This is traverse, but we haven't defined Traversable yet
+mapA : ∀ m. {{Applicative m}} {0 a b} → (a → m b) → List a → m (List b)
+mapA f Nil = return Nil
+mapA f (x :: xs) = return _::_ <*> f x <*> mapA f xs
+
+
+mapM : ∀ m. {{Monad m}} {0 a b} → (a → m b) → List a → m (List b)
+mapM f Nil = pure Nil
+mapM f (x :: xs) = do
+  b <- f x
+  bs <- mapM f xs
+  pure (b :: bs)
+
 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)
@@ -293,9 +366,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)
@@ -303,6 +373,45 @@ pfunc unpack : String -> List Char
     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
@@ -336,3 +445,122 @@ 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
+
+
+instance ∀ a. Applicative (Either a) where
+  return b = Right b
+  Right x <*> Right y = Right (x y)
+  Left x <*> _ = Left x
+  Right x <*> Left y = Left y
+
+instance ∀ a. Monad (Either a) where
+  pure x = Right x
+  bind (Right x) mab = mab x
+  bind (Left x) mab = Left x
+
+instance Monad Maybe where
+  pure x = Just x
+  bind Nothing mab = Nothing
+  bind (Just x) mab = mab x
+
+
+elem : ∀ a. {{Eq a}} → a → List a → Bool
+elem v Nil = False
+elem v (x :: xs) = if v == x then True else elem v xs
+
+-- TODO no empty value on my `Add`, I need a group..
+-- sum : ∀ a. {{Add a}} → List a → a
+-- sum xs = foldl _+_
+pfunc trace uses (debugStr) : ∀ a. String -> a -> a := `(_, msg, a) => { console.log(msg,debugStr(_,a)); return a }`
+
+mapMaybe : ∀ a b. (a → Maybe b) → List a → List b
+mapMaybe f Nil = Nil
+mapMaybe f (x :: xs) = case f x of
+  Just y => y :: mapMaybe f xs
+  Nothing => mapMaybe f xs
+
+zip : ∀ a b. List a → List b → List (a × b)
+zip (x :: xs) (y :: ys) = (x,y) :: zip xs ys
+zip _ _ = Nil
+
+-- TODO add double literals
+ptype Double
+pfunc intToDouble : Int → Double := `(x) => x`
+pfunc doubleToInt : Double → Int := `(x) => x`
+pfunc addDouble : Double → Double → Double := `(x,y) => x + y`
+pfunc subDouble : Double → Double → Double := `(x,y) => x - y`
+pfunc mulDouble : Double → Double → Double := `(x,y) => x * y`
+pfunc divDouble : Double → Double → Double := `(x,y) => x / y`
+pfunc sqrtDouble : Double → Double := `(x) => Math.sqrt(x)`
+pfunc ceilDouble : Double → Double := `(x) => Math.ceil(x)`
+
+instance Add Double where x + y = addDouble x y
+instance Sub Double where x - y = subDouble x y
+instance Mul Double where x * y = mulDouble x y
+instance Div Double where x / y = divDouble x y

src/Lib/Tokenizer.idr

@@ -11,7 +11,7 @@ keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
             "∀", "forall",
             "class", "instance",
             "if", "then", "else",
-            "$", "λ",
+            "$", "λ", "?",
              "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"]
 
 checkKW : String -> Token Kind
@@ -27,7 +27,7 @@ identMore : Lexer
 identMore = alphaNum <|> exact "'" <|> exact "_"
 
 singleton : Lexer
-singleton = oneOf "()\\{}[],?."
+singleton = oneOf "()\\{}[],."
 
 quo : Recognise True
 quo = is '"'