From 817e292760464daf8f777d701c6222b789fd250c Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Tue, 23 Oct 2018 08:36:05 -0400
Subject: [PATCH] Revert "begin splitting up roles.rkt"

This reverts commit da1263dc97a34ffdf680a7325d432165aef35b7b.
---
 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, 171 insertions(+), 192 deletions(-)
 delete mode 100644 racket/typed/base-types.rkt
 delete mode 100644 racket/typed/effects.rkt
 delete mode 100644 racket/typed/judgments/basic.rkt
 delete mode 100644 racket/typed/prim.rkt

diff --git a/racket/typed/base-types.rkt b/racket/typed/base-types.rkt
deleted file mode 100644
index 03a5111..0000000
--- a/racket/typed/base-types.rkt
+++ /dev/null
@@ -1,65 +0,0 @@
-#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
deleted file mode 100644
index 54bb61e..0000000
--- a/racket/typed/effects.rkt
+++ /dev/null
@@ -1,28 +0,0 @@
-#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
deleted file mode 100644
index e498bfd..0000000
--- a/racket/typed/judgments/basic.rkt
+++ /dev/null
@@ -1,11 +0,0 @@
-#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
deleted file mode 100644
index 72ed3df..0000000
--- a/racket/typed/prim.rkt
+++ /dev/null
@@ -1,79 +0,0 @@
-#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 c924b9b..de6f279 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -5,7 +5,11 @@
          #%top-interaction
          require only-in
          ;; Types
-         (all-from-out "base-types.rkt")
+         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
          ;; Statements
          let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
          when unless send!
@@ -23,8 +27,7 @@
          ;; patterns
          bind discard
          ;; primitives
-         (all-from-out "prim.rkt")
-         ;; + - * / and or not > < >= <= = equal? displayln printf define
+         + - * / and or not > < >= <= = equal? displayln printf define
          ;; lists
          list cons first rest member? empty? for for/fold
          ;; sets
@@ -39,13 +42,9 @@
          )
 
 (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))
@@ -73,9 +72,50 @@
 ;; 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
@@ -94,6 +134,22 @@
 
 (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
@@ -256,7 +312,17 @@
       [observe #'syndicate:observe]
       [inbound #'syndicate:inbound]
       [outbound #'syndicate:outbound]
-      [message #'syndicate:message])))
+      [message #'syndicate:message]))
+
+  (define-syntax-class basic-val
+    (pattern (~or boolean
+                  integer
+                  string)))
+
+  (define-syntax-class prim-op
+    (pattern (~or (~literal +)
+                  (~literal -)
+                  (~literal displayln)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Utilities Over Types
@@ -265,6 +331,12 @@
 (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
@@ -856,6 +928,27 @@
 (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
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -1485,6 +1578,75 @@
      (⇒ 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
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;