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

get typed syndicate to work without using the stop list

This commit is contained in:
Sam Caldwell 2020-08-17 11:24:06 -04:00
parent 04995b5fb3
commit a6fc1f20e4
6 changed files with 76 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
racket/typed/core-expressions.rkt
View File

@ -29,12 +29,12 @@
(define-typed-syntax (bind x:id τ:type) ≫
----------------------------------------
[⊢ (error- 'bind "escaped") (⇒ : (Bind τ))])
[⊢ (#%app- error- 'bind "escaped") (⇒ : (Bind τ))])
(define-typed-syntax discard
[_ ≫
--------------------
[⊢ (error- 'discard "escaped") (⇒ : Discard)]])
[⊢ (#%app- error- 'discard "escaped") (⇒ : Discard)]])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Core-ish forms
@ -84,12 +84,13 @@
------------------------------------
[≻ (if e #f (let () s ...))])
;; copied from ext-stlc
(define-typed-syntax let
[(_ ([x e] ...) e_body ...) ⇐ τ_expected ≫
[⊢ e ≫ e- ⇒ : τ_x] ...
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
[[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇐ : τ_expected)
[[x ≫ x- : τ_x] ... ⊢ (block e_body ...) ≫ e_body- (⇐ : τ_expected)
(⇒ ν-ep (~effs eps ...))
(⇒ ν-f (~effs fs ...))
(⇒ ν-s (~effs ss ...))]
@ -101,7 +102,7 @@
[(_ ([x e] ...) e_body ...) ≫
[⊢ e ≫ e- ⇒ : τ_x] ...
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
[[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇒ : τ_body)
[[x ≫ x- : τ_x] ... ⊢ (block e_body ...) ≫ e_body- (⇒ : τ_body)
(⇒ ν-ep (~effs eps ...))
(⇒ ν-f (~effs fs ...))
(⇒ ν-s (~effs ss ...))]
@ -115,7 +116,7 @@
(define-typed-syntax let*
[(_ () e_body ...) ≫
--------
[≻ (begin e_body ...)]]
[≻ (block e_body ...)]]
[(_ ([x e] [x_rst e_rst] ...) e_body ...) ≫
--------
[≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]])
@ -123,7 +124,7 @@
(define-typed-syntax (cond [pred:expr s ...+] ...+) ≫
[⊢ pred ≫ pred- (⇐ : Bool)] ...
#:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure"
[⊢ (begin s ...) ≫ s- (⇒ : τ-s)
[⊢ (block s ...) ≫ s- (⇒ : τ-s)
(⇒ ν-ep (~effs eps ...))
(⇒ ν-f (~effs fs ...))
(⇒ ν-s (~effs ss ...))] ...
@ -141,7 +142,7 @@
#:with (p/e ...) (for/list ([pat (in-syntax #'(p ...))])
(elaborate-pattern/with-type pat #'τ-e))
#:with (([x τ:type] ...) ...) (stx-map pat-bindings #'(p/e ...))
[[x ≫ x- : τ.norm] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s)
[[x ≫ x- : τ.norm] ... ⊢ (block s ...) ≫ s- (⇒ : τ-s)
(⇒ ν-ep (~effs eps ...))
(⇒ ν-f (~effs fs ...))
(⇒ ν-s (~effs ss ...))] ...

28
racket/typed/core-types.rkt
View File

@ -26,6 +26,9 @@
(require rackunit)
(require rackunit/turnstile))
(begin-for-syntax
(current-use-stop-list? #f))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Type Checking Conventions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -1079,7 +1082,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-typed-syntax (lambda ([x:id (~optional (~datum :)) τ:type] ...) body ...+) ≫
[[x ≫ x- : τ] ... ⊢ (begin body ...) ≫ body- (⇒ : τ-e)
[[x ≫ x- : τ] ... ⊢ (block body ...) ≫ body- (⇒ : τ-e)
(⇒ ν-ep (~effs τ-ep ...))
(⇒ ν-s (~effs τ-s ...))
(⇒ ν-f (~effs τ-f ...))]
@ -1265,7 +1268,7 @@
#:with x- (generate-temporary #'x)
#:with x+ (syntax-local-identifier-as-binding #'x)
--------
[⊢ (define/intermediate x+ x- τ.norm e-)
[⊢ (erased (define/intermediate x+ x- τ.norm e-))
(⇒ : ★/t)
(⇒ ν-ep (τ-ep ...))
(⇒ ν-f (τ-f ...))
@ -1276,7 +1279,7 @@
#:with x- (generate-temporary #'x)
#:with x+ (syntax-local-identifier-as-binding #'x)
--------
[⊢ (define/intermediate x+ x- τ e-)
[⊢ (erased (define/intermediate x+ x- τ e-))
(⇒ : ★/t)
(⇒ ν-ep (τ-ep ...))
(⇒ ν-f (τ-f ...))
@ -1284,7 +1287,7 @@
[(_ (f [x (~optional (~datum :)) ty:type] ...
(~or (~datum →) (~datum ->)) ty_out:type)
e ...+) ≫
[⊢ (lambda ([x : ty] ...) (begin e ...)) ≫ e- (⇒ : (~and fun-ty
[⊢ (lambda ([x : ty] ...) (block e ...)) ≫ e- (⇒ : (~and fun-ty
(~→ (~not (~Computation _ ...)) ...
(~Computation (~Value τ-v)
_ ...))))]
@ -1295,7 +1298,7 @@
#;(type->str #'ty_out))
#:with f- (add-orig (generate-temporary #'f) #'f)
--------
[⊢ (define/intermediate f f- fun-ty e-) (⇒ : ★/t)]]
[⊢ (erased (define/intermediate f f- fun-ty e-)) (⇒ : ★/t)]]
[(_ (f [x (~optional (~datum :)) ty] ...)
e ...+) ≫
----------------------------
@ -1307,7 +1310,7 @@
e ...+) ≫
#:with e+ #'(Λ (X ...)
(lambda ([x : ty] ...)
(begin e ...)))
(block e ...)))
[[X ≫ X- :: #%type] ... ⊢ e+ ≫ e-
(⇒ : (~and res-ty
(~∀ (Y ...)
@ -1320,13 +1323,24 @@
#'τ-v #'ty_out)
#:with f- (add-orig (generate-temporary #'f) #'f)
-------------------------------------------------------
[⊢ (define/intermediate f f- res-ty e-) (⇒ : ★/t)]]
[⊢ (erased (define/intermediate f f- res-ty e-)) (⇒ : ★/t)]]
[(_ ((~datum ∀) (X:id ...)
(f [x (~optional (~datum :)) ty] ...))
e ...+) ≫
--------------------------------------------------
[≻ (define (∀ (X ...) (f [x ty] ... -> ★/t)) e ...)]])
(define-typed-syntax block
[(_ e_unit ... e) ≫
#:do [(define-values (e-... τ... ep-effs f-effs s-effs) (walk/bind #'(e_unit ... e)))]
#:with τ (last τ...)
--------
[⊢ (let- () #,@e-...) (⇒ : τ)
(⇒ ν-ep (#,@ep-effs))
(⇒ ν-f (#,@f-effs))
(⇒ ν-s (#,@s-effs))]])
(define-typed-syntax begin
[(_ e_unit ... e) ≫
#:do [(define-values (e-... τ... ep-effs f-effs s-effs) (walk/bind #'(e_unit ... e)))]

42
racket/typed/for-loops.rkt
View File

@ -115,6 +115,14 @@
(type-error #:src e
#:msg "not an iterable type: ~a" τ)]))
(define-for-syntax (bind-renames renames body)
(syntax-parse renames
[([x:id x-:id] ...)
#:with (x-- ...) (map syntax-local-identifier-as-binding (syntax->list #'(x- ...)))
(quasisyntax/loc body
(let- ()
(define-syntax x (make-variable-like-transformer #'x--)) ...
#,body))]))
(define-typed-syntax for/fold
[(for/fold ([acc:id (~optional (~datum :)) τ-acc init])
@ -125,16 +133,15 @@
#:fail-unless (pure? #'init-) "expression must be pure"
#:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
[[x ≫ x-- : τ] ...
[acc ≫ acc- : τ-acc] ⊢ (begin e-body ...) ≫ e-body-
[acc ≫ acc- : τ-acc] ⊢ (block e-body ...) ≫ e-body-
(⇐ : τ-acc)
(⇒ ν-ep (~effs τ-ep ...))
(⇒ ν-s (~effs τ-s ...))
(⇒ ν-f (~effs τ-f ...))]
#:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
-------------------------------------------------------
[⊢ (for/fold- ([acc- init-])
clauses-
e-body--)
#,(bind-renames #'([x-- x-] ...) #'e-body-))
(⇒ : τ-acc)
(⇒ ν-ep (τ-ep ...))
(⇒ ν-s (τ-s ...))
@ -151,34 +158,34 @@
(define-typed-syntax (for/list (clause:iter-clause ...)
e-body ...+) ≫
#:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
[[x ≫ x-- : τ] ... ⊢ (begin e-body ...) ≫ e-body-
[[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
(⇒ : τ-body)
(⇒ ν-ep (~effs τ-ep ...))
(⇒ ν-s (~effs τ-s ...))
(⇒ ν-f (~effs τ-f ...))]
#:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
----------------------------------------------------------------------
[⊢ (for/list- clauses-
e-body--) (⇒ : (List τ-body))
(⇒ ν-ep (τ-ep ...))
(⇒ ν-s (τ-s ...))
(⇒ ν-f (τ-f ...))])
#,(bind-renames #'([x-- x-] ...) #'e-body-))
(⇒ : (List τ-body))
(⇒ ν-ep (τ-ep ...))
(⇒ ν-s (τ-s ...))
(⇒ ν-f (τ-f ...))])
(define-typed-syntax (for/set (clause:iter-clause ...)
e-body ...+) ≫
#:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
[[x ≫ x-- : τ] ... ⊢ (begin e-body ...) ≫ e-body-
[[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
(⇒ : τ-body)
(⇒ ν-ep (~effs τ-ep ...))
(⇒ ν-s (~effs τ-s ...))
(⇒ ν-f (~effs τ-f ...))]
#:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
----------------------------------------------------------------------
[⊢ (for/set- clauses-
e-body--) (⇒ : (Set τ-body))
(⇒ ν-ep (τ-ep ...))
(⇒ ν-s (τ-s ...))
(⇒ ν-f (τ-f ...))])
#,(bind-renames #'([x-- x-] ...) #'e-body-))
(⇒ : (Set τ-body))
(⇒ ν-ep (τ-ep ...))
(⇒ ν-s (τ-s ...))
(⇒ ν-f (τ-f ...))])
(define-typed-syntax (for/sum (clause ...)
e-body ...+) ≫
@ -198,18 +205,17 @@
(define-typed-syntax (for/first (clause:iter-clause ...)
e-body ...+) ≫
#:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
[[x ≫ x-- : τ] ... ⊢ (begin e-body ...) ≫ e-body-
[[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
(⇒ : τ-body)
(⇒ ν-ep (~effs τ-ep ...))
(⇒ ν-s (~effs τ-s ...))
(⇒ ν-f (~effs τ-f ...))]
#:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
[[res ≫ _ : τ-body] ⊢ res ≫ res- (⇒ : _)]
----------------------------------------------------------------------
[⊢ (let- ()
(define- res-
(for/first- clauses-
e-body--))
#,(bind-renames #'([x-- x-] ...) #'e-body-)))
(if- res-
(some res-)
none))

22
racket/typed/roles.rkt
View File

@ -162,7 +162,7 @@
#:with (τ ...) (stx-map type-eval #'((Field τ-f.norm) ...))
#:with MF (type-eval #'MakesField)
----------------------------------------------------------------------
[⊢ (field/intermediate [x x- τ e-] ...)
[⊢ (erased (field/intermediate [x x- τ e-] ...))
(⇒ : ★/t)
(⇒ ν-ep (MF))])
@ -200,7 +200,7 @@
(define-typed-syntax (stop facet-name:id cont ...) ≫
[⊢ facet-name ≫ facet-name- (⇐ : FacetName)]
[⊢ (begin #f cont ...) ≫ cont-
[⊢ (block #f cont ...) ≫ cont-
(⇒ ν-ep (~effs))
(⇒ ν-s (~effs))
(⇒ ν-f (~effs τ-f ...))]
@ -256,7 +256,7 @@
(define-typed-syntax on
#:datum-literals (start stop)
[(on start s ...) ≫
[⊢ (begin s ...) ≫ s- (⇒ ν-ep (~effs))
[⊢ (block s ...) ≫ s- (⇒ ν-ep (~effs))
(⇒ ν-f (~effs τ-f ...))
(⇒ ν-s (~effs τ-s ...))]
#:with τ-r (type-eval #'(Reacts OnStart τ-f ... τ-s ...))
@ -264,7 +264,7 @@
[⊢ (syndicate:on-start s-) (⇒ : ★/t)
(⇒ ν-ep (τ-r))]]
[(on stop s ...) ≫
[⊢ (begin s ...) ≫ s- (⇒ ν-ep (~effs))
[⊢ (block s ...) ≫ s- (⇒ ν-ep (~effs))
(⇒ ν-f (~effs τ-f ...))
(⇒ ν-s (~effs τ-s ...))]
#:with τ-r (type-eval #'(Reacts OnStop τ-f ... τ-s ...))
@ -281,7 +281,7 @@
[⊢ p/e ≫ p-- (⇒ : τp)]
#:fail-unless (pure? #'p--) "pattern not allowed to have effects"
#:with ([x:id τ:type] ...) (pat-bindings #'p/e)
[[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s-
[[x ≫ x- : τ] ... ⊢ (block s ...) ≫ s-
(⇒ ν-ep (~effs))
(⇒ ν-f (~effs τ-f ...))
(⇒ ν-s (~effs τ-s ...))]
@ -295,7 +295,7 @@
(⇒ ν-ep (τ-r))]])
(define-typed-syntax (begin/dataflow s ...+) ≫
[⊢ (begin s ...) ≫ s-
[⊢ (block s ...) ≫ s-
(⇒ : _)
(⇒ ν-ep (~effs))
(⇒ ν-f (~effs τ-f ...))
@ -319,7 +319,7 @@
;; TODO: check that each τ-f is a Role
#:mode (communication-type-mode #'τ-c.norm)
[
[⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
[⊢ (block s) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
]
;; TODO: s shouldn't refer to facets or fields!
#:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-f ...))
@ -570,11 +570,15 @@
;; n.b. this is a blocking operation, so an actor that uses this internally
;; won't necessarily terminate.
(define-typed-syntax (run-ground-dataspace τ-c:type s ...) ≫
[⊢ (dataspace τ-c s ...) ≫ ((~literal erased) ((~literal syndicate:dataspace) s- ...)) (⇒ : t)]
;;#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
#:mode (communication-type-mode #'τ-c.norm)
[
[⊢ s ≫ s- (⇒ : t1)] ...
[⊢ (dataspace τ-c.norm s- ...) ≫ _ (⇒ : t2)]
]
-----------------------------------------------------------------------------------
[⊢ (#%app- syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-c))])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Utilities
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

9
racket/typed/tests/for-loop-regression.rkt Normal file
View File

@ -0,0 +1,9 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type (for/list ([x (for/list ([y (list 1 2 3)])
y)])
x)
: (List Int)
⇒ (list 1 2 3))

2
racket/typed/tests/regression-define-with-effects.rkt
View File

@ -3,7 +3,7 @@
(require rackunit/turnstile)
(check-type
(begin
(let ()
(field [boo Int 0])
(define x (begin (send! "hi") 5))
;; relying on `set` not allowing effects for this to be a good test