syndicate-lang
/
syndicate-2017
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

rename effect keys to not break with updated turnstile

This commit is contained in:
Sam Caldwell 2018-11-19 17:42:08 -05:00
parent d8df2beb3e
commit 221a550aed
1 changed files with 88 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

176
racket/typed/roles.rkt
View File

@ -53,7 +53,7 @@
(module+ test (module+ test
(require rackunit) (require rackunit)
(require turnstile/rackunit-typechecking)) (require rackunit/turnstile))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Debugging ;; Debugging
@ -66,11 +66,11 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; : describes the immediate result of evaluation ;; : describes the immediate result of evaluation
;; ep key aggregates endpoint affects: ;; ν-ep key aggregates endpoint affects:
;; `Shares`, `Reacts`, and `MakesField` ;; `Shares`, `Reacts`, and `MakesField`
;; Note thar MakesField is only an effect, not a type ;; Note thar MakesField is only an effect, not a type
;; f key aggregates facet effects (starting a facet) as `Role`s and message sends, `Sends` ;; ν-f key aggregates facet effects (starting a facet) as `Role`s and message sends, `Sends`
;; s key aggregates spawned actors as `Actor`s ;; ν-s key aggregates spawned actors as `Actor`s
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Types ;; Types
@ -942,7 +942,7 @@
;; DesugaredSyntax -> Bool ;; DesugaredSyntax -> Bool
(define-for-syntax (pure? e-) (define-for-syntax (pure? e-)
(for/and ([key (in-list '(ep f s))]) (for/and ([key (in-list '(ν-ep ν-f ν-s))])
(effect-free? e- key))) (effect-free? e- key)))
;; (SyntaxOf DesugaredSyntax ...) -> Bool ;; (SyntaxOf DesugaredSyntax ...) -> Bool
@ -1017,9 +1017,9 @@
[_ [_
(define τ (syntax-property e- ':)) (define τ (syntax-property e- ':))
(define-values (ep-effs f-effs s-effs) (define-values (ep-effs f-effs s-effs)
(values (syntax->list (get-effect e- 'ep)) (values (syntax->list (get-effect e- 'ν-ep))
(syntax->list (get-effect e- 'f)) (syntax->list (get-effect e- 'ν-f))
(syntax->list (get-effect e- 's)))) (syntax->list (get-effect e- 'ν-s))))
(add-bindings-to-ctx e- def-ctx) (add-bindings-to-ctx e- def-ctx)
(loop more (loop more
(cons e- rev-e-...) (cons e- rev-e-...)
@ -1060,7 +1060,7 @@
[⊢ (syndicate:react (let- ([#,name-- (syndicate:current-facet-id)]) [⊢ (syndicate:react (let- ([#,name-- (syndicate:current-facet-id)])
#,@ep-...)) #,@ep-...))
(⇒ : ★/t) (⇒ : ★/t)
(⇒ f (τ))]) (⇒ ν-f (τ))])
(define-typed-syntax (field [x:id τ-f:type e:expr] ...) ≫ (define-typed-syntax (field [x:id τ-f:type e:expr] ...) ≫
#:fail-unless (stx-andmap flat-type? #'(τ-f ...)) "keep your uppity data outta my fields" #:fail-unless (stx-andmap flat-type? #'(τ-f ...)) "keep your uppity data outta my fields"
@ -1072,7 +1072,7 @@
---------------------------------------------------------------------- ----------------------------------------------------------------------
[⊢ (field/intermediate [x x- τ e-] ...) [⊢ (field/intermediate [x x- τ e-] ...)
(⇒ : ★/t) (⇒ : ★/t)
(⇒ ep (MF))]) (⇒ ν-ep (MF))])
(define-syntax (field/intermediate stx) (define-syntax (field/intermediate stx)
(syntax-parse stx (syntax-parse stx
@ -1085,7 +1085,7 @@
#:with τs (type-eval #'(Shares τ)) #:with τs (type-eval #'(Shares τ))
------------------------------------- -------------------------------------
[⊢ (syndicate:assert e-) (⇒ : ★/t) [⊢ (syndicate:assert e-) (⇒ : ★/t)
(⇒ ep (τs))]) (⇒ ν-ep (τs))])
(define-typed-syntax (send! e:expr) ≫ (define-typed-syntax (send! e:expr) ≫
[⊢ e ≫ e- (⇒ : τ)] [⊢ e ≫ e- (⇒ : τ)]
@ -1093,15 +1093,15 @@
#:with τm (type-eval #'(Sends τ)) #:with τm (type-eval #'(Sends τ))
-------------------------------------- --------------------------------------
[⊢ (syndicate:send! e-) (⇒ : ★/t) [⊢ (syndicate:send! e-) (⇒ : ★/t)
(⇒ f (τm))]) (⇒ ν-f (τm))])
(define-typed-syntax (stop facet-name:id cont ...) ≫ (define-typed-syntax (stop facet-name:id cont ...) ≫
[⊢ facet-name ≫ facet-name- (⇐ : FacetName)] [⊢ facet-name ≫ facet-name- (⇐ : FacetName)]
[⊢ (begin #f cont ...) ≫ cont- (⇒ ep (~effs)) (⇒ s (~effs)) (⇒ f (~effs τ-f ...))] [⊢ (begin #f cont ...) ≫ cont- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
#:with τ (mk-Stop- #`(facet-name- τ-f ...)) #:with τ (mk-Stop- #`(facet-name- τ-f ...))
--------------------------------------------------------------------------------- ---------------------------------------------------------------------------------
[⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t) [⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t)
(⇒ f (τ))]) (⇒ ν-f (τ))])
(begin-for-syntax (begin-for-syntax
(define-syntax-class asserted/retracted/message (define-syntax-class asserted/retracted/message
@ -1118,48 +1118,48 @@
(define-typed-syntax on (define-typed-syntax on
[(on (~literal start) s ...) ≫ [(on (~literal start) s ...) ≫
[⊢ (begin s ...) ≫ s- (⇒ ep (~effs)) [⊢ (begin s ...) ≫ s- (⇒ ν-ep (~effs))
(⇒ f (~effs τ-f ...)) (⇒ ν-f (~effs τ-f ...))
(⇒ s (~effs τ-s ...))] (⇒ ν-s (~effs τ-s ...))]
#:with τ-r (type-eval #'(Reacts OnStart τ-f ... τ-s ...)) #:with τ-r (type-eval #'(Reacts OnStart τ-f ... τ-s ...))
----------------------------------- -----------------------------------
[⊢ (syndicate:on-start s-) (⇒ : ★/t) [⊢ (syndicate:on-start s-) (⇒ : ★/t)
(⇒ ep (τ-r))]] (⇒ ν-ep (τ-r))]]
[(on (~literal stop) s ...) ≫ [(on (~literal stop) s ...) ≫
[⊢ (begin s ...) ≫ s- (⇒ ep (~effs)) [⊢ (begin s ...) ≫ s- (⇒ ν-ep (~effs))
(⇒ f (~effs τ-f ...)) (⇒ ν-f (~effs τ-f ...))
(⇒ s (~effs τ-s ...))] (⇒ ν-s (~effs τ-s ...))]
#:with τ-r (type-eval #'(Reacts OnStop τ-f ... τ-s ...)) #:with τ-r (type-eval #'(Reacts OnStop τ-f ... τ-s ...))
----------------------------------- -----------------------------------
[⊢ (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 ...) ≫
[⊢ p ≫ p-- (⇒ : τp)] [⊢ p ≫ 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) #:with ([x:id τ:type] ...) (pat-bindings #'p)
[[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s- [[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s-
(⇒ ep (~effs)) (⇒ ν-ep (~effs))
(⇒ f (~effs τ-f ...)) (⇒ ν-f (~effs τ-f ...))
(⇒ s (~effs τ-s ...))] (⇒ ν-s (~effs τ-s ...))]
#:with p- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'p)) #:with p- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'p))
#:with τ-r (type-eval #'(Reacts (a/r/m.react-con τp) τ-f ... τ-s ...)) #:with τ-r (type-eval #'(Reacts (a/r/m.react-con τp) τ-f ... τ-s ...))
----------------------------------- -----------------------------------
[⊢ (syndicate:on (a/r/m.syndicate-kw p-) [⊢ (syndicate:on (a/r/m.syndicate-kw p-)
s-) s-)
(⇒ : ★/t) (⇒ : ★/t)
(⇒ ep (τ-r))]]) (⇒ ν-ep (τ-r))]])
(define-typed-syntax (begin/dataflow s ...+) ≫ (define-typed-syntax (begin/dataflow s ...+) ≫
[⊢ (begin s ...) ≫ s- [⊢ (begin s ...) ≫ s-
(⇒ : _) (⇒ : _)
(⇒ ep (~effs)) (⇒ ν-ep (~effs))
(⇒ f (~effs τ-f ...)) (⇒ ν-f (~effs τ-f ...))
(⇒ s (~effs τ-s ...))] (⇒ ν-s (~effs τ-s ...))]
#:with τ-r (type-eval #'(Reacts OnDataflow τ-f ... τ-s ...)) #:with τ-r (type-eval #'(Reacts OnDataflow τ-f ... τ-s ...))
-------------------------------------------------- --------------------------------------------------
[⊢ (syndicate:begin/dataflow s-) [⊢ (syndicate:begin/dataflow s-)
(⇒ : ★/t) (⇒ : ★/t)
(⇒ ep (τ-r))]) (⇒ ν-ep (τ-r))])
;; pat -> ([Id Type] ...) ;; pat -> ([Id Type] ...)
(define-for-syntax (pat-bindings stx) (define-for-syntax (pat-bindings stx)
@ -1215,7 +1215,7 @@
(define-typed-syntax (spawn τ-c:type s) ≫ (define-typed-syntax (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 ...))] [⊢ 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)
@ -1229,11 +1229,11 @@
#: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))])
(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))] ... [⊢ 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"
@ -1242,7 +1242,7 @@
#:with τ-relay (relay-interests #'τ-c.norm) #:with τ-relay (relay-interests #'τ-c.norm)
----------------------------------------------------------------------------------- -----------------------------------------------------------------------------------
[⊢ (syndicate:dataspace s- ...) (⇒ : ★/t) [⊢ (syndicate:dataspace s- ...) (⇒ : ★/t)
(⇒ s ((Actor (U τ-ds-i τ-ds-o τ-relay))))]) (⇒ ν-s ((Actor (U τ-ds-i τ-ds-o τ-relay))))])
(define-typed-syntax (set! x:id e:expr) ≫ (define-typed-syntax (set! x:id e:expr) ≫
[⊢ e ≫ e- (⇒ : τ)] [⊢ e ≫ e- (⇒ : τ)]
@ -1318,9 +1318,9 @@
(define-typed-syntax (lambda ([x:id (~optional (~datum :)) τ:type] ...) body ...+) ≫ (define-typed-syntax (lambda ([x:id (~optional (~datum :)) τ:type] ...) body ...+) ≫
[[x ≫ x- : τ] ... ⊢ (begin body ...) ≫ body- (⇒ : τ-e) [[x ≫ x- : τ] ... ⊢ (begin body ...) ≫ body- (⇒ : τ-e)
(⇒ ep (~effs τ-ep ...)) (⇒ ν-ep (~effs τ-ep ...))
(⇒ s (~effs τ-s ...)) (⇒ ν-s (~effs τ-s ...))
(⇒ f (~effs τ-f ...))] (⇒ ν-f (~effs τ-f ...))]
---------------------------------------- ----------------------------------------
[⊢ (lambda- (x- ...) body-) (⇒ : (→ τ ... (Computation (Value τ-e) [⊢ (lambda- (x- ...) body-) (⇒ : (→ τ ... (Computation (Value τ-e)
(Endpoints τ-ep ...) (Endpoints τ-ep ...)
@ -1339,9 +1339,9 @@
#:fail-unless (stx-andmap pure? #'(e_arg- ...)) "expressions not allowed to have effects" #:fail-unless (stx-andmap pure? #'(e_arg- ...)) "expressions not allowed to have effects"
------------------------------------------------------------------------ ------------------------------------------------------------------------
[⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ-out) [⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ-out)
(⇒ ep (τ-ep ...)) (⇒ ν-ep (τ-ep ...))
(⇒ s (τ-s ...)) (⇒ ν-s (τ-s ...))
(⇒ f (τ-f ...))]) (⇒ ν-f (τ-f ...))])
(define-typed-syntax (tuple e:expr ...) ≫ (define-typed-syntax (tuple e:expr ...) ≫
[⊢ e ≫ e- (⇒ : τ)] ... [⊢ e ≫ e- (⇒ : τ)] ...
@ -1463,27 +1463,27 @@
[⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
#:fail-unless (pure? #'e_tst-) "expression must be pure" #:fail-unless (pure? #'e_tst-) "expression must be pure"
[⊢ e1 ≫ e1- (⇐ : τ-expected) [⊢ e1 ≫ e1- (⇐ : τ-expected)
(⇒ ep (~effs eps1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))] (⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))]
[⊢ e2 ≫ e2- (⇐ : τ-expected) [⊢ e2 ≫ e2- (⇐ : τ-expected)
(⇒ ep (~effs eps2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))] (⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))]
-------- --------
[⊢ (if- e_tst- e1- e2-) [⊢ (if- e_tst- e1- e2-)
(⇒ ep (eps1 ... eps2 ...)) (⇒ ν-ep (eps1 ... eps2 ...))
(⇒ f (fs1 ... fs2 ...)) (⇒ ν-f (fs1 ... fs2 ...))
(⇒ s (ss1 ... ss2 ...))]] (⇒ ν-s (ss1 ... ss2 ...))]]
[(_ e_tst e1 e2) ≫ [(_ e_tst e1 e2) ≫
[⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
#:fail-unless (pure? #'e_tst-) "expression must be pure" #:fail-unless (pure? #'e_tst-) "expression must be pure"
[⊢ e1 ≫ e1- (⇒ : τ1) [⊢ e1 ≫ e1- (⇒ : τ1)
(⇒ ep (~effs eps1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))] (⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))]
[⊢ e2 ≫ e2- (⇒ : τ2) [⊢ e2 ≫ e2- (⇒ : τ2)
(⇒ ep (~effs eps2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))] (⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))]
#:with τ (type-eval #'(U τ1 τ2)) #:with τ (type-eval #'(U τ1 τ2))
-------- --------
[⊢ (if- e_tst- e1- e2-) (⇒ : τ) [⊢ (if- e_tst- e1- e2-) (⇒ : τ)
(⇒ ep (eps1 ... eps2 ...)) (⇒ ν-ep (eps1 ... eps2 ...))
(⇒ f (fs1 ... fs2 ...)) (⇒ ν-f (fs1 ... fs2 ...))
(⇒ s (ss1 ... ss2 ...))]]) (⇒ ν-s (ss1 ... ss2 ...))]])
(define-typed-syntax (when e s ...+) ≫ (define-typed-syntax (when e s ...+) ≫
------------------------------------ ------------------------------------
@ -1500,9 +1500,9 @@
#:with τ (last τ...) #:with τ (last τ...)
-------- --------
[⊢ (begin- #,@e-...) (⇒ : τ) [⊢ (begin- #,@e-...) (⇒ : τ)
(⇒ ep (#,@ep-effs)) (⇒ ν-ep (#,@ep-effs))
(⇒ f (#,@f-effs)) (⇒ ν-f (#,@f-effs))
(⇒ s (#,@s-effs))]]) (⇒ ν-s (#,@s-effs))]])
;; copied from ext-stlc ;; copied from ext-stlc
(define-typed-syntax let (define-typed-syntax let
@ -1510,26 +1510,26 @@
[⊢ e ≫ e- ⇒ : τ_x] ... [⊢ e ≫ e- ⇒ : τ_x] ...
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure" #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
[[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇐ : τ_expected) [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇐ : τ_expected)
(⇒ ep (~effs eps ...)) (⇒ ν-ep (~effs eps ...))
(⇒ f (~effs fs ...)) (⇒ ν-f (~effs fs ...))
(⇒ s (~effs ss ...))] (⇒ ν-s (~effs ss ...))]
---------------------------------------------------------- ----------------------------------------------------------
[⊢ (let- ([x- e-] ...) e_body-) [⊢ (let- ([x- e-] ...) e_body-)
(⇒ ep (eps ...)) (⇒ ν-ep (eps ...))
(⇒ f (fs ...)) (⇒ ν-f (fs ...))
(⇒ s (ss ...))]] (⇒ ν-s (ss ...))]]
[(_ ([x e] ...) e_body ...) ≫ [(_ ([x e] ...) e_body ...) ≫
[⊢ e ≫ e- ⇒ : τ_x] ... [⊢ e ≫ e- ⇒ : τ_x] ...
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure" #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
[[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇒ : τ_body) [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇒ : τ_body)
(⇒ ep (~effs eps ...)) (⇒ ν-ep (~effs eps ...))
(⇒ f (~effs fs ...)) (⇒ ν-f (~effs fs ...))
(⇒ s (~effs ss ...))] (⇒ ν-s (~effs ss ...))]
---------------------------------------------------------- ----------------------------------------------------------
[⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_body) [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_body)
(⇒ ep (eps ...)) (⇒ ν-ep (eps ...))
(⇒ f (fs ...)) (⇒ ν-f (fs ...))
(⇒ s (ss ...))]]) (⇒ ν-s (ss ...))]])
;; copied from ext-stlc ;; copied from ext-stlc
(define-typed-syntax let* (define-typed-syntax let*
@ -1544,23 +1544,23 @@
[⊢ pred ≫ pred- (⇐ : Bool)] ... [⊢ pred ≫ pred- (⇐ : Bool)] ...
#:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure" #:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure"
[⊢ (begin s ...) ≫ s- (⇒ : τ-s) [⊢ (begin s ...) ≫ s- (⇒ : τ-s)
(⇒ ep (~effs eps ...)) (⇒ ν-ep (~effs eps ...))
(⇒ f (~effs fs ...)) (⇒ ν-f (~effs fs ...))
(⇒ s (~effs ss ...))] ... (⇒ ν-s (~effs ss ...))] ...
------------------------------------------------ ------------------------------------------------
[⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...)) [⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...))
(⇒ ep (eps ... ...)) (⇒ ν-ep (eps ... ...))
(⇒ f (fs ... ...)) (⇒ ν-f (fs ... ...))
(⇒ s (ss ... ...))]) (⇒ ν-s (ss ... ...))])
(define-typed-syntax (match e [p s ...+] ...+) ≫ (define-typed-syntax (match e [p s ...+] ...+) ≫
[⊢ e ≫ e- (⇒ : τ-e)] [⊢ e ≫ e- (⇒ : τ-e)]
#:fail-unless (pure? #'e-) "expression must be pure" #:fail-unless (pure? #'e-) "expression must be pure"
#:with (([x τ] ...) ...) (stx-map pat-bindings #'(p ...)) #:with (([x τ] ...) ...) (stx-map pat-bindings #'(p ...))
[[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s) [[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s)
(⇒ ep (~effs eps ...)) (⇒ ν-ep (~effs eps ...))
(⇒ f (~effs fs ...)) (⇒ ν-f (~effs fs ...))
(⇒ s (~effs ss ...))] ... (⇒ ν-s (~effs ss ...))] ...
;; REALLY not sure how to handle p/p-/p.match-pattern, ;; REALLY not sure how to handle p/p-/p.match-pattern,
;; particularly w.r.t. typed terms that appear in p.match-pattern ;; particularly w.r.t. typed terms that appear in p.match-pattern
[⊢ p ≫ p-- ⇒ τ-p] ... [⊢ p ≫ p-- ⇒ τ-p] ...
@ -1574,9 +1574,9 @@
[⊢ (match- e- [p- s-] ... [⊢ (match- e- [p- s-] ...
[_ (error "incomplete pattern match")]) [_ (error "incomplete pattern match")])
(⇒ : (U τ-s ...)) (⇒ : (U τ-s ...))
(⇒ ep (eps ... ...)) (⇒ ν-ep (eps ... ...))
(⇒ f (fs ... ...)) (⇒ ν-f (fs ... ...))
(⇒ s (ss ... ...))]) (⇒ ν-s (ss ... ...))])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Primitives ;; Primitives
@ -1652,17 +1652,17 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-typed-syntax (print-type e) ≫ (define-typed-syntax (print-type e) ≫
[⊢ e ≫ e- (⇒ : τ) (⇒ ep (~effs eps ...)) (⇒ f (~effs fs ...)) (⇒ s (~effs ss ...))] [⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs eps ...)) (⇒ ν-f (~effs fs ...)) (⇒ ν-s (~effs ss ...))]
#:do [(displayln (type->str #'τ))] #:do [(displayln (type->str #'τ))]
---------------------------------- ----------------------------------
[⊢ e- (⇒ : τ) (⇒ ep (eps ...)) (⇒ f (fs ...)) (⇒ s (ss ...))]) [⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
(define-typed-syntax (print-role e) ≫ (define-typed-syntax (print-role e) ≫
[⊢ e ≫ e- (⇒ : τ) (⇒ ep (~effs eps ...)) (⇒ f (~effs fs ...)) (⇒ s (~effs ss ...))] [⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs eps ...)) (⇒ ν-f (~effs fs ...)) (⇒ ν-s (~effs ss ...))]
#:do [(for ([r (in-syntax #'(fs ...))]) #:do [(for ([r (in-syntax #'(fs ...))])
(displayln (type->str r)))] (displayln (type->str r)))]
---------------------------------- ----------------------------------
[⊢ e- (⇒ : τ) (⇒ ep (eps ...)) (⇒ f (fs ...)) (⇒ s (ss ...))]) [⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Lists ;; Lists
@ -1705,15 +1705,15 @@
[⊢ e-list ≫ e-list- ⇒ (~List τ-l)] ... [⊢ e-list ≫ e-list- ⇒ (~List τ-l)] ...
#:fail-unless (all-pure? #'(e-list- ...)) "expressions must be pure" #:fail-unless (all-pure? #'(e-list- ...)) "expressions must be pure"
[[x ≫ x- : τ-l] ... ⊢ (begin e-body ...) ≫ e-body- (⇒ : τ-b) [[x ≫ x- : τ-l] ... ⊢ (begin e-body ...) ≫ e-body- (⇒ : τ-b)
(⇒ ep (~effs eps ...)) (⇒ ν-ep (~effs eps ...))
(⇒ f (~effs fs ...)) (⇒ ν-f (~effs fs ...))
(⇒ s (~effs ss ...))] (⇒ ν-s (~effs ss ...))]
------------------------------------------------------- -------------------------------------------------------
[⊢ (for- ([x- (in-list- e-list-)] ...) [⊢ (for- ([x- (in-list- e-list-)] ...)
e-body-) (⇒ : ★/t) e-body-) (⇒ : ★/t)
(⇒ ep (eps ...)) (⇒ ν-ep (eps ...))
(⇒ f (fs ...)) (⇒ ν-f (fs ...))
(⇒ s (ss ...))]) (⇒ ν-s (ss ...))])
(define-typed-syntax (empty? e) ≫ (define-typed-syntax (empty? e) ≫
[⊢ e ≫ e- ⇒ (~List _)] [⊢ e ≫ e- ⇒ (~List _)]
@ -1887,4 +1887,4 @@
(define id 1234) (define id 1234)
id) id)
(typed-app spawn-cell 42)) (typed-app spawn-cell 42))
1234)) 1234))