tweak how types are printed
This commit is contained in:
parent
eba7ed072c
commit
60ed8c2677
|
@ -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
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
|
|
@ -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 ...))])
|
||||
|
||||
|
|
Loading…
Reference in New Issue