From 6f954b1183fb4fb36b3bc1c26a6bc26baee2ad55 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 25 Nov 2024 16:25:05 -0800 Subject: [PATCH] tweaks to playground files --- TODO.md | 2 ++ playground/samples/Day1.newt | 31 ++++++++++++++------------- playground/samples/Day2.newt | 30 ++++++++++++++------------ playground/samples/Hello.newt | 40 ++--------------------------------- 4 files changed, 36 insertions(+), 67 deletions(-) diff --git a/TODO.md b/TODO.md index e36d00f..6683dc7 100644 --- a/TODO.md +++ b/TODO.md @@ -1,6 +1,8 @@ ## TODO +- [ ] add filenames to FC +- [ ] add namespaces - [ ] imported files leak info messages everywhere - For now, take the start ix for the file and report at end starting there - [ ] update node shim to include idris2-playground changes diff --git a/playground/samples/Day1.newt b/playground/samples/Day1.newt index 7fba860..554f5fa 100644 --- a/playground/samples/Day1.newt +++ b/playground/samples/Day1.newt @@ -51,20 +51,21 @@ part1 text digits = #check digits1 ∘ unpack : String -> List Int -runFile : String -> IO Unit -runFile fn = do - text <- readFile fn - putStrLn fn - putStrLn "part1" - putStrLn $ show (part1 text (digits1 ∘ unpack)) - putStrLn "part2" - putStrLn $ show (part1 text (digits2 ∘ unpack)) - putStrLn "" +-- readFile not in browser / playground +-- runFile : String -> IO Unit +-- runFile fn = do +-- text <- readFile 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 = do - runFile "aoc2023/day1/eg.txt" - runFile "aoc2023/day1/eg2.txt" - runFile "aoc2023/day1/input.txt" +-- -- Argument is a hack to keep it from running at startup. Need to add IO +-- main : IO Unit +-- main = do +-- runFile "aoc2023/day1/eg.txt" +-- runFile "aoc2023/day1/eg2.txt" +-- runFile "aoc2023/day1/input.txt" diff --git a/playground/samples/Day2.newt b/playground/samples/Day2.newt index f5c7028..45f9e76 100644 --- a/playground/samples/Day2.newt +++ b/playground/samples/Day2.newt @@ -82,18 +82,20 @@ part2 (MkGame n parts :: rest) = case foldl maxd (0,0,0) parts of (a,b,c) => a * b * c + part2 rest -run : String -> IO Unit -run fn = do - text <- readFile fn - case mapM parseGame (split (trim text) "\n") of - Left err => putStrLn $ "fail " ++ err - Right games => do - putStrLn "part1" - printLn (part1 games) - putStrLn "part2" - printLn (part2 games) +-- readFile not in browser / playground -main : IO Unit -main = do - run "aoc2023/day2/eg.txt" - run "aoc2023/day2/input.txt" +-- run : String -> IO Unit +-- run fn = do +-- text <- readFile fn +-- case mapM 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 = do +-- run "aoc2023/day2/eg.txt" +-- run "aoc2023/day2/input.txt" diff --git a/playground/samples/Hello.newt b/playground/samples/Hello.newt index 5899e4f..7648652 100644 --- a/playground/samples/Hello.newt +++ b/playground/samples/Hello.newt @@ -1,42 +1,6 @@ -module Main +module Hello --- Monad - -class Monad (m : U → U) where - bind : {a b} → m a → (a → m b) → m b - pure : {a} → a → m a - -infixl 1 _>>=_ _>>_ -_>>=_ : {m} {{Monad m}} {a b} -> (m a) -> (a -> m b) -> m b -ma >>= amb = bind ma amb - -_>>_ : {m} {{Monad m}} {a b} -> m a -> m b -> m b -ma >> mb = mb - --- 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 - - -data Unit : U where - MkUnit : Unit - - -instance Monad IO where - bind ma mab = \ w => case ma w of - MkIORes a w => mab a w - pure a = \ w => MkIORes a w - -ptype String -pfunc putStrLn : String -> IO Unit := "(s) => (w) => { - console.log(s) - return MkIORes(Unit,MkUnit,w) -}" +import Prelude main : IO Unit main = do