Added Data.IOArray

plus scheme primitives for runtime, via vectors

libs/base/Data/IOArray.idr

@@ -0,0 +1,84 @@
+module Data.IOArray
+
+import Data.List
+
+-- Implemented externally
+data ArrayData : Type -> Type where
+
+-- 'unsafe' primitive access, backend dependent
+-- get and set assume that the bounds have been checked. Behavious is undefined
+-- otherwise.
+%extern prim__newArray : forall a . Int -> a -> PrimIO (ArrayData a)
+%extern prim__arrayGet : forall a . ArrayData a -> Int -> PrimIO a
+%extern prim__arraySet : forall a . ArrayData a -> Int -> a -> PrimIO ()
+
+export
+record IOArray elem where
+  constructor MkIOArray
+  max : Int
+  content : ArrayData (Maybe elem)
+
+export
+newArray : Int -> IO (IOArray elem)
+newArray size
+    = pure (MkIOArray size !(primIO (prim__newArray size Nothing)))
+
+export
+writeArray : IOArray elem -> Int -> elem -> IO ()
+writeArray arr pos el
+    = if pos < 0 || pos >= max arr
+         then pure ()
+         else primIO (prim__arraySet (content arr) pos (Just el))
+
+export
+readArray : IOArray elem -> Int -> IO (Maybe elem)
+readArray arr pos
+    = if pos < 0 || pos >= max arr
+         then pure Nothing
+         else primIO (prim__arrayGet (content arr) pos)
+
+-- Make a new array of the given size with the elements copied from the
+-- other array
+export
+newArrayCopy : (newsize : Int) -> IOArray elem -> IO (IOArray elem)
+newArrayCopy newsize arr
+    = do let newsize' = if newsize < max arr then max arr else newsize
+         arr' <- newArray newsize'
+         copyFrom (content arr) (content arr') (max arr - 1)
+         pure arr'
+  where
+    copyFrom : ArrayData (Maybe elem) ->
+               ArrayData (Maybe elem) ->
+               Int -> IO ()
+    copyFrom old new pos
+        = if pos < 0
+             then pure ()
+             else do el <- primIO $ prim__arrayGet old pos
+                     primIO $ prim__arraySet new pos el
+                     assert_total (copyFrom old new (pos - 1))
+
+export
+toList : IOArray elem -> IO (List (Maybe elem))
+toList arr = iter 0 (max arr) []
+  where
+    iter : Int -> Int -> List (Maybe elem) -> IO (List (Maybe elem))
+    iter pos end acc
+         = if pos >= end
+              then pure (reverse acc)
+              else do el <- readArray arr pos
+                      assert_total (iter (pos + 1) end (el :: acc))
+
+export
+fromList : List (Maybe elem) -> IO (IOArray elem)
+fromList ns
+    = do arr <- newArray (cast (length ns))
+         addToArray 0 ns arr
+         pure arr
+  where
+    addToArray : Int -> List (Maybe elem) -> IOArray elem -> IO ()
+    addToArray loc [] arr = pure ()
+    addToArray loc (Nothing :: ns) arr
+        = assert_total (addToArray (loc + 1) ns arr)
+    addToArray loc (Just el :: ns) arr
+        = do primIO $ prim__arraySet (content arr) loc (Just el)
+             assert_total (addToArray (loc + 1) ns arr)

libs/base/base.ipkg

@@ -8,6 +8,7 @@ modules = Control.Monad.Identity,
           Data.Buffer,
           Data.Either,
           Data.Fin,
+          Data.IOArray,
           Data.IORef,
           Data.List,
           Data.List.Elem,

src/Compiler/Scheme/Common.idr

@@ -155,6 +155,7 @@ public export
 data ExtPrim = CCall | SchemeCall | PutStr | GetStr
              | FileOpen | FileClose | FileReadLine | FileWriteLine | FileEOF
              | NewIORef | ReadIORef | WriteIORef
+             | NewArray | ArrayGet | ArraySet
              | Stdin | Stdout | Stderr
              | VoidElim | Unknown Name
 
@@ -172,6 +173,9 @@ Show ExtPrim where
   show NewIORef = "NewIORef"
   show ReadIORef = "ReadIORef"
   show WriteIORef = "WriteIORef"
+  show NewArray = "NewArray"
+  show ArrayGet = "ArrayGet"
+  show ArraySet = "ArraySet"
   show Stdin = "Stdin"
   show Stdout = "Stdout"
   show Stderr = "Stderr"
@@ -193,6 +197,9 @@ toPrim pn@(NS _ n)
             (n == UN "prim__newIORef", NewIORef),
             (n == UN "prim__readIORef", ReadIORef),
             (n == UN "prim__writeIORef", WriteIORef),
+            (n == UN "prim__newArray", NewArray),
+            (n == UN "prim__arrayGet", ArrayGet),
+            (n == UN "prim__arraySet", ArraySet),
             (n == UN "prim__stdin", Stdin),
             (n == UN "prim__stdout", Stdout),
             (n == UN "prim__stderr", Stderr),
@@ -341,6 +348,16 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx
       = pure $ mkWorld $ "(set-box! "
                            ++ !(schExp i vs ref) ++ " "
                            ++ !(schExp i vs val) ++ ")"
+  schExtCommon i vs NewArray [_, size, val, world]
+      = pure $ mkWorld $ "(make-vector " ++ !(schExp i vs size) ++ " "
+                                         ++ !(schExp i vs val) ++ ")"
+  schExtCommon i vs ArrayGet [_, arr, pos, world]
+      = pure $ mkWorld $ "(vector-ref " ++ !(schExp i vs arr) ++ " "
+                                        ++ !(schExp i vs pos) ++ ")"
+  schExtCommon i vs ArraySet [_, arr, pos, val, world]
+      = pure $ mkWorld $ "(vector-set! " ++ !(schExp i vs arr) ++ " "
+                                         ++ !(schExp i vs pos) ++ " "
+                                         ++ !(schExp i vs val) ++ ")"
   schExtCommon i vs VoidElim [_, _]
       = pure "(display \"Error: Executed 'void'\")"
   schExtCommon i vs (Unknown n) args

tests/Main.idr

@@ -65,7 +65,7 @@ typeddTests
 chezTests : List String
 chezTests
    = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
-      "chez007", "chez008", "chez009", "chez010", "chez011"]
+      "chez007", "chez008", "chez009", "chez010", "chez011", "chez012"]
 
 ideModeTests : List String
 ideModeTests

tests/chez/chez012/array.idr

@@ -0,0 +1,11 @@
+import Data.IOArray
+
+main : IO ()
+main
+    = do x <- newArray 20
+         writeArray x 10 "Hello"
+         writeArray x 11 "World"
+         printLn !(toList x)
+
+         y <- fromList (map Just [1,2,3,4,5])
+         printLn !(toList y)

tests/chez/chez012/expected

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

tests/chez/chez012/input

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

tests/chez/chez012/run

@@ -0,0 +1,2 @@
+$1 --no-banner array.idr < input
+rm -rf build