Async, HasIO, and get aoc examples working in web

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"
+  )

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"
+  )

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)`

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

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

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')
         </script>
     </head>
     <body>
-        
+
     </body>
-</html>
+</html>