print types different

This commit is contained in:
Sam Caldwell 2019-06-03 11:15:47 -04:00
parent 5d922fe030
commit d9da970742
3 changed files with 68 additions and 24 deletions

View File

@ -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

View File

@ -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
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

View File

@ -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)))))))"))