track branching for each kind of effect in match
This commit is contained in:
parent
7ceed8e952
commit
6c79e5cd5c
|
@ -158,10 +158,11 @@
|
|||
[⊢ (match- e- [p- s-] ...
|
||||
[_ (#%app- error- "incomplete pattern match")])
|
||||
(⇒ : (U τ-s ...))
|
||||
;; TODO losing branching information here
|
||||
(⇒ ν-ep (eps ... ...))
|
||||
(⇒ ν-ep #,(make-Branch #'((eps ...) ...)))
|
||||
(⇒ ν-f #,(make-Branch #'((fs ...) ...)))
|
||||
(⇒ ν-s (ss ... ...))])
|
||||
(⇒ ν-s #,(make-Branch #'((ss ...) ...)))])
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax (tuple e:expr ...) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)] ...
|
||||
|
|
|
@ -310,6 +310,7 @@
|
|||
identity))
|
||||
|
||||
(define-typed-syntax spawn
|
||||
;; TODO - do the lack of #:cut-s cause bad error messages here?
|
||||
[(spawn τ-c:type s) ≫
|
||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
;; TODO: check that each τ-f is a Role
|
||||
|
|
Loading…
Reference in New Issue