wip

racket/typed/main.rkt

@@ -18,6 +18,7 @@
          Facet)
 
 (require (rename-in racket/match [match-lambda match-lambda-]))
+(require (prefix-in syndicate: syndicate/actor))
 
 (module+ test
   (require rackunit)
@@ -37,10 +38,11 @@
 
 (begin-for-syntax
   (define-syntax-class exp
-    #:datum-literals (tuple λ)
+    #:datum-literals (tuple λ ref)
     (pattern (~or (o:prim-op e:exp ...)
                   basic-val
                   (tuple e:exp ...)
+                  (ref x:id)
                   (λ [p:pat s:stmt] ...))))
 
   (define-syntax-class basic-val
@@ -107,13 +109,63 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; 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)]
+  ;; TODO: (~ τ τ-x)
+  -------------------------
+  [⊢ (x- e-) (⇒ : ⊥) (⇒ :2 ⊥) (⇒ :3 ⊥)])
+
+(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)]
+  ;; TODO: s shouldn't refer to facets or fields!
+  ;; TODO: τ-o <: τ-c
+  ;; TODO: (Actor τ-a) <: (Actor τ-c)
+  ;; TODO: project-safe(strip-?(τ-o) ∩ τ-c, τ-i)
+  ----------------------------------------------
+  [⊢ (syndicate:spawn s-) (⇒ : ⊥) (⇒ :2 ⊥) (⇒ τ-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)])
+
+(define-typed-syntax (let-function f:id (~datum :) τ:type e:expr body:expr) ≫
+  [⊢ e ≫ e- (⇐ : τ.norm)]
+  [[x ≫ x- : τ] ⊢ body ≫ body- (⇒ : τ-body) (⇒ :2 τ-body2) (⇒ :3 τ-body3)]
+  #:fail-unless (procedure-type? #'τ.norm) "let-function only binds procedures"
+   ------------------------------------------------------------------------
   [⊢ (let- ([x- e-]) body-) (⇒ : τ-body) (⇒ :2 τ-body2) (⇒ :3 τ-body3)])
 
+(define-for-syntax (procedure-type? τ)
+  (syntax-parse τ
+    [(~Case (~→ τ1:type τ2:type) ...) #t]
+    [_ #f]))
+
+(define-typed-syntax (begin s:stmt ...) ≫
+  [⊢ s ≫ s- (⇒ : τ1) (⇒ : τ2) (⇒ : τ3)] ...
+  ------------------------------------------
+  [⊢ (begin- s- ...) (⇒ : (U τ1 ...)) (⇒ : (U τ2 ...)) (⇒ : (U τ3 ...))])
+
 (define-typed-syntax nil
   [_:id ≫
    ---------------
@@ -133,6 +185,11 @@
   -----------------------
   [⊢ (list 'tuple e- ...) (⇒ : (Tuple τ ...))])
 
+(define-typed-syntax (ref x:id) ≫
+  [⊢ x ≫ x- ⇒ (Field τ)]
+  ------------------------
+  [⊢ (x-) ⇒ τ])
+
 (define-typed-syntax (λ [p:pat s:stmt] ...) ≫
   #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
   [[x ≫ x- : τ] ... ⊢ s ≫ s- (⇒ : τ1) (⇒ :2 τ2) (⇒ :3 τ3)] ...
@@ -194,4 +251,20 @@
 ;; Tests
 
 (module+ test
-  (check-true (void? ((λ [(bind x Int) nil]) 1))))
+  (check-true (void? ((λ [(bind x Int) nil]) 1))))
+
+(define bank-account
+  #'(facet account
+           (let-field [balance : Int 0]
+                      (begin (assert (list "balance" (ref balance)))
+                             (on (asserted (list "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)))))))