From d41558c21968a8de79fec9d4ca0fd9d9f8cf4585 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 31 Oct 2024 22:17:22 -0700
Subject: [PATCH] thinking about IO

---
 TODO.md           |  1 +
 newt/IO.newt      | 30 ++++++++++++++++++++++--------
 newt/Prelude.newt | 24 ++++++++++++++++++++++++
 src/Main.idr      |  4 +++-
 4 files changed, 50 insertions(+), 9 deletions(-)

diff --git a/TODO.md b/TODO.md
index 8b4158b..e106df1 100644
--- a/TODO.md
+++ b/TODO.md
@@ -33,6 +33,7 @@
 - [x] implicit patterns
 - [x] operators
 - [x] pair syntax (via comma operator)
+- [ ] `data` sugar: `data Maybe a = Nothing | Just a`
 - [x] matching on operators
   - [x] top level
   - [x] case statements
diff --git a/newt/IO.newt b/newt/IO.newt
index fe1f0cd..61437fb 100644
--- a/newt/IO.newt
+++ b/newt/IO.newt
@@ -13,18 +13,32 @@ data IORes : U -> U where
 IO : U -> U
 IO a = World -> IORes a
 
+-- TODO - if I move w to the left, I get "extra pattern variable"
+-- because I'm not looking instide the IO b type, probably should force it.
 iobind : {a b : U} -> IO a -> (a -> IO b) -> IO b
-iobind ma mab w = case ma w of
+iobind ma mab = \ w => case ma w of
   (MkIORes a w) => mab a w
 
-_>>=_ : {a b : U} -> IO a -> (a -> IO b) -> IO b
-_>>=_ = iobind
+iopure : {a : U} -> a -> IO a
+iopure a = \ w => MkIORes a w
 
-infixr 2 _>>=_
-infixr 2 _>>_
+IOMonad : Monad IO
+IOMonad = MkMonad iobind iopure
 
--- FIXME - bad parse error for lambda without the parens
+data Unit : U where
+  MkUnit : Unit
 
-_>>_ :  {a b : U} -> IO a -> IO b -> IO b
-_>>_ ma mb = ma >>= (\ _ => mb)
+ptype String
 
+pfunc log : String -> IO Unit := "(s) => (w) => MkIORes(console.log(s),w)"
+
+-- this version wraps with IO, but leaves this plog in scope
+pfunc plog : String -> Unit := "(s) => console.log(s)"
+
+log2 : String -> IO Unit
+log2 s = pure $ plog s
+
+main : IO Unit
+main = do
+  log "woot"
+  log2 "line 2"
diff --git a/newt/Prelude.newt b/newt/Prelude.newt
index 125f4a5..9769974 100644
--- a/newt/Prelude.newt
+++ b/newt/Prelude.newt
@@ -20,3 +20,27 @@ infixr 0 _$_
 _$_ : {a b : U} -> (a -> b) -> a -> b
 f $ a = f a
 
+
+-- Monad
+
+-- TODO stack with Applicative, etc?
+
+data Monad : (U -> U) -> U where
+  MkMonad : { M : U -> U } ->
+            (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
+            (pure : {A : U} -> A -> M A) ->
+            Monad M
+
+infixl 1 _>>=_ _>>_
+_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
+_>>=_ {a} {b} {m} {{MkMonad bind' _}}  ma amb = bind' {a} {b} ma amb
+
+_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
+ma >> mb = mb
+
+pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
+pure {_} {_} {{MkMonad _ pure'}} a = pure' a
+
+-- IO
+
+
diff --git a/src/Main.idr b/src/Main.idr
index 55f246a..aa280e0 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -43,7 +43,9 @@ writeSource fn = do
   docs <- compile
   let src = unlines $ ["#!/usr/bin/env node"]
         ++ map (render 90) docs
-        ++ [ "main();" ]
+        ++ [ "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })"
+           , "main();"
+           ]
   Right _ <- writeFile fn src
     | Left err => fail (show err)
   Right _ <- chmodRaw fn 493 | Left err => fail (show err)