diff --git a/TODO.md b/TODO.md index 2dd58f5..fce8645 100644 --- a/TODO.md +++ b/TODO.md @@ -1,10 +1,12 @@ ## TODO +- [x] Put worker in iframe on safari - [ ] if we're staying with this version of auto, we might need to list candidates and why they're rejected. e.g. I had a bifunctor fail to solve because the right answer unblocked a Foo vs IO Foo mismatch - [ ] literals for double - [ ] default failing case for constructor matching - [ ] Add icit to Lam (see `check` for details) +- [ ] add jump to definition magic to vscode extension - [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it. - [x] deconstructing `let` (and do arrows) - [x] Fix string printing to be js instead of weird Idris strings diff --git a/aoc2023/Prelude.newt b/aoc2023/Prelude.newt index 299c1d3..683dab1 100644 --- a/aoc2023/Prelude.newt +++ b/aoc2023/Prelude.newt @@ -114,7 +114,7 @@ _>>=_ : {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 +ma >> mb = ma >>= (\ _ => mb) join : ∀ m. {{Monad m}} {0 a} → m (m a) → m a join mma = mma >>= id @@ -622,3 +622,8 @@ isNothing _ = False instance Bifunctor _×_ where bimap f g (a,b) = (f a, g b) +instance Functor IO where + map f a = bind a $ \ a => pure (f a) + +uncurry : ∀ a b c. (a -> b -> c) -> (a × b) -> c +uncurry f (a,b) = f a b diff --git a/aoc2024/Day3.newt b/aoc2024/Day3.newt index d481107..fd5047b 100644 --- a/aoc2024/Day3.newt +++ b/aoc2024/Day3.newt @@ -4,17 +4,12 @@ import Prelude import Node import Aoc -uncurry : ∀ a b c. (a -> b -> c) -> (a × b) -> c -uncurry f (a,b) = f a b - Parser : U → U Parser a = List Char → Maybe (a × List Char) instance Monad Parser where pure a = \ cs => Just (a, cs) - bind ma mab = \ cs => case ma cs of - Nothing => Nothing - Just (a,cs) => mab a cs + bind ma mab = \ cs => ma cs >>= uncurry mab instance Alternative Parser where pa <|> pb = \ cs => case pa cs of diff --git a/aoc2024/Node.newt b/aoc2024/Node.newt new file mode 120000 index 0000000..66718c9 --- /dev/null +++ b/aoc2024/Node.newt @@ -0,0 +1 @@ +../aoc2023/Node.newt \ No newline at end of file diff --git a/aoc2024/Prelude.newt b/aoc2024/Prelude.newt new file mode 120000 index 0000000..faf6e14 --- /dev/null +++ b/aoc2024/Prelude.newt @@ -0,0 +1 @@ +../aoc2023/Prelude.newt \ No newline at end of file