From 151f678f759e6c5172523efd5c7c7a345433556f Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sun, 29 Sep 2024 22:17:51 -0700
Subject: [PATCH] Work on usable codegen

- escape js names
- executable output
- better FC in parsing
- experiment with IO
---
 TODO.md             |  2 ++
 newt/IO.newt        | 30 +++++++++++++++++++++++++++
 newt/JSLib.newt     | 17 ++++++++++++++++
 newt/Prelude.newt   | 22 ++++++++++++++++++++
 src/Lib/Compile.idr | 49 +++++++++++++++++++++++++++++++++------------
 src/Lib/Parser.idr  | 10 +++++----
 src/Main.idr        |  4 +++-
 7 files changed, 116 insertions(+), 18 deletions(-)
 create mode 100644 newt/IO.newt
 create mode 100644 newt/JSLib.newt
 create mode 100644 newt/Prelude.newt

diff --git a/TODO.md b/TODO.md
index 2937238..6d4af47 100644
--- a/TODO.md
+++ b/TODO.md
@@ -3,6 +3,7 @@
 
 I may be done with `U` - I keep typing `Type`.
 
+- [ ] Sanitize JS idents, e.g. `_+_`
 - [ ] Generate some programs that do stuff
 - [x] import
 - [ ] consider making meta application implicit in term, so its more readable when printed
@@ -48,6 +49,7 @@ I may be done with `U` - I keep typing `Type`.
 - [ ] magic tuple? (codegen as array)
 - [ ] magic newtype? (drop in codegen)
 - [ ] records / copatterns
+- [ ] vscode: syntax highlighting for String
 
 - [ ] Read Ulf Norell thesis
 
diff --git a/newt/IO.newt b/newt/IO.newt
new file mode 100644
index 0000000..fe1f0cd
--- /dev/null
+++ b/newt/IO.newt
@@ -0,0 +1,30 @@
+module IO
+
+import Prelude
+
+data Foo : U where
+  MkFoo : Nat -> Nat -> Foo
+
+data World : U where
+
+data IORes : U -> U where
+  MkIORes : {a : U} -> a -> World -> IORes a
+
+IO : U -> U
+IO a = World -> IORes a
+
+iobind : {a b : U} -> IO a -> (a -> IO b) -> IO b
+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
+
+infixr 2 _>>=_
+infixr 2 _>>_
+
+-- FIXME - bad parse error for lambda without the parens
+
+_>>_ :  {a b : U} -> IO a -> IO b -> IO b
+_>>_ ma mb = ma >>= (\ _ => mb)
+
diff --git a/newt/JSLib.newt b/newt/JSLib.newt
new file mode 100644
index 0000000..1004de3
--- /dev/null
+++ b/newt/JSLib.newt
@@ -0,0 +1,17 @@
+module JSLib
+
+ptype Int
+ptype String
+
+infixl 4 _+_
+infixl 5 _*_
+
+pfunc _+_ : Int -> Int -> Int := "(x,y) => x + y"
+pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y"
+
+ptype JVoid
+
+-- REVIEW - maybe we only have body, use names from the pi-type and generate
+-- the arrow (or inline?) ourselves
+pfunc log : String -> JVoid := "x => console.log(x)"
+pfunc debug : {a : U} -> String -> a -> JVoid := "(_,x,a) => console.log(x,a)"
diff --git a/newt/Prelude.newt b/newt/Prelude.newt
new file mode 100644
index 0000000..125f4a5
--- /dev/null
+++ b/newt/Prelude.newt
@@ -0,0 +1,22 @@
+module Prelude
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Maybe : U -> U where
+  Just : {a : U} -> a -> Maybe a
+  Nothing : {a : U} -> Maybe a
+
+data Either : U -> U -> U where
+  Left : {a b : U} -> a -> Either a b
+  Right : {a b : U} -> b -> Either a b
+
+-- TODO this is special cased in some languages, maybe for easier
+-- inference? Figure out why.
+
+infixr 0 _$_
+
+_$_ : {a b : U} -> (a -> b) -> a -> b
+f $ a = f a
+
diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr
index a4b4928..ffe3d38 100644
--- a/src/Lib/Compile.idr
+++ b/src/Lib/Compile.idr
@@ -11,6 +11,8 @@ import Lib.Types
 import Lib.Prettier
 import Lib.CompileExp
 import Data.String
+import Data.Maybe
+import Data.Nat
 
 data Kind = Plain | Return | Assign String
 
@@ -136,9 +138,30 @@ termToJS env (CCase t alts) f =
     maybeCaseStmt nm alts = (JCase (Dot (Var nm) "tag") (map (termToJSAlt nm) alts))
 
 
--- FIXME escape
+-- REVIEW the escaping in show might not match JS
 jsString : String -> Doc
-jsString str = text "\"\{str}\""
+jsString str = text (show str)
+
+||| escape identifiers for js
+jsIdent : String -> Doc
+jsIdent id = text $ pack $ fix (unpack id)
+  where
+    chars : List Char
+    chars = unpack "0123456789ABCDEF"
+
+    toHex : Nat -> List Char
+    toHex 0 = []
+    toHex v = snoc (toHex (div v 16)) (fromMaybe ' ' (getAt (mod v 16) chars))
+
+    fix : List Char -> List Char
+    fix [] = []
+    fix (x :: xs) =
+      if isAlphaNum x || x == '_' then
+        x :: fix xs
+      else if x == '$' then
+        '$' :: '$' :: fix xs
+      else
+        '$' :: (toHex (cast x)) ++ fix xs
 
 stmtToDoc : JSStmt e -> Doc
 
@@ -153,17 +176,17 @@ expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ ", " <+/> e) (map
   where
     entry : (String, JSExp) -> Doc
     -- TODO quote if needed
-    entry (nm, exp) = text nm ++ ":" <+> expToDoc exp
+    entry (nm, exp) = jsIdent nm ++ ":" <+> expToDoc exp
 
 expToDoc (LitString str) = jsString str
 expToDoc (LitInt i) = text $ show i
 expToDoc (Apply x xs) = expToDoc x ++ "(" ++ commaSep (map expToDoc xs) ++ ")"
-expToDoc (Var nm) = text nm
-expToDoc (JLam nms (JReturn exp)) = text "(" <+> text (joinBy ", " nms) <+> ") =>" <+> "(" ++ expToDoc exp ++ ")"
-expToDoc (JLam nms body) = text "(" <+> text (joinBy ", " nms) <+> ") =>" <+> bracket "{" (stmtToDoc body) "}"
+expToDoc (Var nm) = jsIdent nm
+expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> "(" ++ expToDoc exp ++ ")"
+expToDoc (JLam nms body) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> bracket "{" (stmtToDoc body) "}"
 expToDoc JUndefined = text "undefined"
 expToDoc (Index obj ix) = expToDoc obj ++ "[" ++ expToDoc ix ++ "]"
-expToDoc (Dot obj nm) = expToDoc obj ++ "." ++ text nm
+expToDoc (Dot obj nm) = expToDoc obj ++ "." ++ jsIdent nm
 
 caseBody : JSStmt e -> Doc
 caseBody stmt@(JReturn x) = nest 2 (line ++ stmtToDoc stmt)
@@ -176,11 +199,11 @@ altToDoc (JDefAlt stmt) = text "default" ++ ":" ++ caseBody stmt
 stmtToDoc (JSnoc x y) = stmtToDoc x </> stmtToDoc y
 stmtToDoc (JPlain x) = expToDoc x ++ ";"
 -- I might not need these split yet.
-stmtToDoc (JLet nm body) = "let" <+> text nm ++ ";" </> stmtToDoc body
-stmtToDoc (JAssign nm expr) = text nm <+> "=" <+> expToDoc expr ++ ";"
-stmtToDoc (JConst nm x) = text "const" <+> text nm <+> "=" <+/> expToDoc x ++ ";"
+stmtToDoc (JLet nm body) = "let" <+> jsIdent nm ++ ";" </> stmtToDoc body
+stmtToDoc (JAssign nm expr) = jsIdent nm <+> "=" <+> expToDoc expr ++ ";"
+stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> "=" <+/> expToDoc x ++ ";"
 stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ ";"
-stmtToDoc (JError str) = text "throw new Error(" ++ text str ++ ");"
+stmtToDoc (JError str) = text "throw new Error(" ++ jsString str ++ ");"
 stmtToDoc (JCase sc alts) =
   text "switch (" ++ expToDoc sc ++ ")" <+> bracket "{" (stack $ map altToDoc alts) "}"
 
@@ -204,12 +227,12 @@ entryToDoc (MkEntry name ty (Fn tm)) = do
   ct <- compileFun tm
   -- now show for ct...
   let body = stmtToDoc $ termToJS [] ct JPlain
-  pure (text "const" <+> text name <+> text "=" <+/> body)
+  pure (text "const" <+> jsIdent name <+> text "=" <+/> body)
 entryToDoc (MkEntry name type Axiom) = pure ""
 entryToDoc (MkEntry name type (TCon strs)) = pure $ dcon name (piArity type)
 entryToDoc (MkEntry name type (DCon arity str)) = pure $ dcon name arity
 entryToDoc (MkEntry name type PrimTCon) = pure $ dcon name (piArity type)
-entryToDoc (MkEntry name _ (PrimFn src)) = pure $ text "const" <+> text name <+> "=" <+> text src
+entryToDoc (MkEntry name _ (PrimFn src)) = pure $ text "const" <+> jsIdent name <+> "=" <+> text src
 
 export
 compile : M Doc
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 8366ef0..28fd9e4 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -68,8 +68,10 @@ atom = RU <$> getPos <* keyword "U"
     <|> parens typeExpr
 
 -- Argument to a Spine
-pArg : Parser (Icit,Raw)
-pArg = (Explicit,) <$> atom <|> (Implicit,) <$> braces typeExpr
+pArg : Parser (Icit,FC,Raw)
+pArg = do
+  fc <- getPos
+  (Explicit,fc,) <$> atom <|> (Implicit,fc,) <$> braces typeExpr
 
 
 -- starter pack, but we'll move some to prelude
@@ -84,10 +86,10 @@ pArg = (Explicit,) <$> atom <|> (Implicit,) <$> braces typeExpr
 
 parseApp : Parser Raw
 parseApp = do
+  fc <- getPos
   hd <- atom
   rest <- many pArg
-  fc <- getPos
-  pure $ foldl (\a, (c,b) => RApp fc a b c) hd rest
+  pure $ foldl (\a, (icit,fc,b) => RApp fc a b icit) hd rest
 
 parseOp : Parser Raw
 parseOp = parseApp >>= go 0
diff --git a/src/Main.idr b/src/Main.idr
index ee0a58a..0227808 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -46,8 +46,10 @@ dumpSource = do
 writeSource : String -> M ()
 writeSource fn = do
   doc <- compile
-  Right _ <- writeFile fn $ render 90 doc
+  let src = "#!/usr/bin/env node\n" ++ render 90 doc ++ "\nmain();"
+  Right _ <- writeFile fn src
     | Left err => fail (show err)
+  Right _ <- chmodRaw fn 493 | Left err => fail (show err)
   pure ()
 
 parseFile : String -> M (String,Module)