[ codegen ] more flexible array implementation on JS backends (#2966)

CHANGELOG.md

@@ -36,6 +36,7 @@
 * Generated JavaScript files now include a shebang when using the Node.js backend
 * NodeJS now supports `popen`/`pclose` for the `Read` mode.
 * `getChar` is now supported on Node.js and `putChar` is supported on both JavaScript backends.
+* Integer-indexed arrays are now supported.
 
 ### Compiler changes
 

src/Compiler/ES/Codegen.idr

@@ -557,9 +557,9 @@ jsPrim nm docs = case (dropAllNS nm, docs) of
   (UN (Basic "prim__newIORef"), [_,v,_]) => pure $ hcat ["({value:", v, "})"]
   (UN (Basic "prim__readIORef"), [_,r,_]) => pure $ hcat ["(", r, ".value)"]
   (UN (Basic "prim__writeIORef"), [_,r,v,_]) => pure $ hcat ["(", r, ".value=", v, ")"]
-  (UN (Basic "prim__newArray"), [_,s,v,_]) => pure $ hcat ["(Array(", s, ").fill(", v, "))"]
-  (UN (Basic "prim__arrayGet"), [_,x,p,_]) => pure $ hcat ["(", x, "[", p, "])"]
-  (UN (Basic "prim__arraySet"), [_,x,p,v,_]) => pure $ hcat ["(", x, "[", p, "]=", v, ")"]
+  (UN (Basic "prim__newArray"), [_,s,v,_]) => pure $ hcat ["(Array(", fromBigInt s, ").fill(", v, "))"]
+  (UN (Basic "prim__arrayGet"), [_,x,p,_]) => pure $ hcat ["(", x, "[", fromBigInt p, "])"]
+  (UN (Basic "prim__arraySet"), [_,x,p,v,_]) => pure $ hcat ["(", x, "[", fromBigInt p, "]=", v, ")"]
   (UN (Basic "void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
   (UN (Basic "prim__void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
   (UN (Basic "prim__codegen"), []) => do

tests/Main.idr

@@ -363,6 +363,7 @@ nodeTests = MkTestPool "Node backend" [] (Just Node)
     , "fix1839"
     , "tailrec_libs"
     , "nomangle001", "nomangle002"
+    , "integer_array"
     ]
 
 vmcodeInterpTests : IO TestPool

tests/node/integer_array/array.idr

@@ -0,0 +1,48 @@
+import System
+
+import Data.Nat
+
+data ArrayData : Type -> Type where [external]
+
+-- We use `Integer` for indexing here instead of `Int` as in `Data.IOArray.Prims`
+%extern prim__newArray : forall a . Integer -> a -> PrimIO (ArrayData a)
+%extern prim__arrayGet : forall a . ArrayData a -> Integer -> PrimIO a
+%extern prim__arraySet : forall a . ArrayData a -> Integer -> a -> PrimIO ()
+
+record IOArray (n : Nat) a where
+  constructor MkIOArray
+  content : ArrayData a
+
+newArray : HasIO io => (n : Nat) -> a -> io (IOArray n a)
+newArray size v = pure (MkIOArray !(primIO (prim__newArray (cast size) v)))
+
+writeArray :
+     HasIO io
+  => IOArray n a
+  -> (m : Nat)
+  -> {auto 0 lt : LT m n}
+  -> a
+  -> io ()
+writeArray arr pos el = primIO (prim__arraySet (content arr) (cast pos) el)
+
+readArray :
+     HasIO io
+  => IOArray n a
+  -> (m : Nat)
+  -> {auto 0 lt : LT m n}
+  -> io a
+readArray arr pos = primIO (prim__arrayGet (content arr) (cast pos))
+
+toList : {n : _} -> HasIO io => IOArray n a -> io (List a)
+toList arr = iter n reflexive []
+where
+  iter : (m : Nat) -> (0 lte : LTE m n) -> List a -> io (List a)
+  iter 0     _ acc = pure acc
+  iter (S k) p acc = readArray arr k >>= \el => iter k (lteSuccLeft p) (el :: acc)
+
+main : IO ()
+main = do
+  x <- newArray 20 ""
+  writeArray x 11 "World"
+  writeArray x 10 "Hello"
+  printLn !(toList x)

tests/node/integer_array/expected

@@ -0,0 +1,3 @@
+1/1: Building array (array.idr)
+Main> ["", "", "", "", "", "", "", "", "", "", "Hello", "World", "", "", "", "", "", "", "", ""]
+Main> Bye for now!

tests/node/integer_array/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/node/integer_array/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --cg node --no-banner array.idr < input