From d9da9707428300e0b171ce3c948793a3779780e9 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Mon, 3 Jun 2019 11:15:47 -0400
Subject: [PATCH] print types different

---
 racket/typed/core-types.rkt        | 61 +++++++++++++++++++-----------
 racket/typed/roles.rkt             | 10 ++++-
 racket/typed/tests/phantom-rho.rkt | 21 ++++++++++
 3 files changed, 68 insertions(+), 24 deletions(-)
 create mode 100644 racket/typed/tests/phantom-rho.rkt

diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt
index dd9c84e..cc5c4dc 100644
--- a/racket/typed/core-types.rkt
+++ b/racket/typed/core-types.rkt
@@ -295,6 +295,13 @@
                             (Spawns))))
 
 (begin-for-syntax
+  (define-syntax ~Base
+    (pattern-expander
+     (syntax-parser
+       [(_ nm:id)
+        #'((~literal #%plain-app) nm)])))
+
+
   (define-syntax ~→fn
     (pattern-expander
      (syntax-parser
@@ -789,36 +796,44 @@
      (reassemble-type #'τ-cons subitems)]
     [_ t]))
 
-;; Copied and modified from turnstile
-;; try to handle type variables for Stop references and polymorphic effects
-;; better
+;; Type -> String
 (define-for-syntax (type->strX ty)
-  (define τ (get-orig ty))
-  (cond
-    [(and (row-variable? τ)
-          (stx-list? ty))
-     (string-join (stx-map type->strX ty)
-                  #:before-first "("
-                  #:after-last ")")]
-    [(identifier? τ)
-     (symbol->string (syntax->datum τ))]
-    [(stx-list? τ) (string-join (stx-map type->strX τ)
-                                #:before-first "("
-                                #:after-last ")")]
-    [else (format "~s" (syntax->datum τ))]))
+  ;; Identifier -> String
+  ;; this won't work for any names with numbers in them :\
+  (define (un-gensym x)
+    (define GENSYMED #px"^(\\D*)\\d*$")
+    (second (regexp-match GENSYMED (symbol->string (syntax-e x)))))
+  ;; (Listof String) -> String
+  (define (paren-join xs)
+    (string-join xs
+                 #:before-first "("
+                 #:after-last ")"))
+  (syntax-parse ty
+    [X:id
+     (un-gensym #'X)]
+    [(~U* τ ...)
+     (paren-join (cons "U" (stx-map type->strX #'(τ ...))))]
+    [(~Base x)
+     (un-gensym #'x)]
+    [(~Any/bvs τ-cons (X ...) τ ...)
+     (define ctor (un-gensym #'τ-cons))
+     (define body (stx-map type->strX #'(τ ...)))
+     (define desc
+       (cond
+         [(empty? (syntax->list #'(X ...)))
+          (list* ctor body)]
+         [else
+          (define vars
+            (paren-join (stx-map type->strX #'(X ...))))
+          (list* ctor vars body)]))
+     (paren-join desc)]))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Subtyping and Judgments on Types
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (begin-for-syntax
- (define-syntax ~Base
-   (pattern-expander
-    (syntax-parser
-      [(_ nm:id)
-       #'((~literal #%plain-app) nm)])))
-
- (define trace-sub? (make-parameter #f))
+  (define trace-sub? (make-parameter #f))
 
  ;; Type Type -> Bool
  ;; subtyping
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 9f99353..c7d7fab 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -53,7 +53,7 @@
          (all-from-out "maybe.rkt")
          (all-from-out "either.rkt")
          ;; DEBUG and utilities
-         print-type print-role
+         print-type print-role role-strings
          ;; Extensions
          match cond
          ;; require & provides
@@ -470,6 +470,14 @@
   ----------------------------------
   [⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
 
+;; this is mainly for testing
+(define-typed-syntax (role-strings e) ≫
+  [⊢ e ≫ e- (⇒ : τ) (⇒ ν-f (~effs fs ...))]
+  #:with (s ...) (for/list ([r (in-syntax #'(fs ...))])
+                   (type->strX r))
+  ----------------------------------------
+  [⊢ (#%app- list- (#%datum- . s) ...) (⇒ : (List String))])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Tests
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/racket/typed/tests/phantom-rho.rkt b/racket/typed/tests/phantom-rho.rkt
new file mode 100644
index 0000000..bad4152
--- /dev/null
+++ b/racket/typed/tests/phantom-rho.rkt
@@ -0,0 +1,21 @@
+#lang typed/syndicate/roles
+
+(require rackunit/turnstile)
+
+;; make sure that we can look at the type of the facet without the ρ in it
+(check-type
+ (role-strings
+   (start-facet x
+     (define (push-results)
+       (cond
+         [(zero? 0)
+          (start-facet done (assert #t))]
+         [else
+          #f]))
+    (define (∀ (ρ) (perform-task [k : (proc -> ★/t #:roles (ρ))]))
+        (start-facet perform
+         (on start (stop perform (k)))))
+    (on start (call/inst perform-task push-results))))
+ : (List String)
+ -> (list
+     "(Role (x) (Reacts OnStart (Role (perform) (Reacts OnStart (Stop perform (Branch (Effs (Role (done) (Shares Bool))) (Effs)))))))"))