From a4aae0a656582fe9a69f6ffee0a819d36076975c Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sun, 24 Nov 2024 23:47:11 -0600 Subject: [PATCH 01/53] Initial implementation of non-blocking version of blodwen-channel-get. --- support/chez/support.ss | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/support/chez/support.ss b/support/chez/support.ss index 8162585b87..2487c2789a 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -439,6 +439,30 @@ (condition-signal read-cv) the-val)) +(define (blodwen-channel-get-non-blocking ty chan) + (if (mutex-acquire (channel-read-mut chan)) + (let* ([val-box (channel-val-box chan)] + [the-val (unbox val-box)] + ) + (if (eq? the-val #f) + (#f) + ((channel-get-while-helper chan) + (let* ([val-box (channel-val-box chan)] + [read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)] + [the-val (unbox val-box)] + ) + (set-box! val-box '()) + (set-box! read-box #t) + (mutex-release (channel-read-mut chan)) + (condition-signal read-cv) + the-val)) + ) + ) + (#f) + ) +) + ;; Mutex (define (blodwen-make-mutex) From f26182148a59c59bde20f46d9896ab6996708504 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sun, 24 Nov 2024 23:57:39 -0600 Subject: [PATCH 02/53] Adding channelGetNonBlocking function to System.Concurrency.idr (non-compiling). --- libs/base/System/Concurrency.idr | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index d6ba41cc33..f8129763cb 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -187,6 +187,8 @@ data Channel : Type -> Type where [external] prim__makeChannel : PrimIO (Channel a) %foreign "scheme:blodwen-channel-get" prim__channelGet : Channel a -> PrimIO a +%foreign "scheme:blodwen-channel-get-non-blocking" +prim__channelGetNonBlocking : Channel a -> Maybe (PrimIO a) %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () @@ -208,6 +210,14 @@ export channelGet : HasIO io => (chan : Channel a) -> io a channelGet chan = primIO (prim__channelGet chan) +||| Non-blocking version of channelGet. Returns `Nothing` if +||| either the mutex could not be acquired or the box was empty. +||| +||| @ chan the channel to receive on +export +channelGetNonBlocking : HasIO io => (chan : Channel a) -> Maybe (io a) +channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) + ||| Puts a value on the given channel. ||| ||| @ chan the `Channel` to send the value over From 68ecf8b655eff571f6f29e5724fdb2bfefdab61c Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 00:03:44 -0600 Subject: [PATCH 03/53] Adding matching mutex-release call to initial mutex-acquire call. --- support/chez/support.ss | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 2487c2789a..f9a5168633 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -441,7 +441,8 @@ (define (blodwen-channel-get-non-blocking ty chan) (if (mutex-acquire (channel-read-mut chan)) - (let* ([val-box (channel-val-box chan)] + ((mutex-release (channel-read-mut chan)) + (let* ([val-box (channel-val-box chan)] [the-val (unbox val-box)] ) (if (eq? the-val #f) @@ -458,6 +459,7 @@ (condition-signal read-cv) the-val)) ) + ) ) (#f) ) From 89f7991e413274f5a15937f3c77c31c65cd5dfe7 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 00:10:49 -0600 Subject: [PATCH 04/53] Fixing indentation in blodwen-channel-get-non-blocking. --- support/chez/support.ss | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index f9a5168633..e9da73aadb 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -443,22 +443,22 @@ (if (mutex-acquire (channel-read-mut chan)) ((mutex-release (channel-read-mut chan)) (let* ([val-box (channel-val-box chan)] - [the-val (unbox val-box)] - ) - (if (eq? the-val #f) - (#f) - ((channel-get-while-helper chan) - (let* ([val-box (channel-val-box chan)] - [read-box (channel-read-box chan)] - [read-cv (channel-read-cv chan)] - [the-val (unbox val-box)] - ) - (set-box! val-box '()) - (set-box! read-box #t) - (mutex-release (channel-read-mut chan)) - (condition-signal read-cv) - the-val)) - ) + [the-val (unbox val-box)] + ) + (if (eq? the-val #f) + (#f) + ((channel-get-while-helper chan) + (let* ([val-box (channel-val-box chan)] + [read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)] + [the-val (unbox val-box)] + ) + (set-box! val-box '()) + (set-box! read-box #t) + (mutex-release (channel-read-mut chan)) + (condition-signal read-cv) + the-val)) + ) ) ) (#f) From 9381947634177728fb6f0ddc14df3e6964ad8372 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 00:15:34 -0600 Subject: [PATCH 05/53] Adding matching mutex-release call to initial mutex-acquire call (again). --- support/chez/support.ss | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index e9da73aadb..38aba67643 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -461,7 +461,9 @@ ) ) ) - (#f) + ((mutex-release (channel-read-mut chan)) + (#f) + ) ) ) From a5610fa22be6769e73194e04a159ef75f5618980 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 00:23:50 -0600 Subject: [PATCH 06/53] Fixing return values for blodwen-channel-get-non-blocking. --- support/chez/support.ss | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 38aba67643..01e10123ac 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -445,8 +445,8 @@ (let* ([val-box (channel-val-box chan)] [the-val (unbox val-box)] ) - (if (eq? the-val #f) - (#f) + (if (eq? the-val '()) + ('()) ((channel-get-while-helper chan) (let* ([val-box (channel-val-box chan)] [read-box (channel-read-box chan)] @@ -462,7 +462,7 @@ ) ) ((mutex-release (channel-read-mut chan)) - (#f) + ('()) ) ) ) From fb04471d2225c843c758340471255347d98f1d5f Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 00:46:28 -0600 Subject: [PATCH 07/53] Fixing extern type signature and channelGetNonBlocking function, along with return values of blodwen-channel-get-non-blocking. --- libs/base/System/Concurrency.idr | 13 ++++++++++--- support/chez/support.ss | 4 ++-- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index f8129763cb..949b3a17e7 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -188,7 +188,7 @@ prim__makeChannel : PrimIO (Channel a) %foreign "scheme:blodwen-channel-get" prim__channelGet : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-get-non-blocking" -prim__channelGetNonBlocking : Channel a -> Maybe (PrimIO a) +prim__channelGetNonBlocking : Channel a -> PrimIO (Either a Bool) %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () @@ -215,8 +215,15 @@ channelGet chan = primIO (prim__channelGet chan) ||| ||| @ chan the channel to receive on export -channelGetNonBlocking : HasIO io => (chan : Channel a) -> Maybe (io a) -channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) +channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a) +channelGetNonBlocking chan = + case !(primIO (prim__channelGetNonBlocking chan)) of + Right False => + pure Nothing + Right True => + pure Nothing + Left x => + pure $ Just x ||| Puts a value on the given channel. ||| diff --git a/support/chez/support.ss b/support/chez/support.ss index 01e10123ac..b788866a20 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -446,7 +446,7 @@ [the-val (unbox val-box)] ) (if (eq? the-val '()) - ('()) + (#f) ((channel-get-while-helper chan) (let* ([val-box (channel-val-box chan)] [read-box (channel-read-box chan)] @@ -462,7 +462,7 @@ ) ) ((mutex-release (channel-read-mut chan)) - ('()) + (#f) ) ) ) From 9a53f9a98e55b002d86688d946fd87338d4a32c1 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 00:59:07 -0600 Subject: [PATCH 08/53] Removing blocking aspect from blodwen-channel-get-non-blocking. --- support/chez/support.ss | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index b788866a20..6f58d6ca2b 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -447,8 +447,7 @@ ) (if (eq? the-val '()) (#f) - ((channel-get-while-helper chan) - (let* ([val-box (channel-val-box chan)] + ((let* ([val-box (channel-val-box chan)] [read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)] [the-val (unbox val-box)] From 818c5ba869373bd00c193ea153aba9f4ba536d46 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 01:00:24 -0600 Subject: [PATCH 09/53] Fixing styling of blodwen-channel-get-non-blocking. --- support/chez/support.ss | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 6f58d6ca2b..e5d8cafed9 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -457,14 +457,10 @@ (mutex-release (channel-read-mut chan)) (condition-signal read-cv) the-val)) - ) - ) - ) + ))) ((mutex-release (channel-read-mut chan)) (#f) - ) - ) -) + ))) ;; Mutex From fe1dd2d6f86036e5c9eba3a51e8ae4ab168afa6b Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 09:30:29 -0600 Subject: [PATCH 10/53] Removing extra mutex-release call. --- support/chez/support.ss | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index e5d8cafed9..0296912159 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -441,8 +441,7 @@ (define (blodwen-channel-get-non-blocking ty chan) (if (mutex-acquire (channel-read-mut chan)) - ((mutex-release (channel-read-mut chan)) - (let* ([val-box (channel-val-box chan)] + ((let* ([val-box (channel-val-box chan)] [the-val (unbox val-box)] ) (if (eq? the-val '()) From 8754137a6d5ac9df203f5da7df99d842db02ed09 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 09:47:29 -0600 Subject: [PATCH 11/53] Removing duplicate val calls. --- support/chez/support.ss | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 0296912159..b3924acc63 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -446,10 +446,8 @@ ) (if (eq? the-val '()) (#f) - ((let* ([val-box (channel-val-box chan)] - [read-box (channel-read-box chan)] + ((let* ([read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)] - [the-val (unbox val-box)] ) (set-box! val-box '()) (set-box! read-box #t) From 7936ae1d1606890cee0585c090bd795010efea85 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 11:25:10 -0600 Subject: [PATCH 12/53] Fixing return type. --- support/chez/support.ss | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index b3924acc63..15d3161367 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -445,7 +445,7 @@ [the-val (unbox val-box)] ) (if (eq? the-val '()) - (#f) + ('()) ((let* ([read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)] ) @@ -456,7 +456,7 @@ the-val)) ))) ((mutex-release (channel-read-mut chan)) - (#f) + ('()) ))) ;; Mutex From 45dfec5f5541f26516816cd84532a630d2713daa Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 11:37:25 -0600 Subject: [PATCH 13/53] Fixing return type. --- support/chez/support.ss | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 15d3161367..5104b06d83 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -445,7 +445,7 @@ [the-val (unbox val-box)] ) (if (eq? the-val '()) - ('()) + (void) ((let* ([read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)] ) @@ -456,7 +456,7 @@ the-val)) ))) ((mutex-release (channel-read-mut chan)) - ('()) + (void) ))) ;; Mutex From 21e877a16d3e0413f96e6ae954e42ab6ff86572d Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 11:38:36 -0600 Subject: [PATCH 14/53] Fixing channelGetNonBlocking. --- libs/base/System/Concurrency.idr | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 949b3a17e7..96be3596b5 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -188,7 +188,7 @@ prim__makeChannel : PrimIO (Channel a) %foreign "scheme:blodwen-channel-get" prim__channelGet : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-get-non-blocking" -prim__channelGetNonBlocking : Channel a -> PrimIO (Either a Bool) +prim__channelGetNonBlocking : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () @@ -215,15 +215,16 @@ channelGet chan = primIO (prim__channelGet chan) ||| ||| @ chan the channel to receive on export -channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a) -channelGetNonBlocking chan = - case !(primIO (prim__channelGetNonBlocking chan)) of +channelGetNonBlocking : HasIO io => (chan : Channel a) -> io a +channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) + {- Right False => pure Nothing Right True => pure Nothing Left x => pure $ Just x + -} ||| Puts a value on the given channel. ||| From 82defeec0baf5c3e6e64c4c47351a9781d0a0831 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 11:42:55 -0600 Subject: [PATCH 15/53] Reverting return type fix. --- support/chez/support.ss | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 5104b06d83..15d3161367 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -445,7 +445,7 @@ [the-val (unbox val-box)] ) (if (eq? the-val '()) - (void) + ('()) ((let* ([read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)] ) @@ -456,7 +456,7 @@ the-val)) ))) ((mutex-release (channel-read-mut chan)) - (void) + ('()) ))) ;; Mutex From af8f499c31496fc05f4a105c3ff71c2ed307e3b5 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 11:45:20 -0600 Subject: [PATCH 16/53] Removing unnecessary comments. --- libs/base/System/Concurrency.idr | 8 -------- 1 file changed, 8 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 96be3596b5..4abe6668ca 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -217,14 +217,6 @@ channelGet chan = primIO (prim__channelGet chan) export channelGetNonBlocking : HasIO io => (chan : Channel a) -> io a channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) - {- - Right False => - pure Nothing - Right True => - pure Nothing - Left x => - pure $ Just x - -} ||| Puts a value on the given channel. ||| From dbf8e8325acf215b229264eb8a56db7b32bced1a Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 12:23:30 -0600 Subject: [PATCH 17/53] Remove incorrect documentation. --- libs/base/System/Concurrency.idr | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 4abe6668ca..9110757e76 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -210,13 +210,19 @@ export channelGet : HasIO io => (chan : Channel a) -> io a channelGet chan = primIO (prim__channelGet chan) -||| Non-blocking version of channelGet. Returns `Nothing` if -||| either the mutex could not be acquired or the box was empty. +||| Non-blocking version of channelGet. ||| ||| @ chan the channel to receive on export channelGetNonBlocking : HasIO io => (chan : Channel a) -> io a channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) +{- + case !(primIO (prim__channelGetNonBlocking chan)) of + [] => + pure Nothing + (x :: xs) => + pure $ Just (x :: xs) + -} ||| Puts a value on the given channel. ||| From fadb1e94065e9f49d8fa71e915ee0333b5a0dc76 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 12:43:29 -0600 Subject: [PATCH 18/53] Altering blodwen-channel-get-non-blocking to error when mutex cant be acquired, or the box is empty. --- support/chez/support.ss | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 15d3161367..5c3ad9983a 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -445,7 +445,8 @@ [the-val (unbox val-box)] ) (if (eq? the-val '()) - ('()) + ((mutex-release (channel-read-mut chan)) + (error blodwen-channel-get-non-blocking "empty channel")) ((let* ([read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)] ) @@ -456,8 +457,8 @@ the-val)) ))) ((mutex-release (channel-read-mut chan)) - ('()) - ))) + (error blodwen-channel-get-non-blocking "could not acquire mutex")) + )) ;; Mutex From fb8fb26ea7b27b985b9e4228b038e36fd01aca7b Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 12:44:31 -0600 Subject: [PATCH 19/53] Cleaning up commented out code. --- libs/base/System/Concurrency.idr | 7 ------- 1 file changed, 7 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 9110757e76..991968470b 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -216,13 +216,6 @@ channelGet chan = primIO (prim__channelGet chan) export channelGetNonBlocking : HasIO io => (chan : Channel a) -> io a channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) -{- - case !(primIO (prim__channelGetNonBlocking chan)) of - [] => - pure Nothing - (x :: xs) => - pure $ Just (x :: xs) - -} ||| Puts a value on the given channel. ||| From 2b6077b623db09b4c4477b224e409fbc89272934 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 15:38:59 -0600 Subject: [PATCH 20/53] Adding blodwen-channel-check scheme function to enable correct handling of channelGetNonBlocking. --- libs/base/System/Concurrency.idr | 12 ++++++++++-- support/chez/support.ss | 9 +++++++-- 2 files changed, 17 insertions(+), 4 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 991968470b..583a2ebf9f 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -191,6 +191,8 @@ prim__channelGet : Channel a -> PrimIO a prim__channelGetNonBlocking : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () +%foreign "scheme:blodwen-channel-check" +prim__channelCheck : a -> PrimIO Bool ||| Creates and returns a new `Channel`. ||| @@ -214,8 +216,14 @@ channelGet chan = primIO (prim__channelGet chan) ||| ||| @ chan the channel to receive on export -channelGetNonBlocking : HasIO io => (chan : Channel a) -> io a -channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) +channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a) +channelGetNonBlocking chan = do + c <- primIO (prim__channelGetNonBlocking chan) + case !(primIO (prim__channelCheck c)) of + True => + pure Nothing + False => + pure $ Just c ||| Puts a value on the given channel. ||| diff --git a/support/chez/support.ss b/support/chez/support.ss index 5c3ad9983a..22e1784453 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -446,7 +446,7 @@ ) (if (eq? the-val '()) ((mutex-release (channel-read-mut chan)) - (error blodwen-channel-get-non-blocking "empty channel")) + '()) ((let* ([read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)] ) @@ -457,9 +457,14 @@ the-val)) ))) ((mutex-release (channel-read-mut chan)) - (error blodwen-channel-get-non-blocking "could not acquire mutex")) + '()) )) +(define (blodwen-channel-check result) + (if (eq? result '()) + #t ; Return #t if the result is empty + #f)) ; Return #f if the result is a value + ;; Mutex (define (blodwen-make-mutex) From f8c24af333885a3f849e5cee292eb995ed27563a Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 21:31:04 -0600 Subject: [PATCH 21/53] Optimizing blodwen-channel-get-non-blocking. --- support/chez/support.ss | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 22e1784453..5776ec7e55 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -440,7 +440,7 @@ the-val)) (define (blodwen-channel-get-non-blocking ty chan) - (if (mutex-acquire (channel-read-mut chan)) + (if (mutex-acquire (channel-read-mut chan) #f) ((let* ([val-box (channel-val-box chan)] [the-val (unbox val-box)] ) @@ -456,14 +456,14 @@ (condition-signal read-cv) the-val)) ))) - ((mutex-release (channel-read-mut chan)) - '()) + ('()) )) + (define (blodwen-channel-check result) (if (eq? result '()) - #t ; Return #t if the result is empty - #f)) ; Return #f if the result is a value + 0 ; Return 0 if the result is empty + 1)) ; Return 1 if the result is a value ;; Mutex From 9e7ba4855f476b1c33bf289e8a42c662e9ee557d Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 25 Nov 2024 22:40:49 -0600 Subject: [PATCH 22/53] Changing Boolean comparision to Int (compatible with expected Prim types). --- libs/base/System/Concurrency.idr | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 583a2ebf9f..5da1148105 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -192,7 +192,7 @@ prim__channelGetNonBlocking : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () %foreign "scheme:blodwen-channel-check" -prim__channelCheck : a -> PrimIO Bool +prim__channelCheck : a -> PrimIO Int ||| Creates and returns a new `Channel`. ||| @@ -220,9 +220,9 @@ channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a) channelGetNonBlocking chan = do c <- primIO (prim__channelGetNonBlocking chan) case !(primIO (prim__channelCheck c)) of - True => + 0 => pure Nothing - False => + _ => pure $ Just c ||| Puts a value on the given channel. From 0684a10f254bd072cdba4d85fc008a95f21decd4 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 00:17:33 -0600 Subject: [PATCH 23/53] Adding decoding support for channelGetNonBlocking. --- libs/base/System/Concurrency.idr | 197 ++++++++++++++++++++++++++++--- support/chez/support.ss | 9 +- 2 files changed, 183 insertions(+), 23 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 5da1148105..ac02c10444 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -72,19 +72,15 @@ data Condition : Type where [external] %foreign "scheme,racket:blodwen-make-cv" "scheme,chez:blodwen-make-condition" prim__makeCondition : PrimIO Condition - %foreign "scheme,racket:blodwen-cv-wait" "scheme,chez:blodwen-condition-wait" prim__conditionWait : Condition -> Mutex -> PrimIO () - %foreign "scheme,chez:blodwen-condition-wait-timeout" -- "scheme,racket:blodwen-cv-wait-timeout" prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO () - %foreign "scheme,racket:blodwen-cv-signal" "scheme,chez:blodwen-condition-signal" prim__conditionSignal : Condition -> PrimIO () - %foreign "scheme,racket:blodwen-cv-broadcast" "scheme,chez:blodwen-condition-broadcast" prim__conditionBroadcast : Condition -> PrimIO () @@ -183,16 +179,170 @@ barrierWait barrier = primIO (prim__barrierWait barrier) export data Channel : Type -> Type where [external] +data ChannelObj : Type where [external] + +data ChannelSchemeObj : Type where + Null : ChannelSchemeObj + Cons : ChannelSchemeObj -> ChannelSchemeObj -> ChannelSchemeObj + IntegerVal : Integer -> ChannelSchemeObj + FloatVal : Double -> ChannelSchemeObj + StringVal : String -> ChannelSchemeObj + CharVal : Char -> ChannelSchemeObj + Symbol : String -> ChannelSchemeObj + Box : ChannelSchemeObj -> ChannelSchemeObj + Vector : Integer -> List ChannelSchemeObj -> ChannelSchemeObj + Procedure : ChannelObj -> ChannelSchemeObj + +export +interface Scheme a where + fromScheme : ChannelSchemeObj -> Maybe a + +export +Scheme Integer where + fromScheme (IntegerVal x) = Just x + fromScheme _ = Nothing + +export +Scheme Int where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Int8 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Int16 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Int32 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Int64 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Bits8 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Bits16 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Bits32 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Bits64 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme String where + fromScheme (StringVal x) = Just x + fromScheme _ = Nothing + +export +Scheme Double where + fromScheme (FloatVal x) = Just x + fromScheme _ = Nothing + +export +Scheme Char where + fromScheme (CharVal x) = Just x + fromScheme _ = Nothing + +export +Scheme Bool where + fromScheme (IntegerVal 0) = Just False + fromScheme (IntegerVal 1) = Just True + fromScheme _ = Nothing + +export +Scheme a => Scheme (List a) where + fromScheme Null = Just [] + fromScheme (Cons x xs) = Just $ !(fromScheme x) :: !(fromScheme xs) + fromScheme _ = Nothing + +export +(Scheme a, Scheme b) => Scheme (a, b) where + fromScheme (Cons x y) = Just (!(fromScheme x), !(fromScheme y)) + fromScheme _ = Nothing + +export +Scheme a => Scheme (Maybe a) where + fromScheme Null = Just Nothing + fromScheme (Box x) = Just $ Just !(fromScheme x) + fromScheme _ = Nothing + +%foreign "scheme:blodwen-is-number" +prim_isNumber : ChannelObj -> Int +%foreign "scheme:blodwen-is-integer" +prim_isInteger : ChannelObj -> Int +%foreign "scheme:blodwen-is-float" +prim_isFloat : ChannelObj -> Int +%foreign "scheme:blodwen-is-char" +prim_isChar : ChannelObj -> Int +%foreign "scheme:blodwen-is-string" +prim_isString : ChannelObj -> Int +%foreign "scheme:blodwen-is-procedure" +prim_isProcedure : ChannelObj -> Int +%foreign "scheme:blodwen-is-symbol" +prim_isSymbol : ChannelObj -> Int +%foreign "scheme:blodwen-is-nil" +prim_isNil : ChannelObj -> Int +%foreign "scheme:blodwen-is-pair" +prim_isPair : ChannelObj -> Int +%foreign "scheme:blodwen-is-vector" +prim_isVector : ChannelObj -> Int +%foreign "scheme:blodwen-id" +unsafeGetInteger : ChannelObj -> Integer +%foreign "scheme:blodwen-id" +unsafeGetString : ChannelObj -> String +%foreign "scheme:blodwen-id" +unsafeGetFloat : ChannelObj -> Double +%foreign "scheme:blodwen-id" +unsafeGetChar : ChannelObj -> Char +%foreign "scheme:car" +unsafeFst : ChannelObj -> ChannelObj +%foreign "scheme:cdr" +unsafeSnd : ChannelObj -> ChannelObj +%foreign "scheme:blodwen-vector-ref" +unsafeVectorRef : ChannelObj -> Integer -> ChannelObj +%foreign "scheme:blodwen-unbox" +unsafeUnbox : ChannelObj -> ChannelObj +%foreign "scheme:blodwen-vector-length" +unsafeVectorLength : ChannelObj -> Integer +%foreign "scheme:blodwen-vector-list" +unsafeVectorToList : ChannelObj -> List ChannelObj +%foreign "scheme:blodwen-read-symbol" +unsafeReadSymbol : ChannelObj -> String +%foreign "scheme:blodwen-is-box" +prim_isBox : ChannelObj -> Int %foreign "scheme:blodwen-make-channel" prim__makeChannel : PrimIO (Channel a) %foreign "scheme:blodwen-channel-get" prim__channelGet : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-get-non-blocking" -prim__channelGetNonBlocking : Channel a -> PrimIO a +prim__channelGetNonBlocking : Channel a -> PrimIO ChannelObj +%foreign "scheme:blodwen-unbox" +prim__channelUnbox : ChannelObj -> a +%foreign "scheme:blodwen-channel-eval-okay" +prim__channelEvalOkay : ChannelObj -> Int +%foreign "scheme:blodwen-eval-chan-result" +prim__chanEvalResult : ChannelObj -> a %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () -%foreign "scheme:blodwen-channel-check" -prim__channelCheck : a -> PrimIO Int ||| Creates and returns a new `Channel`. ||| @@ -215,15 +365,32 @@ channelGet chan = primIO (prim__channelGet chan) ||| Non-blocking version of channelGet. ||| ||| @ chan the channel to receive on +partial export -channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a) -channelGetNonBlocking chan = do - c <- primIO (prim__channelGetNonBlocking chan) - case !(primIO (prim__channelCheck c)) of - 0 => - pure Nothing - _ => - pure $ Just c +channelGetNonBlocking : HasIO io => Scheme a => (chan : Channel a) -> io (Maybe a) +channelGetNonBlocking chan = + pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetNonBlocking chan)) + where + decodeObj : ChannelObj -> ChannelSchemeObj + decodeObj obj = + if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) + else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) + (readVector (unsafeVectorLength obj) 1 obj) + else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) + (decodeObj (unsafeSnd obj)) + else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) + else if prim_isString obj == 1 then StringVal (unsafeGetString obj) + else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) + else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) + else if prim_isProcedure obj == 1 then Procedure obj + else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) + else Null + where + readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj + readVector len i obj + = if len == i + then [] + else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj ||| Puts a value on the given channel. ||| diff --git a/support/chez/support.ss b/support/chez/support.ss index 5776ec7e55..c7afce2fd9 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -456,15 +456,9 @@ (condition-signal read-cv) the-val)) ))) - ('()) + '() )) - -(define (blodwen-channel-check result) - (if (eq? result '()) - 0 ; Return 0 if the result is empty - 1)) ; Return 1 if the result is a value - ;; Mutex (define (blodwen-make-mutex) @@ -525,7 +519,6 @@ (define (blodwen-clock-second time) (time-second time)) (define (blodwen-clock-nanosecond time) (time-nanosecond time)) - (define (blodwen-arg-count) (length (command-line))) From 56d42bd649a508fe5715a2986e6227c888d1f91d Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 00:22:49 -0600 Subject: [PATCH 24/53] Removing extra %foreign pragmas. --- libs/base/System/Concurrency.idr | 6 ------ 1 file changed, 6 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index ac02c10444..0d2152e889 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -335,12 +335,6 @@ prim__makeChannel : PrimIO (Channel a) prim__channelGet : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-get-non-blocking" prim__channelGetNonBlocking : Channel a -> PrimIO ChannelObj -%foreign "scheme:blodwen-unbox" -prim__channelUnbox : ChannelObj -> a -%foreign "scheme:blodwen-channel-eval-okay" -prim__channelEvalOkay : ChannelObj -> Int -%foreign "scheme:blodwen-eval-chan-result" -prim__chanEvalResult : ChannelObj -> a %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () From e8a39f316cb23b5d53434bab813333ecb11397fb Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 00:37:01 -0600 Subject: [PATCH 25/53] Removing extra %foreign. --- libs/base/System/Concurrency.idr | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 0d2152e889..dcd4dd1c37 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -285,8 +285,6 @@ Scheme a => Scheme (Maybe a) where fromScheme (Box x) = Just $ Just !(fromScheme x) fromScheme _ = Nothing -%foreign "scheme:blodwen-is-number" -prim_isNumber : ChannelObj -> Int %foreign "scheme:blodwen-is-integer" prim_isInteger : ChannelObj -> Int %foreign "scheme:blodwen-is-float" @@ -369,9 +367,9 @@ channelGetNonBlocking chan = decodeObj obj = if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) - (readVector (unsafeVectorLength obj) 1 obj) + (readVector (unsafeVectorLength obj) 1 obj) else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) - (decodeObj (unsafeSnd obj)) + (decodeObj (unsafeSnd obj)) else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) else if prim_isString obj == 1 then StringVal (unsafeGetString obj) else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) From 5a18386ecf7ea7c52eda3ab5f8b75aea97e7cb65 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 12:02:58 -0600 Subject: [PATCH 26/53] Fixing blodwen-channel-get-non-blocking by removing extra set of parentheses around let*. --- support/chez/support.ss | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index c7afce2fd9..f2f3ac686f 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -441,22 +441,22 @@ (define (blodwen-channel-get-non-blocking ty chan) (if (mutex-acquire (channel-read-mut chan) #f) - ((let* ([val-box (channel-val-box chan)] - [the-val (unbox val-box)] - ) + (let* ([val-box (channel-val-box chan)] + [the-val (unbox val-box)] + ) (if (eq? the-val '()) ((mutex-release (channel-read-mut chan)) - '()) - ((let* ([read-box (channel-read-box chan)] - [read-cv (channel-read-cv chan)] - ) + 0) + (let* ([read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)] + ) (set-box! val-box '()) (set-box! read-box #t) (mutex-release (channel-read-mut chan)) (condition-signal read-cv) - the-val)) - ))) - '() + the-val) + )) + 0 )) ;; Mutex From 6e8c4a59739407ac7a9e48f767bc4655e9240454 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 12:04:40 -0600 Subject: [PATCH 27/53] Adding channelGetNonBlocking test. --- tests/allschemes/channels007/Main.idr | 23 +++++++++++++++++++++++ tests/allschemes/channels007/expected | 2 ++ tests/allschemes/channels007/run | 3 +++ 3 files changed, 28 insertions(+) create mode 100644 tests/allschemes/channels007/Main.idr create mode 100644 tests/allschemes/channels007/expected create mode 100644 tests/allschemes/channels007/run diff --git a/tests/allschemes/channels007/Main.idr b/tests/allschemes/channels007/Main.idr new file mode 100644 index 0000000000..fadcada109 --- /dev/null +++ b/tests/allschemes/channels007/Main.idr @@ -0,0 +1,23 @@ +import System.Concurrency +import System + +-- Test that using channelGetNonBlocking works as expected. +main : IO () +main = do + chan <- makeChannel + threadID <- fork $ do + channelPut chan "Hello" + channelPut chan "Goodbye" + sleep 1 + case !(channelGetNonBlocking chan) of + Nothing => + putStrLn "Nothing" + Just val' => + putStrLn val' + case !(channelGetNonBlocking chan) of + Nothing => + putStrLn "Nothing" + Just val' => + putStrLn val' + sleep 1 + diff --git a/tests/allschemes/channels007/expected b/tests/allschemes/channels007/expected new file mode 100644 index 0000000000..c86756d193 --- /dev/null +++ b/tests/allschemes/channels007/expected @@ -0,0 +1,2 @@ +Hello +Goodbye diff --git a/tests/allschemes/channels007/run b/tests/allschemes/channels007/run new file mode 100644 index 0000000000..c6e6f2ab79 --- /dev/null +++ b/tests/allschemes/channels007/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run Main.idr From 0c4b2dd14668914b64cc3f69b05b95d49f88a08a Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 13:27:09 -0600 Subject: [PATCH 28/53] Changing 0 to () for the return on failed mutex acquisition or an empty box in blodwen-channel-get-non-blocking. --- support/chez/support.ss | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index f2f3ac686f..769219ce4d 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -446,7 +446,7 @@ ) (if (eq? the-val '()) ((mutex-release (channel-read-mut chan)) - 0) + '()) (let* ([read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)] ) @@ -456,7 +456,7 @@ (condition-signal read-cv) the-val) )) - 0 + '() )) ;; Mutex From 042799d225565c2d632a6bda9312ddb5a29a1a5e Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 13:31:17 -0600 Subject: [PATCH 29/53] Removing extraneous whitespace. --- libs/base/System/Concurrency.idr | 2 +- tests/allschemes/channels007/Main.idr | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index dcd4dd1c37..32715f5d62 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -363,7 +363,7 @@ channelGetNonBlocking : HasIO io => Scheme a => (chan : Channel a) -> io (Maybe channelGetNonBlocking chan = pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetNonBlocking chan)) where - decodeObj : ChannelObj -> ChannelSchemeObj + decodeObj : ChannelObj -> ChannelSchemeObj decodeObj obj = if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) diff --git a/tests/allschemes/channels007/Main.idr b/tests/allschemes/channels007/Main.idr index fadcada109..0512bc0ed3 100644 --- a/tests/allschemes/channels007/Main.idr +++ b/tests/allschemes/channels007/Main.idr @@ -1,7 +1,7 @@ import System.Concurrency import System --- Test that using channelGetNonBlocking works as expected. +-- Test that using channelGetNonBlocking works as expected. main : IO () main = do chan <- makeChannel From 636ca501321499eaa334d3ac7ed9ed5e88afe9a1 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 13:50:21 -0600 Subject: [PATCH 30/53] Removing unnecessary scheme decoding. --- libs/base/System/Concurrency.idr | 179 ++----------------------------- 1 file changed, 7 insertions(+), 172 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 32715f5d62..e1f179bc0f 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -179,160 +179,12 @@ barrierWait barrier = primIO (prim__barrierWait barrier) export data Channel : Type -> Type where [external] -data ChannelObj : Type where [external] - -data ChannelSchemeObj : Type where - Null : ChannelSchemeObj - Cons : ChannelSchemeObj -> ChannelSchemeObj -> ChannelSchemeObj - IntegerVal : Integer -> ChannelSchemeObj - FloatVal : Double -> ChannelSchemeObj - StringVal : String -> ChannelSchemeObj - CharVal : Char -> ChannelSchemeObj - Symbol : String -> ChannelSchemeObj - Box : ChannelSchemeObj -> ChannelSchemeObj - Vector : Integer -> List ChannelSchemeObj -> ChannelSchemeObj - Procedure : ChannelObj -> ChannelSchemeObj - -export -interface Scheme a where - fromScheme : ChannelSchemeObj -> Maybe a - -export -Scheme Integer where - fromScheme (IntegerVal x) = Just x - fromScheme _ = Nothing - -export -Scheme Int where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme Int8 where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme Int16 where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme Int32 where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme Int64 where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme Bits8 where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme Bits16 where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme Bits32 where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme Bits64 where - fromScheme (IntegerVal x) = Just (cast x) - fromScheme _ = Nothing - -export -Scheme String where - fromScheme (StringVal x) = Just x - fromScheme _ = Nothing - -export -Scheme Double where - fromScheme (FloatVal x) = Just x - fromScheme _ = Nothing - -export -Scheme Char where - fromScheme (CharVal x) = Just x - fromScheme _ = Nothing - -export -Scheme Bool where - fromScheme (IntegerVal 0) = Just False - fromScheme (IntegerVal 1) = Just True - fromScheme _ = Nothing - -export -Scheme a => Scheme (List a) where - fromScheme Null = Just [] - fromScheme (Cons x xs) = Just $ !(fromScheme x) :: !(fromScheme xs) - fromScheme _ = Nothing - -export -(Scheme a, Scheme b) => Scheme (a, b) where - fromScheme (Cons x y) = Just (!(fromScheme x), !(fromScheme y)) - fromScheme _ = Nothing - -export -Scheme a => Scheme (Maybe a) where - fromScheme Null = Just Nothing - fromScheme (Box x) = Just $ Just !(fromScheme x) - fromScheme _ = Nothing - -%foreign "scheme:blodwen-is-integer" -prim_isInteger : ChannelObj -> Int -%foreign "scheme:blodwen-is-float" -prim_isFloat : ChannelObj -> Int -%foreign "scheme:blodwen-is-char" -prim_isChar : ChannelObj -> Int -%foreign "scheme:blodwen-is-string" -prim_isString : ChannelObj -> Int -%foreign "scheme:blodwen-is-procedure" -prim_isProcedure : ChannelObj -> Int -%foreign "scheme:blodwen-is-symbol" -prim_isSymbol : ChannelObj -> Int -%foreign "scheme:blodwen-is-nil" -prim_isNil : ChannelObj -> Int -%foreign "scheme:blodwen-is-pair" -prim_isPair : ChannelObj -> Int -%foreign "scheme:blodwen-is-vector" -prim_isVector : ChannelObj -> Int -%foreign "scheme:blodwen-id" -unsafeGetInteger : ChannelObj -> Integer -%foreign "scheme:blodwen-id" -unsafeGetString : ChannelObj -> String -%foreign "scheme:blodwen-id" -unsafeGetFloat : ChannelObj -> Double -%foreign "scheme:blodwen-id" -unsafeGetChar : ChannelObj -> Char -%foreign "scheme:car" -unsafeFst : ChannelObj -> ChannelObj -%foreign "scheme:cdr" -unsafeSnd : ChannelObj -> ChannelObj -%foreign "scheme:blodwen-vector-ref" -unsafeVectorRef : ChannelObj -> Integer -> ChannelObj -%foreign "scheme:blodwen-unbox" -unsafeUnbox : ChannelObj -> ChannelObj -%foreign "scheme:blodwen-vector-length" -unsafeVectorLength : ChannelObj -> Integer -%foreign "scheme:blodwen-vector-list" -unsafeVectorToList : ChannelObj -> List ChannelObj -%foreign "scheme:blodwen-read-symbol" -unsafeReadSymbol : ChannelObj -> String -%foreign "scheme:blodwen-is-box" -prim_isBox : ChannelObj -> Int %foreign "scheme:blodwen-make-channel" prim__makeChannel : PrimIO (Channel a) %foreign "scheme:blodwen-channel-get" prim__channelGet : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-get-non-blocking" -prim__channelGetNonBlocking : Channel a -> PrimIO ChannelObj +prim__channelGetNonBlocking : Channel a -> PrimIO (Maybe a) %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () @@ -359,30 +211,13 @@ channelGet chan = primIO (prim__channelGet chan) ||| @ chan the channel to receive on partial export -channelGetNonBlocking : HasIO io => Scheme a => (chan : Channel a) -> io (Maybe a) +channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a) channelGetNonBlocking chan = - pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetNonBlocking chan)) - where - decodeObj : ChannelObj -> ChannelSchemeObj - decodeObj obj = - if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) - else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) - (readVector (unsafeVectorLength obj) 1 obj) - else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) - (decodeObj (unsafeSnd obj)) - else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) - else if prim_isString obj == 1 then StringVal (unsafeGetString obj) - else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) - else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) - else if prim_isProcedure obj == 1 then Procedure obj - else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) - else Null - where - readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj - readVector len i obj - = if len == i - then [] - else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj + case !(primIO (prim__channelGetNonBlocking chan)) of + Nothing => + pure Nothing + Just xs => + pure $ Just xs ||| Puts a value on the given channel. ||| From 2d1b96c4b9d9f6026d95995575c77f2c28ae6cc3 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 15:32:38 -0600 Subject: [PATCH 31/53] Fixing initial channelGetNonBlocking test. --- tests/allschemes/channels007/Main.idr | 6 ------ tests/allschemes/channels007/expected | 1 - 2 files changed, 7 deletions(-) diff --git a/tests/allschemes/channels007/Main.idr b/tests/allschemes/channels007/Main.idr index 0512bc0ed3..c422dfb816 100644 --- a/tests/allschemes/channels007/Main.idr +++ b/tests/allschemes/channels007/Main.idr @@ -7,13 +7,7 @@ main = do chan <- makeChannel threadID <- fork $ do channelPut chan "Hello" - channelPut chan "Goodbye" sleep 1 - case !(channelGetNonBlocking chan) of - Nothing => - putStrLn "Nothing" - Just val' => - putStrLn val' case !(channelGetNonBlocking chan) of Nothing => putStrLn "Nothing" diff --git a/tests/allschemes/channels007/expected b/tests/allschemes/channels007/expected index c86756d193..e965047ad7 100644 --- a/tests/allschemes/channels007/expected +++ b/tests/allschemes/channels007/expected @@ -1,2 +1 @@ Hello -Goodbye From 4a4699f316a98dc67420f079229b64370e82be40 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 27 Nov 2024 17:38:22 -0600 Subject: [PATCH 32/53] Fixing indentation for blodwen-channel-get-non-blocking. --- support/chez/support.ss | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 769219ce4d..fc21941a0f 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -441,23 +441,22 @@ (define (blodwen-channel-get-non-blocking ty chan) (if (mutex-acquire (channel-read-mut chan) #f) - (let* ([val-box (channel-val-box chan)] - [the-val (unbox val-box)] - ) - (if (eq? the-val '()) - ((mutex-release (channel-read-mut chan)) - '()) - (let* ([read-box (channel-read-box chan)] - [read-cv (channel-read-cv chan)] - ) - (set-box! val-box '()) - (set-box! read-box #t) - (mutex-release (channel-read-mut chan)) - (condition-signal read-cv) - the-val) - )) - '() - )) + (let* ([val-box (channel-val-box chan)] + [the-val (unbox val-box)] + ) + (if (eq? the-val '()) + ((mutex-release (channel-read-mut chan)) + '()) + (let* ([read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)] + ) + (set-box! val-box '()) + (set-box! read-box #t) + (mutex-release (channel-read-mut chan)) + (condition-signal read-cv) + the-val) + )) + '())) ;; Mutex From 5db18d8a7b040091022cbcb6076e46d5e79bef02 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 28 Nov 2024 01:16:17 -0600 Subject: [PATCH 33/53] Adding back decoding support, fixing blodwen-channel-get-non-blocking, and fixing inital test for channelGetNonBlocking. --- libs/base/System/Concurrency.idr | 181 +++++++++++++++++++++++++- support/chez/support.ss | 23 ++-- tests/allschemes/channels007/Main.idr | 6 + tests/allschemes/channels007/expected | 1 + 4 files changed, 193 insertions(+), 18 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index e1f179bc0f..4b113a297f 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -179,12 +179,162 @@ barrierWait barrier = primIO (prim__barrierWait barrier) export data Channel : Type -> Type where [external] +data ChannelObj : Type where [external] + +data ChannelSchemeObj : Type where + Null : ChannelSchemeObj + Cons : ChannelSchemeObj -> ChannelSchemeObj -> ChannelSchemeObj + IntegerVal : Integer -> ChannelSchemeObj + FloatVal : Double -> ChannelSchemeObj + StringVal : String -> ChannelSchemeObj + CharVal : Char -> ChannelSchemeObj + Symbol : String -> ChannelSchemeObj + Box : ChannelSchemeObj -> ChannelSchemeObj + Vector : Integer -> List ChannelSchemeObj -> ChannelSchemeObj + Procedure : ChannelObj -> ChannelSchemeObj + +export +interface Scheme a where + fromScheme : ChannelSchemeObj -> Maybe a + +export +Scheme Integer where + fromScheme (IntegerVal x) = Just x + fromScheme _ = Nothing + +export +Scheme Int where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Int8 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Int16 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Int32 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Int64 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Bits8 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Bits16 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Bits32 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme Bits64 where + fromScheme (IntegerVal x) = Just (cast x) + fromScheme _ = Nothing + +export +Scheme String where + fromScheme (StringVal x) = Just x + fromScheme _ = Nothing + +export +Scheme Double where + fromScheme (FloatVal x) = Just x + fromScheme _ = Nothing + +export +Scheme Char where + fromScheme (CharVal x) = Just x + fromScheme _ = Nothing + +export +Scheme Bool where + fromScheme (IntegerVal 0) = Just False + fromScheme (IntegerVal 1) = Just True + fromScheme _ = Nothing + +export +Scheme a => Scheme (List a) where + fromScheme Null = Just [] + fromScheme (Cons x xs) = Just $ !(fromScheme x) :: !(fromScheme xs) + fromScheme _ = Nothing + +export +(Scheme a, Scheme b) => Scheme (a, b) where + fromScheme (Cons x y) = Just (!(fromScheme x), !(fromScheme y)) + fromScheme _ = Nothing + +export +Scheme a => Scheme (Maybe a) where + fromScheme Null = Just Nothing + fromScheme (Box x) = Just $ Just !(fromScheme x) + fromScheme _ = Nothing + +%foreign "scheme:blodwen-is-number" +prim_isNumber : ChannelObj -> Int +%foreign "scheme:blodwen-is-integer" +prim_isInteger : ChannelObj -> Int +%foreign "scheme:blodwen-is-float" +prim_isFloat : ChannelObj -> Int +%foreign "scheme:blodwen-is-char" +prim_isChar : ChannelObj -> Int +%foreign "scheme:blodwen-is-string" +prim_isString : ChannelObj -> Int +%foreign "scheme:blodwen-is-procedure" +prim_isProcedure : ChannelObj -> Int +%foreign "scheme:blodwen-is-symbol" +prim_isSymbol : ChannelObj -> Int +%foreign "scheme:blodwen-is-nil" +prim_isNil : ChannelObj -> Int +%foreign "scheme:blodwen-is-pair" +prim_isPair : ChannelObj -> Int +%foreign "scheme:blodwen-is-vector" +prim_isVector : ChannelObj -> Int +%foreign "scheme:blodwen-id" +unsafeGetInteger : ChannelObj -> Integer +%foreign "scheme:blodwen-id" +unsafeGetString : ChannelObj -> String +%foreign "scheme:blodwen-id" +unsafeGetFloat : ChannelObj -> Double +%foreign "scheme:blodwen-id" +unsafeGetChar : ChannelObj -> Char +%foreign "scheme:car" +unsafeFst : ChannelObj -> ChannelObj +%foreign "scheme:cdr" +unsafeSnd : ChannelObj -> ChannelObj +%foreign "scheme:blodwen-vector-ref" +unsafeVectorRef : ChannelObj -> Integer -> ChannelObj +%foreign "scheme:blodwen-unbox" +unsafeUnbox : ChannelObj -> ChannelObj +%foreign "scheme:blodwen-vector-length" +unsafeVectorLength : ChannelObj -> Integer +%foreign "scheme:blodwen-vector-list" +unsafeVectorToList : ChannelObj -> List ChannelObj +%foreign "scheme:blodwen-read-symbol" +unsafeReadSymbol : ChannelObj -> String +%foreign "scheme:blodwen-is-box" +prim_isBox : ChannelObj -> Int %foreign "scheme:blodwen-make-channel" prim__makeChannel : PrimIO (Channel a) %foreign "scheme:blodwen-channel-get" prim__channelGet : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-get-non-blocking" -prim__channelGetNonBlocking : Channel a -> PrimIO (Maybe a) +prim__channelGetNonBlocking : Channel a -> PrimIO ChannelObj %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () @@ -211,13 +361,30 @@ channelGet chan = primIO (prim__channelGet chan) ||| @ chan the channel to receive on partial export -channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a) +channelGetNonBlocking : HasIO io => Scheme a => (chan : Channel a) -> io (Maybe a) channelGetNonBlocking chan = - case !(primIO (prim__channelGetNonBlocking chan)) of - Nothing => - pure Nothing - Just xs => - pure $ Just xs + pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetNonBlocking chan)) + where + decodeObj : ChannelObj -> ChannelSchemeObj + decodeObj obj = + if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) + else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) + (readVector (unsafeVectorLength obj) 1 obj) + else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) + (decodeObj (unsafeSnd obj)) + else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) + else if prim_isString obj == 1 then StringVal (unsafeGetString obj) + else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) + else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) + else if prim_isProcedure obj == 1 then Procedure obj + else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) + else Null + where + readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj + readVector len i obj + = if len == i + then [] + else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj ||| Puts a value on the given channel. ||| diff --git a/support/chez/support.ss b/support/chez/support.ss index fc21941a0f..fd8e54de16 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -441,20 +441,21 @@ (define (blodwen-channel-get-non-blocking ty chan) (if (mutex-acquire (channel-read-mut chan) #f) - (let* ([val-box (channel-val-box chan)] + (let* ([val-box (channel-val-box chan)] + [read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)] [the-val (unbox val-box)] ) - (if (eq? the-val '()) - ((mutex-release (channel-read-mut chan)) + (if (null? the-val) + (begin + (mutex-release (channel-read-mut chan)) '()) - (let* ([read-box (channel-read-box chan)] - [read-cv (channel-read-cv chan)] - ) - (set-box! val-box '()) - (set-box! read-box #t) - (mutex-release (channel-read-mut chan)) - (condition-signal read-cv) - the-val) + (begin + (set-box! val-box '()) + (set-box! read-box #t) + (mutex-release (channel-read-mut chan)) + (condition-signal read-cv) + the-val) )) '())) diff --git a/tests/allschemes/channels007/Main.idr b/tests/allschemes/channels007/Main.idr index c422dfb816..0512bc0ed3 100644 --- a/tests/allschemes/channels007/Main.idr +++ b/tests/allschemes/channels007/Main.idr @@ -7,7 +7,13 @@ main = do chan <- makeChannel threadID <- fork $ do channelPut chan "Hello" + channelPut chan "Goodbye" sleep 1 + case !(channelGetNonBlocking chan) of + Nothing => + putStrLn "Nothing" + Just val' => + putStrLn val' case !(channelGetNonBlocking chan) of Nothing => putStrLn "Nothing" diff --git a/tests/allschemes/channels007/expected b/tests/allschemes/channels007/expected index e965047ad7..c86756d193 100644 --- a/tests/allschemes/channels007/expected +++ b/tests/allschemes/channels007/expected @@ -1 +1,2 @@ Hello +Goodbye From 87265de59187749d9436c5e6501ef75ee9395151 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 28 Nov 2024 01:20:21 -0600 Subject: [PATCH 34/53] Adding another test for channelGetNonBlocking. --- tests/allschemes/channels008/Main.idr | 22 ++++++++++++++++++++++ tests/allschemes/channels008/expected | 2 ++ tests/allschemes/channels008/run | 3 +++ 3 files changed, 27 insertions(+) create mode 100644 tests/allschemes/channels008/Main.idr create mode 100644 tests/allschemes/channels008/expected create mode 100644 tests/allschemes/channels008/run diff --git a/tests/allschemes/channels008/Main.idr b/tests/allschemes/channels008/Main.idr new file mode 100644 index 0000000000..1928c92c3c --- /dev/null +++ b/tests/allschemes/channels008/Main.idr @@ -0,0 +1,22 @@ +import System.Concurrency +import System + +-- Test that using channelGetNonBlocking works as expected. +main : IO () +main = do + chan <- makeChannel + threadID <- fork $ do + channelPut chan "Hello" + channelPut chan "Goodbye" + case !(channelGetNonBlocking chan) of + Nothing => + putStrLn "Nothing" + Just val' => + putStrLn val' + case !(channelGetNonBlocking chan) of + Nothing => + putStrLn "Nothing" + Just val' => + putStrLn val' + sleep 1 + diff --git a/tests/allschemes/channels008/expected b/tests/allschemes/channels008/expected new file mode 100644 index 0000000000..99131d9260 --- /dev/null +++ b/tests/allschemes/channels008/expected @@ -0,0 +1,2 @@ +Nothing +Nothing diff --git a/tests/allschemes/channels008/run b/tests/allschemes/channels008/run new file mode 100644 index 0000000000..c6e6f2ab79 --- /dev/null +++ b/tests/allschemes/channels008/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run Main.idr From 714e5b192d8cea0bac48696627b13bfa72c97ccf Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 28 Nov 2024 01:52:46 -0600 Subject: [PATCH 35/53] Removing tabs from blodwen-channel-get-non-blocking. --- support/chez/support.ss | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index fd8e54de16..1eddb10b74 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -448,10 +448,10 @@ ) (if (null? the-val) (begin - (mutex-release (channel-read-mut chan)) - '()) + (mutex-release (channel-read-mut chan)) + '()) (begin - (set-box! val-box '()) + (set-box! val-box '()) (set-box! read-box #t) (mutex-release (channel-read-mut chan)) (condition-signal read-cv) From 126a52a27bd1938d5ee3f2616f3f019300be8465 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sun, 1 Dec 2024 18:55:35 -0600 Subject: [PATCH 36/53] Adding initial skeleton for blodwen-channel-get-with-timeout. --- support/chez/support.ss | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/support/chez/support.ss b/support/chez/support.ss index 1eddb10b74..fa4124dbc7 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -459,6 +459,38 @@ )) '())) +(define (blodwen-channel-get-with-timeout ty chan timeout) + (if (mutex-acquire (channel-read-mut chan) #f) + (let* ([val-box (channel-val-box chan)] + [read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)] + [the-val (unbox val-box)] + [waittime (make-time 'time-duration (current-time + timeout) current-time)] + ) + + + ))) + +#| + (let* ([val-box (channel-val-box chan)] + [read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)] + [the-val (unbox val-box)] + ) + (if (null? the-val) + (begin + (mutex-release (channel-read-mut chan)) + '()) + (begin + (set-box! val-box '()) + (set-box! read-box #t) + (mutex-release (channel-read-mut chan)) + (condition-signal read-cv) + the-val) + )) + '())) +|# + ;; Mutex (define (blodwen-make-mutex) From 8d78679280f89201bb723dcedb830c71a1fa4ca1 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 2 Dec 2024 19:04:37 -0600 Subject: [PATCH 37/53] Adding initial blodwen-channel-get-with-timeout function and associated channelGetWithTimeout function. --- libs/base/System/Concurrency.idr | 33 +++++++++++++++++++ support/chez/support.ss | 54 ++++++++++++++------------------ 2 files changed, 56 insertions(+), 31 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 4b113a297f..815aae7134 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -335,6 +335,8 @@ prim__makeChannel : PrimIO (Channel a) prim__channelGet : Channel a -> PrimIO a %foreign "scheme:blodwen-channel-get-non-blocking" prim__channelGetNonBlocking : Channel a -> PrimIO ChannelObj +%foreign "scheme:blodwen-channel-get-with-timeout" +prim__channelGetWithTimeout : Channel a -> Nat -> PrimIO ChannelObj %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () @@ -386,6 +388,37 @@ channelGetNonBlocking chan = then [] else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj +||| Timeout version of channelGet. +||| +||| @ chan the channel to receive on +||| @ seconds how many seconds to wait until timeout +partial +export +channelGetWithTimeout : HasIO io => Scheme a => (chan : Channel a) -> (seconds : Nat) -> io (Maybe a) +channelGetWithTimeout chan seconds = + pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetWithTimeout chan seconds)) + where + decodeObj : ChannelObj -> ChannelSchemeObj + decodeObj obj = + if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) + else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) + (readVector (unsafeVectorLength obj) 1 obj) + else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) + (decodeObj (unsafeSnd obj)) + else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) + else if prim_isString obj == 1 then StringVal (unsafeGetString obj) + else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) + else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) + else if prim_isProcedure obj == 1 then Procedure obj + else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) + else Null + where + readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj + readVector len i obj + = if len == i + then [] + else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj + ||| Puts a value on the given channel. ||| ||| @ chan the `Channel` to send the value over diff --git a/support/chez/support.ss b/support/chez/support.ss index fa4124dbc7..50c63f8700 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -459,37 +459,29 @@ )) '())) -(define (blodwen-channel-get-with-timeout ty chan timeout) - (if (mutex-acquire (channel-read-mut chan) #f) - (let* ([val-box (channel-val-box chan)] - [read-box (channel-read-box chan)] - [read-cv (channel-read-cv chan)] - [the-val (unbox val-box)] - [waittime (make-time 'time-duration (current-time + timeout) current-time)] - ) - - - ))) - -#| - (let* ([val-box (channel-val-box chan)] - [read-box (channel-read-box chan)] - [read-cv (channel-read-cv chan)] - [the-val (unbox val-box)] - ) - (if (null? the-val) - (begin - (mutex-release (channel-read-mut chan)) - '()) - (begin - (set-box! val-box '()) - (set-box! read-box #t) - (mutex-release (channel-read-mut chan)) - (condition-signal read-cv) - the-val) - )) - '())) -|# +(define (blodwen-channel-get-with-timeout ty chan seconds) + (let loop ([start-time (current-time)]) ; Record the start time + (let ([elapsed (- (current-time) start-time)]) ; Calculate elapsed time in seconds + (if (>= elapsed seconds) + '() ; Timeout reached, return '() for empty value + (if (mutex-acquire (channel-read-mut chan) #f) + (let* ([val-box (channel-val-box chan)] + [the-val (unbox val-box)]) + (if (null? the-val) + (begin + (mutex-release (channel-read-mut chan)) + (sleep (make-time 'time-duration 0 0.001)) ; Sleep for 1ms before retrying + (loop start-time)) ; Continue with the same start-time + (let* ([read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)]) + (set-box! val-box '()) + (set-box! read-box #t) + (mutex-release (channel-read-mut chan)) + (condition-signal read-cv) + the-val))) + (begin + (sleep (make-time 'time-duration 0 0.001)) ; Sleep for 1ms before retrying + (loop start-time))))))) ; Continue with the same start-time ;; Mutex From b3fa699d5b654f3d7965649b61588627d7788943 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 3 Dec 2024 01:08:43 -0600 Subject: [PATCH 38/53] Fixing small issue with blodwen-channel-get-with-timeout. --- support/chez/support.ss | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index 50c63f8700..b1901804d2 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -460,9 +460,11 @@ '())) (define (blodwen-channel-get-with-timeout ty chan seconds) - (let loop ([start-time (current-time)]) ; Record the start time - (let ([elapsed (- (current-time) start-time)]) ; Calculate elapsed time in seconds - (if (>= elapsed seconds) + (let loop ([start-time (current-time)] + [seconds-time (make-time 'time-duration 0 seconds)] + ) ; Record the start time + (let ([elapsed (make-time 'time-duration (current-time) start-time)]) ; Calculate elapsed time in seconds + (if (time>=? elapsed seconds-time) '() ; Timeout reached, return '() for empty value (if (mutex-acquire (channel-read-mut chan) #f) (let* ([val-box (channel-val-box chan)] From 8ee6e4b40e5b33b3df1ec5770d21590f69f2e302 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 3 Dec 2024 22:36:37 -0600 Subject: [PATCH 39/53] Adding corrected blodwen-channel-get-with-timeout implementation and updated tests. --- support/chez/support.ss | 17 +++++----- tests/allschemes/channels008/Main.idr | 49 +++++++++++++++++---------- tests/allschemes/channels008/expected | 4 +-- 3 files changed, 41 insertions(+), 29 deletions(-) diff --git a/support/chez/support.ss b/support/chez/support.ss index b1901804d2..1f3c6202be 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -461,19 +461,18 @@ (define (blodwen-channel-get-with-timeout ty chan seconds) (let loop ([start-time (current-time)] - [seconds-time (make-time 'time-duration 0 seconds)] - ) ; Record the start time - (let ([elapsed (make-time 'time-duration (current-time) start-time)]) ; Calculate elapsed time in seconds - (if (time>=? elapsed seconds-time) - '() ; Timeout reached, return '() for empty value + ) + (let ([elapsed (time-difference (current-time) start-time)]) + (if (time>=? elapsed (make-time 'time-duration 0 seconds)) + '() (if (mutex-acquire (channel-read-mut chan) #f) (let* ([val-box (channel-val-box chan)] [the-val (unbox val-box)]) (if (null? the-val) (begin (mutex-release (channel-read-mut chan)) - (sleep (make-time 'time-duration 0 0.001)) ; Sleep for 1ms before retrying - (loop start-time)) ; Continue with the same start-time + (sleep (make-time 'time-duration 1000000 0)) + (loop start-time)) (let* ([read-box (channel-read-box chan)] [read-cv (channel-read-cv chan)]) (set-box! val-box '()) @@ -482,8 +481,8 @@ (condition-signal read-cv) the-val))) (begin - (sleep (make-time 'time-duration 0 0.001)) ; Sleep for 1ms before retrying - (loop start-time))))))) ; Continue with the same start-time + (sleep (make-time 'time-duration 1000000 0)) + (loop start-time))))))) ;; Mutex diff --git a/tests/allschemes/channels008/Main.idr b/tests/allschemes/channels008/Main.idr index 1928c92c3c..fc303fe646 100644 --- a/tests/allschemes/channels008/Main.idr +++ b/tests/allschemes/channels008/Main.idr @@ -1,22 +1,35 @@ -import System.Concurrency import System +import System.Concurrency + +-- Simple producing thread. +producer : Channel String -> IO () +producer c = ignore $ loop 2 + where + loop : Nat -> IO () + loop Z = pure () + loop (S n) = do + channelPut c $ show n + sleep 1 + loop (minus n 1) --- Test that using channelGetNonBlocking works as expected. +-- Test that channelGetWithTimeout works as expected. main : IO () -main = do - chan <- makeChannel - threadID <- fork $ do - channelPut chan "Hello" - channelPut chan "Goodbye" - case !(channelGetNonBlocking chan) of - Nothing => - putStrLn "Nothing" - Just val' => - putStrLn val' - case !(channelGetNonBlocking chan) of - Nothing => - putStrLn "Nothing" - Just val' => - putStrLn val' - sleep 1 +main = + do c <- makeChannel + tids <- for [0..1] $ \_ => fork $ producer c + sleep 5 + vals <- for [0..1] $ \_ => channelGetWithTimeout c 5 + ignore $ traverse (\t => threadWait t) tids + for_ vals $ \val => + case val of + Nothing => + putStrLn "Nothing" + Just val' => + putStrLn val' + {- + let s = sum vals + if s == 50500 + then putStrLn "Success!" + else putStrLn "How did we get here?" + -} diff --git a/tests/allschemes/channels008/expected b/tests/allschemes/channels008/expected index 99131d9260..6ed281c757 100644 --- a/tests/allschemes/channels008/expected +++ b/tests/allschemes/channels008/expected @@ -1,2 +1,2 @@ -Nothing -Nothing +1 +1 From fdc11b63654a3ef3dc068c1aa347b37302d409c5 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 3 Dec 2024 22:42:06 -0600 Subject: [PATCH 40/53] Updating documentation for channelGetWithTimeout function. --- libs/base/System/Concurrency.idr | 1 + 1 file changed, 1 insertion(+) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 815aae7134..e59c60afd2 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -389,6 +389,7 @@ channelGetNonBlocking chan = else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj ||| Timeout version of channelGet. +||| Continously loops with 1ms delays until `seconds` has elapsed, or a value is provided through `chan`. ||| ||| @ chan the channel to receive on ||| @ seconds how many seconds to wait until timeout From 98b485ae3fc47a884ce8fb7e0fdf551bb520a9a9 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 3 Dec 2024 23:24:42 -0600 Subject: [PATCH 41/53] Adding Scheme Nat implementation and fixing test. --- libs/base/System/Concurrency.idr | 5 ++++ tests/allschemes/channels008/Main.idr | 36 ++++++++++++--------------- tests/allschemes/channels008/expected | 3 +-- 3 files changed, 22 insertions(+), 22 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index e59c60afd2..f6bf98eb05 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -202,6 +202,11 @@ Scheme Integer where fromScheme (IntegerVal x) = Just x fromScheme _ = Nothing +export +Scheme Nat where + fromScheme (IntegerVal x) = Just $ integerToNat x + fromScheme _ = Nothing + export Scheme Int where fromScheme (IntegerVal x) = Just (cast x) diff --git a/tests/allschemes/channels008/Main.idr b/tests/allschemes/channels008/Main.idr index fc303fe646..427377d473 100644 --- a/tests/allschemes/channels008/Main.idr +++ b/tests/allschemes/channels008/Main.idr @@ -2,34 +2,30 @@ import System import System.Concurrency -- Simple producing thread. -producer : Channel String -> IO () -producer c = ignore $ loop 2 +producer : Channel Nat -> Nat -> IO () +producer c n = ignore $ producer' n where - loop : Nat -> IO () - loop Z = pure () - loop (S n) = do - channelPut c $ show n + producer' : Nat -> IO () + producer' Z = pure () + producer' (S n) = do + channelPut c n sleep 1 - loop (minus n 1) -- Test that channelGetWithTimeout works as expected. main : IO () main = do c <- makeChannel - tids <- for [0..1] $ \_ => fork $ producer c - sleep 5 - vals <- for [0..1] $ \_ => channelGetWithTimeout c 5 + tids <- for [0..11] $ \n => fork $ producer c n + vals <- for [0..11] $ \_ => channelGetWithTimeout c 5 ignore $ traverse (\t => threadWait t) tids - for_ vals $ \val => - case val of - Nothing => - putStrLn "Nothing" - Just val' => - putStrLn val' - {- - let s = sum vals - if s == 50500 + let vals' = map (\val => case val of + Nothing => + 0 + Just val' => + val' + ) vals + s = sum vals' + if s == 55 then putStrLn "Success!" else putStrLn "How did we get here?" - -} diff --git a/tests/allschemes/channels008/expected b/tests/allschemes/channels008/expected index 6ed281c757..f985b46aff 100644 --- a/tests/allschemes/channels008/expected +++ b/tests/allschemes/channels008/expected @@ -1,2 +1 @@ -1 -1 +Success! From 8eb7457a816627e76c14dc8b220a19c4288b901f Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 3 Dec 2024 23:26:51 -0600 Subject: [PATCH 42/53] Re-ordering imports for channel007 test. --- tests/allschemes/channels007/Main.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/allschemes/channels007/Main.idr b/tests/allschemes/channels007/Main.idr index 0512bc0ed3..43cc2cd993 100644 --- a/tests/allschemes/channels007/Main.idr +++ b/tests/allschemes/channels007/Main.idr @@ -1,5 +1,5 @@ -import System.Concurrency import System +import System.Concurrency -- Test that using channelGetNonBlocking works as expected. main : IO () From 4f85729773df9c05198b0437a98bd1866798c0b5 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 3 Dec 2024 23:35:20 -0600 Subject: [PATCH 43/53] Adding changes of this PR to CHANGELOG_NEXT.md. --- CHANGELOG_NEXT.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 2e5c753c35..4cc5f0172a 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -240,6 +240,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * Added `Data.IORef.atomically` for the chez backend. +* Added `System.Concurrency.channelGetNonBlocking` for the chez backend. + +* Added `System.Concurrency.channelGetWithTimeout` for the chez backend. + #### Contrib * `Data.List.Lazy` was moved from `contrib` to `base`. From 474bd6ba58f3490a9111c57d807c60917737b453 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 3 Dec 2024 23:41:58 -0600 Subject: [PATCH 44/53] Fixing linting issues. --- libs/base/System/Concurrency.idr | 4 ++-- tests/allschemes/channels008/Main.idr | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index f6bf98eb05..822a226ad1 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -372,7 +372,7 @@ channelGetNonBlocking : HasIO io => Scheme a => (chan : Channel a) -> io (Maybe channelGetNonBlocking chan = pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetNonBlocking chan)) where - decodeObj : ChannelObj -> ChannelSchemeObj + decodeObj : ChannelObj -> ChannelSchemeObj decodeObj obj = if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) @@ -404,7 +404,7 @@ channelGetWithTimeout : HasIO io => Scheme a => (chan : Channel a) -> (seconds : channelGetWithTimeout chan seconds = pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetWithTimeout chan seconds)) where - decodeObj : ChannelObj -> ChannelSchemeObj + decodeObj : ChannelObj -> ChannelSchemeObj decodeObj obj = if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) diff --git a/tests/allschemes/channels008/Main.idr b/tests/allschemes/channels008/Main.idr index 427377d473..5160d7baaf 100644 --- a/tests/allschemes/channels008/Main.idr +++ b/tests/allschemes/channels008/Main.idr @@ -16,7 +16,7 @@ main : IO () main = do c <- makeChannel tids <- for [0..11] $ \n => fork $ producer c n - vals <- for [0..11] $ \_ => channelGetWithTimeout c 5 + vals <- for [0..11] $ \_ => channelGetWithTimeout c 5 ignore $ traverse (\t => threadWait t) tids let vals' = map (\val => case val of Nothing => From cd24d351522a628f24cd98ad298f9b83e660c383 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Wed, 4 Dec 2024 08:24:54 -0600 Subject: [PATCH 45/53] Adding additional sleep in channel007 test. --- tests/allschemes/channels007/Main.idr | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/allschemes/channels007/Main.idr b/tests/allschemes/channels007/Main.idr index 43cc2cd993..df62813c70 100644 --- a/tests/allschemes/channels007/Main.idr +++ b/tests/allschemes/channels007/Main.idr @@ -14,6 +14,7 @@ main = do putStrLn "Nothing" Just val' => putStrLn val' + sleep 1 case !(channelGetNonBlocking chan) of Nothing => putStrLn "Nothing" From 970ace4b4661652ab67655b5e0977f4d4caa0fac Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 5 Dec 2024 00:01:34 -0600 Subject: [PATCH 46/53] Addressing comments. --- libs/base/System/Concurrency.idr | 289 ++++++++++++++++--------------- 1 file changed, 149 insertions(+), 140 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 822a226ad1..7aeb887ef1 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -181,170 +181,221 @@ data Channel : Type -> Type where [external] data ChannelObj : Type where [external] -data ChannelSchemeObj : Type where - Null : ChannelSchemeObj - Cons : ChannelSchemeObj -> ChannelSchemeObj -> ChannelSchemeObj - IntegerVal : Integer -> ChannelSchemeObj - FloatVal : Double -> ChannelSchemeObj - StringVal : String -> ChannelSchemeObj - CharVal : Char -> ChannelSchemeObj - Symbol : String -> ChannelSchemeObj - Box : ChannelSchemeObj -> ChannelSchemeObj - Vector : Integer -> List ChannelSchemeObj -> ChannelSchemeObj - Procedure : ChannelObj -> ChannelSchemeObj - -export -interface Scheme a where +data ChannelSchemeObj + = Null + | Cons ChannelSchemeObj ChannelSchemeObj + | IntegerVal Integer + | FloatVal Double + | StringVal String + | CharVal Char + | Symbol String + | Box ChannelSchemeObj + | Vector Integer (List ChannelSchemeObj) + | Procedure ChannelObj + +%foreign "scheme:blodwen-is-number" +prim_isNumber : ChannelObj -> Int +%foreign "scheme:blodwen-is-integer" +prim_isInteger : ChannelObj -> Int +%foreign "scheme:blodwen-is-float" +prim_isFloat : ChannelObj -> Int +%foreign "scheme:blodwen-is-char" +prim_isChar : ChannelObj -> Int +%foreign "scheme:blodwen-is-string" +prim_isString : ChannelObj -> Int +%foreign "scheme:blodwen-is-procedure" +prim_isProcedure : ChannelObj -> Int +%foreign "scheme:blodwen-is-symbol" +prim_isSymbol : ChannelObj -> Int +%foreign "scheme:blodwen-is-nil" +prim_isNil : ChannelObj -> Int +%foreign "scheme:blodwen-is-pair" +prim_isPair : ChannelObj -> Int +%foreign "scheme:blodwen-is-vector" +prim_isVector : ChannelObj -> Int +%foreign "scheme:blodwen-is-box" +prim_isBox : ChannelObj -> Int +%foreign "scheme:blodwen-id" +unsafeGetInteger : ChannelObj -> Integer +%foreign "scheme:blodwen-id" +unsafeGetString : ChannelObj -> String +%foreign "scheme:blodwen-id" +unsafeGetFloat : ChannelObj -> Double +%foreign "scheme:blodwen-id" +unsafeGetChar : ChannelObj -> Char +%foreign "scheme:car" +unsafeFst : ChannelObj -> ChannelObj +%foreign "scheme:cdr" +unsafeSnd : ChannelObj -> ChannelObj +%foreign "scheme:blodwen-vector-ref" +unsafeVectorRef : ChannelObj -> Integer -> ChannelObj +%foreign "scheme:blodwen-unbox" +unsafeUnbox : ChannelObj -> ChannelObj +%foreign "scheme:blodwen-vector-length" +unsafeVectorLength : ChannelObj -> Integer +%foreign "scheme:blodwen-vector-list" +unsafeVectorToList : ChannelObj -> List ChannelObj +%foreign "scheme:blodwen-read-symbol" +unsafeReadSymbol : ChannelObj -> String +%foreign "scheme:blodwen-make-channel" +prim__makeChannel : PrimIO (Channel a) +%foreign "scheme:blodwen-channel-get" +prim__channelGet : Channel a -> PrimIO a +%foreign "scheme:blodwen-channel-get-non-blocking" +prim__channelGetNonBlocking : Channel a -> PrimIO ChannelObj +%foreign "scheme:blodwen-channel-get-with-timeout" +prim__channelGetWithTimeout : Channel a -> Nat -> PrimIO ChannelObj +%foreign "scheme:blodwen-channel-put" +prim__channelPut : Channel a -> a -> PrimIO () + +export +interface FromScheme a where fromScheme : ChannelSchemeObj -> Maybe a +{- +partial +private +decodeObj : ChannelObj -> ChannelSchemeObj +decodeObj obj = + if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) + else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) + (readVector (unsafeVectorLength obj) 1 obj) + else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) + (decodeObj (unsafeSnd obj)) + else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) + else if prim_isString obj == 1 then StringVal (unsafeGetString obj) + else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) + else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) + else if prim_isProcedure obj == 1 then Procedure obj + else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) + else Null + where + readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj + readVector len i obj + = if len == i + then [] + else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj +-} + +partial +private +decodeObj : ChannelObj -> (ChannelObj -> Int) -> ChannelSchemeObj +decodeObj obj f = + case f obj == 1 of + + + if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) + else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) + (readVector (unsafeVectorLength obj) 1 obj) + else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) + (decodeObj (unsafeSnd obj)) + else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) + else if prim_isString obj == 1 then StringVal (unsafeGetString obj) + else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) + else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) + else if prim_isProcedure obj == 1 then Procedure obj + else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) + else Null + where + readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj + readVector len i obj + = if len == i + then [] + else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj + export -Scheme Integer where +FromScheme Integer where fromScheme (IntegerVal x) = Just x fromScheme _ = Nothing export -Scheme Nat where +FromScheme Nat where fromScheme (IntegerVal x) = Just $ integerToNat x fromScheme _ = Nothing export -Scheme Int where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Int where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme Int8 where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Int8 where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme Int16 where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Int16 where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme Int32 where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Int32 where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme Int64 where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Int64 where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme Bits8 where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Bits8 where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme Bits16 where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Bits16 where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme Bits32 where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Bits32 where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme Bits64 where - fromScheme (IntegerVal x) = Just (cast x) +FromScheme Bits64 where + fromScheme (IntegerVal x) = Just $ cast x fromScheme _ = Nothing export -Scheme String where +FromScheme String where fromScheme (StringVal x) = Just x fromScheme _ = Nothing export -Scheme Double where +FromScheme Double where fromScheme (FloatVal x) = Just x fromScheme _ = Nothing export -Scheme Char where +FromScheme Char where fromScheme (CharVal x) = Just x fromScheme _ = Nothing export -Scheme Bool where +FromScheme Bool where fromScheme (IntegerVal 0) = Just False fromScheme (IntegerVal 1) = Just True fromScheme _ = Nothing export -Scheme a => Scheme (List a) where +FromScheme a => FromScheme (List a) where fromScheme Null = Just [] fromScheme (Cons x xs) = Just $ !(fromScheme x) :: !(fromScheme xs) fromScheme _ = Nothing export -(Scheme a, Scheme b) => Scheme (a, b) where +(FromScheme a, FromScheme b) => FromScheme (a, b) where fromScheme (Cons x y) = Just (!(fromScheme x), !(fromScheme y)) fromScheme _ = Nothing export -Scheme a => Scheme (Maybe a) where +FromScheme a => FromScheme (Maybe a) where fromScheme Null = Just Nothing fromScheme (Box x) = Just $ Just !(fromScheme x) fromScheme _ = Nothing -%foreign "scheme:blodwen-is-number" -prim_isNumber : ChannelObj -> Int -%foreign "scheme:blodwen-is-integer" -prim_isInteger : ChannelObj -> Int -%foreign "scheme:blodwen-is-float" -prim_isFloat : ChannelObj -> Int -%foreign "scheme:blodwen-is-char" -prim_isChar : ChannelObj -> Int -%foreign "scheme:blodwen-is-string" -prim_isString : ChannelObj -> Int -%foreign "scheme:blodwen-is-procedure" -prim_isProcedure : ChannelObj -> Int -%foreign "scheme:blodwen-is-symbol" -prim_isSymbol : ChannelObj -> Int -%foreign "scheme:blodwen-is-nil" -prim_isNil : ChannelObj -> Int -%foreign "scheme:blodwen-is-pair" -prim_isPair : ChannelObj -> Int -%foreign "scheme:blodwen-is-vector" -prim_isVector : ChannelObj -> Int -%foreign "scheme:blodwen-id" -unsafeGetInteger : ChannelObj -> Integer -%foreign "scheme:blodwen-id" -unsafeGetString : ChannelObj -> String -%foreign "scheme:blodwen-id" -unsafeGetFloat : ChannelObj -> Double -%foreign "scheme:blodwen-id" -unsafeGetChar : ChannelObj -> Char -%foreign "scheme:car" -unsafeFst : ChannelObj -> ChannelObj -%foreign "scheme:cdr" -unsafeSnd : ChannelObj -> ChannelObj -%foreign "scheme:blodwen-vector-ref" -unsafeVectorRef : ChannelObj -> Integer -> ChannelObj -%foreign "scheme:blodwen-unbox" -unsafeUnbox : ChannelObj -> ChannelObj -%foreign "scheme:blodwen-vector-length" -unsafeVectorLength : ChannelObj -> Integer -%foreign "scheme:blodwen-vector-list" -unsafeVectorToList : ChannelObj -> List ChannelObj -%foreign "scheme:blodwen-read-symbol" -unsafeReadSymbol : ChannelObj -> String -%foreign "scheme:blodwen-is-box" -prim_isBox : ChannelObj -> Int -%foreign "scheme:blodwen-make-channel" -prim__makeChannel : PrimIO (Channel a) -%foreign "scheme:blodwen-channel-get" -prim__channelGet : Channel a -> PrimIO a -%foreign "scheme:blodwen-channel-get-non-blocking" -prim__channelGetNonBlocking : Channel a -> PrimIO ChannelObj -%foreign "scheme:blodwen-channel-get-with-timeout" -prim__channelGetWithTimeout : Channel a -> Nat -> PrimIO ChannelObj -%foreign "scheme:blodwen-channel-put" -prim__channelPut : Channel a -> a -> PrimIO () - ||| Creates and returns a new `Channel`. ||| ||| The channel can be used with `channelGet` to receive a value through the @@ -368,30 +419,9 @@ channelGet chan = primIO (prim__channelGet chan) ||| @ chan the channel to receive on partial export -channelGetNonBlocking : HasIO io => Scheme a => (chan : Channel a) -> io (Maybe a) +channelGetNonBlocking : HasIO io => FromScheme a => (chan : Channel a) -> io (Maybe a) channelGetNonBlocking chan = pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetNonBlocking chan)) - where - decodeObj : ChannelObj -> ChannelSchemeObj - decodeObj obj = - if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) - else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) - (readVector (unsafeVectorLength obj) 1 obj) - else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) - (decodeObj (unsafeSnd obj)) - else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) - else if prim_isString obj == 1 then StringVal (unsafeGetString obj) - else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) - else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) - else if prim_isProcedure obj == 1 then Procedure obj - else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) - else Null - where - readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj - readVector len i obj - = if len == i - then [] - else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj ||| Timeout version of channelGet. ||| Continously loops with 1ms delays until `seconds` has elapsed, or a value is provided through `chan`. @@ -400,30 +430,9 @@ channelGetNonBlocking chan = ||| @ seconds how many seconds to wait until timeout partial export -channelGetWithTimeout : HasIO io => Scheme a => (chan : Channel a) -> (seconds : Nat) -> io (Maybe a) +channelGetWithTimeout : HasIO io => FromScheme a => (chan : Channel a) -> (seconds : Nat) -> io (Maybe a) channelGetWithTimeout chan seconds = pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetWithTimeout chan seconds)) - where - decodeObj : ChannelObj -> ChannelSchemeObj - decodeObj obj = - if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) - else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) - (readVector (unsafeVectorLength obj) 1 obj) - else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) - (decodeObj (unsafeSnd obj)) - else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) - else if prim_isString obj == 1 then StringVal (unsafeGetString obj) - else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) - else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) - else if prim_isProcedure obj == 1 then Procedure obj - else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) - else Null - where - readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj - readVector len i obj - = if len == i - then [] - else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj ||| Puts a value on the given channel. ||| From 0a79b4611b2b29cae1da35c0beb0ef9fe65e0f8d Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 5 Dec 2024 00:02:48 -0600 Subject: [PATCH 47/53] Addressing comments (fixed). --- libs/base/System/Concurrency.idr | 28 ---------------------------- 1 file changed, 28 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 7aeb887ef1..9b54ace5f9 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -252,38 +252,10 @@ export interface FromScheme a where fromScheme : ChannelSchemeObj -> Maybe a -{- partial private decodeObj : ChannelObj -> ChannelSchemeObj decodeObj obj = - if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) - else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) - (readVector (unsafeVectorLength obj) 1 obj) - else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) - (decodeObj (unsafeSnd obj)) - else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) - else if prim_isString obj == 1 then StringVal (unsafeGetString obj) - else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) - else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) - else if prim_isProcedure obj == 1 then Procedure obj - else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) - else Null - where - readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj - readVector len i obj - = if len == i - then [] - else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj --} - -partial -private -decodeObj : ChannelObj -> (ChannelObj -> Int) -> ChannelSchemeObj -decodeObj obj f = - case f obj == 1 of - - if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) (readVector (unsafeVectorLength obj) 1 obj) From 6a5129ffafc3537450199fb42a5d7b366f495df1 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 5 Dec 2024 00:17:52 -0600 Subject: [PATCH 48/53] Addressing comments (tests). --- tests/allschemes/channels007/Main.idr | 12 ++++-------- tests/allschemes/channels008/Main.idr | 14 +++----------- tests/allschemes/channels008/expected | 2 +- 3 files changed, 8 insertions(+), 20 deletions(-) diff --git a/tests/allschemes/channels007/Main.idr b/tests/allschemes/channels007/Main.idr index df62813c70..1c3ef4e8aa 100644 --- a/tests/allschemes/channels007/Main.idr +++ b/tests/allschemes/channels007/Main.idr @@ -10,15 +10,11 @@ main = do channelPut chan "Goodbye" sleep 1 case !(channelGetNonBlocking chan) of - Nothing => - putStrLn "Nothing" - Just val' => - putStrLn val' + Nothing => putStrLn "Nothing" + Just val' => putStrLn val' sleep 1 case !(channelGetNonBlocking chan) of - Nothing => - putStrLn "Nothing" - Just val' => - putStrLn val' + Nothing => putStrLn "Nothing" + Just val' => putStrLn val' sleep 1 diff --git a/tests/allschemes/channels008/Main.idr b/tests/allschemes/channels008/Main.idr index 5160d7baaf..bd876d64ad 100644 --- a/tests/allschemes/channels008/Main.idr +++ b/tests/allschemes/channels008/Main.idr @@ -1,3 +1,4 @@ +import Data.Maybe import System import System.Concurrency @@ -17,15 +18,6 @@ main = do c <- makeChannel tids <- for [0..11] $ \n => fork $ producer c n vals <- for [0..11] $ \_ => channelGetWithTimeout c 5 - ignore $ traverse (\t => threadWait t) tids - let vals' = map (\val => case val of - Nothing => - 0 - Just val' => - val' - ) vals - s = sum vals' - if s == 55 - then putStrLn "Success!" - else putStrLn "How did we get here?" + ignore $ traverse (\t => threadWait t) tids + putStrLn $ show $ sum $ fromMaybe 0 <$> vals diff --git a/tests/allschemes/channels008/expected b/tests/allschemes/channels008/expected index f985b46aff..c3f407c095 100644 --- a/tests/allschemes/channels008/expected +++ b/tests/allschemes/channels008/expected @@ -1 +1 @@ -Success! +55 From 917b2403e91f8acfb51505303f05026819fe2cad Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 5 Dec 2024 00:18:43 -0600 Subject: [PATCH 49/53] Fixing linting. --- tests/allschemes/channels008/Main.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/allschemes/channels008/Main.idr b/tests/allschemes/channels008/Main.idr index bd876d64ad..81f6d2d7e5 100644 --- a/tests/allschemes/channels008/Main.idr +++ b/tests/allschemes/channels008/Main.idr @@ -18,6 +18,6 @@ main = do c <- makeChannel tids <- for [0..11] $ \n => fork $ producer c n vals <- for [0..11] $ \_ => channelGetWithTimeout c 5 - ignore $ traverse (\t => threadWait t) tids + ignore $ traverse (\t => threadWait t) tids putStrLn $ show $ sum $ fromMaybe 0 <$> vals From 2a70bad3057a0288cd4b0928fd1668240b967860 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Thu, 5 Dec 2024 20:36:20 -0600 Subject: [PATCH 50/53] Addressing comments. --- libs/base/System/Concurrency.idr | 123 ++++++++++++------------------- 1 file changed, 49 insertions(+), 74 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 9b54ace5f9..ef0e470d2b 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -181,18 +181,6 @@ data Channel : Type -> Type where [external] data ChannelObj : Type where [external] -data ChannelSchemeObj - = Null - | Cons ChannelSchemeObj ChannelSchemeObj - | IntegerVal Integer - | FloatVal Double - | StringVal String - | CharVal Char - | Symbol String - | Box ChannelSchemeObj - | Vector Integer (List ChannelSchemeObj) - | Procedure ChannelObj - %foreign "scheme:blodwen-is-number" prim_isNumber : ChannelObj -> Int %foreign "scheme:blodwen-is-integer" @@ -250,123 +238,110 @@ prim__channelPut : Channel a -> a -> PrimIO () export interface FromScheme a where - fromScheme : ChannelSchemeObj -> Maybe a + fromScheme : ChannelObj -> Maybe a partial private -decodeObj : ChannelObj -> ChannelSchemeObj -decodeObj obj = - if prim_isInteger obj == 1 then IntegerVal (unsafeGetInteger obj) - else if prim_isVector obj == 1 then Vector (unsafeGetInteger (unsafeVectorRef obj 0)) - (readVector (unsafeVectorLength obj) 1 obj) - else if prim_isPair obj == 1 then Cons (decodeObj (unsafeFst obj)) - (decodeObj (unsafeSnd obj)) - else if prim_isFloat obj == 1 then FloatVal (unsafeGetFloat obj) - else if prim_isString obj == 1 then StringVal (unsafeGetString obj) - else if prim_isChar obj == 1 then CharVal (unsafeGetChar obj) - else if prim_isSymbol obj == 1 then Symbol (unsafeReadSymbol obj) - else if prim_isProcedure obj == 1 then Procedure obj - else if prim_isBox obj == 1 then Box (decodeObj (unsafeUnbox obj)) - else Null - where - readVector : Integer -> Integer -> ChannelObj -> List ChannelSchemeObj - readVector len i obj - = if len == i - then [] - else decodeObj (unsafeVectorRef obj i) :: readVector len (i + 1) obj +marshalChannelObj : (pred : ChannelObj -> Int) + -> (unsafeGet : ChannelObj -> a) + -> ChannelObj + -> Maybe a +marshalChannelObj pred unsafeGet obj = + case pred obj of + 1 => Just $ unsafeGet obj + _ => Nothing export FromScheme Integer where - fromScheme (IntegerVal x) = Just x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger unsafeGetInteger export FromScheme Nat where - fromScheme (IntegerVal x) = Just $ integerToNat x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (integerToNat . unsafeGetInteger) export FromScheme Int where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme Int8 where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme Int16 where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme Int32 where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme Int64 where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme Bits8 where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme Bits16 where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme Bits32 where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme Bits64 where - fromScheme (IntegerVal x) = Just $ cast x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) export FromScheme String where - fromScheme (StringVal x) = Just x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isString unsafeGetString export FromScheme Double where - fromScheme (FloatVal x) = Just x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isFloat unsafeGetFloat export FromScheme Char where - fromScheme (CharVal x) = Just x - fromScheme _ = Nothing + fromScheme = marshalChannelObj prim_isChar unsafeGetChar export FromScheme Bool where - fromScheme (IntegerVal 0) = Just False - fromScheme (IntegerVal 1) = Just True - fromScheme _ = Nothing + fromScheme obj = + case prim_isInteger obj == 1 of + False => Nothing + True => case unsafeGetInteger obj of + 0 => Just False + 1 => Just True + _ => Nothing +partial export FromScheme a => FromScheme (List a) where - fromScheme Null = Just [] - fromScheme (Cons x xs) = Just $ !(fromScheme x) :: !(fromScheme xs) - fromScheme _ = Nothing + fromScheme obj = + case prim_isNil obj == 1 of + True => Just [] + False => case prim_isPair obj == 1 of + False => Nothing + True => Just $ !(fromScheme $ unsafeFst obj) :: !(fromScheme $ unsafeSnd obj) export (FromScheme a, FromScheme b) => FromScheme (a, b) where - fromScheme (Cons x y) = Just (!(fromScheme x), !(fromScheme y)) - fromScheme _ = Nothing + fromScheme obj = + case prim_isPair obj == 1 of + False => Nothing + True => Just (!(fromScheme $ unsafeFst obj), !(fromScheme $ unsafeSnd obj)) export FromScheme a => FromScheme (Maybe a) where - fromScheme Null = Just Nothing - fromScheme (Box x) = Just $ Just !(fromScheme x) - fromScheme _ = Nothing + fromScheme obj = + case prim_isNil obj == 1 of + True => Just Nothing + False => case prim_isBox obj == 1 of + False => Nothing + True => Just $ Just !(fromScheme $ unsafeUnbox obj) ||| Creates and returns a new `Channel`. ||| @@ -393,7 +368,7 @@ partial export channelGetNonBlocking : HasIO io => FromScheme a => (chan : Channel a) -> io (Maybe a) channelGetNonBlocking chan = - pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetNonBlocking chan)) + pure $ fromScheme !(primIO (prim__channelGetNonBlocking chan)) ||| Timeout version of channelGet. ||| Continously loops with 1ms delays until `seconds` has elapsed, or a value is provided through `chan`. @@ -404,7 +379,7 @@ partial export channelGetWithTimeout : HasIO io => FromScheme a => (chan : Channel a) -> (seconds : Nat) -> io (Maybe a) channelGetWithTimeout chan seconds = - pure $ (fromScheme . decodeObj) !(primIO (prim__channelGetWithTimeout chan seconds)) + pure $ fromScheme !(primIO (prim__channelGetWithTimeout chan seconds)) ||| Puts a value on the given channel. ||| From 6b13dc8106ce9fd5c6b237118796cf306e41eab5 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 7 Dec 2024 17:47:50 -0600 Subject: [PATCH 51/53] Addressing @cypheon's comments. --- libs/base/System/Concurrency.idr | 178 ++----------------------------- support/chez/support.ss | 59 +++++----- tests/chez/channels007/Main.idr | 24 +++++ tests/chez/channels007/expected | 3 + tests/chez/channels007/run | 3 + tests/chez/channels008/Main.idr | 23 ++++ tests/chez/channels008/expected | 1 + tests/chez/channels008/run | 3 + 8 files changed, 102 insertions(+), 192 deletions(-) create mode 100644 tests/chez/channels007/Main.idr create mode 100644 tests/chez/channels007/expected create mode 100644 tests/chez/channels007/run create mode 100644 tests/chez/channels008/Main.idr create mode 100644 tests/chez/channels008/expected create mode 100644 tests/chez/channels008/run diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index ef0e470d2b..5cc521737b 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -179,170 +179,17 @@ barrierWait barrier = primIO (prim__barrierWait barrier) export data Channel : Type -> Type where [external] -data ChannelObj : Type where [external] - -%foreign "scheme:blodwen-is-number" -prim_isNumber : ChannelObj -> Int -%foreign "scheme:blodwen-is-integer" -prim_isInteger : ChannelObj -> Int -%foreign "scheme:blodwen-is-float" -prim_isFloat : ChannelObj -> Int -%foreign "scheme:blodwen-is-char" -prim_isChar : ChannelObj -> Int -%foreign "scheme:blodwen-is-string" -prim_isString : ChannelObj -> Int -%foreign "scheme:blodwen-is-procedure" -prim_isProcedure : ChannelObj -> Int -%foreign "scheme:blodwen-is-symbol" -prim_isSymbol : ChannelObj -> Int -%foreign "scheme:blodwen-is-nil" -prim_isNil : ChannelObj -> Int -%foreign "scheme:blodwen-is-pair" -prim_isPair : ChannelObj -> Int -%foreign "scheme:blodwen-is-vector" -prim_isVector : ChannelObj -> Int -%foreign "scheme:blodwen-is-box" -prim_isBox : ChannelObj -> Int -%foreign "scheme:blodwen-id" -unsafeGetInteger : ChannelObj -> Integer -%foreign "scheme:blodwen-id" -unsafeGetString : ChannelObj -> String -%foreign "scheme:blodwen-id" -unsafeGetFloat : ChannelObj -> Double -%foreign "scheme:blodwen-id" -unsafeGetChar : ChannelObj -> Char -%foreign "scheme:car" -unsafeFst : ChannelObj -> ChannelObj -%foreign "scheme:cdr" -unsafeSnd : ChannelObj -> ChannelObj -%foreign "scheme:blodwen-vector-ref" -unsafeVectorRef : ChannelObj -> Integer -> ChannelObj -%foreign "scheme:blodwen-unbox" -unsafeUnbox : ChannelObj -> ChannelObj -%foreign "scheme:blodwen-vector-length" -unsafeVectorLength : ChannelObj -> Integer -%foreign "scheme:blodwen-vector-list" -unsafeVectorToList : ChannelObj -> List ChannelObj -%foreign "scheme:blodwen-read-symbol" -unsafeReadSymbol : ChannelObj -> String %foreign "scheme:blodwen-make-channel" prim__makeChannel : PrimIO (Channel a) %foreign "scheme:blodwen-channel-get" prim__channelGet : Channel a -> PrimIO a -%foreign "scheme:blodwen-channel-get-non-blocking" -prim__channelGetNonBlocking : Channel a -> PrimIO ChannelObj -%foreign "scheme:blodwen-channel-get-with-timeout" -prim__channelGetWithTimeout : Channel a -> Nat -> PrimIO ChannelObj +%foreign "scheme,chez:blodwen-channel-get-non-blocking" +prim__channelGetNonBlocking : Channel a -> PrimIO (Maybe a) +%foreign "scheme,chez:blodwen-channel-get-with-timeout" +prim__channelGetWithTimeout : Channel a -> Nat -> PrimIO (Maybe a) %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () -export -interface FromScheme a where - fromScheme : ChannelObj -> Maybe a - -partial -private -marshalChannelObj : (pred : ChannelObj -> Int) - -> (unsafeGet : ChannelObj -> a) - -> ChannelObj - -> Maybe a -marshalChannelObj pred unsafeGet obj = - case pred obj of - 1 => Just $ unsafeGet obj - _ => Nothing - -export -FromScheme Integer where - fromScheme = marshalChannelObj prim_isInteger unsafeGetInteger - -export -FromScheme Nat where - fromScheme = marshalChannelObj prim_isInteger (integerToNat . unsafeGetInteger) - -export -FromScheme Int where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme Int8 where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme Int16 where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme Int32 where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme Int64 where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme Bits8 where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme Bits16 where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme Bits32 where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme Bits64 where - fromScheme = marshalChannelObj prim_isInteger (cast . unsafeGetInteger) - -export -FromScheme String where - fromScheme = marshalChannelObj prim_isString unsafeGetString - -export -FromScheme Double where - fromScheme = marshalChannelObj prim_isFloat unsafeGetFloat - -export -FromScheme Char where - fromScheme = marshalChannelObj prim_isChar unsafeGetChar - -export -FromScheme Bool where - fromScheme obj = - case prim_isInteger obj == 1 of - False => Nothing - True => case unsafeGetInteger obj of - 0 => Just False - 1 => Just True - _ => Nothing - -partial -export -FromScheme a => FromScheme (List a) where - fromScheme obj = - case prim_isNil obj == 1 of - True => Just [] - False => case prim_isPair obj == 1 of - False => Nothing - True => Just $ !(fromScheme $ unsafeFst obj) :: !(fromScheme $ unsafeSnd obj) - -export -(FromScheme a, FromScheme b) => FromScheme (a, b) where - fromScheme obj = - case prim_isPair obj == 1 of - False => Nothing - True => Just (!(fromScheme $ unsafeFst obj), !(fromScheme $ unsafeSnd obj)) - -export -FromScheme a => FromScheme (Maybe a) where - fromScheme obj = - case prim_isNil obj == 1 of - True => Just Nothing - False => case prim_isBox obj == 1 of - False => Nothing - True => Just $ Just !(fromScheme $ unsafeUnbox obj) - ||| Creates and returns a new `Channel`. ||| ||| The channel can be used with `channelGet` to receive a value through the @@ -361,25 +208,22 @@ export channelGet : HasIO io => (chan : Channel a) -> io a channelGet chan = primIO (prim__channelGet chan) -||| Non-blocking version of channelGet. +||| Non-blocking version of channelGet (chez backend). ||| ||| @ chan the channel to receive on partial export -channelGetNonBlocking : HasIO io => FromScheme a => (chan : Channel a) -> io (Maybe a) -channelGetNonBlocking chan = - pure $ fromScheme !(primIO (prim__channelGetNonBlocking chan)) +channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a) +channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) -||| Timeout version of channelGet. -||| Continously loops with 1ms delays until `seconds` has elapsed, or a value is provided through `chan`. +||| Timeout version of channelGet (chez backend). ||| ||| @ chan the channel to receive on -||| @ seconds how many seconds to wait until timeout +||| @ milliseconds how many milliseconds to wait until timeout partial export -channelGetWithTimeout : HasIO io => FromScheme a => (chan : Channel a) -> (seconds : Nat) -> io (Maybe a) -channelGetWithTimeout chan seconds = - pure $ fromScheme !(primIO (prim__channelGetWithTimeout chan seconds)) +channelGetWithTimeout : HasIO io => (chan : Channel a) -> (milliseconds : Nat) -> io (Maybe a) +channelGetWithTimeout chan milliseconds = primIO (prim__channelGetWithTimeout chan milliseconds) ||| Puts a value on the given channel. ||| diff --git a/support/chez/support.ss b/support/chez/support.ss index 1f3c6202be..ffb37d4ee1 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -455,34 +455,43 @@ (set-box! read-box #t) (mutex-release (channel-read-mut chan)) (condition-signal read-cv) - the-val) + (box the-val)) )) '())) -(define (blodwen-channel-get-with-timeout ty chan seconds) - (let loop ([start-time (current-time)] - ) - (let ([elapsed (time-difference (current-time) start-time)]) - (if (time>=? elapsed (make-time 'time-duration 0 seconds)) - '() - (if (mutex-acquire (channel-read-mut chan) #f) - (let* ([val-box (channel-val-box chan)] - [the-val (unbox val-box)]) - (if (null? the-val) - (begin - (mutex-release (channel-read-mut chan)) - (sleep (make-time 'time-duration 1000000 0)) - (loop start-time)) - (let* ([read-box (channel-read-box chan)] - [read-cv (channel-read-cv chan)]) - (set-box! val-box '()) - (set-box! read-box #t) - (mutex-release (channel-read-mut chan)) - (condition-signal read-cv) - the-val))) - (begin - (sleep (make-time 'time-duration 1000000 0)) - (loop start-time))))))) +(define (blodwen-channel-get-with-timeout ty chan timeout) + (let loop () + (let* ([sec (div timeout 1000)]) + (if (mutex-acquire (channel-read-mut chan) #f) + (let* ([val-box (channel-val-box chan)] + [val-cv (channel-val-cv chan)] + [the-val (unbox val-box)]) + (if (null? the-val) + (begin + ;; Wait for the condition timeout + (condition-wait val-cv (channel-read-mut chan) (make-time 'time-duration 0 sec)) + (let* ([the-val (unbox val-box)]) ; Check again after wait + (if (null? the-val) + (begin + (mutex-release (channel-read-mut chan)) + '()) ; Still empty after timeout + (let* ([read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)]) + ;; Value now available + (set-box! val-box '()) + (set-box! read-box #t) + (mutex-release (channel-read-mut chan)) + (condition-signal read-cv) + (box the-val))))) + (let* ([read-box (channel-read-box chan)] + [read-cv (channel-read-cv chan)]) + ;; Value available immediately + (set-box! val-box '()) + (set-box! read-box #t) + (mutex-release (channel-read-mut chan)) + (condition-signal read-cv) + (box the-val)))) + loop)))) ; Failed to acquire mutex ;; Mutex diff --git a/tests/chez/channels007/Main.idr b/tests/chez/channels007/Main.idr new file mode 100644 index 0000000000..4958eda431 --- /dev/null +++ b/tests/chez/channels007/Main.idr @@ -0,0 +1,24 @@ +import System +import System.Concurrency + +-- Test that using channelGetNonBlocking works as expected. +main : IO () +main = do + chan <- makeChannel + threadID <- fork $ do + channelPut chan "Hello" + channelPut chan "Goodbye" + sleep 1 + case !(channelGetNonBlocking chan) of + Nothing => putStrLn "Nothing" + Just val' => putStrLn val' + sleep 1 + case !(channelGetNonBlocking chan) of + Nothing => putStrLn "Nothing" + Just val' => putStrLn val' + sleep 1 + case !(channelGetNonBlocking chan) of + Nothing => putStrLn "Nothing" + Just val' => putStrLn val' + sleep 1 + diff --git a/tests/chez/channels007/expected b/tests/chez/channels007/expected new file mode 100644 index 0000000000..9b5ee8a709 --- /dev/null +++ b/tests/chez/channels007/expected @@ -0,0 +1,3 @@ +Hello +Goodbye +Nothing diff --git a/tests/chez/channels007/run b/tests/chez/channels007/run new file mode 100644 index 0000000000..c6e6f2ab79 --- /dev/null +++ b/tests/chez/channels007/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run Main.idr diff --git a/tests/chez/channels008/Main.idr b/tests/chez/channels008/Main.idr new file mode 100644 index 0000000000..a57b18035b --- /dev/null +++ b/tests/chez/channels008/Main.idr @@ -0,0 +1,23 @@ +import Data.Maybe +import System +import System.Concurrency + +-- Simple producing thread. +producer : Channel Nat -> Nat -> IO () +producer c n = ignore $ producer' n + where + producer' : Nat -> IO () + producer' Z = pure () + producer' (S n) = do + channelPut c n + sleep 1 + +-- Test that channelGetWithTimeout works as expected. +main : IO () +main = + do c <- makeChannel + tids <- for [0..11] $ \n => fork $ producer c n + vals <- for [0..11] $ \_ => channelGetWithTimeout c 5000 + ignore $ traverse (\t => threadWait t) tids + putStrLn $ show $ sum $ fromMaybe 0 <$> vals + diff --git a/tests/chez/channels008/expected b/tests/chez/channels008/expected new file mode 100644 index 0000000000..c3f407c095 --- /dev/null +++ b/tests/chez/channels008/expected @@ -0,0 +1 @@ +55 diff --git a/tests/chez/channels008/run b/tests/chez/channels008/run new file mode 100644 index 0000000000..c6e6f2ab79 --- /dev/null +++ b/tests/chez/channels008/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run Main.idr From fa50df76de7892dc42f5588a36fb5657a4299242 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Sat, 7 Dec 2024 17:54:35 -0600 Subject: [PATCH 52/53] Removing duplicate tests from allscheme. --- tests/allschemes/channels007/Main.idr | 20 -------------------- tests/allschemes/channels007/expected | 2 -- tests/allschemes/channels007/run | 3 --- tests/allschemes/channels008/Main.idr | 23 ----------------------- tests/allschemes/channels008/expected | 1 - tests/allschemes/channels008/run | 3 --- 6 files changed, 52 deletions(-) delete mode 100644 tests/allschemes/channels007/Main.idr delete mode 100644 tests/allschemes/channels007/expected delete mode 100644 tests/allschemes/channels007/run delete mode 100644 tests/allschemes/channels008/Main.idr delete mode 100644 tests/allschemes/channels008/expected delete mode 100644 tests/allschemes/channels008/run diff --git a/tests/allschemes/channels007/Main.idr b/tests/allschemes/channels007/Main.idr deleted file mode 100644 index 1c3ef4e8aa..0000000000 --- a/tests/allschemes/channels007/Main.idr +++ /dev/null @@ -1,20 +0,0 @@ -import System -import System.Concurrency - --- Test that using channelGetNonBlocking works as expected. -main : IO () -main = do - chan <- makeChannel - threadID <- fork $ do - channelPut chan "Hello" - channelPut chan "Goodbye" - sleep 1 - case !(channelGetNonBlocking chan) of - Nothing => putStrLn "Nothing" - Just val' => putStrLn val' - sleep 1 - case !(channelGetNonBlocking chan) of - Nothing => putStrLn "Nothing" - Just val' => putStrLn val' - sleep 1 - diff --git a/tests/allschemes/channels007/expected b/tests/allschemes/channels007/expected deleted file mode 100644 index c86756d193..0000000000 --- a/tests/allschemes/channels007/expected +++ /dev/null @@ -1,2 +0,0 @@ -Hello -Goodbye diff --git a/tests/allschemes/channels007/run b/tests/allschemes/channels007/run deleted file mode 100644 index c6e6f2ab79..0000000000 --- a/tests/allschemes/channels007/run +++ /dev/null @@ -1,3 +0,0 @@ -. ../../testutils.sh - -run Main.idr diff --git a/tests/allschemes/channels008/Main.idr b/tests/allschemes/channels008/Main.idr deleted file mode 100644 index 81f6d2d7e5..0000000000 --- a/tests/allschemes/channels008/Main.idr +++ /dev/null @@ -1,23 +0,0 @@ -import Data.Maybe -import System -import System.Concurrency - --- Simple producing thread. -producer : Channel Nat -> Nat -> IO () -producer c n = ignore $ producer' n - where - producer' : Nat -> IO () - producer' Z = pure () - producer' (S n) = do - channelPut c n - sleep 1 - --- Test that channelGetWithTimeout works as expected. -main : IO () -main = - do c <- makeChannel - tids <- for [0..11] $ \n => fork $ producer c n - vals <- for [0..11] $ \_ => channelGetWithTimeout c 5 - ignore $ traverse (\t => threadWait t) tids - putStrLn $ show $ sum $ fromMaybe 0 <$> vals - diff --git a/tests/allschemes/channels008/expected b/tests/allschemes/channels008/expected deleted file mode 100644 index c3f407c095..0000000000 --- a/tests/allschemes/channels008/expected +++ /dev/null @@ -1 +0,0 @@ -55 diff --git a/tests/allschemes/channels008/run b/tests/allschemes/channels008/run deleted file mode 100644 index c6e6f2ab79..0000000000 --- a/tests/allschemes/channels008/run +++ /dev/null @@ -1,3 +0,0 @@ -. ../../testutils.sh - -run Main.idr From eddaf30b1cb60f30b1bc0367927391df71416ef6 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Tue, 7 Jan 2025 15:45:56 -0600 Subject: [PATCH 53/53] Changing Nat to Int for FFI type on prim__channelGetWithTimeout. --- libs/base/System/Concurrency.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/libs/base/System/Concurrency.idr b/libs/base/System/Concurrency.idr index 5cc521737b..db600fe03d 100644 --- a/libs/base/System/Concurrency.idr +++ b/libs/base/System/Concurrency.idr @@ -186,7 +186,7 @@ prim__channelGet : Channel a -> PrimIO a %foreign "scheme,chez:blodwen-channel-get-non-blocking" prim__channelGetNonBlocking : Channel a -> PrimIO (Maybe a) %foreign "scheme,chez:blodwen-channel-get-with-timeout" -prim__channelGetWithTimeout : Channel a -> Nat -> PrimIO (Maybe a) +prim__channelGetWithTimeout : Channel a -> Int -> PrimIO (Maybe a) %foreign "scheme:blodwen-channel-put" prim__channelPut : Channel a -> a -> PrimIO () @@ -223,7 +223,7 @@ channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan) partial export channelGetWithTimeout : HasIO io => (chan : Channel a) -> (milliseconds : Nat) -> io (Maybe a) -channelGetWithTimeout chan milliseconds = primIO (prim__channelGetWithTimeout chan milliseconds) +channelGetWithTimeout chan milliseconds = primIO (prim__channelGetWithTimeout chan (cast milliseconds)) ||| Puts a value on the given channel. |||