From 0f2469c364c5cd07bc507520279aa1d6ed5a3125 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samcaldwell@utexas.edu>
Date: Tue, 14 Aug 2018 16:35:39 -0400
Subject: [PATCH] query set

---
 .../typed/examples/roles/simple-query-set.rkt | 22 ++++++++++++++++++
 racket/typed/roles.rkt                        | 23 +++++++++++++++++--
 2 files changed, 43 insertions(+), 2 deletions(-)
 create mode 100644 racket/typed/examples/roles/simple-query-set.rkt

diff --git a/racket/typed/examples/roles/simple-query-set.rkt b/racket/typed/examples/roles/simple-query-set.rkt
new file mode 100644
index 0000000..059be43
--- /dev/null
+++ b/racket/typed/examples/roles/simple-query-set.rkt
@@ -0,0 +1,22 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; size: 0
+;; size: 2
+
+(define-type-alias ds-type
+  (U (Tuple String Int)
+     (Observe ★/t)))
+
+(dataspace ds-type
+  (spawn ds-type
+    (start-facet querier
+      (define/query-set key (tuple "key" (bind v Int)) v)
+      (assert (tuple "size" (set-count (ref key))))))
+  (spawn ds-type
+    (start-facet client
+      (assert (tuple "key" 18))
+      (assert (tuple "key" 88))
+      (during (tuple "size" (bind v Int))
+        (on start
+            (printf "size: ~v\n" v))))))
\ No newline at end of file
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index b2cfcf8..eb5d66a 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -13,7 +13,7 @@
          ;; Statements
          let let* if spawn dataspace start-facet set! begin stop #;unsafe-do
          ;; Derived Forms
-         during define/query-value
+         during define/query-value define/query-set
          ;; endpoints
          assert on field
          ;; expressions
@@ -30,7 +30,7 @@
          ;; lists
          list first rest member? empty? for for/fold
          ;; sets
-         Set set set-member? set-add set-count set-union set-subtract set-intersect
+         Set set set-member? set-add set-remove set-count set-union set-subtract set-intersect
          list->set set->list
          ;; DEBUG and utilities
          print-type print-role
@@ -946,6 +946,17 @@
             (on (retracted p)
                 (set! x e0-)))])
 
+(define-typed-syntax (define/query-set x:id p e) ≫
+  #:with ([y τ] ...) (pat-bindings #'p)
+  ;; e will be re-expanded :/
+  [[y ≫ y- : τ] ... ⊢ e ≫ e- ⇒ τ-e]
+  ----------------------------------------
+  [≻ (begin (field [x (Set τ-e) (set)])
+            (on (asserted p)
+                (set! x (set-add (ref x) e)))
+            (on (retracted p)
+                (set! x (set-remove (ref x) e))))])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Expressions
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -1370,6 +1381,14 @@
   -------------------------
   [⊢ (set-add- st- v-) ⇒ (Set (U τs τv))])
 
+(define-typed-syntax (set-remove st v) ≫
+  [⊢ st ≫ st- ⇒ (~Set τs)]
+  #:fail-unless (pure? #'st-) "expression must be pure"
+  [⊢ v ≫ v- ⇐ τs]
+  #:fail-unless (pure? #'v-) "expression must be pure"
+  -------------------------
+  [⊢ (set-remove- st- v-) ⇒ (Set τs)])
+
 (define-typed-syntax (set-member? st v) ≫
   [⊢ st ≫ st- ⇒ (~Set τs)]
   #:fail-unless (pure? #'st-) "expression must be pure"