diff --git a/TODO.md b/TODO.md index 7e43f57..2b2ed4d 100644 --- a/TODO.md +++ b/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) diff --git a/aoc2023/Aoc.newt b/aoc2023/Aoc.newt new file mode 100644 index 0000000..65fc575 --- /dev/null +++ b/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 diff --git a/aoc2023/Day3.newt b/aoc2023/Day3.newt index a4566bd..f632338 100644 --- a/aoc2023/Day3.newt +++ b/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 diff --git a/aoc2023/Day6.newt b/aoc2023/Day6.newt new file mode 100644 index 0000000..30b7b9a --- /dev/null +++ b/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" diff --git a/aoc2023/Prelude.newt b/aoc2023/Prelude.newt index 170179e..631c202 100644 --- a/aoc2023/Prelude.newt +++ b/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 diff --git a/aoc2023/day6/eg.txt b/aoc2023/day6/eg.txt new file mode 100644 index 0000000..28f5ae9 --- /dev/null +++ b/aoc2023/day6/eg.txt @@ -0,0 +1,2 @@ +Time: 7 15 30 +Distance: 9 40 200 diff --git a/playground/samples/Prelude.newt b/playground/samples/Prelude.newt index 170179e..631c202 100644 --- a/playground/samples/Prelude.newt +++ b/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 diff --git a/port/Prelude.newt b/port/Prelude.newt index cfe663b..631c202 100644 --- a/port/Prelude.newt +++ b/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 - Nothing : {a : U} -> Maybe a + Just : ∀ a. a -> 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 --- 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 +-- This is now handled by the parser, and LHS becomes `f a`. +-- 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 -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 diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index 183d866..2fb5507 100644 --- a/src/Lib/Tokenizer.idr +++ b/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 '"'