tweak how types are printed
This commit is contained in:
parent
7994bfb9c6
commit
6230ed577e
|
@ -11,6 +11,7 @@
|
||||||
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
|
(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 turnstile/examples/util/filter-maximal))
|
||||||
(require (for-syntax macrotypes/type-constraints macrotypes/variance-constraints))
|
(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
|
(require (for-syntax racket/struct-info
|
||||||
syntax/id-table))
|
syntax/id-table))
|
||||||
(require macrotypes/postfix-in)
|
(require macrotypes/postfix-in)
|
||||||
|
@ -807,6 +808,24 @@
|
||||||
(reassemble-type #'τ-cons subitems)]
|
(reassemble-type #'τ-cons subitems)]
|
||||||
[_ t]))
|
[_ 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
|
;; Subtyping and Judgments on Types
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
|
@ -121,7 +121,8 @@
|
||||||
#:with facet-name-ty (type-eval #'FacetName)
|
#:with facet-name-ty (type-eval #'FacetName)
|
||||||
#:do [(define ctx (syntax-local-make-definition-context))
|
#:do [(define ctx (syntax-local-make-definition-context))
|
||||||
(define unique (gensym 'start-facet))
|
(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)
|
(int-def-ctx-bind-type-rename #'name+ #'name- #'facet-name-ty ctx)
|
||||||
(define-values (ep-... τ... ep-effects facet-effects spawn-effects)
|
(define-values (ep-... τ... ep-effects facet-effects spawn-effects)
|
||||||
(walk/bind #'(ep ...) ctx unique))
|
(walk/bind #'(ep ...) ctx unique))
|
||||||
|
@ -502,7 +503,7 @@
|
||||||
(define-typed-syntax (print-role e) ≫
|
(define-typed-syntax (print-role e) ≫
|
||||||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs eps ...)) (⇒ ν-f (~effs fs ...)) (⇒ ν-s (~effs ss ...))]
|
[⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs eps ...)) (⇒ ν-f (~effs fs ...)) (⇒ ν-s (~effs ss ...))]
|
||||||
#:do [(for ([r (in-syntax #'(fs ...))])
|
#:do [(for ([r (in-syntax #'(fs ...))])
|
||||||
(pretty-display (type->str r)))]
|
(pretty-display (type->strX r)))]
|
||||||
----------------------------------
|
----------------------------------
|
||||||
[⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
|
[⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue