print types different
This commit is contained in:
parent
6b272ad3d3
commit
0711cd3232
|
@ -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,35 +796,43 @@
|
|||
(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))
|
||||
;; 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
|
||||
[(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 τ))]))
|
||||
[(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))
|
||||
|
||||
;; Type Type -> Bool
|
||||
|
|
|
@ -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
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
|
|
@ -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)))))))"))
|
Loading…
Reference in New Issue