diff --git a/libs/base/Data/IOArray.idr b/libs/base/Data/IOArray.idr new file mode 100644 index 0000000..2a42918 --- /dev/null +++ b/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) diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index c54b0d6..a566785 100644 --- a/libs/base/base.ipkg +++ b/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, diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index b73adc3..727059e 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/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 diff --git a/tests/Main.idr b/tests/Main.idr index f7e5309..88047dc 100644 --- a/tests/Main.idr +++ b/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 diff --git a/tests/chez/chez012/array.idr b/tests/chez/chez012/array.idr new file mode 100644 index 0000000..209677f --- /dev/null +++ b/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) diff --git a/tests/chez/chez012/expected b/tests/chez/chez012/expected new file mode 100644 index 0000000..364c6cd --- /dev/null +++ b/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! diff --git a/tests/chez/chez012/input b/tests/chez/chez012/input new file mode 100644 index 0000000..fc5992c --- /dev/null +++ b/tests/chez/chez012/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/chez/chez012/run b/tests/chez/chez012/run new file mode 100755 index 0000000..8405356 --- /dev/null +++ b/tests/chez/chez012/run @@ -0,0 +1,2 @@ +$1 --no-banner array.idr < input +rm -rf build