edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-08-17 03:40:33 +03:00
Code Issues Projects Releases Wiki Activity

Switch buffers back to scheme FFI

Browse Source 
It's just easier to deal with the memory management! But we should do
something more flexible here later.
This commit is contained in:
Edwin Brady 2020-05-17 22:49:41 +01:00
parent 463f1b3233
commit a130952928
5 changed files with 124 additions and 66 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

116
libs/base/Data/Buffer.idr
View File

@ -3,114 +3,100 @@ module Data.Buffer
import System.File
export
data Buffer : Type where
MkBuffer : AnyPtr -> (size : Int) -> (loc : Int) -> Buffer
data Buffer : Type where [external]
support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support"
%foreign support "idris2_getBufferSize"
prim__bufferSize : AnyPtr -> Int
%foreign "scheme:blodwen-buffer-size"
prim__bufferSize : Buffer -> Int
export
rawSize : Buffer -> IO Int
rawSize (MkBuffer buf _ _)
= pure (prim__bufferSize buf)
rawSize buf = pure (prim__bufferSize buf)
%foreign support "idris2_newBuffer"
prim__newBuffer : Int -> PrimIO AnyPtr
%foreign support "idris2_freeBuffer"
prim__freeBuffer : AnyPtr -> PrimIO ()
%foreign "scheme:blodwen-new-buffer"
prim__newBuffer : Int -> PrimIO Buffer
export
newBuffer : Int -> IO (Maybe Buffer)
newBuffer size
= do buf <- primIO (prim__newBuffer size)
if prim__nullAnyPtr buf /= 0
then pure Nothing
else pure $ Just $ MkBuffer buf size 0
pure $ Just buf
-- if prim__nullAnyPtr buf /= 0
-- then pure Nothing
-- else pure $ Just $ MkBuffer buf size 0
-- might be needed if we do this in C...
export
freeBuffer : Buffer -> IO ()
freeBuffer (MkBuffer buf _ _) = primIO (prim__freeBuffer buf)
freeBuffer buf = pure ()
export
resetBuffer : Buffer -> Buffer
resetBuffer (MkBuffer ptr s l) = MkBuffer ptr s 0
export
size : Buffer -> Int
size (MkBuffer _ s _) = s
%foreign support "idris2_setBufferByte"
prim__setByte : AnyPtr -> Int -> Int -> PrimIO ()
%foreign "scheme:blodwen-buffer-setbyte"
prim__setByte : Buffer -> Int -> Int -> PrimIO ()
-- Assumes val is in the range 0-255
export
setByte : Buffer -> (loc : Int) -> (val : Int) -> IO ()
setByte (MkBuffer buf _ _) loc val
setByte buf loc val
= primIO (prim__setByte buf loc val)
%foreign support "idris2_getBufferByte"
prim__getByte : AnyPtr -> Int -> PrimIO Int
%foreign "scheme:blodwen-buffer-getbyte"
prim__getByte : Buffer -> Int -> PrimIO Int
export
getByte : Buffer -> (loc : Int) -> IO Int
getByte (MkBuffer buf _ _) loc
getByte buf loc
= primIO (prim__getByte buf loc)
%foreign support "idris2_setBufferInt"
prim__setInt : AnyPtr -> Int -> Int -> PrimIO ()
%foreign "scheme:blodwen-buffer-setint"
prim__setInt : Buffer -> Int -> Int -> PrimIO ()
export
setInt : Buffer -> (loc : Int) -> (val : Int) -> IO ()
setInt (MkBuffer buf _ _) loc val
setInt buf loc val
= primIO (prim__setInt buf loc val)
%foreign support "idris2_getBufferInt"
prim__getInt : AnyPtr -> Int -> PrimIO Int
%foreign "scheme:blodwen-buffer-getint"
prim__getInt : Buffer -> Int -> PrimIO Int
export
getInt : Buffer -> (loc : Int) -> IO Int
getInt (MkBuffer buf _ _) loc
getInt buf loc
= primIO (prim__getInt buf loc)
%foreign support "idris2_setBufferDouble"
prim__setDouble : AnyPtr -> Int -> Double -> PrimIO ()
%foreign "scheme:blodwen-buffer-setdouble"
prim__setDouble : Buffer -> Int -> Double -> PrimIO ()
export
setDouble : Buffer -> (loc : Int) -> (val : Double) -> IO ()
setDouble (MkBuffer buf _ _) loc val
setDouble buf loc val
= primIO (prim__setDouble buf loc val)
%foreign support "idris2_getBufferDouble"
prim__getDouble : AnyPtr -> Int -> PrimIO Double
%foreign "scheme:blodwen-buffer-getdouble"
prim__getDouble : Buffer -> Int -> PrimIO Double
export
getDouble : Buffer -> (loc : Int) -> IO Double
getDouble (MkBuffer buf _ _) loc
getDouble buf loc
= primIO (prim__getDouble buf loc)
-- Get the length of a string in bytes, rather than characters
export
%foreign support "strlen"
%foreign "C:strlen,libc 6"
stringByteLength : String -> Int
%foreign support "idris2_setBufferString"
prim__setString : AnyPtr -> Int -> String -> PrimIO ()
%foreign "scheme:blodwen-buffer-setstring"
prim__setString : Buffer -> Int -> String -> PrimIO ()
export
setString : Buffer -> (loc : Int) -> (val : String) -> IO ()
setString (MkBuffer buf _ _) loc val
setString buf loc val
= primIO (prim__setString buf loc val)
%foreign support "idris2_getBufferString"
prim__getString : AnyPtr -> Int -> Int -> PrimIO String
%foreign "scheme:blodwen-buffer-getstring"
prim__getString : Buffer -> Int -> Int -> PrimIO String
export
getString : Buffer -> (loc : Int) -> (len : Int) -> IO String
getString (MkBuffer buf _ _) loc len
getString buf loc len
= primIO (prim__getString buf loc len)
export
@ -125,13 +111,13 @@ bufferData buf
= do val <- getByte buf (loc - 1)
unpackTo (val :: acc) (loc - 1)
%foreign support "idris2_copyBuffer"
prim__copyData : AnyPtr -> Int -> Int -> AnyPtr -> Int -> PrimIO ()
%foreign "scheme:blodwen-buffer-copydata"
prim__copyData : Buffer -> Int -> Int -> Buffer -> Int -> PrimIO ()
export
copyData : (src : Buffer) -> (start, len : Int) ->
(dest : Buffer) -> (loc : Int) -> IO ()
copyData (MkBuffer src _ _) start len (MkBuffer dest _ _) loc
copyData src start len dest loc
= primIO (prim__copyData src start len dest loc)
-- %foreign "scheme:blodwen-readbuffer-bytes"
@ -146,8 +132,11 @@ copyData (MkBuffer src _ _) start len (MkBuffer dest _ _) loc
-- then pure (Right (MkBuffer buf size (loc + read)))
-- else pure (Left FileReadError)
%foreign support "idris2_readBufferFromFile"
prim__readBufferFromFile : String -> PrimIO AnyPtr
%foreign "scheme:blodwen-read-bytevec"
prim__readBufferFromFile : String -> PrimIO Buffer
%foreign "scheme:blodwen-isbytevec"
prim__isBuffer : Buffer -> Int
-- Create a new buffer by reading all the contents from the given file
-- Fails if no bytes can be read or buffer can't be created
@ -155,20 +144,20 @@ export
createBufferFromFile : String -> IO (Either FileError Buffer)
createBufferFromFile fn
= do buf <- primIO (prim__readBufferFromFile fn)
if prim__nullAnyPtr buf /= 0
if prim__isBuffer buf /= 0
then pure (Left FileReadError)
else do let sz = prim__bufferSize buf
pure (Right (MkBuffer buf sz sz))
pure (Right buf)
%foreign support "idris2_writeBufferToFile"
prim__writeBuffer : String -> AnyPtr -> Int -> PrimIO Int
%foreign "scheme:blodwen-write-bytevec"
prim__writeBuffer : String -> Buffer -> Int -> PrimIO Int
export
writeBufferToFile : String -> Buffer -> (maxbytes : Int) ->
IO (Either FileError ())
writeBufferToFile fn (MkBuffer buf size loc) max
writeBufferToFile fn buf max
= do res <- primIO (prim__writeBuffer fn buf max)
if res == 0
if res /= 0
then pure (Left FileWriteError)
else pure (Right ())
@ -179,7 +168,8 @@ resizeBuffer old newsize
| Nothing => pure Nothing
-- If the new buffer is smaller than the old one, just copy what
-- fits
let oldsize = size old
oldsize <- rawSize old
let len = if newsize < oldsize then newsize else oldsize
copyData old 0 len buf 0
freeBuffer old
pure (Just buf)

68
support/chez/support.ss
View File

@ -75,6 +75,74 @@
chr))
void))
;; Buffers
(define (blodwen-new-buffer size)
(make-bytevector size 0))
(define (blodwen-buffer-size buf)
(bytevector-length buf))
(define (blodwen-buffer-setbyte buf loc val)
(bytevector-u8-set! buf loc val))
(define (blodwen-buffer-getbyte buf loc)
(bytevector-u8-ref buf loc))
(define (blodwen-buffer-setint buf loc val)
(bytevector-s32-set! buf loc val (native-endianness)))
(define (blodwen-buffer-getint buf loc)
(bytevector-s32-ref buf loc (native-endianness)))
(define (blodwen-buffer-setdouble buf loc val)
(bytevector-ieee-double-set! buf loc val (native-endianness)))
(define (blodwen-buffer-getdouble buf loc)
(bytevector-ieee-double-ref buf loc (native-endianness)))
(define (blodwen-stringbytelen str)
(bytevector-length (string->utf8 str)))
(define (blodwen-buffer-setstring buf loc val)
(let* [(strvec (string->utf8 val))
(len (bytevector-length strvec))]
(bytevector-copy! strvec 0 buf loc len)))
(define (blodwen-buffer-getstring buf loc len)
(let [(newvec (make-bytevector len))]
(bytevector-copy! buf loc newvec 0 len)
(utf8->string newvec)))
(define (blodwen-buffer-copydata buf start len dest loc)
(bytevector-copy! buf start dest loc len))
(define (blodwen-read-bytevec fname)
(guard
(x (#t #f))
(let* [(h (open-file-input-port fname
(file-options)
(buffer-mode line) #f))
(vec (get-bytevector-all h))]
(begin (close-port h)
vec))))
(define (blodwen-isbytevec v)
(if (bytevector? v)
0
-1))
(define (blodwen-write-bytevec fname vec max)
(guard
(x (#t -1))
(let* [(h (open-file-output-port fname (file-options no-fail)
(buffer-mode line) #f))]
(begin (put-bytevector h vec 0 max)
(close-port h)
0))))
;; Threads
(define blodwen-thread-data (make-thread-parameter #f))

2
tests/ideMode/ideMode001/expected
View File

@ -8,7 +8,7 @@
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:741:1--748:1 n[2] m[4]) a[3])))")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

2
tests/ideMode/ideMode003/expected
View File

@ -8,7 +8,7 @@
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:741:1--748:1 n[2] m[4]) a[3])))")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

2
tests/idris2/total006/expected
View File

@ -1,6 +1,6 @@
1/1: Building Total (Total.idr)
Main> Main.count is total
Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:1004:1--1009:1 -> Prelude.map
Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:1010:1--1015:1 -> Prelude.map
Main> Main.process is total
Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
Main> Main.doubleInt is total