query-value

racket/typed/examples/roles/simple-query-value.rkt

@@ -0,0 +1,21 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; query: 0
+;; query: 19
+
+(define-type-alias ds-type
+  (U (Tuple String Int)
+     (Observe ★/t)))
+
+(dataspace ds-type
+  (spawn ds-type
+    (start-facet querier
+      (define/query-value key 0 (tuple "key" (bind v Int)) (+ v 1))
+      (assert (tuple "query" (ref key)))))
+  (spawn ds-type
+    (start-facet client
+      (assert (tuple "key" 18))
+      (during (tuple "query" (bind v Int))
+        (on start
+            (printf "query: ~v\n" v))))))

racket/typed/roles.rkt

@@ -13,7 +13,7 @@
          ;; Statements
          let let* if spawn dataspace start-facet set! begin stop #;unsafe-do
          ;; Derived Forms
-         during
+         during define/query-value
          ;; endpoints
          assert on field
          ;; expressions
@@ -648,28 +648,9 @@
                                  (add-orig (assign-type #'#,x- #'#,t #:wrap? #f) #'#,x))
                               ctx))
 
-;; -> (Values e-... (Listof Type) (Listof EndpointEffects) (Listof FacetEffects) (Listof SpawnEffects))
-;; recognizes local binding forms
-;; (field/intermediate [x e] ...
-;; (define/intermediate x x- τ e)
-(define-for-syntax (walk/bind e...
-                              [def-ctx (syntax-local-make-definition-context)]
-                              [unique (gensym 'walk/bind)])
-  (define-values (rev-e-... rev-τ... ep-effects facet-effects spawn-effects)
-    (for/fold ([rev-e-... '()]
-               [rev-τ... '()]
-               [ep-effects '()]
-               [facet-effects '()]
-               [spawn-effects '()])
-              ([e (in-syntax e...)])
-      (define e- (local-expand e (list unique) (list #'erased) def-ctx))
-      (define τ (syntax-property e- ':))
-      (define-values (ep-effs f-effs s-effs)
-        (values (syntax->list (get-effect e- 'ep))
-                (syntax->list (get-effect e- 'f))
-                (syntax->list (get-effect e- 's))))
-      (syntax-parse e-
-        #:literals (erased field/intermediate define/intermediate)
+(define-for-syntax (add-bindings-to-ctx e- def-ctx)
+  (syntax-parse e-
+        #:literals (erased field/intermediate define/intermediate begin-)
         [(erased (field/intermediate (x:id x-:id τ e-) ...))
          (for ([orig-name (in-syntax #'(x ... ))]
                [new-name (in-syntax #'(x- ...))]
@@ -677,12 +658,52 @@
            (int-def-ctx-bind-type-rename orig-name new-name field-ty def-ctx))]
         [(erased (define/intermediate x:id x-:id τ e-))
          (int-def-ctx-bind-type-rename #'x #'x- #'τ def-ctx)]
-        [_ (void)])
-      (values (cons e- rev-e-...)
-              (cons τ rev-τ...)
-              (append ep-effs ep-effects)
-              (append f-effs facet-effects)
-              (append s-effs spawn-effects))))
+        #;[(erased (begin- e ...))
+         (for ([e (in-syntax #'(e ...))])
+           (add-bindings-to-ctx e def-ctx))]
+        [_ (void)]))
+
+;; -> (Values e-... (Listof Type) (Listof EndpointEffects) (Listof FacetEffects) (Listof SpawnEffects))
+;; recognizes local binding forms
+;; (field/intermediate [x e] ...
+;; (define/intermediate x x- τ e)
+(define-for-syntax (walk/bind e...
+                              [def-ctx (syntax-local-make-definition-context #f #f)]
+                              [unique (gensym 'walk/bind)])
+  (define-values (rev-e-... rev-τ... ep-effects facet-effects spawn-effects)
+    (let loop ([e... (syntax->list e...)]
+               [rev-e-... '()]
+               [rev-τ... '()]
+               [ep-effects '()]
+               [facet-effects '()]
+               [spawn-effects '()])
+      (match e...
+        ['()
+         (values rev-e-... rev-τ... ep-effects facet-effects spawn-effects)]
+        [(cons e more)
+         (define e- (local-expand e (list unique) (list #'erased #'begin) def-ctx))
+         (syntax-parse e-
+           #:literals (begin)
+           [(begin e ...)
+            (loop (append (syntax->list #'(e ...)) more)
+                  rev-e-...
+                  rev-τ...
+                  ep-effects
+                  facet-effects
+                  spawn-effects)]
+           [_
+            (define τ (syntax-property e- ':))
+            (define-values (ep-effs f-effs s-effs)
+              (values (syntax->list (get-effect e- 'ep))
+                      (syntax->list (get-effect e- 'f))
+                      (syntax->list (get-effect e- 's))))
+            (add-bindings-to-ctx e- def-ctx)
+            (loop more
+                  (cons e- rev-e-...)
+                  (cons τ rev-τ...)
+                  (append ep-effs ep-effects)
+                  (append f-effs facet-effects)
+                  (append s-effs spawn-effects))])])))
   (values (reverse rev-e-...)
           (reverse rev-τ...)
           ep-effects
@@ -915,14 +936,22 @@
       [_
        pat])))
 
+(define-typed-syntax (define/query-value x:id e0 p e) ≫
+  [⊢ e0 ≫ e0- (⇒ : τ)]
+  #:fail-unless (pure? #'e0-) "expression must be pure"
+  ----------------------------------------
+  [≻ (begin (field [x τ e0-])
+            (on (asserted p)
+                (set! x e))
+            (on (retracted p)
+                (set! x e0-)))])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Expressions
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (define-typed-syntax (ref x:id) ≫
-  ;; #:do [(printf "reference info ~a\n" (syntax-debug-info #'x))]
   [⊢ x ≫ x- ⇒ (~Field τ)]
-  ;; #:do [(printf "~a ≫ ~a\n" #'x #'x-)]
   ------------------------
   [⊢ (x-) (⇒ : τ)])