acb2efb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

prim__vm needs to take a World reference

Otherwise we might inline it in the wrong VM and send messages to the wrong places

commitacb2efb8d40e5662987ea20846710d87af2d67a4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 29 Aug 2016, 18:29 (10 years ago) parente0c893c

8 files changed+47−31

compare with master

unifiedsplit

libs/base/System/Concurrency/Raw.idr+22−16 libs/contrib/System/Concurrency/Process.idr+4−2 libs/prelude/Builtins.idr+1−1 libs/prelude/IO.idr+6−2 libs/prelude/Prelude/File.idr+3−2 src/IRTS/CodegenC.hs+1−1 test/io003/test018.idr+2−1 test/proofsearch002/Process.idr+8−6

libs/base/System/Concurrency/Raw.idr+22−16

@@ -13,13 +13,14 @@ import System

1313||| the receiver will create a new channel ID

1414sendToThread : (thread_id : Ptr) -> (channel : Int) -> a -> IO Int

1515sendToThread {a} dest channel val

16− = foreign FFI_C "idris_sendMessage" (Ptr -> Int -> Ptr -> Raw a -> IO Int)

17− prim__vm channel dest (MkRaw val)

16+ = do me <- getMyVM

17+ foreign FFI_C "idris_sendMessage" (Ptr -> Int -> Ptr -> Raw a -> IO Int)

18+ me channel dest (MkRaw val)

1819

1920||| Check for messages in the process inbox

2021checkMsgs : IO Bool

21−checkMsgs = do msgs <- foreign FFI_C "idris_checkMessages" (Ptr -> IO Ptr)

22− prim__vm

22+checkMsgs = do me <- getMyVM

23+ msgs <- foreign FFI_C "idris_checkMessages" (Ptr -> IO Ptr) me

2324 null <- nullPtr msgs

2425 pure (not null)

2526

@@ -27,8 +28,9 @@ checkMsgs = do msgs <- foreign FFI_C "idris_checkMessages" (Ptr -> IO Ptr)

2728||| If no messages, waits for the given number of seconds

2829checkMsgsTimeout : Int -> IO Bool

2930checkMsgsTimeout timeout

30− = do msgs <- foreign FFI_C "idris_checkMessagesTimeout"

31− (Ptr -> Int -> IO Ptr) prim__vm timeout

31+ = do me <- getMyVM

32+ msgs <- foreign FFI_C "idris_checkMessagesTimeout"

33+ (Ptr -> Int -> IO Ptr) me timeout

3234 null <- nullPtr msgs

3335 pure (not null)

3436

@@ -44,8 +46,9 @@ channel_id msg = foreign FFI_C "idris_getChannel" (Ptr -> IO Int) msg

4446||| Returns either 'Nothing', if none, or 'Just (pid, channel)' as pid

4547||| of sender and new channel id.

4648listenMsgs : IO (Maybe (Ptr, Int))

47−listenMsgs = do msg <- foreign FFI_C "idris_checkInitMessages" (Ptr -> IO Ptr)

48− prim__vm

49+listenMsgs = do me <- getMyVM

50+ msg <- foreign FFI_C "idris_checkInitMessages" (Ptr -> IO Ptr)

51+ me

4952 null <- nullPtr msg

5053 if null then pure Nothing

5154 else do s_id <- sender msg

@@ -56,8 +59,9 @@ listenMsgs = do msg <- foreign FFI_C "idris_checkInitMessages" (Ptr -> IO Ptr)

5659||| If channel is '0', accept on any channel.

5760checkMsgsFrom : Ptr -> (channel : Int) -> IO Bool

5861checkMsgsFrom sender channel

59− = do msgs <- foreign FFI_C "idris_checkMessagesFrom" (Ptr -> Int -> Ptr -> IO Ptr)

60− prim__vm channel sender

62+ = do me <- getMyVM

63+ msgs <- foreign FFI_C "idris_checkMessagesFrom" (Ptr -> Int -> Ptr -> IO Ptr)

64+ me channel sender

6165 null <- nullPtr msgs

6266 pure (not null)

6367

@@ -66,8 +70,8 @@ checkMsgsFrom sender channel

6670||| Note that this is not at all type safe! It is intended to be used in

6771||| a type safe wrapper.

6872getMsg : IO a

69−getMsg {a} = do m <- foreign FFI_C "idris_recvMessage"

70− (Ptr -> IO Ptr) prim__vm

73+getMsg {a} = do me <- getMyVM

74+ m <- foreign FFI_C "idris_recvMessage" (Ptr -> IO Ptr) me

7175 MkRaw x <- foreign FFI_C "idris_getMsg" (Ptr -> IO (Raw a)) m

7276 pure x

7377

@@ -77,8 +81,9 @@ getMsg {a} = do m <- foreign FFI_C "idris_recvMessage"

7781||| a type safe wrapper.

7882getMsgWithSender : IO (Ptr, Int, a)

7983getMsgWithSender {a}

80− = do m <- foreign FFI_C "idris_recvMessage"

81− (Ptr -> IO Ptr) prim__vm

84+ = do me <- getMyVM

85+ m <- foreign FFI_C "idris_recvMessage"

86+ (Ptr -> IO Ptr) me

8287 MkRaw x <- foreign FFI_C "idris_getMsg" (Ptr -> IO (Raw a)) m

8388 vm <- sender m

8489 chan <- channel_id m

@@ -90,8 +95,9 @@ getMsgWithSender {a}

9095||| alive

9196getMsgFrom : Ptr -> (channel : Int) -> IO (Maybe a)

9297getMsgFrom {a} sender channel

93− = do m <- foreign FFI_C "idris_recvMessageFrom"

94− (Ptr -> Int -> Ptr -> IO Ptr) prim__vm channel sender

98+ = do me <- getMyVM

99+ m <- foreign FFI_C "idris_recvMessageFrom"

100+ (Ptr -> Int -> Ptr -> IO Ptr) me channel sender

95101 null <- nullPtr m

96102 if null

97103 then pure Nothing

libs/contrib/System/Concurrency/Process.idr+4−2

@@ -32,13 +32,15 @@ run (Lift prog) = prog

3232||| Get current process ID

3333export

3434myID : Process msg (ProcID msg)

35−myID = Lift (pure (MkPID prim__vm))

35+myID = Lift (do me <- getMyVM

36+ pure (MkPID me))

3637

3738||| Send a message to another process

3839||| Returns whether the send was unsuccessful.

3940export

4041send : ProcID msg -> msg -> Process msg Bool

41−send (MkPID p) m = Lift (do x <- sendToThread p 0 (prim__vm, m)

42+send (MkPID p) m = Lift (do me <- getMyVM

43+ x <- sendToThread p 0 (me, m)

4244 pure (x /= 0))

4345

4446||| Return whether a message is waiting in the queue

libs/prelude/Builtins.idr+1−1

@@ -204,7 +204,7 @@ export data CData : Type

204204%extern prim__readFile : prim__WorldType -> Ptr -> String

205205%extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int

206206

207−%extern prim__vm : Ptr

207+%extern prim__vm : prim__WorldType -> Ptr

208208%extern prim__stdin : Ptr

209209%extern prim__stdout : Ptr

210210%extern prim__stderr : Ptr

libs/prelude/IO.idr+6−2

@@ -205,7 +205,7 @@ run__provider : IO a -> PrimIO a

205205run__provider (MkIO f) = f (TheWorld prim__TheWorld)

206206

207207prim_fork : PrimIO () -> PrimIO Ptr

208−prim_fork x = prim_io_pure prim__vm -- compiled specially

208+prim_fork x = prim_io_pure (prim__vm prim__TheWorld) -- compiled specially

209209

210210namespace IO

211211 fork : IO' l () -> IO' l Ptr

@@ -214,8 +214,12 @@ namespace IO

214214 (\ x => prim_io_pure x)))

215215 (\x => prim_io_pure x))

216216

217+ getMyVM : IO' l Ptr

218+ getMyVM = MkIO (\w => prim_io_pure (prim__vm (world w)))

219+

217220 forceGC : IO ()

218− forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

221+ forceGC = io_bind getMyVM

222+ (\vm => foreign FFI_C "idris_forceGC" (Ptr -> IO ()) vm)

219223

220224 getErrno : IO Int

221225 getErrno = foreign FFI_C "idris_errno" (IO Int)

libs/prelude/Prelude/File.idr+3−2

@@ -40,8 +40,9 @@ strError err = unsafePerformIO -- yeah, yeah...

4040 (foreign FFI_C "idris_showerror" (Int -> IO String) err)

4141

4242getFileError : IO FileError

43−getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"

44− (Ptr -> IO (Raw FileError)) prim__vm

43+getFileError = do vm <- getMyVM

44+ MkRaw err <- foreign FFI_C "idris_mkFileError"

45+ (Ptr -> IO (Raw FileError)) vm

4546 pure err

4647

4748Show FileError where

src/IRTS/CodegenC.hs+1−1

@@ -627,11 +627,11 @@ doOp v (LExternal wf) [_,x,s]

627627 = v ++ "MKINT((i_int)(idris_writeStr(GETPTR(" ++ creg x

628628 ++ "),GETSTR("

629629 ++ creg s ++ "))))"

630−doOp v (LExternal vm) [] | vm == sUN "prim__vm" = v ++ "MKPTR(vm, vm)"

631630doOp v (LExternal si) [] | si == sUN "prim__stdin" = v ++ "MKPTR(vm, stdin)"

632631doOp v (LExternal so) [] | so == sUN "prim__stdout" = v ++ "MKPTR(vm, stdout)"

633632doOp v (LExternal se) [] | se == sUN "prim__stderr" = v ++ "MKPTR(vm, stderr)"

634633

634+doOp v (LExternal vm) [_] | vm == sUN "prim__vm" = v ++ "MKPTR(vm, vm)"

635635doOp v (LExternal nul) [] | nul == sUN "prim__null" = v ++ "MKPTR(vm, NULL)"

636636doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqPtr"

637637 = v ++ "MKINT((i_int)(GETPTR(" ++ creg x ++ ") == GETPTR(" ++ creg y ++ ")))"

test/io003/test018.idr+2−1

@@ -14,7 +14,8 @@ pong = do (sender, x) <- recvMsg

1414 pure ()

1515

1616ping : Ptr -> IO ()

17−ping thread = do sendToThread thread 0 (prim__vm, "Hello!")

17+ping thread = do me <- getMyVM

18+ sendToThread thread 0 (me, "Hello!")

1819 pure ()

1920

2021pingpong : IO ()

test/proofsearch002/Process.idr+8−6

@@ -378,7 +378,8 @@ eval st (Fork proc) k

378378 k (MkPID ptr) st

379379

380380eval st (Work proc cont) k

381− = do ptr <- fork (eval (MkEvalState [] [] 0 0) (proc (MkPID prim__vm))

381+ = do me <- getMyVM

382+ ptr <- fork (eval (MkEvalState [] [] 0 0) (proc (MkPID me))

382383 (\_, _ => pure ()))

383384 eval (record { clients = clients st + 1 } st) cont k

384385

@@ -420,11 +421,12 @@ eval {iface} {hs} st (Respond f) k

420421 k val st''')

421422

422423eval {hs} st (Connect {serveri} (MkPID pid)) k

423− = if pid == prim__vm then k False st else do

424− v <- sendToThread pid 0 (MsgQuery {iface=serveri} {hs}

425− ConnectMsg)

426− -- TODO: Wait for ACK

427− k (v == 1) st

424+ = do me <- getMyVM

425+ if pid == me then k False st else do

426+ v <- sendToThread pid 0 (MsgQuery {iface=serveri} {hs}

427+ ConnectMsg)

428+ -- TODO: Wait for ACK

429+ k (v == 1) st

428430

429431eval {hs} st (Disconnect {serveri} (MkPID pid)) k

430432 = do v <- sendToThread pid 0 (MsgQuery {iface=serveri} {hs}