wip
This commit is contained in:
Sam Caldwell
parent
aa5bcee3eb
commit
6f553c6130
|
|
@ -9,18 +9,4 @@
|
|||
(on (asserted (list "hello"))
|
||||
(printf "hello\n")))
|
||||
|
||||
(check-type 1 : Int)
|
||||
|
||||
(check-type (let-field x : Int 5 nil) : ⊥)
|
||||
(check-type (let-field x : Int 5 nil) :2 ⊥)
|
||||
(check-type (let-field x : Int 5 nil) :3 ⊥)
|
||||
|
||||
(check-type (tuple 1 2 3) : (Tuple Int Int Int))
|
||||
|
||||
(typecheck-fail (let-field x : Int 5
|
||||
(let-field y : (Field Int) x nil))
|
||||
#:with-msg "Keep your functions out of fields")
|
||||
|
||||
(check-type (tuple discard 1 (bind x Int)) : (Tuple Discard Int (Bind Int)))
|
||||
|
||||
(check-type (λ [(bind x Int) nil]) : (Case [→ (Bind Int) (Facet ⊥ ⊥ ⊥)]))
|
||||
(spawn ⊥ (assert "hello"))
|
||||
|
|
@ -1,24 +1,28 @@
|
|||
#lang turnstile
|
||||
|
||||
(provide #%module-begin
|
||||
(provide (rename-out [syndicate:#%module-begin #%module-begin])
|
||||
#%app
|
||||
#%top-interaction
|
||||
require
|
||||
Int
|
||||
let-field
|
||||
;; Types
|
||||
Int ⊥ Tuple Bind Discard Case → Facet Field
|
||||
;; Statements
|
||||
nil let-field let-function spawn dataspace facet set! begin stop
|
||||
;; endpoints
|
||||
assert on
|
||||
;; expressions
|
||||
tuple λ ref
|
||||
;; values
|
||||
#%datum
|
||||
Field
|
||||
⊥
|
||||
nil
|
||||
tuple Tuple
|
||||
bind Bind
|
||||
discard Discard
|
||||
+ -
|
||||
λ Case →
|
||||
Facet)
|
||||
;; patterns
|
||||
bind discard
|
||||
;; primitives
|
||||
+ - displayln
|
||||
)
|
||||
|
||||
(require (rename-in racket/match [match-lambda match-lambda-]))
|
||||
(require (prefix-in syndicate: syndicate/actor))
|
||||
(require (prefix-in syndicate: (only-in syndicate/actor-lang #%module-begin)))
|
||||
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
|
|
@ -52,7 +56,8 @@
|
|||
|
||||
(define-syntax-class prim-op
|
||||
(pattern (~or (~literal +)
|
||||
(~literal -))))
|
||||
(~literal -)
|
||||
(~literal displayln))))
|
||||
|
||||
(define-syntax-class stmt
|
||||
#:datum-literals (:
|
||||
|
|
@ -63,10 +68,11 @@
|
|||
spawn
|
||||
dataspace
|
||||
stop
|
||||
facet)
|
||||
facet
|
||||
nil)
|
||||
(pattern (~or (begin seq:stmt ...)
|
||||
(e1:exp e2:exp)
|
||||
nil ;; TODO - remove, only for making some initial examples
|
||||
;; nil ;; TODO - remove, only for making some initial examples
|
||||
(let-field [x:id : τ:type e:exp] lf-body:stmt)
|
||||
(let-function [f:id : τ:type e:exp] let-fun-body:stmt)
|
||||
(set! x:id e:exp)
|
||||
|
|
@ -109,22 +115,6 @@
|
|||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Statements
|
||||
|
||||
#;(define-syntax-class stmt
|
||||
#:datum-literals (spawn
|
||||
dataspace
|
||||
stop
|
||||
facet)
|
||||
(pattern (~or (begin seq:stmt ...)
|
||||
(e1:exp e2:exp)
|
||||
nil ;; TODO - remove, only for making some initial examples
|
||||
(let-field [x:id : τ:type e:exp] lf-body:stmt)
|
||||
(let-function [f:id : τ:type e:exp] let-fun-body:stmt)
|
||||
(set! x:id e:exp)
|
||||
(spawn τ:type s:stmt)
|
||||
(dataspace τ:type nested:stmt ...)
|
||||
(stop x:id s:stmt)
|
||||
(facet x:id ep:endpoint ...))))
|
||||
|
||||
(define-typed-syntax (set! x:id e:exp) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
[⊢ x ≫ x- ⇒ (Field τ-x)]
|
||||
|
|
@ -132,6 +122,41 @@
|
|||
-------------------------
|
||||
[⊢ (x- e-) (⇒ : ⊥) (⇒ :2 ⊥) (⇒ :3 ⊥)])
|
||||
|
||||
(define-typed-syntax (stop facet-name:id cont:stmt) ≫
|
||||
[⊢ facet-name ≫ facet-name- ⇐ Facet]
|
||||
[⊢ cont ≫ cont- (⇒ : τ-i) (⇒ :2 τ-o) (⇒ :3 τ-a)]
|
||||
--------------------------------------------------
|
||||
[⊢ (syndicate:stop facet-name- cont-) (⇒ : τ-i) (⇒ :2 τ-o) (⇒ :3 τ-a)])
|
||||
|
||||
(define-typed-syntax (facet name:id ep:endpoint ...) ≫
|
||||
[[name ≫ name- : Facet] ⊢ ep ≫ ep- (⇒ : τ-i) (⇒ :2 τ-o) (⇒ :3 τ-a)] ...
|
||||
--------------------------------------------------------------
|
||||
;; name NOT name- here because I get an error that way.
|
||||
;; Since name is just an identifier I think it's OK?
|
||||
[⊢ (syndicate:react (let- ([name (syndicate:current-facet-id)]) ep- ...))
|
||||
(⇒ : (U τ-i ...)) (⇒ :2 (U τ-o ...)) (⇒ :3 (U τ-a ...))])
|
||||
|
||||
(define-typed-syntax (dataspace τ-c:type s:stmt ...) ≫
|
||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
[⊢ (spawn s) ≫ (_ s-) ⇒ _] ...
|
||||
#:with τ-i (strip-inbound #'τ-c.norm)
|
||||
#:with τ-o (strip-outbound #'τ-c.norm)
|
||||
#:with τ-relay (relay-interests #'τ-c.norm)
|
||||
----------------------------------------------
|
||||
[⊢ (syndicate:dataspace s- ...) (⇒ : τ-i) (⇒ :2 (U τ-o τ-relay)) (⇒ :3 ⊥)])
|
||||
|
||||
(define-for-syntax (strip-inbound t)
|
||||
(syntax-parse t
|
||||
[_ #'⊥]))
|
||||
|
||||
(define-for-syntax (strip-outbound t)
|
||||
(syntax-parse t
|
||||
[_ #'⊥]))
|
||||
|
||||
(define-for-syntax (relay-interests t)
|
||||
(syntax-parse t
|
||||
[_ #'⊥]))
|
||||
|
||||
(define-typed-syntax (spawn τ-c:type s:stmt) ≫
|
||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
[⊢ s ≫ s- (⇒ : τ-i) (⇒ :2 τ-o) (⇒ :3 τ-a)]
|
||||
|
|
@ -140,14 +165,14 @@
|
|||
;; TODO: (Actor τ-a) <: (Actor τ-c)
|
||||
;; TODO: project-safe(strip-?(τ-o) ∩ τ-c, τ-i)
|
||||
----------------------------------------------
|
||||
[⊢ (syndicate:spawn s-) (⇒ : ⊥) (⇒ :2 ⊥) (⇒ τ-c)])
|
||||
[⊢ (syndicate:spawn s-) (⇒ : ⊥) (⇒ :2 ⊥) (⇒ :3 τ-c)])
|
||||
|
||||
(define-typed-syntax (let-field x:id (~datum :) τ:type e:expr body:expr) ≫
|
||||
[⊢ e ≫ e- (⇐ : τ.norm)]
|
||||
[[x ≫ x- : (Field τ)] ⊢ body ≫ body- (⇒ : τ-body) (⇒ :2 τ-body2) (⇒ :3 τ-body3)]
|
||||
#:fail-unless (flat-type? #'τ.norm) "Keep your functions out of fields"
|
||||
------------------------------------------------------------------------
|
||||
[⊢ (begin- (syndicate:field [x- e-]) body-) (⇒ : τ-body) (⇒ :2 τ-body2) (⇒ :3 τ-body3)])
|
||||
[⊢ (let () (syndicate:field [x- e-]) body-) (⇒ : τ-body) (⇒ :2 τ-body2) (⇒ :3 τ-body3)])
|
||||
|
||||
(define-typed-syntax (let-function f:id (~datum :) τ:type e:expr body:expr) ≫
|
||||
[⊢ e ≫ e- (⇐ : τ.norm)]
|
||||
|
|
@ -177,6 +202,22 @@
|
|||
[(~Field _) #f]
|
||||
[_ #t]))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Endpoints
|
||||
|
||||
#;(define-syntax-class endpoint
|
||||
#:datum-literals (on start stop)
|
||||
(pattern (~or (on ed:event-desc s:stmt)
|
||||
(assert e:exp))))
|
||||
|
||||
(define-typed-syntax (on ed:event-desc s:stmt) ≫
|
||||
-------------------
|
||||
[⊢ (void-) (⇒ : ⊥) (⇒ :2 ⊥) (⇒ :3 ⊥)])
|
||||
|
||||
(define-typed-syntax (assert e:exp) ≫
|
||||
-------------------
|
||||
[⊢ (void-) (⇒ : ⊥) (⇒ :2 ⊥) (⇒ :3 ⊥)])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Expressions
|
||||
|
||||
|
|
@ -233,6 +274,12 @@
|
|||
(define-primop + (→ Int Int Int))
|
||||
(define-primop - (→ Int Int Int))
|
||||
|
||||
(define-typed-syntax (displayln e:exp) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
---------------
|
||||
[⊢ (displayln- e-) ⇒ ⊥])
|
||||
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Basic Values
|
||||
|
||||
|
|
@ -251,20 +298,52 @@
|
|||
;; Tests
|
||||
|
||||
(module+ test
|
||||
(check-true (void? ((λ [(bind x Int) nil]) 1))))
|
||||
(check-type 1 : Int)
|
||||
|
||||
(check-type (let-field x : Int 5 nil) : ⊥)
|
||||
(check-type (let-field x : Int 5 nil) :2 ⊥)
|
||||
(check-type (let-field x : Int 5 nil) :3 ⊥)
|
||||
|
||||
(check-type (tuple 1 2 3) : (Tuple Int Int Int))
|
||||
|
||||
(typecheck-fail (let-field x : Int 5
|
||||
(let-field y : (Field Int) x nil))
|
||||
#:with-msg "Keep your functions out of fields")
|
||||
|
||||
(check-type (tuple discard 1 (bind x Int)) : (Tuple Discard Int (Bind Int)))
|
||||
|
||||
(check-type (λ [(bind x Int) (begin)]) : (Case [→ (Bind Int) (Facet ⊥ ⊥ ⊥)]))
|
||||
(check-true (void? ((λ [(bind x Int) (begin)]) 1))))
|
||||
|
||||
(define bank-account
|
||||
#'(facet account
|
||||
(let-field [balance : Int 0]
|
||||
(begin (assert (list "balance" (ref balance)))
|
||||
(on (asserted (list "deposit" (bind amount Int)))
|
||||
;; this bit isn't valid because `assert` is not a statement
|
||||
(begin (assert (tuple "balance" (ref balance)))
|
||||
(on (asserted (tuple "deposit" (bind amount Int)))
|
||||
(set! balance (+ (ref balance) amount)))))))
|
||||
|
||||
(define client
|
||||
#'(facet client
|
||||
(let-field [deposits : Int 3]
|
||||
(on (asserted (list "balance" (bind amount Int)))
|
||||
(assert (list "deposit" 100))
|
||||
(set! deposits (- (ref deposits) 1))
|
||||
(if (= (ref deposits) 0)
|
||||
(stop client (begin)))))))
|
||||
#'(spawn
|
||||
(let-field [deposits : Int 3]
|
||||
(facet client
|
||||
(on (asserted (tuple "balance" (bind amount Int)))
|
||||
;; this bit isn't valid because `assert` is not a statement
|
||||
(begin (assert (tuple "deposit" 100))
|
||||
(set! deposits (- (ref deposits) 1))
|
||||
;; also `if` isn't in the grammar
|
||||
(if (= (ref deposits) 0)
|
||||
(stop client (begin))
|
||||
(begin))))))))
|
||||
|
||||
(require rackunit)
|
||||
|
||||
(define-syntax (test-syntax-class stx)
|
||||
(syntax-parse stx
|
||||
[(_ e class:id)
|
||||
#`(let ()
|
||||
(define-syntax (test-result stx)
|
||||
(syntax-parse e
|
||||
[(~var _ class) #'#t]
|
||||
[_ #'#f]))
|
||||
(test-result))]))
|
||||
Loading…
Reference in New Issue