Use the communication type (via a turnstile `mode`) when elaborating
patterns in facets
This commit is contained in:
parent
296a77d714
commit
22a228ab4b
|
@ -78,6 +78,7 @@
|
||||||
|
|
||||||
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
|
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
|
||||||
(require macrotypes/postfix-in)
|
(require macrotypes/postfix-in)
|
||||||
|
(require (for-syntax turnstile/mode))
|
||||||
(require (postfix-in - racket/list))
|
(require (postfix-in - racket/list))
|
||||||
(require (postfix-in - racket/set))
|
(require (postfix-in - racket/set))
|
||||||
|
|
||||||
|
@ -93,6 +94,22 @@
|
||||||
(define-simple-macro (assertion-struct name:id (~datum :) Name:id (slot:id ...))
|
(define-simple-macro (assertion-struct name:id (~datum :) Name:id (slot:id ...))
|
||||||
(define-constructor* (name : Name slot ...)))
|
(define-constructor* (name : Name slot ...)))
|
||||||
|
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
;; Compile-time State
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
(define current-communication-type (make-parameter #f))
|
||||||
|
;; Type -> Mode
|
||||||
|
(define (communication-type-mode ty)
|
||||||
|
(make-param-mode current-communication-type ty))
|
||||||
|
|
||||||
|
(define (elaborate-pattern/with-com-ty pat)
|
||||||
|
(define τ? (current-communication-type))
|
||||||
|
(if τ?
|
||||||
|
(elaborate-pattern/with-type pat τ?)
|
||||||
|
(elaborate-pattern pat))))
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Core forms
|
;; Core forms
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
@ -193,7 +210,7 @@
|
||||||
[⊢ (syndicate:on-stop s-) (⇒ : ★/t)
|
[⊢ (syndicate:on-stop s-) (⇒ : ★/t)
|
||||||
(⇒ ν-ep (τ-r))]]
|
(⇒ ν-ep (τ-r))]]
|
||||||
[(on (a/r/m:asserted/retracted/message p) s ...) ≫
|
[(on (a/r/m:asserted/retracted/message p) s ...) ≫
|
||||||
#:with p/e (elaborate-pattern #'p)
|
#:with p/e (elaborate-pattern/with-com-ty #'p)
|
||||||
[⊢ p/e ≫ p-- (⇒ : τp)]
|
[⊢ p/e ≫ p-- (⇒ : τp)]
|
||||||
#:fail-unless (pure? #'p--) "pattern not allowed to have effects"
|
#:fail-unless (pure? #'p--) "pattern not allowed to have effects"
|
||||||
#:with ([x:id τ:type] ...) (pat-bindings #'p/e)
|
#:with ([x:id τ:type] ...) (pat-bindings #'p/e)
|
||||||
|
@ -227,10 +244,14 @@
|
||||||
(lambda (id) #`($ #,id))
|
(lambda (id) #`($ #,id))
|
||||||
identity))
|
identity))
|
||||||
|
|
||||||
(define-typed-syntax (spawn τ-c:type s) ≫
|
(define-typed-syntax spawn
|
||||||
|
[(spawn τ-c:type s) ≫
|
||||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||||
;; TODO: check that each τ-f is a Role
|
;; TODO: check that each τ-f is a Role
|
||||||
[⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
|
#:mode (communication-type-mode #'τ-c.norm)
|
||||||
|
[
|
||||||
|
[⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
|
||||||
|
]
|
||||||
;; TODO: s shouldn't refer to facets or fields!
|
;; TODO: s shouldn't refer to facets or fields!
|
||||||
#:with (τ-i τ-o τ-a) (analyze-roles #'(τ-f ...))
|
#:with (τ-i τ-o τ-a) (analyze-roles #'(τ-f ...))
|
||||||
#:fail-unless (<: #'τ-o #'τ-c.norm)
|
#:fail-unless (<: #'τ-o #'τ-c.norm)
|
||||||
|
@ -244,11 +265,19 @@
|
||||||
#:with τ-final (type-eval #'(Actor τ-c.norm))
|
#:with τ-final (type-eval #'(Actor τ-c.norm))
|
||||||
--------------------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------------------
|
||||||
[⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
|
[⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
|
||||||
(⇒ ν-s (τ-final))])
|
(⇒ ν-s (τ-final))]]
|
||||||
|
[(spawn s) ≫
|
||||||
|
#:do [(define τc (current-communication-type))]
|
||||||
|
#:when τc
|
||||||
|
----------------------------------------
|
||||||
|
[≻ (spawn #,τc s)]])
|
||||||
|
|
||||||
(define-typed-syntax (dataspace τ-c:type s ...) ≫
|
(define-typed-syntax (dataspace τ-c:type s ...) ≫
|
||||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||||
[⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs))] ...
|
#:mode (communication-type-mode #'τ-c.norm)
|
||||||
|
[
|
||||||
|
[⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs))] ...
|
||||||
|
]
|
||||||
#:with τ-actor (type-eval #'(Actor τ-c.norm))
|
#:with τ-actor (type-eval #'(Actor τ-c.norm))
|
||||||
#:fail-unless (stx-andmap (lambda (t) (<: t #'τ-actor)) #'(τ-s ... ...))
|
#:fail-unless (stx-andmap (lambda (t) (<: t #'τ-actor)) #'(τ-s ... ...))
|
||||||
"Not all actors conform to communication type"
|
"Not all actors conform to communication type"
|
||||||
|
@ -272,7 +301,7 @@
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
(define-typed-syntax (during p s ...) ≫
|
(define-typed-syntax (during p s ...) ≫
|
||||||
#:with p+ (elaborate-pattern #'p)
|
#:with p+ (elaborate-pattern/with-com-ty #'p)
|
||||||
#:with inst-p (instantiate-pattern #'p+)
|
#:with inst-p (instantiate-pattern #'p+)
|
||||||
----------------------------------------
|
----------------------------------------
|
||||||
[≻ (on (asserted p+)
|
[≻ (on (asserted p+)
|
||||||
|
@ -313,7 +342,7 @@
|
||||||
|
|
||||||
;; TODO: #:on-add
|
;; TODO: #:on-add
|
||||||
(define-typed-syntax (define/query-set x:id p e) ≫
|
(define-typed-syntax (define/query-set x:id p e) ≫
|
||||||
#:with p+ (elaborate-pattern #'p)
|
#:with p+ (elaborate-pattern/with-com-ty #'p)
|
||||||
#:with ([y τ] ...) (pat-bindings #'p+)
|
#:with ([y τ] ...) (pat-bindings #'p+)
|
||||||
;; e will be re-expanded :/
|
;; e will be re-expanded :/
|
||||||
[[y ≫ y- : τ] ... ⊢ e ≫ e- ⇒ τ-e]
|
[[y ≫ y- : τ] ... ⊢ e ≫ e- ⇒ τ-e]
|
||||||
|
@ -325,7 +354,7 @@
|
||||||
(set! x (set-remove (ref x) e))))])
|
(set! x (set-remove (ref x) e))))])
|
||||||
|
|
||||||
(define-typed-syntax (define/query-hash x:id p e-key e-value) ≫
|
(define-typed-syntax (define/query-hash x:id p e-key e-value) ≫
|
||||||
#:with p+ (elaborate-pattern #'p)
|
#:with p+ (elaborate-pattern/with-com-ty #'p)
|
||||||
#:with ([y τ] ...) (pat-bindings #'p+)
|
#:with ([y τ] ...) (pat-bindings #'p+)
|
||||||
;; e-key and e-value will be re-expanded :/
|
;; e-key and e-value will be re-expanded :/
|
||||||
;; but it's the most straightforward way to keep bindings in sync with
|
;; but it's the most straightforward way to keep bindings in sync with
|
||||||
|
@ -426,7 +455,7 @@
|
||||||
(check-type (spawn (U (Message (Tuple String Int))
|
(check-type (spawn (U (Message (Tuple String Int))
|
||||||
(Observe (Tuple String ★/t)))
|
(Observe (Tuple String ★/t)))
|
||||||
(start-facet echo
|
(start-facet echo
|
||||||
(on (message (tuple "ping" (bind x Int)))
|
(on (message (tuple "ping" $x))
|
||||||
(send! (tuple "pong" x)))))
|
(send! (tuple "pong" x)))))
|
||||||
: ★/t)
|
: ★/t)
|
||||||
(typecheck-fail (spawn (U (Message (Tuple String Int))
|
(typecheck-fail (spawn (U (Message (Tuple String Int))
|
||||||
|
|
|
@ -0,0 +1,20 @@
|
||||||
|
#lang typed/syndicate/roles
|
||||||
|
|
||||||
|
(require rackunit/turnstile)
|
||||||
|
|
||||||
|
(define-type-alias τc
|
||||||
|
(U (Tuple Int)
|
||||||
|
(Observe (Tuple ★/t))))
|
||||||
|
|
||||||
|
;; I actually think this is OK, since elaborating the pattern inserts a type
|
||||||
|
;; that will still be checked by `project-safe?`
|
||||||
|
|
||||||
|
(check-type (lambda ()
|
||||||
|
(spawn τc
|
||||||
|
(begin
|
||||||
|
(define (on!)
|
||||||
|
(on (asserted (tuple $x))
|
||||||
|
#f))
|
||||||
|
(start-facet x
|
||||||
|
(on!)))))
|
||||||
|
: (proc -> ★/t #:spawns ((Actor τc))))
|
Loading…
Reference in New Issue