From 6230ed577edf30a7294ce36e307910dbb2b3d704 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Wed, 29 May 2019 11:28:46 -0400 Subject: [PATCH] tweak how types are printed --- racket/typed/core-types.rkt | 19 +++++++++++++++++++ racket/typed/roles.rkt | 5 +++-- 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt index 2f01c79..6c3771d 100644 --- a/racket/typed/core-types.rkt +++ b/racket/typed/core-types.rkt @@ -11,6 +11,7 @@ (require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base)) (require (for-syntax turnstile/examples/util/filter-maximal)) (require (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) +#;(require (only-in (for-syntax macrotypes/typecheck-core) get-orig)) (require (for-syntax racket/struct-info syntax/id-table)) (require macrotypes/postfix-in) @@ -807,6 +808,24 @@ (reassemble-type #'τ-cons subitems)] [_ t])) +;; Copied and modified from turnstile +;; try to handle type variables for Stop references and polymorphic effects +;; better +(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 τ))])) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Subtyping and Judgments on Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 7bb383d..1815b26 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -121,7 +121,8 @@ #:with facet-name-ty (type-eval #'FacetName) #:do [(define ctx (syntax-local-make-definition-context)) (define unique (gensym 'start-facet)) - (define name-- (internal-definition-context-introduce ctx #'name- 'add)) + (define name-- (add-orig (internal-definition-context-introduce ctx #'name- 'add) + #'name)) (int-def-ctx-bind-type-rename #'name+ #'name- #'facet-name-ty ctx) (define-values (ep-... τ... ep-effects facet-effects spawn-effects) (walk/bind #'(ep ...) ctx unique)) @@ -502,7 +503,7 @@ (define-typed-syntax (print-role e) ≫ [⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs eps ...)) (⇒ ν-f (~effs fs ...)) (⇒ ν-s (~effs ss ...))] #:do [(for ([r (in-syntax #'(fs ...))]) - (pretty-display (type->str r)))] + (pretty-display (type->strX r)))] ---------------------------------- [⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])