From da1263dc97a34ffdf680a7325d432165aef35b7b Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Mon, 1 Oct 2018 13:06:17 -0400
Subject: [PATCH] begin splitting up roles.rkt

---
 racket/typed/base-types.rkt      |  65 +++++++++++
 racket/typed/effects.rkt         |  28 +++++
 racket/typed/judgments/basic.rkt |  11 ++
 racket/typed/prim.rkt            |  79 ++++++++++++++
 racket/typed/roles.rkt           | 180 ++-----------------------------
 5 files changed, 192 insertions(+), 171 deletions(-)
 create mode 100644 racket/typed/base-types.rkt
 create mode 100644 racket/typed/effects.rkt
 create mode 100644 racket/typed/judgments/basic.rkt
 create mode 100644 racket/typed/prim.rkt

diff --git a/racket/typed/base-types.rkt b/racket/typed/base-types.rkt
new file mode 100644
index 0000000..03a5111
--- /dev/null
+++ b/racket/typed/base-types.rkt
@@ -0,0 +1,65 @@
+#lang turnstile
+
+(provide (all-defined-out)
+         (for-syntax (all-defined-out)))
+
+(require (for-syntax turnstile/examples/util/filter-maximal))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Types
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-binding-type Role #:arity >= 0 #:bvs = 1)
+(define-type-constructor Shares #:arity = 1)
+(define-type-constructor Sends #:arity = 1)
+(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)
+(define-base-types OnStart OnStop OnDataflow MakesField)
+(define-for-syntax field-prop-name 'fields)
+
+(define-type-constructor Tuple #:arity >= 0)
+(define-type-constructor Observe #:arity = 1)
+(define-type-constructor Inbound #:arity = 1)
+(define-type-constructor Outbound #:arity = 1)
+(define-type-constructor Actor #:arity = 1)
+(define-type-constructor AssertionSet #:arity = 1)
+(define-type-constructor Patch #:arity = 2)
+(define-type-constructor List #:arity = 1)
+(define-type-constructor Set #:arity = 1)
+
+(define-type-constructor → #:arity > 0)
+;; for describing the RHS
+;; a value and a description of the effects
+(define-type-constructor Computation #:arity = 4)
+(define-type-constructor Value #:arity = 1)
+(define-type-constructor Endpoints #:arity >= 0)
+(define-type-constructor Roles #:arity >= 0)
+(define-type-constructor Spawns #:arity >= 0)
+
+
+(define-base-types Discard ★/t FacetName)
+
+(define-type-constructor U* #:arity >= 0)
+
+
+
+(define-for-syntax (prune+sort tys)
+  (stx-sort 
+   (filter-maximal 
+    (stx->list tys)
+    typecheck?)))
+  
+(define-syntax (U stx)
+  (syntax-parse stx
+    [(_ . tys)
+     ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys
+     #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys)
+     #:with tys- (prune+sort #'(ty1- ... ... ty2- ...))
+     (if (= 1 (stx-length #'tys-))
+         (stx-car #'tys-)
+         (syntax/loc stx (U* . tys-)))]))
\ No newline at end of file
diff --git a/racket/typed/effects.rkt b/racket/typed/effects.rkt
new file mode 100644
index 0000000..54bb61e
--- /dev/null
+++ b/racket/typed/effects.rkt
@@ -0,0 +1,28 @@
+#lang turnstile
+
+(provide (for-syntax get-effect
+           effect-free?
+           pure?
+           all-pure?))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Effect Checking
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; DesugaredSyntax EffectName -> (Syntaxof Effect ...)
+(define-for-syntax (get-effect e- eff)
+  (or (syntax-property e- eff) #'()))
+
+;; DesugaredSyntax EffectName -> Bool
+(define-for-syntax (effect-free? e- eff)
+  (define prop (syntax-property e- eff))
+  (or (false? prop) (stx-null? prop)))
+
+;; DesugaredSyntax -> Bool
+(define-for-syntax (pure? e-)
+  (for/and ([key (in-list '(ep f s))])
+    (effect-free? e- key)))
+
+;; (SyntaxOf DesugaredSyntax ...) -> Bool
+(define-for-syntax (all-pure? es)
+  (stx-andmap pure? es))
\ No newline at end of file
diff --git a/racket/typed/judgments/basic.rkt b/racket/typed/judgments/basic.rkt
new file mode 100644
index 0000000..e498bfd
--- /dev/null
+++ b/racket/typed/judgments/basic.rkt
@@ -0,0 +1,11 @@
+#lang turnstile
+
+(provide (for-syntax flat-type?)) #;(flat-type? Type)
+
+(require "../base-types.rkt")
+
+(define-for-syntax (flat-type? τ)
+  (syntax-parse τ
+    [(~→ τ ...) #f]
+    [(~Actor τ) #f]
+    [_ #t]))
\ No newline at end of file
diff --git a/racket/typed/prim.rkt b/racket/typed/prim.rkt
new file mode 100644
index 0000000..72ed3df
--- /dev/null
+++ b/racket/typed/prim.rkt
@@ -0,0 +1,79 @@
+#lang turnstile
+
+(provide (all-defined-out)
+         (for-syntax (all-defined-out)))
+
+(require "base-types.rkt"
+         "effects.rkt"
+         "judgments/basic.rkt")
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Basic Values and Their Types
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-base-types Int Bool String)
+
+(define-typed-syntax #%datum
+  [(_ . n:integer) ≫
+  ----------------
+  [⊢ (#%datum- . n) (⇒ : Int)]]
+  [(_ . b:boolean) ≫
+  ----------------
+  [⊢ (#%datum- . b) (⇒ : Bool)]]
+  [(_ . s:string) ≫
+  ----------------
+  [⊢ (#%datum- . s) (⇒ : String)]])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Primitives
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; hmmm
+(define-primop + (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
+(define-primop - (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
+(define-primop * (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
+#;(define-primop and (→ Bool Bool Bool))
+(define-primop or (→ Bool Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop not (→ Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop < (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop > (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+
+(define-typed-syntax (/ e1 e2) ≫
+  [⊢ e1 ≫ e1- (⇐ : Int)]
+  [⊢ e2 ≫ e2- (⇐ : Int)]
+  #:fail-unless (pure? #'e1-) "expression not allowed to have effects"
+  #:fail-unless (pure? #'e2-) "expression not allowed to have effects"
+  ------------------------
+  [⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int)])
+
+;; for some reason defining `and` as a prim op doesn't work
+(define-typed-syntax (and e ...) ≫
+  [⊢ e ≫ e- (⇐ : Bool)] ...
+  #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
+  ------------------------
+  [⊢ (and- e- ...) (⇒ : Bool)])
+
+(define-typed-syntax (equal? e1:expr e2:expr) ≫
+  [⊢ e1 ≫ e1- (⇒ : τ1)]
+  #:fail-unless (flat-type? #'τ1)
+  (format "equality only available on flat data; got ~a" (type->str #'τ1))
+  [⊢ e2 ≫ e2- (⇐ : τ1)]
+  #:fail-unless (pure? #'e1-) "expression not allowed to have effects"
+  #:fail-unless (pure? #'e2-) "expression not allowed to have effects"
+  ---------------------------------------------------------------------------
+  [⊢ (equal?- e1- e2-) (⇒ : Bool)])
+
+(define-typed-syntax (displayln e:expr) ≫
+  [⊢ e ≫ e- (⇒ : τ)]
+  #:fail-unless (pure? #'e-) "expression not allowed to have effects"
+  ---------------
+  [⊢ (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)])
\ No newline at end of file
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index de6f279..c924b9b 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -5,11 +5,7 @@
          #%top-interaction
          require only-in
          ;; Types
-         Int Bool String Tuple Bind Discard → List
-         Role Reacts Shares Know ¬Know Message OnDataflow Stop OnStart OnStop
-         FacetName Field ★/t
-         Observe Inbound Outbound Actor U
-         Computation Value Endpoints Roles Spawns
+         (all-from-out "base-types.rkt")
          ;; Statements
          let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
          when unless send!
@@ -27,7 +23,8 @@
          ;; patterns
          bind discard
          ;; primitives
-         + - * / and or not > < >= <= = equal? displayln printf define
+         (all-from-out "prim.rkt")
+         ;; + - * / and or not > < >= <= = equal? displayln printf define
          ;; lists
          list cons first rest member? empty? for for/fold
          ;; sets
@@ -42,9 +39,13 @@
          )
 
 (require (prefix-in syndicate: syndicate/actor-lang))
+(require "base-types.rkt"
+         "effects.rkt"
+         "prim.rkt"
+         "judgments/basic.rkt")
 
 (require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx))
-(require (for-syntax turnstile/examples/util/filter-maximal))
+
 (require macrotypes/postfix-in)
 (require (rename-in racket/math [exact-truncate exact-truncate-]))
 (require (postfix-in - racket/list))
@@ -72,50 +73,9 @@
 ;; f key aggregates facet effects (starting a facet) as `Role`s and message sends, `Sends`
 ;; s key aggregates spawned actors as `Actor`s
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Types
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-binding-type Role #:arity >= 0 #:bvs = 1)
-(define-type-constructor Shares #:arity = 1)
-(define-type-constructor Sends #:arity = 1)
-(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)
-(define-base-types OnStart OnStop OnDataflow MakesField)
-(define-for-syntax field-prop-name 'fields)
-
-(define-type-constructor Tuple #:arity >= 0)
-(define-type-constructor Observe #:arity = 1)
-(define-type-constructor Inbound #:arity = 1)
-(define-type-constructor Outbound #:arity = 1)
-(define-type-constructor Actor #:arity = 1)
-(define-type-constructor AssertionSet #:arity = 1)
-(define-type-constructor Patch #:arity = 2)
-(define-type-constructor List #:arity = 1)
-(define-type-constructor Set #:arity = 1)
-
-(define-type-constructor → #:arity > 0)
-;; for describing the RHS
-;; a value and a description of the effects
-(define-type-constructor Computation #:arity = 4)
-(define-type-constructor Value #:arity = 1)
-(define-type-constructor Endpoints #:arity >= 0)
-(define-type-constructor Roles #:arity >= 0)
-(define-type-constructor Spawns #:arity >= 0)
-
-
-(define-base-types Int Bool String Discard ★/t FacetName)
-
 (define-for-syntax (type-eval t)
   ((current-type-eval) t))
 
-(define-type-constructor U* #:arity >= 0)
-
 ;; τ.norm in 1st case causes "not valid type" error when referring to ⊥ in another file.
 ;; however, this version expands the type at every reference, incurring a potentially large
 ;; overhead---2x in the case of book-club.rkt
@@ -134,22 +94,6 @@
 
 (define-type-alias ⊥ (U*))
 
-(define-for-syntax (prune+sort tys)
-  (stx-sort 
-   (filter-maximal 
-    (stx->list tys)
-    typecheck?)))
-  
-(define-syntax (U stx)
-  (syntax-parse stx
-    [(_ . tys)
-     ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys
-     #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys)
-     #:with tys- (prune+sort #'(ty1- ... ... ty2- ...))
-     (if (= 1 (stx-length #'tys-))
-         (stx-car #'tys-)
-         (syntax/loc stx (U* . tys-)))]))
-
 ;; for looking at the "effects"
 (begin-for-syntax
   (define-syntax ~effs
@@ -312,17 +256,7 @@
       [observe #'syndicate:observe]
       [inbound #'syndicate:inbound]
       [outbound #'syndicate:outbound]
-      [message #'syndicate:message]))
-
-  (define-syntax-class basic-val
-    (pattern (~or boolean
-                  integer
-                  string)))
-
-  (define-syntax-class prim-op
-    (pattern (~or (~literal +)
-                  (~literal -)
-                  (~literal displayln)))))
+      [message #'syndicate:message])))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Utilities Over Types
@@ -331,12 +265,6 @@
 (define-for-syntax (bot? t)
   (<: t (type-eval #'(U*))))
 
-(define-for-syntax (flat-type? τ)
-  (syntax-parse τ
-    [(~→ τ ...) #f]
-    [(~Actor τ) #f]
-    [_ #t]))
-
 (define-for-syntax (strip-? t)
   (type-eval
    (syntax-parse t
@@ -928,27 +856,6 @@
 (begin-for-syntax
   (current-typecheck-relation <:))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Effect Checking
-
-;; DesugaredSyntax EffectName -> (Syntaxof Effect ...)
-(define-for-syntax (get-effect e- eff)
-  (or (syntax-property e- eff) #'()))
-
-;; DesugaredSyntax EffectName -> Bool
-(define-for-syntax (effect-free? e- eff)
-  (define prop (syntax-property e- eff))
-  (or (false? prop) (stx-null? prop)))
-
-;; DesugaredSyntax -> Bool
-(define-for-syntax (pure? e-)
-  (for/and ([key (in-list '(ep f s))])
-    (effect-free? e- key)))
-
-;; (SyntaxOf DesugaredSyntax ...) -> Bool
-(define-for-syntax (all-pure? es)
-  (stx-andmap pure? es))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Core forms
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -1578,75 +1485,6 @@
      (⇒ f (fs ... ...))
      (⇒ s (ss ... ...))])
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Primitives
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; hmmm
-(define-primop + (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
-(define-primop - (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
-(define-primop * (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
-#;(define-primop and (→ Bool Bool Bool))
-(define-primop or (→ Bool Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop not (→ Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop < (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop > (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-
-(define-typed-syntax (/ e1 e2) ≫
-  [⊢ e1 ≫ e1- (⇐ : Int)]
-  [⊢ e2 ≫ e2- (⇐ : Int)]
-  #:fail-unless (pure? #'e1-) "expression not allowed to have effects"
-  #:fail-unless (pure? #'e2-) "expression not allowed to have effects"
-  ------------------------
-  [⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int)])
-
-;; for some reason defining `and` as a prim op doesn't work
-(define-typed-syntax (and e ...) ≫
-  [⊢ e ≫ e- (⇐ : Bool)] ...
-  #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
-  ------------------------
-  [⊢ (and- e- ...) (⇒ : Bool)])
-
-(define-typed-syntax (equal? e1:expr e2:expr) ≫
-  [⊢ e1 ≫ e1- (⇒ : τ1)]
-  #:fail-unless (flat-type? #'τ1)
-  (format "equality only available on flat data; got ~a" (type->str #'τ1))
-  [⊢ e2 ≫ e2- (⇐ : τ1)]
-  #:fail-unless (pure? #'e1-) "expression not allowed to have effects"
-  #:fail-unless (pure? #'e2-) "expression not allowed to have effects"
-  ---------------------------------------------------------------------------
-  [⊢ (equal?- e1- e2-) (⇒ : Bool)])
-
-(define-typed-syntax (displayln e:expr) ≫
-  [⊢ e ≫ e- (⇒ : τ)]
-  #:fail-unless (pure? #'e-) "expression not allowed to have effects"
-  ---------------
-  [⊢ (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
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-typed-syntax #%datum
-  [(_ . n:integer) ≫
-  ----------------
-  [⊢ (#%datum- . n) (⇒ : Int)]]
-  [(_ . b:boolean) ≫
-  ----------------
-  [⊢ (#%datum- . b) (⇒ : Bool)]]
-  [(_ . s:string) ≫
-  ----------------
-  [⊢ (#%datum- . s) (⇒ : String)]])
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Utilities
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;