From 3705d95856e4b8aa3ddafb8079f13bb0049743b2 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samcaldwell@utexas.edu>
Date: Mon, 30 Jul 2018 14:01:56 -0400
Subject: [PATCH] stop statement

---
 .../examples/roles/simple-stop-facet.rkt      | 32 +++++++++++++++++++
 racket/typed/roles.rkt                        | 28 +++++++++++++---
 2 files changed, 56 insertions(+), 4 deletions(-)
 create mode 100644 racket/typed/examples/roles/simple-stop-facet.rkt

diff --git a/racket/typed/examples/roles/simple-stop-facet.rkt b/racket/typed/examples/roles/simple-stop-facet.rkt
new file mode 100644
index 0000000..9fffe04
--- /dev/null
+++ b/racket/typed/examples/roles/simple-stop-facet.rkt
@@ -0,0 +1,32 @@
+#lang typed/syndicate/roles
+
+;; Expected Output:
+;; +42
+;; +18
+;; +88
+;; -18
+
+(define-type-alias ds-type
+  (U (Tuple Int)
+     (Observe (Tuple ★/t))))
+
+(dataspace ds-type
+  (spawn ds-type
+   (print-role
+   (start-facet doomed
+     (fields)
+     (assert (tuple 18))
+     (on (asserted (tuple 42))
+         (stop doomed
+                (start-facet the-afterlife
+                  (fields)
+                  (assert (tuple 88))))))))
+
+  (spawn ds-type
+    (start-facet obs
+      (fields)
+      (assert (tuple 42))
+      (on (asserted (tuple (bind x Int)))
+          (printf "+~v\n" x))
+      (on (retracted (tuple (bind x Int)))
+          (printf "-~v\n" x)))))
\ No newline at end of file
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index d120525..40ff37a 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -6,11 +6,11 @@
          require only-in
          ;; Types
          Int Bool String Tuple Bind Discard → List
-         Role Reacts Shares Know ¬Know Message
+         Role Reacts Shares Know ¬Know Message Stop
          FacetName Field ★/t
          Observe Inbound Outbound Actor U
          ;; Statements
-         #;let spawn dataspace start-facet set! #;begin #;stop #;unsafe-do
+         #;let spawn dataspace start-facet set! #;begin stop #;unsafe-do
          ;; endpoints
          assert on
          ;; expressions
@@ -20,13 +20,12 @@
          ;; patterns
          bind discard
          ;; primitives
-         + - * / and or not > < >= <= = equal? displayln
+         + - * / and or not > < >= <= = equal? displayln printf
          ;; making types
          define-type-alias
          define-constructor
          ;; DEBUG and utilities
          print-type print-role
-         (rename-out [printf- printf])
          ;; Extensions
          ;; match if cond
          )
@@ -66,6 +65,7 @@
 (define-type-constructor Reacts #:arity >= 1)
 (define-type-constructor Know #:arity = 1)
 (define-type-constructor ¬Know #:arity = 1)
+(define-type-constructor Stop #:arity >= 1)
 (define-type-constructor Message #:arity = 1)
 (define-type-constructor Field #:arity = 1)
 (define-type-constructor Bind #:arity = 1)
@@ -350,6 +350,8 @@
 ;; RoleType -> (Values Type Type)
 (define-for-syntax (analyze-role-input/output t)
   (syntax-parse t
+    [(~Stop name:id τ-r)
+     (analyze-role-input/output #'τ-r)]
     [(~Role (name:id)
        (~or (~Shares τ-s)
             (~Reacts τ-if τ-then ...)) ...
@@ -638,6 +640,17 @@
                            (⇒ f ())
                            (⇒ s ())])
 
+(define-typed-syntax (stop facet-name:id cont) ≫
+  [⊢ facet-name ≫ facet-name- (⇐ : FacetName)]
+  [⊢ cont ≫ cont- (⇒ a (~effs)) (⇒ r (~effs)) (⇒ s (~effs)) (⇒ f (~effs τ-f ...))]
+  #:with τ (mk-Stop- #'(facet-name- τ-f ...))
+  ---------------------------------------------------------------------------------
+  [⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t)
+                                              (⇒ s ())
+                                              (⇒ a ())
+                                              (⇒ r ())
+                                              (⇒ f (τ))])
+
 (begin-for-syntax
   (define-syntax-class asserted-or-retracted
     #:datum-literals (asserted retracted)
@@ -719,6 +732,7 @@
 
 (define-typed-syntax (spawn τ-c:type s) ≫
   #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
+  ;; TODO: check that each τ-f is a Role
   [⊢ s ≫ s- (⇒ a (~effs)) (⇒ r (~effs)) (⇒ s (~effs)) (⇒ f (~effs τ-f ...))]
   ;; TODO: s shouldn't refer to facets or fields!
   #:with (τ-i τ-o) (analyze-roles #'(τ-f ...))
@@ -915,6 +929,12 @@
   ---------------
   [⊢ (displayln- e-) (⇒ : ★/t)])
 
+(define-typed-syntax (printf e ...+) ≫
+  [⊢ e ≫ e- (⇒ : τ)] ...
+  #:fail-unless (stx-andmap pure? #'(e- ...)) "expression not allowed to have effects"
+  ---------------
+  [⊢ (printf- e- ...) (⇒ : ★/t)])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Basic Values
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;