acb2efb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

prim__vm needs to take a World reference

acb2efbEdwin Brady10 years ago

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

compare with master

unifiedsplit

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

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

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

15sendToThread {a} dest channel val

16+ = do me <- getMyVM

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

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

17− prim__vm channel dest (MkRaw val)

18+ me channel dest (MkRaw val)

19||| Check for messages in the process inbox

20||| Check for messages in the process inbox

20checkMsgs : IO Bool

21checkMsgs : IO Bool

22+checkMsgs = do me <- getMyVM

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

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

22− prim__vm

23 null <- nullPtr msgs

24 null <- nullPtr msgs

24 pure (not null)

25 pure (not null)

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

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

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

28checkMsgsTimeout : Int -> IO Bool

29checkMsgsTimeout : Int -> IO Bool

29checkMsgsTimeout timeout

30checkMsgsTimeout timeout

31+ = do me <- getMyVM

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

32+ msgs <- foreign FFI_C "idris_checkMessagesTimeout"

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

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

32 null <- nullPtr msgs

34 null <- nullPtr msgs

33 pure (not null)

35 pure (not null)

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

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

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

45||| of sender and new channel id.

47||| of sender and new channel id.

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

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

49+listenMsgs = do me <- getMyVM

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

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

48− prim__vm

51+ me

49 null <- nullPtr msg

52 null <- nullPtr msg

50 if null then pure Nothing

53 if null then pure Nothing

51 else do s_id <- sender msg

54 else do s_id <- sender msg

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

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

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

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

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

58checkMsgsFrom sender channel

61checkMsgsFrom sender channel

62+ = do me <- getMyVM

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

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

60− prim__vm channel sender

64+ me channel sender

61 null <- nullPtr msgs

65 null <- nullPtr msgs

62 pure (not null)

66 pure (not null)

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

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

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

67||| a type safe wrapper.

71||| a type safe wrapper.

68getMsg : IO a

72getMsg : IO a

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

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

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

70− (Ptr -> IO Ptr) prim__vm

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

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

72 pure x

76 pure x

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

77||| a type safe wrapper.

81||| a type safe wrapper.

78getMsgWithSender : IO (Ptr, Int, a)

82getMsgWithSender : IO (Ptr, Int, a)

79getMsgWithSender {a}

83getMsgWithSender {a}

84+ = do me <- getMyVM

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

85+ m <- foreign FFI_C "idris_recvMessage"

81− (Ptr -> IO Ptr) prim__vm

86+ (Ptr -> IO Ptr) me

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

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

83 vm <- sender m

88 vm <- sender m

84 chan <- channel_id m

89 chan <- channel_id m

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

90||| alive

95||| alive

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

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

92getMsgFrom {a} sender channel

97getMsgFrom {a} sender channel

98+ = do me <- getMyVM

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

99+ m <- foreign FFI_C "idris_recvMessageFrom"

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

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

95 null <- nullPtr m

101 null <- nullPtr m

96 if null

102 if null

97 then pure Nothing

103 then pure Nothing

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

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

32||| Get current process ID

33export

34myID : Process msg (ProcID msg)

35+myID = Lift (do me <- getMyVM

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

36+ pure (MkPID me))

37||| Send a message to another process

38||| Send a message to another process

38||| Returns whether the send was unsuccessful.

39||| Returns whether the send was unsuccessful.

39export

40export

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

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

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

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

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

42 pure (x /= 0))

44 pure (x /= 0))

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

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

libs/prelude/Builtins.idr+1−1

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

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

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

206

207−%extern prim__vm : Ptr

207+%extern prim__vm : prim__WorldType -> Ptr

208%extern prim__stdin : Ptr

209%extern prim__stdout : Ptr

210%extern prim__stderr : Ptr

libs/prelude/IO.idr+6−2

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

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

206

207prim_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

209

210namespace IO

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

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

214 (\ x => prim_io_pure x)))

215 (\x => prim_io_pure x))

216

217+ getMyVM : IO' l Ptr

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

219+

217 forceGC : IO ()

220 forceGC : IO ()

221+ forceGC = io_bind getMyVM

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

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

219

223

220 getErrno : IO Int

224 getErrno : IO Int

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

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

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

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

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

42getFileError : IO FileError

43+getFileError = do vm <- getMyVM

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

44+ MkRaw err <- foreign FFI_C "idris_mkFileError"

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

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

45 pure err

46 pure err

47Show FileError where

48Show FileError where

src/IRTS/CodegenC.hs+1−1

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

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

628 ++ "),GETSTR("

629 ++ creg s ++ "))))"

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

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

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

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

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

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

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

634

633

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

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

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

637 = 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

14 pure ()

16ping : Ptr -> IO ()

17+ping thread = do me <- getMyVM

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

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

18 pure ()

19 pure ()

20pingpong : IO ()

21pingpong : IO ()

test/proofsearch002/Process.idr+8−6

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

378 k (MkPID ptr) st

379

380eval st (Work proc cont) k

381+ = do me <- getMyVM

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

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

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

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

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

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

384

385

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

420 k val st''')

421 k val st''')

421

422

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

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

424+ = do me <- getMyVM

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

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

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

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

425− ConnectMsg)

427+ ConnectMsg)

426− -- TODO: Wait for ACK

428+ -- TODO: Wait for ACK

427− k (v == 1) st

429+ k (v == 1) st

428

430

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

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

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

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