From fe0a947bb05168a82a73098e0458f7a3729d7c60 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Sat, 14 Feb 2009 20:27:37 +0000 Subject: [PATCH] type keys now work, mostly svn: r13580 original commit: e198478055f13631ec9ab6154edcf71c6c3f7ef3 --- collects/typed-scheme/env/init-envs.ss | 4 +- collects/typed-scheme/private/subtype.ss | 264 +++++++++--------- .../private/type-effect-printer.ss | 2 +- collects/typed-scheme/private/type-utils.ss | 2 +- collects/typed-scheme/private/union.ss | 2 +- collects/typed-scheme/rep/rep-utils.ss | 54 ++-- collects/typed-scheme/rep/type-rep.ss | 67 +++-- collects/typed-scheme/utils/utils.ss | 15 +- 8 files changed, 226 insertions(+), 184 deletions(-) diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index e087666b..0b645105 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -32,9 +32,9 @@ [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))] [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))] [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))] - [(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) + [(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals))) `(,(gen-constructor tag) ,@(map sub vals))] - [(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) + [(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals))) `(,(gen-constructor tag) ,@(map sub vals))] [_ (basic v)])) diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 4832711c..513c4535 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -1,7 +1,7 @@ #lang scheme/base (require "../utils/utils.ss") -(require (except-in (rep type-rep effect-rep) sub-eff) +(require (except-in (rep type-rep effect-rep rep-utils) sub-eff) (utils tc-utils) "type-utils.ss" "type-comparison.ss" @@ -156,139 +156,139 @@ (define (subtype* A s t) (parameterize ([match-equality-test type-equal?] [current-seen A]) - (if (seen? s t) - A - (let* ([A0 (remember s t A)]) - (parameterize ([current-seen A0]) - #;(match t - [(Name: n) (when (eq? 'heap (syntax-e n)) - (trace subtype*))] - [_ #f]) + (let ([ks (Type-key s)] [kt (Type-key t)]) + (cond + [(or (seen? s t) (type-equal? s t)) A] + [(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) (fail! s t)] + [(and (symbol? ks) (pair? kt) (not (memq ks kt))) (fail! s t)] + [(and (pair? ks) (pair? kt) + (for/and ([i (in-list ks)]) (not (memq i kt)))) + (fail! s t)] + [else + (let* ([A0 (remember s t A)]) + (parameterize ([current-seen A0]) (match (list s t) - ;; subtyping is reflexive - [(list t t) A0] - ;; univ is top - [(list _ (Univ:)) A0] - ;; error is top and bot - [(list _ (Error:)) A0] - [(list (Error:) _) A0] - ;; (Un) is bot - [(list _ (Union: (list))) (fail! s t)] - [(list (Union: (list)) _) A0] - ;; value types - [(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] - ;; integers are numbers too - [(list (Base: 'Integer _) (Base: 'Number _)) A0] - ;; values are subtypes of their "type" - [(list (Value: (? integer? n)) (Base: 'Integer _)) A0] - [(list (Value: (? number? n)) (Base: 'Number _)) A0] - [(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0] - [(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0] - [(list (Value: (? string? n)) (Base: 'String _)) A0] - ;; tvars are equal if they are the same variable - [(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))] - ;; case-lambda - [(list (Function: arr1) (Function: arr2)) - (when (null? arr1) (fail! s t)) - (let loop-arities ([A* A0] - [arr2 arr2]) - (cond - [(null? arr2) A*] - [(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))] - [else (fail! s t)]))] - ;; recur structurally on pairs - [(list (Pair: a d) (Pair: a* d*)) - (let ([A1 (subtype* A0 a a*)]) - (and A1 (subtype* A1 d d*)))] - ;; quantification over two types preserves subtyping - [(list (Poly: ns b1) (Poly: ms b2)) - (=> unmatch) - (unless (= (length ns) (length ms)) - (unmatch)) - ;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2)) - (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))] - ;; use unification to see if we can use the polytype here - [(list (Poly: vs b) s) - (=> unmatch) - (if (unify vs (list b) (list s)) A0 (unmatch))] - [(list s (Poly: vs b)) - (=> unmatch) - (if (null? (fv b)) (subtype* A0 s b) (unmatch))] - ;; names are compared for equality: - [(list (Name: n) (Name: n*)) - (=> unmatch) - (if (free-identifier=? n n*) - A0 - (unmatch))] - ;; just unfold the recursive types - [(list _ (? Mu?)) (subtype* A0 s (unfold t))] - [(list (? Mu?) _) (subtype* A0 (unfold s) t)] - ;; for unions, we check the cross-product - [(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)] - [(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)] - ;; subtyping on immutable structs is covariant - [(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _)) - (subtypes* A0 flds flds*)] - [(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _)) - (subtypes* A0 (cons proc flds) (cons proc* flds*))] - ;; subtyping on structs follows the declared hierarchy - [(list (Struct: nm (? Type? parent) flds proc _ _ _) other) - ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other) - (subtype* A0 parent other)] - ;; applications and names are structs too - [(list (App: (Name: n) args stx) other) - (let ([t (lookup-type-name n)]) - (unless (Type? t) - (fail! s t)) - #;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other - (instantiate-poly t args)) - (unless (Poly? t) - (tc-error/stx stx "cannot apply non-polymorphic type ~a" t)) - (match t [(Poly-unsafe: n _) - (unless (= n (length args)) - (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a" - n (length args)))]) - (let ([v (subtype* A0 (instantiate-poly t args) other)]) - #;(printf "val: ~a~n" v) - v))] - [(list other (App: (Name: n) args stx)) - (let ([t (lookup-type-name n)]) - (unless (Type? t) - (fail! s t)) - #;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other - (instantiate-poly t args)) - (unless (Poly? t) - (tc-error/stx stx "cannot apply non-polymorphic type ~a" t)) - (match t [(Poly-unsafe: n _) - (unless (= n (length args)) - (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a" - n (length args)))]) - ;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args)) - (let ([v (subtype* A0 other (instantiate-poly t args))]) - #;(printf "2 val: ~a~n" v) - v))] - [(list (Name: n) other) - (let ([t (lookup-type-name n)]) - ;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other) - (if (Type? t) - (subtype* A0 t other) - (fail! s t)))] - ;; Promises are covariant - [(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)] - ;; subtyping on values is pointwise - [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] - ;; single values shouldn't actually happen, but they're just like the type - [(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))] - [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))] - ;; subtyping on other stuff - [(list (Syntax: t) (Syntax: t*)) - (subtype* A0 t t*)] - [(list (Instance: t) (Instance: t*)) - (subtype* A0 t t*)] - ;; otherwise, not a subtype - [_ (fail! s t) #;(printf "failed")])))))) + [(list _ (Univ:)) A0] + ;; error is top and bot + [(list _ (Error:)) A0] + [(list (Error:) _) A0] + ;; (Un) is bot + [(list _ (Union: (list))) (fail! s t)] + [(list (Union: (list)) _) A0] + ;; value types + [(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] + ;; integers are numbers too + [(list (Base: 'Integer _) (Base: 'Number _)) A0] + ;; values are subtypes of their "type" + [(list (Value: (? integer? n)) (Base: 'Integer _)) A0] + [(list (Value: (? number? n)) (Base: 'Number _)) A0] + [(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0] + [(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0] + [(list (Value: (? string? n)) (Base: 'String _)) A0] + ;; tvars are equal if they are the same variable + [(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))] + ;; case-lambda + [(list (Function: arr1) (Function: arr2)) + (when (null? arr1) (fail! s t)) + (let loop-arities ([A* A0] + [arr2 arr2]) + (cond + [(null? arr2) A*] + [(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))] + [else (fail! s t)]))] + ;; recur structurally on pairs + [(list (Pair: a d) (Pair: a* d*)) + (let ([A1 (subtype* A0 a a*)]) + (and A1 (subtype* A1 d d*)))] + ;; quantification over two types preserves subtyping + [(list (Poly: ns b1) (Poly: ms b2)) + (=> unmatch) + (unless (= (length ns) (length ms)) + (unmatch)) + ;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2)) + (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))] + ;; use unification to see if we can use the polytype here + [(list (Poly: vs b) s) + (=> unmatch) + (if (unify vs (list b) (list s)) A0 (unmatch))] + [(list s (Poly: vs b)) + (=> unmatch) + (if (null? (fv b)) (subtype* A0 s b) (unmatch))] + ;; names are compared for equality: + [(list (Name: n) (Name: n*)) + (=> unmatch) + (if (free-identifier=? n n*) + A0 + (unmatch))] + ;; just unfold the recursive types + [(list _ (? Mu?)) (subtype* A0 s (unfold t))] + [(list (? Mu?) _) (subtype* A0 (unfold s) t)] + ;; for unions, we check the cross-product + [(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)] + [(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)] + ;; subtyping on immutable structs is covariant + [(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _)) + (subtypes* A0 flds flds*)] + [(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _)) + (subtypes* A0 (cons proc flds) (cons proc* flds*))] + ;; subtyping on structs follows the declared hierarchy + [(list (Struct: nm (? Type? parent) flds proc _ _ _) other) + ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other) + (subtype* A0 parent other)] + ;; applications and names are structs too + [(list (App: (Name: n) args stx) other) + (let ([t (lookup-type-name n)]) + (unless (Type? t) + (fail! s t)) + #;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other + (instantiate-poly t args)) + (unless (Poly? t) + (tc-error/stx stx "cannot apply non-polymorphic type ~a" t)) + (match t [(Poly-unsafe: n _) + (unless (= n (length args)) + (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a" + n (length args)))]) + (let ([v (subtype* A0 (instantiate-poly t args) other)]) + #;(printf "val: ~a~n" v) + v))] + [(list other (App: (Name: n) args stx)) + (let ([t (lookup-type-name n)]) + (unless (Type? t) + (fail! s t)) + #;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other + (instantiate-poly t args)) + (unless (Poly? t) + (tc-error/stx stx "cannot apply non-polymorphic type ~a" t)) + (match t [(Poly-unsafe: n _) + (unless (= n (length args)) + (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a" + n (length args)))]) + ;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args)) + (let ([v (subtype* A0 other (instantiate-poly t args))]) + #;(printf "2 val: ~a~n" v) + v))] + [(list (Name: n) other) + (let ([t (lookup-type-name n)]) + ;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other) + (if (Type? t) + (subtype* A0 t other) + (fail! s t)))] + ;; Promises are covariant + [(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)] + ;; subtyping on values is pointwise + [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] + ;; single values shouldn't actually happen, but they're just like the type + [(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))] + [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))] + ;; subtyping on other stuff + [(list (Syntax: t) (Syntax: t*)) + (subtype* A0 t t*)] + [(list (Instance: t) (Instance: t*)) + (subtype* A0 t t*)] + ;; otherwise, not a subtype + [_ (fail! s t) #;(printf "failed")])))])))) -(define (type-compare? a b) + (define (type-compare? a b) (and (subtype a b) (subtype b a))) (provide subtype type-compare? subtypes/varargs subtypes) diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss index b5852df8..5a5a5d03 100644 --- a/collects/typed-scheme/private/type-effect-printer.ss +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -9,7 +9,7 @@ ;; FIXME - currently broken (define print-poly-types? #f) ;; do we use simple type aliases in printing -(define print-aliases #t) +(define print-aliases #f) ;; does t have a type name associated with it currently? ;; has-name : Type -> Maybe[Symbol] diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index 567cdd56..f24f7258 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -37,7 +37,7 @@ (define (sb t) (substitute image name t)) (if (hash-ref (free-vars* target) name #f) (type-case sb target - [#:Union tys (Un (map sb tys))] + ;[#:Union tys (Un (map sb tys))] [#:F name* (if (eq? name* name) image target)] [#:arr dom rng rest drest kws thn-eff els-eff (begin diff --git a/collects/typed-scheme/private/union.ss b/collects/typed-scheme/private/union.ss index e8830edc..756ac4b8 100644 --- a/collects/typed-scheme/private/union.ss +++ b/collects/typed-scheme/private/union.ss @@ -53,7 +53,7 @@ (if (andmap Values? types) (make-Values (apply map Un (map Values-types types))) (int-err "Un: should not take the union of multiple values with some other type: ~a" types))] - [else (make-union* #;(remove-subtypes types) (foldr union2 (list (car types)) (remove-subtypes (cdr types))))]))])) + [else (make-union* #;(remove-subtypes types) (foldr union2 (list) (remove-subtypes types)))]))])) #;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args) diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss index 14e39c96..679b2e33 100644 --- a/collects/typed-scheme/rep/rep-utils.ss +++ b/collects/typed-scheme/rep/rep-utils.ss @@ -13,7 +13,7 @@ syntax/stx (utils utils))) -(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq) +(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq Type-key) @@ -25,9 +25,9 @@ ;; all types are Type? -(define-struct/printer Type (seq) (lambda (a b c) ((unbox print-type*) a b c))) +(define-struct/printer Type (seq key) (lambda (a b c) ((unbox print-type*) a b c))) -(define-struct/printer Effect (seq) (lambda (a b c) ((unbox print-effect*) a b c))) +(define-struct/printer Effect (seq key) (lambda (a b c) ((unbox print-effect*) a b c))) @@ -44,31 +44,34 @@ (define-syntaxes (dt de) (let () (define (parse-opts opts stx) - (let loop ([provide? #t] [intern? #f] [frees #t] [fold-rhs #f] [opts opts]) + (let loop ([provide? #t] [intern? #f] [frees #t] [fold-rhs #f] [key '(#f)] [opts opts]) (cond - [(null? opts) (values provide? intern? frees fold-rhs)] + [(null? opts) (values provide? intern? frees fold-rhs key)] [(eq? '#:no-provide (syntax-e (stx-car opts))) - (loop #f intern? frees fold-rhs (cdr opts))] + (loop #f intern? frees fold-rhs key (cdr opts))] [(eq? '#:no-frees (syntax-e (stx-car opts))) - (loop #f intern? #f fold-rhs (cdr opts))] + (loop #f intern? #f fold-rhs key (cdr opts))] [(not (and (stx-pair? opts) (stx-pair? (stx-car opts)))) (raise-syntax-error #f "bad options" stx)] [(eq? '#:intern (syntax-e (stx-car (car opts)))) - (loop provide? (stx-car (stx-cdr (car opts))) frees fold-rhs (cdr opts))] + (loop provide? (stx-car (stx-cdr (car opts))) frees fold-rhs key (cdr opts))] [(eq? '#:frees (syntax-e (stx-car (car opts)))) - (loop provide? intern? (stx-cdr (car opts)) fold-rhs (cdr opts))] + (loop provide? intern? (stx-cdr (car opts)) fold-rhs key (cdr opts))] [(eq? '#:fold-rhs (syntax-e (stx-car (car opts)))) - (loop provide? intern? frees (stx-cdr (car opts)) (cdr opts))] + (loop provide? intern? frees (stx-cdr (car opts)) key (cdr opts))] + [(eq? '#:key (syntax-e (stx-car (car opts)))) + (loop provide? intern? frees fold-rhs (stx-cdr (car opts)) (cdr opts))] [else (raise-syntax-error #f "bad options" stx)]))) (define (mk par ht-stx) (lambda (stx) (syntax-case stx () [(dform nm flds . opts) - (let*-values ([(provide? intern? frees fold-rhs) (parse-opts (syntax->list #'opts) #'opts)] + (let*-values ([(provide? intern? frees fold-rhs key-expr) (parse-opts (syntax->list #'opts) #'opts)] [(kw) (string->keyword (symbol->string (syntax-e #'nm)))]) (with-syntax* ([ex (id #'nm #'nm ":")] [kw-stx kw] + [(key-expr) key-expr] [parent par] [(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)] [(flds* ...) #'flds] @@ -82,7 +85,12 @@ #'(lambda (tr er) #'fr))] [fold-rhs (raise-syntax-error fold-rhs "something went wrong")] - [else #'(lambda (type-rec-id effect-rec-id) #`(*maker (#,type-rec-id flds*) ...))])] + [else #'(lambda (type-rec-id effect-rec-id) + #; + (printf "about to call ~a with ~a args~n" + '*maker + (length '(flds* ...))) + #`(*maker (#,type-rec-id flds*) ...))])] [provides (if provide? #`(begin (provide ex pred acc ...) @@ -90,19 +98,18 @@ #'(begin))] [intern (cond [(syntax? intern?) - #`(defintern (**maker . flds) maker #,intern?)] + #`(defintern (**maker key . flds) maker #,intern?)] [(null? (syntax-e #'flds)) - #'(defintern (**maker . flds) maker #f)] - [(stx-null? (stx-cdr #'flds)) #'(defintern (**maker . flds) maker . flds)] - [else #'(defintern (**maker . flds) maker (list . flds))])] + #'(defintern (**maker key . flds) maker #f)] + [(stx-null? (stx-cdr #'flds)) #'(defintern (**maker key . flds) maker . flds)] + [else #'(defintern (**maker key . flds) maker (list . flds))])] [frees (cond [(not frees) #'(begin)] ;; we know that this has no free vars [(and (pair? frees) (syntax? (car frees)) (not (syntax-e (car frees)))) (syntax/loc stx (define (*maker . flds) - (define v (**maker . flds)) - #;(printf "~a entered in #f case~n" '*maker) + (define v (**maker key-expr . flds)) (unless-in-table var-table v (hash-set! var-table v empty-hash-table) @@ -113,16 +120,14 @@ [(and (pair? frees) (pair? (cdr frees))) (quasisyntax/loc stx - (define (*maker . flds) - (define v (**maker . flds)) - #;(printf "~a entered in expr case ~n~a~n~a ~n" '*maker '#,(car frees) '#,(cadr frees)) + (define (*maker . flds) + (define v (**maker key-expr . flds)) #, (quasisyntax/loc (car frees) (unless-in-table var-table v (hash-set! var-table v #,(car frees)) (hash-set! index-table v #,(cadr frees)))) - #;(printf "~a exited in expr case~n" '*maker) v))] [else (let @@ -134,8 +139,7 @@ [(e ...) #`(combine-frees (list (#,f e) ...))]))]) (quasisyntax/loc stx (define (*maker . flds) - (define v (**maker . flds)) - #;(printf "~a entered in default case~n" '*maker) + (define v (**maker key-expr . flds)) (unless-in-table var-table v (define fvs #,(combiner #'free-vars* #'flds)) @@ -150,7 +154,7 @@ (... (syntax-case s () [(__ . fs) - (with-syntax ([flds** (syntax/loc s (_ . fs))]) + (with-syntax ([flds** (syntax/loc s (_ _ . fs))]) (quasisyntax/loc s (struct nm flds**)))])))) (begin-for-syntax (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx))) diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index bd286cf8..ea2d2017 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -13,7 +13,7 @@ ;; Type is defined in rep-utils.ss ;; t must be a Type -(dt Scope (t)) +(dt Scope (t) [#:key (Type-key t)]) ;; this is ONLY used when a type error ocurrs (dt Error () [#:frees #f] [#:fold-rhs #:base]) @@ -41,39 +41,52 @@ stx)]) ;; left and right are Types -(dt Pair (left right)) +(dt Pair (left right) [#:key 'pair]) ;; elem is a Type -(dt Vector (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]) +(dt Vector (elem) + [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))] + [#:key 'vector]) ;; elem is a Type -(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]) +(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))] + [#:key 'box]) ;; name is a Symbol (not a Name) -(dt Base (name contract) [#:frees #f] [#:fold-rhs #:base] [#:intern name]) +(dt Base (name contract) [#:frees #f] [#:fold-rhs #:base] [#:intern name] + [#:key (case name + [(Number Integer) 'number] + [(Boolean) 'boolean] + [(String) 'string] + [(Symbol) 'symbol] + [(Keyword) 'keyword] + [else #f])]) ;; body is a Scope (dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))] - [#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]) + [#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))] + [#:key (Type-key body)]) ;; n is how many variables are bound here ;; body is a Scope (dt Poly (n body) #:no-provide [#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:fold-rhs (let ([body* (remove-scopes n body)]) - (*Poly n (add-scopes n (type-rec-id body*))))]) + (*Poly n (add-scopes n (type-rec-id body*))))] + [#:key (Type-key body)]) ;; n is how many variables are bound here ;; there are n-1 'normal' vars and 1 ... var ;; body is a Scope (dt PolyDots (n body) #:no-provide + [#:key (Type-key body)] [#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:fold-rhs (let ([body* (remove-scopes n body)]) (*PolyDots n (add-scopes n (type-rec-id body*))))]) ;; pred : identifier ;; cert : syntax certifier -(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base]) +(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred]) ;; name : symbol ;; parent : Struct @@ -92,7 +105,8 @@ (and proc (type-rec-id proc)) poly? pred-id - cert)]) + cert)] + [#:key (gensym)]) ;; kw : keyword? ;; ty : Type @@ -100,7 +114,8 @@ (dt Keyword (kw ty required?) [#:frees (free-vars* ty) (free-idxs* ty)] - [#:fold-rhs (*Keyword kw (type-rec-id ty) required?)]) + [#:fold-rhs (*Keyword kw (type-rec-id ty) required?)] + [#:key 'keyword]) ;; dom : Listof[Type] ;; rng : Type @@ -112,6 +127,7 @@ ;; els-eff : Effect ;; arr is NOT a Type (dt arr (dom rng rest drest kws thn-eff els-eff) + [#:key 'procedure] [#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null) (map Keyword-ty kws) dom))) @@ -153,13 +169,22 @@ [#:fold-rhs (*Function (map type-rec-id arities))]) ;; v : Scheme Value -(dt Value (v) [#:frees #f] [#:fold-rhs #:base]) +(dt Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number] + [(boolean? v) 'boolean] + [(null? v) 'null] + [else #f])]) ;; elems : Listof[Type] (dt Union (elems) [#:frees (combine-frees (map free-vars* elems)) (combine-frees (map free-idxs* elems))] - [#:fold-rhs ((get-union-maker) (map type-rec-id elems))]) - + [#:fold-rhs ((get-union-maker) (map type-rec-id elems))] + [#:key (let loop ([res null] [ts elems]) + (if (null? ts) res + (let ([k (Type-key (car ts))]) + (cond [(pair? k) (loop (append k res) (cdr ts))] + [k (loop (cons k res) (cdr ts))] + [else #f]))))]) + (dt Univ () [#:frees #f] [#:fold-rhs #:base]) ;; types : Listof[Type] @@ -167,23 +192,25 @@ #:no-provide [#:frees (combine-frees (map free-vars* types)) (combine-frees (map free-idxs* types))] - [#:fold-rhs (*Values (map type-rec-id types))]) + [#:fold-rhs (*Values (map type-rec-id types))] + [#:key 'values]) (dt ValuesDots (types dty dbound) [#:frees (combine-frees (map free-vars* (cons dty types))) (combine-frees (map free-idxs* (cons dty types)))] - [#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)]) + [#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)] + [#:key 'values]) ;; in : Type ;; out : Type -(dt Param (in out)) +(dt Param (in out) [#:key 'parameter]) ;; key : Type ;; value : Type -(dt Hashtable (key value)) +(dt Hashtable (key value) [#:key 'hash]) ;; t : Type -(dt Syntax (t)) +(dt Syntax (t) [#:key 'syntax]) ;; pos-flds : (Listof Type) ;; name-flds : (Listof (Tuple Symbol Type Boolean)) @@ -197,7 +224,7 @@ (map free-idxs* (append pos-flds (map cadr name-flds) (map cadr methods))))] - + [#:key 'class] [#:fold-rhs (match (list pos-flds name-flds methods) [(list pos-tys @@ -211,7 +238,7 @@ (map list mname (map type-rec-id mty)))])]) ;; cls : Class -(dt Instance (cls)) +(dt Instance (cls) [#:key 'instance]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss index f08a44ff..8cb1559c 100644 --- a/collects/typed-scheme/utils/utils.ss +++ b/collects/typed-scheme/utils/utils.ss @@ -166,16 +166,27 @@ [(_ val) #'(? (lambda (x) (equal? val x)))]))) -(define-for-syntax printing? #t) +(define-for-syntax printing? #f) (define print-type* (box (lambda _ (error "print-type* not yet defined")))) (define print-effect* (box (lambda _ (error "print-effect* not yet defined")))) +(require scheme/pretty mzlib/pconvert) + (define-syntax (define-struct/printer stx) (syntax-case stx () [(form name (flds ...) printer) #`(define-struct/properties name (flds ...) - #,(if printing? #'([prop:custom-write printer]) #'()) + #,(if printing? + #'([prop:custom-write printer]) + #'([prop:custom-write (lambda (s port mode) + (parameterize ([current-output-port port] + [show-sharing #f] + [booleans-as-true/false #f] + [constructor-style-printing #t]) + (newline) + (pretty-print (print-convert s)) + (newline)))])) #f)])) (define (id kw . args)