From a8363c7a45ff9f37764edc340b9edf3cfce1c876 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 26 Nov 2024 20:05:25 -0800 Subject: [PATCH] Async, HasIO, and get aoc examples working in web --- playground/samples/Day1.newt | 42 ++++++++++++++++++--------------- playground/samples/Day2.newt | 37 +++++++++++++++++------------ playground/samples/Node.newt | 7 ++++++ playground/samples/Prelude.newt | 15 +++++++++--- playground/samples/Web.newt | 26 ++++++++++++++++++++ playground/samples/frame.html | 14 ++++++----- playground/src/main.ts | 4 ++++ playground/src/worker.ts | 1 + 8 files changed, 103 insertions(+), 43 deletions(-) create mode 100644 playground/samples/Node.newt create mode 100644 playground/samples/Web.newt diff --git a/playground/samples/Day1.newt b/playground/samples/Day1.newt index 554f5fa..8420e7f 100644 --- a/playground/samples/Day1.newt +++ b/playground/samples/Day1.newt @@ -1,7 +1,12 @@ --- Doesn't run in playground because it's using the node `fs` module 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 Prelude + +import Web digits1 : List Char -> List Int digits1 Nil = Nil @@ -51,21 +56,20 @@ part1 text digits = #check digits1 ∘ unpack : String -> List Int --- readFile not in browser / playground +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 "" --- 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 = runAsync (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 5ebcae8..c3930f4 100644 --- a/playground/samples/Day2.newt +++ b/playground/samples/Day2.newt @@ -1,6 +1,12 @@ module Day2 -import Prelude +/- + 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 @@ -84,18 +90,19 @@ part2 (MkGame n parts :: rest) = -- readFile not in browser / playground --- 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) +run : String -> Async Unit +run fn = do + text <- fetchText 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" +main : IO Unit +main = runAsync (do + run "aoc2023/day2/eg.txt" + run "aoc2023/day2/input.txt" + ) diff --git a/playground/samples/Node.newt b/playground/samples/Node.newt new file mode 100644 index 0000000..6077b96 --- /dev/null +++ b/playground/samples/Node.newt @@ -0,0 +1,7 @@ +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/Prelude.newt b/playground/samples/Prelude.newt index 9ac4446..f5f680d 100644 --- a/playground/samples/Prelude.newt +++ b/playground/samples/Prelude.newt @@ -266,11 +266,20 @@ instance Monad IO where MkIORes a w => mab a w pure a = \ w => MkIORes a w -pfunc putStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => { +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 @@ -322,8 +331,8 @@ instance Sub Int where instance Ord Int where x < y = ltInt x y -printLn : {a} {{Show a}} → a → IO Unit -printLn a = putStrLn $ show a +printLn : {m} {{HasIO m}} {a} {{Show a}} → a → m Unit +printLn a = putStrLn (show a) -- opaque JSObject ptype JSObject diff --git a/playground/samples/Web.newt b/playground/samples/Web.newt new file mode 100644 index 0000000..efba02d --- /dev/null +++ b/playground/samples/Web.newt @@ -0,0 +1,26 @@ +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/frame.html b/playground/samples/frame.html index 9556a3c..86c3b3c 100644 --- a/playground/samples/frame.html +++ b/playground/samples/frame.html @@ -4,7 +4,8 @@ realLog = console.log messages = [] console.log = (...args) => { - messages.push(args.join(' ')) + window.parent.postMessage({message: args.join(' ')}, '*') + // messages.push(args.join(' ')) realLog(...args) } window.addEventListener('message', (ev) => { @@ -12,18 +13,19 @@ window.addEventListener('message', (ev) => { let {cmd, src} = ev.data if (cmd === 'exec') { try { - eval(src) + window.parent.postMessage({messages: []}, '*') + eval(src) } catch (e) { console.log(e) } } - window.parent.postMessage({messages}, '*') + // window.parent.postMessage({messages}, '*') messages = [] -}) +}) realLog('IFRAME INITIALIZED') - + - \ No newline at end of file + diff --git a/playground/src/main.ts b/playground/src/main.ts index ca30725..d76dcc0 100644 --- a/playground/src/main.ts +++ b/playground/src/main.ts @@ -32,6 +32,9 @@ function runOutput() { window.onmessage = (ev) => { console.log("window got", ev.data); if (ev.data.messages) state.messages.value = ev.data.messages; + if (ev.data.message) { + state.messages.value = [...state.messages.value, ev.data.message] + } }; newtWorker.onmessage = (ev) => { @@ -213,6 +216,7 @@ const SAMPLES = [ "Lists.newt", "Day1.newt", "Day2.newt", + "Node.newt", "Prelude.newt", "TypeClass.newt", "Combinatory.newt", diff --git a/playground/src/worker.ts b/playground/src/worker.ts index ea4b326..fe8d855 100644 --- a/playground/src/worker.ts +++ b/playground/src/worker.ts @@ -119,6 +119,7 @@ process.stdout.write = (s) => { // hack for now const preload = [ "Prelude.newt", + "Web.newt", "aoc2023/day1/eg.txt", "aoc2023/day1/eg2.txt", ]