From 6e8727c7846803e73cdd46cd57db2abff17f6d1c Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 18 Dec 2024 14:00:59 -0800 Subject: [PATCH] try to fix missing Aoc.newt in playground --- TODO.md | 2 +- playground/samples/aoc2023/Day1.newt | 71 --- playground/samples/aoc2023/Day2.newt | 92 --- playground/samples/aoc2023/Day3.newt | 115 ---- playground/samples/aoc2023/Day4.newt | 67 --- playground/samples/aoc2023/Node.newt | 7 - playground/samples/aoc2023/Prelude.newt | 725 ------------------------ playground/samples/aoc2023/Web.newt | 26 - playground/samples/aoc2023/day1/eg.txt | 5 - playground/samples/aoc2023/day1/eg2.txt | 7 - playground/samples/aoc2023/day2/eg.txt | 5 - playground/samples/aoc2023/day3/eg.txt | 10 - playground/samples/aoc2023/day4/eg.txt | 6 - playground/samples/aoc2024/Aoc.newt | 2 +- 14 files changed, 2 insertions(+), 1138 deletions(-) delete mode 100644 playground/samples/aoc2023/Day1.newt delete mode 100644 playground/samples/aoc2023/Day2.newt delete mode 100644 playground/samples/aoc2023/Day3.newt delete mode 100644 playground/samples/aoc2023/Day4.newt delete mode 100644 playground/samples/aoc2023/Node.newt delete mode 100644 playground/samples/aoc2023/Prelude.newt delete mode 100644 playground/samples/aoc2023/Web.newt delete mode 100644 playground/samples/aoc2023/day1/eg.txt delete mode 100644 playground/samples/aoc2023/day1/eg2.txt delete mode 100644 playground/samples/aoc2023/day2/eg.txt delete mode 100644 playground/samples/aoc2023/day3/eg.txt delete mode 100644 playground/samples/aoc2023/day4/eg.txt diff --git a/TODO.md b/TODO.md index 88291b7..5bc8985 100644 --- a/TODO.md +++ b/TODO.md @@ -7,7 +7,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [x] for parse error, seek to col 0 token and process next decl - [ ] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality) - [ ] Keep a `compare` function on `SortedMap` (like lean) -- [ ] keymap for monaco +- [x] keymap for monaco - [x] SortedMap.newt issue in `where` - [x] fix "insufficient patterns", wire in M or Either String - [x] Matching _,_ when Maybe is expected should be an error diff --git a/playground/samples/aoc2023/Day1.newt b/playground/samples/aoc2023/Day1.newt deleted file mode 100644 index becd768..0000000 --- a/playground/samples/aoc2023/Day1.newt +++ /dev/null @@ -1,71 +0,0 @@ -module Day1 -/- - I ported a couple of Advent of Code 2023 solutions from Lean4 - as an early test case. Here I've adapted them to the web playground - by replacing `readFile` with an async `fetchText`. --/ - - -import Web - -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 - --- 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 - -#check digits1 ∘ unpack : String -> List Int - -runFile : String -> Async Unit -runFile fn = do - text <- fetchText fn - putStrLn fn - putStrLn "part1" - putStrLn $ show (part1 text (digits1 ∘ unpack)) - putStrLn "part2" - putStrLn $ show (part1 text (digits2 ∘ unpack)) - putStrLn "" - --- Argument is a hack to keep it from running at startup. Need to add IO -main : IO Unit -main = runAsync (do - runFile "aoc2023/day1/eg.txt" - runFile "aoc2023/day1/eg2.txt" - -- runFile "aoc2023/day1/input.txt" - ) diff --git a/playground/samples/aoc2023/Day2.newt b/playground/samples/aoc2023/Day2.newt deleted file mode 100644 index 7c45184..0000000 --- a/playground/samples/aoc2023/Day2.newt +++ /dev/null @@ -1,92 +0,0 @@ -module Day2 - -/- - I ported a couple of Advent of Code 2023 solutions from Lean4 - as an early test case. Here I've adapted them to the web playground - by replacing `readFile` with an async `fetchText`. --/ - -import Web - -Draw : U -Draw = Int × Int × Int - -data Game : U where - MkGame : Int -> List Draw -> Game - --- Original had class and instance... --- Add, Sub, Mul, Neg - -max : Int -> Int -> Int -max x y = case x < y of - True => y - False => x - -pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o` -pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, ' ')` -pfunc toInt : String -> Int := `s => Number(s)` - -maxd : Draw -> Draw -> Draw -maxd (a,b,c) (d,e,f) = (max a d, max b e, max c f) - -lte : Draw -> Draw -> Bool -lte (a,b,c) (d,e,f) = a <= d && b <= e && c <= f - -parseColor : String -> Either String Draw -parseColor line = case split line " " of - (n :: "red" :: Nil) => Right (toInt n,0,0) - (n :: "green" :: Nil) => Right (0,toInt n,0) - (n :: "blue" :: Nil) => Right (0,0,toInt n) - x => Left $ "Bad draw" ++ repr x - -parseDraw : String -> Either String Draw -parseDraw line = case mapM {Either String} parseColor $ split line ", " of - Right parts => Right $ foldl maxd (0,0,0) parts - Left err => Left err - -parseGame : String -> Either String Game -parseGame line = - -- Need the Idris | sugar... - case split line ": " of - -- this is splitting on the Nil instead of the a - (a :: b :: Nil) => case split a " " of - ("Game" :: ns :: Nil) => - let num = toInt ns in - case mapM {Either String} parseDraw $ split b "; " of - Right parts => Right $ MkGame num parts - Left err => Left err - _ => Left "No Game" - _ => Left $ "No colon in " ++ line - -part1 : List Game -> Int -part1 Nil = 0 -part1 (MkGame n parts :: rest) = - let total = foldl maxd (0,0,0) parts in - case lte total (12,13,14) of - True => n + part1 rest - False => part1 rest - -part2 : List Game -> Int -part2 Nil = 0 -part2 (MkGame n parts :: rest) = - case foldl maxd (0,0,0) parts of - (a,b,c) => a * b * c + part2 rest - --- readFile not in browser / playground - -run : String -> Async Unit -run fn = do - text <- fetchText fn - case mapM {Either String} parseGame (split (trim text) "\n") of - Left err => putStrLn $ "fail " ++ err - Right games => do - putStrLn "part1" - printLn (part1 games) - putStrLn "part2" - printLn (part2 games) - -main : IO Unit -main = runAsync (do - run "aoc2023/day2/eg.txt" - run "aoc2023/day2/input.txt" - ) diff --git a/playground/samples/aoc2023/Day3.newt b/playground/samples/aoc2023/Day3.newt deleted file mode 100644 index 53d0e9f..0000000 --- a/playground/samples/aoc2023/Day3.newt +++ /dev/null @@ -1,115 +0,0 @@ -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, ' ')` - - -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 case span isDigit (c :: cs) of - (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" - diff --git a/playground/samples/aoc2023/Day4.newt b/playground/samples/aoc2023/Day4.newt deleted file mode 100644 index 534a8d7..0000000 --- a/playground/samples/aoc2023/Day4.newt +++ /dev/null @@ -1,67 +0,0 @@ -module Day4 - -import Prelude -import Node - -Round : U -Round = List Int × List Int - -parseRound : String → Maybe Round -parseRound s = - case split s ": " of - (a :: b :: Nil) => case split b " | " of - (l :: r :: Nil) => Just (nums l, nums r) - _ => Nothing - _ => Nothing - where - -- Nat or Int here? - nums : String → List Int - -- catch - split returns empty strings that become zeros - nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " " - -parse : String -> Maybe (List Round) -parse s = mapM parseRound (split (trim s) "\n") - -pfunc pow : Int → Int → Int := `(x,y) => x ** y` - -part1 : List Round → Int -part1 rounds = foldl _+_ 0 $ map score rounds - where - -- TODO we'll keep the math in Int land until we have magic Nat - score : Round → Int - score (a,b) = let count = natToInt $ length $ filter (\ n => elem n b) a - in if count == 0 then 0 else pow 2 (count - 1) - -part2 : List Round → Int -part2 rounds = go 0 $ map (_,_ 1) rounds - where - mark : Int -> Nat → List (Int × Round) → List (Int × Round) - mark _ _ Nil = Nil - mark v Z rounds = rounds - mark v (S k) ((cnt, round) :: rounds) = (cnt + v, round) :: mark v k rounds - - go : Int → List (Int × Round) → Int - go acc Nil = acc - go acc ((cnt, a, b) :: rounds) = - let n = length $ filter (\ n => elem n b) a - in go (acc + cnt) $ mark cnt n rounds - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - - case parse text of - Nothing => putStrLn "fail" - Just cards => do - putStrLn "part1" - printLn (part1 cards) - putStrLn "part2" - printLn (part2 cards) - --- 13/30 --- 25004/14427616 -main : IO Unit -main = do - run "aoc2023/day4/eg.txt" - run "aoc2023/day4/input.txt" diff --git a/playground/samples/aoc2023/Node.newt b/playground/samples/aoc2023/Node.newt deleted file mode 100644 index 6077b96..0000000 --- a/playground/samples/aoc2023/Node.newt +++ /dev/null @@ -1,7 +0,0 @@ -module Node - -import Prelude - -pfunc fs : JSObject := `require('fs')` -pfunc getArgs : List String := `arrayToList(String, process.argv)` -pfunc readFile uses (fs) : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)` diff --git a/playground/samples/aoc2023/Prelude.newt b/playground/samples/aoc2023/Prelude.newt deleted file mode 100644 index ed156b8..0000000 --- a/playground/samples/aoc2023/Prelude.newt +++ /dev/null @@ -1,725 +0,0 @@ -module Prelude - -id : ∀ a. a → a -id x = x - -the : (a : U) → a → a -the _ a = a - -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 - -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. 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 - --- 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 - -fst : ∀ a b. a × b → a -fst (a,b) = a - -snd : ∀ a b. a × b → b -snd (a,b) = 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 _>>=_ _>>_ -_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b -ma >>= amb = bind ma amb - -_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b -ma >> mb = ma >>= (\ _ => mb) - -join : ∀ m a. {{Monad m}} → 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 - -class Traversable (t : U → U) where - traverse : ∀ f a b. {{Applicative f}} → (a → f b) → t a → f (t b) - -instance Traversable List where - traverse f Nil = return Nil - traverse f (x :: xs) = return _::_ <*> f x <*> traverse f xs - -for : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f (t b) -for stuff fun = traverse fun stuff - -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 - -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 - -class Div 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` -pfunc jsLT 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 intToNat uses (Z S) : Int -> Nat := `(n) => { - let rval = Z - for (;n>0;n--) rval = S(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. 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 x = \ w => MkIORes x 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 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 uses (Nil _::_) : String -> List Char - := `(s) => { - let acc = Nil(undefined) - for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(undefined, 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 === undefined) return "_" - if (obj.tag === '_,_') { - let rval = '(' - while (obj?.tag === '_,_') { - rval += go(obj.h2) + ', ' - obj = obj.h3 - } - return rval + go(obj) + ')' - } - if (obj?.tag === '_::_' || obj?.tag === 'Nil') { - let stuff = listToArray(undefined,obj) - return '['+(stuff.map(go).join(', '))+']' - } - if (obj instanceof Array) { - return 'io['+(obj.map(go).join(', '))+']' - } - if (obj?.tag === 'S' || obj?.tag === 'Z') { - 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) -}` - -debugLog : ∀ a. a → IO Unit -debugLog a = putStrLn (debugStr a) - -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 divInt : Int → Int → Int := `(x,y) => x / y|0` -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 Div Int where - x / y = divInt 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 - - -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 - -ptype IOArray : U → U - -pfunc newArray uses (MkIORes) : ∀ a. Int → a → IO (IOArray a) := - `(_, n, v) => (w) => MkIORes(undefined,Array(n).fill(v),w)` -pfunc arrayGet : ∀ a. IOArray a → Int → IO a := `(_, arr, ix) => w => MkIORes(undefined, arr[ix], w)` -pfunc arraySet uses (MkUnit) : ∀ a. IOArray a → Int → a → IO Unit := `(_, arr, ix, v) => w => { - arr[ix] = v - return MkIORes(undefined, MkUnit, w) -}` -pfunc arraySize uses (MkIORes) : ∀ a. IOArray a → IO Int := `(_, arr) => w => MkIORes(undefined, arr.length, w)` - -pfunc ioArrayToList uses (Nil _::_ MkIORes) : {0 a} → IOArray a → IO (List a) := `(a,arr) => w => { - let rval = Nil(a) - for (let i = arr.length - 1;i >= 0; i--) { - rval = _$3A$3A_(a, arr[i], rval) - } - return MkIORes(undefined, rval, w) -}` - -pfunc listToIOArray uses (MkIORes) : {0 a} → List a → IO (Array a) := `(a,list) => w => { - let rval = [] - while (list.tag === '_::_') { - rval.push(list.h1) - list = list.h2 - } - return MkIORes(undefined,rval,w) -}` - -class Cast a b where - cast : a → b - -instance Cast Nat Int where - cast = natToInt - -instance Cast Int Double where - cast = intToDouble - -instance Applicative IO where - return a = \ w => MkIORes a w - f <*> a = \ w => - let (MkIORes f w) = trace "fw" $ f w in - let (MkIORes a w) = trace "aw" $ a w in - MkIORes (f a) w - -class Bifunctor (f : U → U → U) where - bimap : ∀ a b c d. (a → c) → (b → d) → f a b → f c d - -mapFst : ∀ a b c f. {{Bifunctor f}} → (a → c) → f a b → f c b -mapFst f ab = bimap f id ab - -mapSnd : ∀ a b c f. {{Bifunctor f}} → (b → c) → f a b → f a c -mapSnd f ab = bimap id f ab - -isNothing : ∀ a. Maybe a → Bool -isNothing Nothing = True -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 - --- TODO Idris has a tail recursive version of this -instance Applicative List where - return a = a :: Nil - Nil <*> _ = Nil - fs <*> ys = join $ map (\ f => map f ys) fs - -tail : ∀ a. List a → List a -tail Nil = Nil -tail (x :: xs) = xs - --- - -infixl 6 _<_ _<=_ -class Ord a where - -- isEq : Eq a - _<_ : a → a → Bool - -_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool -a <= b = a == b || a < b - - -search : ∀ cl. {{cl}} -> cl -search {{x}} = x - -instance Ord Nat where - -- isEq = search - _ < Z = False - Z < S _ = True - S n < S m = n < m - - -instance Ord Int where - -- isEq = ? - x < y = ltInt x y - -instance Ord Char where - x < y = jsLT x y - --- foo : ∀ a. {{Ord a}} -> a -> Bool --- foo a = a == a - - -flip : ∀ a b c. (a → b → c) → (b → a → c) -flip f b a = f a b - -partition : ∀ a. (a → Bool) → List a → List a × List a -partition {a} pred xs = go xs Nil Nil - where - go : List a → List a → List a → List a × List a - go Nil as bs = (as, bs) - go (x :: xs) as bs = if pred x - then go xs (x :: as) bs - else go xs as (x :: bs) - --- probably not super efficient, but it works -qsort : ∀ a. (a → a → Bool) → List a → List a -qsort lt Nil = Nil -qsort lt (x :: xs) = qsort lt (filter (λ y => not $ lt x y) xs) ++ x :: qsort lt (filter (lt x) xs) - -ordNub : ∀ a. {{Eq a}} {{Ord a}} -> List a -> List a -ordNub {a} {{ordA}} xs = go $ qsort _<_ xs - where - go : List a → List a - go (a :: b :: xs) = if a == b then go (a :: xs) else a :: go (b :: xs) - go t = t - -ite : ∀ a. Bool → a → a → a -ite c t e = if c then t else e - -instance Ord String where - a < b = jsLT a b - -instance Cast Int Nat where - cast n = intToNat n diff --git a/playground/samples/aoc2023/Web.newt b/playground/samples/aoc2023/Web.newt deleted file mode 100644 index efba02d..0000000 --- a/playground/samples/aoc2023/Web.newt +++ /dev/null @@ -1,26 +0,0 @@ -module Web - -import Prelude - -ptype Async : U -> U -pfunc resolve : ∀ a. a -> Async a := `(_, a) => Promise.resolve(a)` -pfunc andThen : ∀ a b. Async a -> (a -> Async b) -> Async b := `(A,B,a,ab) => a.then(ab)` -pfunc reject : ∀ a. String -> Async a := `(_, msg) => Promise.reject(msg)` - -instance Monad Async where - bind = andThen - pure = resolve - --- It'd be nice to be able to declare operators and JS "projections" -pfunc fetchText : String -> Async String := `async (url) => { - let response = await fetch(url) - return response.text() -}` - -pfunc liftAsync : ∀ a. IO a -> Async a := `(_, a) => Promise.resolve(a(undefined).h0)` - -instance HasIO Async where - liftIO = liftAsync - -runAsync : ∀ a. Async a -> IO Unit -runAsync foo = pure MkUnit diff --git a/playground/samples/aoc2023/day1/eg.txt b/playground/samples/aoc2023/day1/eg.txt deleted file mode 100644 index 4cba7d0..0000000 --- a/playground/samples/aoc2023/day1/eg.txt +++ /dev/null @@ -1,5 +0,0 @@ -1abc2 -pqr3stu8vwx -a1b2c3d4e5f -treb7uchet - diff --git a/playground/samples/aoc2023/day1/eg2.txt b/playground/samples/aoc2023/day1/eg2.txt deleted file mode 100644 index 41aa89c..0000000 --- a/playground/samples/aoc2023/day1/eg2.txt +++ /dev/null @@ -1,7 +0,0 @@ -two1nine -eightwothree -abcone2threexyz -xtwone3four -4nineeightseven2 -zoneight234 -7pqrstsixteen diff --git a/playground/samples/aoc2023/day2/eg.txt b/playground/samples/aoc2023/day2/eg.txt deleted file mode 100644 index 295c36d..0000000 --- a/playground/samples/aoc2023/day2/eg.txt +++ /dev/null @@ -1,5 +0,0 @@ -Game 1: 3 blue, 4 red; 1 red, 2 green, 6 blue; 2 green -Game 2: 1 blue, 2 green; 3 green, 4 blue, 1 red; 1 green, 1 blue -Game 3: 8 green, 6 blue, 20 red; 5 blue, 4 red, 13 green; 5 green, 1 red -Game 4: 1 green, 3 red, 6 blue; 3 green, 6 red; 3 green, 15 blue, 14 red -Game 5: 6 red, 1 blue, 3 green; 2 blue, 1 red, 2 green diff --git a/playground/samples/aoc2023/day3/eg.txt b/playground/samples/aoc2023/day3/eg.txt deleted file mode 100644 index b20187f..0000000 --- a/playground/samples/aoc2023/day3/eg.txt +++ /dev/null @@ -1,10 +0,0 @@ -467..114.. -...*...... -..35..633. -......#... -617*...... -.....+.58. -..592..... -......755. -...$.*.... -.664.598.. diff --git a/playground/samples/aoc2023/day4/eg.txt b/playground/samples/aoc2023/day4/eg.txt deleted file mode 100644 index 9bdb874..0000000 --- a/playground/samples/aoc2023/day4/eg.txt +++ /dev/null @@ -1,6 +0,0 @@ -Card 1: 41 48 83 86 17 | 83 86 6 31 17 9 48 53 -Card 2: 13 32 20 16 61 | 61 30 68 82 17 32 24 19 -Card 3: 1 21 53 59 44 | 69 82 63 72 16 21 14 1 -Card 4: 41 92 73 84 69 | 59 84 76 51 58 5 54 83 -Card 5: 87 83 26 28 32 | 88 30 70 12 93 22 82 36 -Card 6: 31 18 13 56 72 | 74 77 10 23 35 67 36 11 diff --git a/playground/samples/aoc2024/Aoc.newt b/playground/samples/aoc2024/Aoc.newt index cac5bec..61f3831 120000 --- a/playground/samples/aoc2024/Aoc.newt +++ b/playground/samples/aoc2024/Aoc.newt @@ -1 +1 @@ -../../../aoc2024/Aoc.newt \ No newline at end of file +../../../aoc2023/Aoc.newt \ No newline at end of file