diff --git a/racket/typed/examples/roles/simple-query-value.rkt b/racket/typed/examples/roles/simple-query-value.rkt new file mode 100644 index 0000000..32c51c5 --- /dev/null +++ b/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)))))) \ No newline at end of file diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 2e2d490..b2cfcf8 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 + 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-) (⇒ : τ)])