From 06f6d82e5ab705c9466dd03046b78a456a169085 Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Thu, 16 Dec 2021 14:55:05 -0500 Subject: [PATCH 1/4] wip --- typed-racket-lib/typed-racket/private/parse-type.rkt | 6 ++++++ typed-racket-lib/typed-racket/rep/type-constr.rkt | 11 +++++++++++ typed-racket-test/unit-tests/interactive-tests.rkt | 2 ++ 3 files changed, 19 insertions(+) diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index 648a383a2..63d606dad 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -1222,6 +1222,12 @@ (cond [(current-in-struct-prop) (attribute id.type)] [else (parse-error (~a (syntax-e #'id) " is not allowed outside the type annotation for Struct-Property"))])] + [id:List*^ + #:when ret-type-op? + (TypeConstructorStub 1 #t #t)] + [id:List^ + #:when ret-type-op? + (TypeConstructorStub 0 #t #t)] [id:identifier (define v (syntax-e #'id)) (cond diff --git a/typed-racket-lib/typed-racket/rep/type-constr.rkt b/typed-racket-lib/typed-racket/rep/type-constr.rkt index 714776d99..0cbc5aad8 100644 --- a/typed-racket-lib/typed-racket/rep/type-constr.rkt +++ b/typed-racket-lib/typed-racket/rep/type-constr.rkt @@ -8,6 +8,7 @@ (provide print-kind make-type-constr (struct-out TypeConstructor) + (struct-out TypeConstructorStub) (struct-out exn:fail:contract:arity:type-constructor)) (define-values (prop:kind kind? kind-acc) (make-struct-type-property 'kind)) @@ -68,6 +69,8 @@ (TypeConstructor type-maker arity kind*? productive))) +(struct TypeConstructorStub [arity kind*? productive?] #:transparent) + (define (print-kind type-or-type-op) (match type-or-type-op [(struct* TypeConstructor ([arity arity] @@ -78,4 +81,12 @@ mandatory-stars)) (format "(~a ~a *)" (if productive? "->" "-o") (string-join all-stars))] + [(struct* TypeConstructorStub ([arity arity] + [kind*? kind*?] + [productive? productive?])) + (define mandatory-stars (make-list arity "*")) + (define all-stars (if kind*? (append mandatory-stars (list "* ...")) + mandatory-stars)) + (format "(~a ~a *)" (if productive? "->" "-o") + (string-join all-stars))] [_ "*"])) diff --git a/typed-racket-test/unit-tests/interactive-tests.rkt b/typed-racket-test/unit-tests/interactive-tests.rkt index dd542c8ae..b57b575a5 100644 --- a/typed-racket-test/unit-tests/interactive-tests.rkt +++ b/typed-racket-test/unit-tests/interactive-tests.rkt @@ -195,6 +195,8 @@ (test-form (regexp-quote "(-> * *)") (:kind MListof)) (test-form (regexp-quote "(-> * *)") (:kind Thread-Cellof)) (test-form (regexp-quote "(-> * *)") (:kind Weak-Boxof)) + (test-form (regexp-quote "(-> * * ... *)") (:kind List*)) + (test-form (regexp-quote "(-> * ... *)") (:kind List)) (test-form (regexp-quote "(-> * *)") (:kind Vectorof)) (test-form-not-exn (define-type (Bar a) a)) (test-form (regexp-quote "(-o * *)") From 9347e628dd6f66911ab8a6c351dfe39eb6b9c371 Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Thu, 16 Dec 2021 15:36:00 -0500 Subject: [PATCH 2/4] wip2 --- .../typed-racket/env/init-envs.rkt | 4 +-- .../typed-racket/private/parse-type.rkt | 4 +-- .../typed-racket/rep/type-constr.rkt | 28 ++++++++++--------- .../typed-racket/typecheck/tc-structs.rkt | 3 +- 4 files changed, 21 insertions(+), 18 deletions(-) diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt index 67ae08d39..b9b8a4e41 100644 --- a/typed-racket-lib/typed-racket/env/init-envs.rkt +++ b/typed-racket-lib/typed-racket/env/init-envs.rkt @@ -364,7 +364,7 @@ ;; Most Top types are in the predefined table, the ones here ;; are not [(StructTop: name) `(make-StructTop ,(type->sexp name))] - [(TypeConstructor constr arity kind*? productive?) + [(TypeConstructor arity kind*? productive? constr) (define constr^ (gen-serialize-type-rep constr type->sexp)) `(make-type-constr ,constr^ ,arity ,productive? #:kind*? ,kind*?)])) @@ -489,7 +489,7 @@ kind-env-map (lambda (id v) ;; TODO: turn this into a function - (match-define (TypeConstructor constr arity kind*? productive?) v) + (match-define (TypeConstructor arity kind*? productive? constr) v) (define constr^ (gen-serialize-type-rep constr type->sexp)) #`(register-type-constructor! #'#,id (make-type-constr #,constr^ #,arity #,productive? #:kind*? #,kind*?))))) diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index 63d606dad..7a3ccfb56 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -69,7 +69,7 @@ (values (c:listof identifier?) (c:listof identifier?) boolean?))] - [parse-type-or-type-constructor (syntax? . c:-> . (c:or/c Type? TypeConstructor?))] + [parse-type-or-type-constructor (syntax? . c:-> . (c:or/c Type? TypeConstructor? TypeConstructorStub?))] ;; Parse the given identifier using the lexical ;; context of the given syntax object [parse-type/id (syntax? c:any/c . c:-> . Type?)] @@ -1305,7 +1305,7 @@ #:ret-type-op? #t)) (define args^ (let ([lvl (match rator - [(struct* TypeConstructor ([productive? #t])) + [(and (? TypeConstructor?) (? type-constr-productive?)) (add1 current-level)] ;; when checking user-defined type constructors, structure types ;; defined in the enclosing module have not been registerd yet, so we diff --git a/typed-racket-lib/typed-racket/rep/type-constr.rkt b/typed-racket-lib/typed-racket/rep/type-constr.rkt index 0cbc5aad8..49315342c 100644 --- a/typed-racket-lib/typed-racket/rep/type-constr.rkt +++ b/typed-racket-lib/typed-racket/rep/type-constr.rkt @@ -7,6 +7,8 @@ (provide print-kind make-type-constr + type-constr-productive? + type-constr-arity (struct-out TypeConstructor) (struct-out TypeConstructorStub) (struct-out exn:fail:contract:arity:type-constructor)) @@ -32,16 +34,24 @@ [gen-serialize-type-rep type-rep-maker ty->sexp]) +(struct TypeConstructorBase (arity kind*? productive?) #:transparent) + +(define (type-constr-productive? ty-op) + (TypeConstructorBase-productive? ty-op)) + +(define (type-constr-arity ty-op) + (TypeConstructorBase-arity ty-op)) + ;; real-trep-constr: the underlying *named* type rep constructor ;; arity: the mandatory arity ;; kind*: whether this type constructor can take an arbitrary number of arguments ;; productive?: whether this type constructor is productive. -(struct TypeConstructor (real-trep-constr arity kind*? productive?) +(struct TypeConstructor TypeConstructorBase (real-trep-constr) #:transparent #:property prop:kind #t #:property prop:procedure (lambda (me . args) - (match-define (TypeConstructor real-trep-constr arity kind*? _) me) + (match-define (TypeConstructor arity kind*? _ real-trep-constr) me) ;; FIXME: real-trep-constr can take other arguments than types. ;; This could make handling k* more complicated. ;; naive assumpution: type arguments come first in args. @@ -66,22 +76,14 @@ (if (and (zero? arity) (not kind*?)) type-maker - (TypeConstructor type-maker arity kind*? productive))) + (TypeConstructor arity kind*? productive type-maker))) -(struct TypeConstructorStub [arity kind*? productive?] #:transparent) +(struct TypeConstructorStub TypeConstructorBase [] #:transparent) (define (print-kind type-or-type-op) (match type-or-type-op - [(struct* TypeConstructor ([arity arity] - [kind*? kind*?] - [productive? productive?])) - (define mandatory-stars (make-list arity "*")) - (define all-stars (if kind*? (append mandatory-stars (list "* ...")) - mandatory-stars)) - (format "(~a ~a *)" (if productive? "->" "-o") - (string-join all-stars))] - [(struct* TypeConstructorStub ([arity arity] + [(struct* TypeConstructorBase ([arity arity] [kind*? kind*?] [productive? productive?])) (define mandatory-stars (make-list arity "*")) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt index b8f8b93c3..66934f154 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt @@ -573,7 +573,8 @@ (define tvars (map syntax-e vars)) (define new-tvars (map make-F tvars)) (define parent (match parent^ - [(struct* TypeConstructor ([arity expected])) + [(? TypeConstructor?) + (define expected (type-constr-arity parent^)) (define given (length new-tvars)) (unless (<= expected given) (tc-error (~a "wrong number of arguments to type constructor" From 00859825fe6a95da42f61aac5abee52dc7068d62 Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Thu, 16 Dec 2021 15:41:40 -0500 Subject: [PATCH 3/4] remove unnecessary (add1 current-level) --- typed-racket-lib/typed-racket/private/parse-type.rkt | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index 7a3ccfb56..fb010e266 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -860,14 +860,12 @@ (if res (parse-values-type res do-parse do-parse-multi) (-values (list -Void))))] [(:List^ ts ...) (parse-list-type stx - (lambda (stx) - (do-parse stx (add1 current-level))) - (lambda (stx-li) - (do-parse-multi stx-li (add1 current-level))))] + do-parse + do-parse-multi)] [(:List*^ ts ... t) - (-Tuple* (do-parse-multi #'(ts ...) (add1 current-level)) (do-parse #'t (add1 current-level)))] + (-Tuple* (do-parse-multi #'(ts ...)) (do-parse #'t))] [(:cons^ fst rst) - (-pair (do-parse #'fst (add1 current-level)) (do-parse #'rst (add1 current-level)))] + (-pair (do-parse #'fst) (do-parse #'rst))] [(:pred^ t) (make-pred-ty (do-parse #'t))] [((~and :case->^ operator) tys ...) From 48c4fd98c6370a238a44be4d160c1b0f1dd61145 Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Thu, 16 Dec 2021 17:25:58 -0500 Subject: [PATCH 4/4] wip3 --- .../typed-racket/private/parse-type.rkt | 23 ++++++++++++------- .../unit-tests/interactive-tests.rkt | 7 ++++++ 2 files changed, 22 insertions(+), 8 deletions(-) diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index fb010e266..0a19b6d1a 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -118,6 +118,16 @@ e ...)) +(define type-constr-stub-tbl (make-hash)) + +(define (get-type-constr-stub id) + (hash-ref type-constr-stub-tbl (syntax->datum id) #f)) + +(define-syntax-rule (define-literal-type-constr-stub id arity kind* productive?) + (begin + (define-literal-syntax-class #:for-label id) + (hash-set! type-constr-stub-tbl (quote id) (TypeConstructorStub arity kind* productive?)))) + (define-literal-syntax-class #:for-label car) (define-literal-syntax-class #:for-label cdr) (define-literal-syntax-class #:for-label vector-length) @@ -133,8 +143,8 @@ (define-literal-syntax-class #:for-label init-depend) (define-literal-syntax-class #:for-label Refinement) (define-literal-syntax-class #:for-label Instance) -(define-literal-syntax-class #:for-label List) -(define-literal-syntax-class #:for-label List*) +(define-literal-type-constr-stub List 0 #t #t) +(define-literal-type-constr-stub List* 1 #t #t) (define-literal-syntax-class #:for-label pred) (define-literal-syntax-class #:for-label ->) (define-literal-syntax-class #:for-label ->*) @@ -1220,12 +1230,6 @@ (cond [(current-in-struct-prop) (attribute id.type)] [else (parse-error (~a (syntax-e #'id) " is not allowed outside the type annotation for Struct-Property"))])] - [id:List*^ - #:when ret-type-op? - (TypeConstructorStub 1 #t #t)] - [id:List^ - #:when ret-type-op? - (TypeConstructorStub 0 #t #t)] [id:identifier (define v (syntax-e #'id)) (cond @@ -1261,6 +1265,9 @@ [(bound-index? v) (parse-error "type variable must be used with ..." "variable" v)] + [(and ret-type-op? (get-type-constr-stub #'id)) + => (lambda (t) + t)] ;; if it's a type alias, we expand it (the expanded type is stored in the HT) [(lookup-type-alias #'id do-parse (lambda () #f)) => diff --git a/typed-racket-test/unit-tests/interactive-tests.rkt b/typed-racket-test/unit-tests/interactive-tests.rkt index b57b575a5..a18641f7c 100644 --- a/typed-racket-test/unit-tests/interactive-tests.rkt +++ b/typed-racket-test/unit-tests/interactive-tests.rkt @@ -197,6 +197,13 @@ (test-form (regexp-quote "(-> * *)") (:kind Weak-Boxof)) (test-form (regexp-quote "(-> * * ... *)") (:kind List*)) (test-form (regexp-quote "(-> * ... *)") (:kind List)) + (test-form #rx"^$" + (begin + (define-type MyList List) + (define-type MyList* List*))) + (test-form (regexp-quote "(-> * ... *)") (:kind MyList)) + (test-form (regexp-quote "(-> * * ... *)") (:kind MyList*)) + (test-form (regexp-quote "(-> * *)") (:kind Vectorof)) (test-form-not-exn (define-type (Bar a) a)) (test-form (regexp-quote "(-o * *)")