From 65d14de735b58003782dd042d3cef6574ef8b424 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Thu, 5 Mar 2020 10:37:50 -0500 Subject: [PATCH] track branching for each kind of effect in match --- racket/typed/core-expressions.rkt | 7 ++++--- racket/typed/roles.rkt | 1 + 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/racket/typed/core-expressions.rkt b/racket/typed/core-expressions.rkt index 4f9095e..6480f4f 100644 --- a/racket/typed/core-expressions.rkt +++ b/racket/typed/core-expressions.rkt @@ -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- (⇒ : τ)] ... diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index fe576c4..d8bd35a 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -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