-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlinearLibPoly.idr
133 lines (94 loc) · 3.88 KB
/
linearLibPoly.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
import System.FFI
import PrimIO
import Prelude
import Control.Linear.LIO
import Control.App
import Control.App.Console
import System.FFI
import PrimIO
import Prelude
import Control.Linear.LIO
import Control.Monad.State.State
import Control.Monad.State
import Data.Fin
import Data.Nat
--Create Arrays
%foreign "C:getArray, libsmall"
getArray : Int -> PrimIO (Ptr Int)
%foreign "C:getArray, libsmall"
getArrayChar : Int -> PrimIO (Ptr Char)
--Read Arrays
%foreign "C:readPointerOffset, libsmall"
readPointerOffset : Int -> (1 mem : Ptr Int) -> PrimIO Int
%foreign "C:readPointerOffsetChar, libsmall"
readPointerOffsetChar : Int -> (1 mem : Ptr Char) -> PrimIO Char
--Write Arrays
%foreign "C:writeOffset, libsmall"
writeOffset : Int -> (1 mem : Ptr Int) -> Int -> PrimIO ()
%foreign "C:writeOffsetChar, libsmall"
writeOffsetChar : Int -> (1 mem : Ptr Char) -> Char -> PrimIO ()
--Free Pointer
%foreign "C:freePointer, libsmall"
freePointer : (1 mem : Ptr Int) -> PrimIO ()
%foreign "C:freePointerChar, libsmall"
freePointerChar : (1 mem : Ptr Char) -> PrimIO ()
MyPtr = L IO {use=1} (Ptr Int)
-- Need to make Arr constructor private
export
data MyVect : Nat -> Type -> Type where
Arr : (size : Nat) -> (1 _ : Ptr a) -> MyVect (S size) a
%name MyVect arr, arr1, arr2
interface CType a where
createArr : (size : Nat) -> L IO {use=1} (MyVect (S size) a)
getIndex : (index : Fin m) -> (1 mem : (MyVect m a)) -> L IO {use=1} (Res a (\_ => MyVect m a))
writeArr : a -> (index : Fin m) -> (1 mem : MyVect m a) -> L IO {use=1} (MyVect m a)
freeArr : (1 mem : MyVect m a) -> L IO ()
conv : (Fin m) -> Int
conv = cast . finToInteger
getIndex' : (index : Fin m) -> (MyVect m Int) -> L IO {use=1} (Res Int (\_ => MyVect m Int))
getIndex' index (Arr size ptr) = do
x <- liftIO1 {io=L IO} (fromPrim $ readPointerOffset (conv index) ptr)
pure1 (x # (Arr size ptr))
writeArr' : Int -> (index : Fin m) -> (MyVect m Int) -> L IO {use=1} (MyVect m Int)
writeArr' toWrite index (Arr size ptr) = do
liftIO1 {io = L IO} (fromPrim (writeOffset (conv index) ptr toWrite))
pure1 (Arr size ptr)
export
CType Int where
createArr (size) = do
x <- liftIO1 {io=L IO} (fromPrim (getArray (cast (S size))))
pure1 (Arr size x)
getIndex index = assert_linear (getIndex' index)
writeArr toWrite index = assert_linear (writeArr' toWrite index)
freeArr (Arr s ptr) = liftIO1 {io = L IO} (fromPrim $ freePointer ptr)
getIndexChar' : (index : Fin m) -> (MyVect m Char) -> L IO {use=1} (Res Char (\_ => MyVect m Char))
getIndexChar' index (Arr size ptr) = do
x <- liftIO1 {io=L IO} (fromPrim $ readPointerOffsetChar (conv index) ptr)
pure1 (x # (Arr size ptr))
writeArrChar' : Char -> (index : Fin m) -> (MyVect m Char) -> L IO {use=1} (MyVect m Char)
writeArrChar' toWrite index (Arr size ptr) = do
liftIO1 {io = L IO} (fromPrim (writeOffsetChar (conv index) ptr toWrite))
pure1 (Arr size ptr)
export
CType Char where
createArr (size) = do
x <- liftIO1 {io=L IO} (fromPrim (getArrayChar (cast (S size))))
pure1 (Arr size x)
getIndex index = assert_linear (getIndexChar' index)
writeArr toWrite index = assert_linear (writeArrChar' toWrite index)
freeArr (Arr s ptr) = liftIO1 {io = L IO} (fromPrim $ freePointerChar ptr)
export
runLin : (Applicative io, LinearBind io) => (1 _ : L io a) -> io a
runLin = Control.Linear.LIO.run
main : IO ()
main = runLin $ do
x <- createArr 10
x <- writeArr (the Char 'c') 5 x
val # x <- getIndex 5 x
print val
freeArr x
x : IO ()
x = runLin $ do
x <- createArr 10
x <- writeArr (the Int 100) 5 x
freeArr x