suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge in changes from type-keys branch:

Browse Source 
- Use stxclass for defintern/dt/de
- Add type keys to optimize subtyping
- Fancier printing when regular printing is disabled for debugging.
- Caching of the results of subtyping.
- Contracts for hashtable types (still insufficent)
- add type for `last-pair' from `scheme/list'
- new "private/type-abbrev.ss" which contains things 
  from "private/type-effect-convenience.ss" that don't 
  need subtyping/unions
- Don't use the real union constructor on mu unfolding
- more work on (not yet enabled) stxclass type parser
- Naming sanity in tests

svn: r13628
This commit is contained in:
Sam Tobin-Hochstadt 2009-02-15 22:56:14 +00:00
commit 24e4cf5aca
17 changed files with 608 additions and 534 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
View File

@ -3,13 +3,14 @@
(require (utils tc-utils) (require (utils tc-utils)
(env type-alias-env type-environments type-name-env init-envs) (env type-alias-env type-environments type-name-env init-envs)
(rep type-rep) (rep type-rep)
(private type-comparison parse-type subtype (rename-in (private type-comparison parse-type subtype
union type-utils) union type-utils)
[Un t:Un])
(schemeunit)) (schemeunit))
(require (rename-in (private type-effect-convenience) [-> t:->]) (require (rename-in (private type-effect-convenience) [-> t:->])
(private base-types) (private base-types base-types-extra)
(for-template (private base-types))) (for-template (private base-types base-types-extra)))
(provide parse-type-tests) (provide parse-type-tests)
@ -72,9 +73,9 @@
[(Number Number Number Boolean -> Number) (N N N B . t:-> . N)] [(Number Number Number Boolean -> Number) (N N N B . t:-> . N)]
[(Number Number Number * -> Boolean) ((list N N) N . ->* . B)] [(Number Number Number * -> Boolean) ((list N N) N . ->* . B)]
;[((. Number) -> Number) (->* (list) N N)] ;; not legal syntax ;[((. Number) -> Number) (->* (list) N N)] ;; not legal syntax
[(U Number Boolean) (Un N B)] [(U Number Boolean) (t:Un N B)]
[(U Number Boolean Number) (Un N B)] [(U Number Boolean Number) (t:Un N B)]
[(U Number Boolean 1) (Un N B)] [(U Number Boolean 1) (t:Un N B)]
[(All (a) (Listof a)) (-poly (a) (make-Listof a))] [(All (a) (Listof a)) (-poly (a) (make-Listof a))]
[(All (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))] [(All (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))]
[(∀ (a) (Listof a)) (-poly (a) (make-Listof a))] [(∀ (a) (Listof a)) (-poly (a) (make-Listof a))]

4
collects/typed-scheme/env/init-envs.ss vendored
View File

@ -32,9 +32,9 @@
[(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))] [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(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))] [(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))] `(,(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))] `(,(gen-constructor tag) ,@(map sub vals))]
[_ (basic v)])) [_ (basic v)]))

9
collects/typed-scheme/private/base-env.ss
View File

@ -517,8 +517,8 @@
[expand (-> (-Syntax Univ) (-Syntax Univ))] [expand (-> (-Syntax Univ) (-Syntax Univ))]
[expand-once (-> (-Syntax Univ) (-Syntax Univ))] [expand-once (-> (-Syntax Univ) (-Syntax Univ))]
[syntax-source (-poly (a) (-> (-Syntax a) Univ))] [syntax-source (-> (-Syntax Univ) Univ)]
[syntax-position (-poly (a) (-> (-Syntax a) (-opt N)))] [syntax-position (-> (-Syntax Univ) (-opt N))]
[datum->syntax (cl->* [datum->syntax (cl->*
(-> (-opt (-Syntax Univ)) Sym (-Syntax Sym)) (-> (-opt (-Syntax Univ)) Sym (-Syntax Sym))
(-> (-opt (-Syntax Univ)) Univ (-Syntax Univ)))] (-> (-opt (-Syntax Univ)) Univ (-Syntax Univ)))]
@ -538,6 +538,11 @@
[maybe-print-message (-String . -> . -Void)] [maybe-print-message (-String . -> . -Void)]
;; scheme/list
[last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
. -> .
(Un (-pair a a) (-pair a (-val '())))))]
;; scheme/tcp ;; scheme/tcp
[tcp-listener? (make-pred-ty -TCP-Listener)] [tcp-listener? (make-pred-ty -TCP-Listener)]
[tcp-abandon-port (-Port . -> . -Void)] [tcp-abandon-port (-Port . -> . -Void)]

25
collects/typed-scheme/private/parse-type.ss
View File

@ -28,10 +28,12 @@
(define (stx-cadr stx) (stx-car (stx-cdr stx))) (define (stx-cadr stx) (stx-car (stx-cdr stx)))
(define-syntax-class star (define-syntax-class star
#:description "*"
(pattern star:id (pattern star:id
#:when (eq? '* #'star.datum))) #:when (eq? '* #'star.datum)))
(define-syntax-class ddd (define-syntax-class ddd
#:description "..."
(pattern ddd:id (pattern ddd:id
#:when (eq? '... #'ddd.datum))) #:when (eq? '... #'ddd.datum)))
@ -77,6 +79,7 @@
(define-syntax-class fun-ty (define-syntax-class fun-ty
#:literals (t:-> :) #:literals (t:-> :)
#:transparent
#:description "function type" #:description "function type"
;; FIXME - shouldn't have to use syntax->datum ;; FIXME - shouldn't have to use syntax->datum
(pattern (dom*:type t:-> rng:type : pred:type) (pattern (dom*:type t:-> rng:type : pred:type)
@ -118,31 +121,44 @@
#:with t (-values (syntax->datum #'(ts.t ...))))) #:with t (-values (syntax->datum #'(ts.t ...)))))
(define-syntax-class type-name (define-syntax-class type-name
#:description "type name"
(pattern i:id (pattern i:id
#:when (lookup-type-name #'i (lambda () #f)) #:when (lookup-type-name #'i (lambda () #f))
#:with t #'(make-Name #'i) #:with t #'(make-Name #'i)
#:when (add-type-name-reference #'i))) #:when (add-type-name-reference #'i)))
(define-syntax-class type-alias (define-syntax-class type-alias
#:description "type alias"
(pattern i:id (pattern i:id
#:with t (lookup-type-alias #'i parse-type* (lambda () #f)) #:with t (lookup-type-alias #'i parse-type* (lambda () #f))
#:when #'t #:when #'t
#:when (add-type-name-reference #'i))) #:when (add-type-name-reference #'i)))
(define-syntax-class all-type (define-syntax-class all-ddd-formals
#:description "\na sequence of identifiers with a ... after the last identifier\n"
(pattern (v:id ... v-last:id _:ddd)))
(define-syntax-class all-formals
#:description "\na sequence of identifiers\n"
(pattern (v:id ...)))
(define-syntax-class all-type
#:description "All type"
#:transparent
#:literals (t:All) #:literals (t:All)
(pattern (t:All (v:id ... v-last:id _:ddd) b) (pattern (t:All :all-ddd-formals b)
#:with b.t (parse/get #'b t (type/tvars (cons #'v-last.datum (syntax->datum #'(v ...))) #:with b.t (parse/get #'b t (type/tvars (cons #'v-last.datum (syntax->datum #'(v ...)))
(cons (make-Dotted (make-F #'v-last.datum)) (cons (make-Dotted (make-F #'v-last.datum))
(map make-F (syntax->datum #'(v ...)))))) (map make-F (syntax->datum #'(v ...))))))
#:when (add-type-name-reference #'All) #:when (add-type-name-reference #'All)
#:with t (make-PolyDots (syntax->datum #'(v ... v-last)) #'b.t)) #:with t (make-PolyDots (syntax->datum #'(v ... v-last)) #'b.t))
(pattern (t:All (v:id ...) b) (pattern (t:All :all-formals b)
#:with b.t (parse/get #'b t (type/tvars (syntax->datum #'(v ...)) (map make-F (syntax->datum #'(v ...))))) #:with b.t (parse/get #'b t (type/tvars (syntax->datum #'(v ...)) (map make-F (syntax->datum #'(v ...)))))
#:when (add-type-name-reference #'All) #:when (add-type-name-reference #'All)
#:with t (make-Poly (syntax->datum #'(v ...)) #'b.t))) #:with t (make-Poly (syntax->datum #'(v ...)) #'b.t)))
(define-syntax-class type-app (define-syntax-class type-app
#:attributes (t)
(pattern (i arg:type args:type ...) (pattern (i arg:type args:type ...)
#:declare i type #:declare i type
#:when (identifier? #'i) #:when (identifier? #'i)
@ -165,6 +181,7 @@
Err])))) Err]))))
(define-syntax-class not-kw-id (define-syntax-class not-kw-id
#:attributes (datum)
(pattern i:id (pattern i:id
#:when (not (for/or ([e (syntax->list #:when (not (for/or ([e (syntax->list
#'(quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance #'(quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance
@ -174,6 +191,8 @@
#:with datum #'i.datum)) #:with datum #'i.datum))
(define-syntax-class type (define-syntax-class type
#:transparent
#:attributes (t)
#:literals (quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance) #:literals (quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance)
(pattern ty (pattern ty
#:declare ty (3d Type?) #:declare ty (3d Type?)

2
collects/typed-scheme/private/remove-intersect.ss
View File

@ -3,7 +3,7 @@
(require (except-in "../utils/utils.ss" extend)) (require (except-in "../utils/utils.ss" extend))
(require (rep type-rep) (require (rep type-rep)
(private union subtype resolve-type type-effect-convenience type-utils) (private union subtype resolve-type type-effect-convenience type-utils)
mzlib/plt-match mzlib/trace) scheme/match mzlib/trace)
(provide (rename-out [*remove remove]) overlap) (provide (rename-out [*remove remove]) overlap)

2
collects/typed-scheme/private/resolve-type.ss
View File

@ -3,7 +3,7 @@
(require (rep type-rep) (env type-name-env) (utils tc-utils) (require (rep type-rep) (env type-name-env) (utils tc-utils)
"type-utils.ss" "type-utils.ss"
mzlib/plt-match scheme/match
mzlib/trace) mzlib/trace)
(provide resolve-name resolve-app needs-resolving? resolve-once) (provide resolve-name resolve-app needs-resolving? resolve-once)

289
collects/typed-scheme/private/subtype.ss
View File

@ -1,14 +1,15 @@
#lang scheme/base #lang scheme/base
(require "../utils/utils.ss") (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) (utils tc-utils)
"type-utils.ss" "type-utils.ss"
"type-comparison.ss" "type-comparison.ss"
"resolve-type.ss" "resolve-type.ss"
"type-abbrev.ss"
(env type-name-env) (env type-name-env)
(only-in (infer infer-dummy) unify) (only-in (infer infer-dummy) unify)
mzlib/plt-match scheme/match
mzlib/trace) mzlib/trace)
@ -39,13 +40,26 @@
(define (remember s t A) (cons (seen-before s t) A)) (define (remember s t A) (cons (seen-before s t) A))
(define (seen? s t) (member (seen-before s t) (current-seen))) (define (seen? s t) (member (seen-before s t) (current-seen)))
(define subtype-cache (make-hash))
(define (cache-types s t)
(cache-keys (Type-seq s) (Type-seq t)))
(define (cache-keys ks kt)
(hash-set! subtype-cache (cons ks kt) #t))
(define (cached? s t)
(hash-ref subtype-cache (cons (Type-seq s) (Type-seq t)) #f))
;; is s a subtype of t? ;; is s a subtype of t?
;; type type -> boolean ;; type type -> boolean
(define (subtype s t) (define (subtype s t)
(with-handlers (define k (cons (Type-seq s) (Type-seq t)))
([exn:subtype? (lambda _ #f)]) (define lookup? (hash-ref subtype-cache k 'no))
(subtype* (current-seen) s t))) (if (eq? 'no lookup?)
(let ([result (with-handlers
([exn:subtype? (lambda _ #f)])
(subtype* (current-seen) s t))])
(hash-set! subtype-cache k result)
result)
lookup?))
;; are all the s's subtypes of all the t's? ;; are all the s's subtypes of all the t's?
;; [type] [type] -> boolean ;; [type] [type] -> boolean
@ -155,139 +169,139 @@
(define (subtype* A s t) (define (subtype* A s t)
(parameterize ([match-equality-test type-equal?] (parameterize ([match-equality-test type-equal?]
[current-seen A]) [current-seen A])
(if (seen? s t) (let ([ks (Type-key s)] [kt (Type-key t)])
A (cond
(let* ([A0 (remember s t A)]) [(or (seen? s t) (type-equal? s t)) A]
(parameterize ([current-seen A0]) [(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) (fail! s t)]
#;(match t [(and (symbol? ks) (pair? kt) (not (memq ks kt))) (fail! s t)]
[(Name: n) (when (eq? 'heap (syntax-e n)) [(and (pair? ks) (pair? kt)
(trace subtype*))] (for/and ([i (in-list ks)]) (not (memq i kt))))
[_ #f]) (fail! s t)]
[else
(let* ([A0 (remember s t A)])
(parameterize ([current-seen A0])
(match (list s t) (match (list s t)
;; subtyping is reflexive [(list _ (Univ:)) A0]
[(list t t) A0] ;; error is top and bot
;; univ is top [(list _ (Error:)) A0]
[(list _ (Univ:)) A0] [(list (Error:) _) A0]
;; error is top and bot ;; (Un) is bot
[(list _ (Error:)) A0] [(list _ (Union: (list))) (fail! s t)]
[(list (Error:) _) A0] [(list (Union: (list)) _) A0]
;; (Un) is bot ;; value types
[(list _ (Union: (list))) (fail! s t)] [(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
[(list (Union: (list)) _) A0] ;; integers are numbers too
;; value types [(list (Base: 'Integer _) (Base: 'Number _)) A0]
[(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] ;; values are subtypes of their "type"
;; integers are numbers too [(list (Value: (? integer? n)) (Base: 'Integer _)) A0]
[(list (Base: 'Integer _) (Base: 'Number _)) A0] [(list (Value: (? number? n)) (Base: 'Number _)) A0]
;; values are subtypes of their "type" [(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0]
[(list (Value: (? integer? n)) (Base: 'Integer _)) A0] [(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0]
[(list (Value: (? number? n)) (Base: 'Number _)) A0] [(list (Value: (? string? n)) (Base: 'String _)) A0]
[(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0] ;; tvars are equal if they are the same variable
[(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0] [(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
[(list (Value: (? string? n)) (Base: 'String _)) A0] ;; case-lambda
;; tvars are equal if they are the same variable [(list (Function: arr1) (Function: arr2))
[(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))] (when (null? arr1) (fail! s t))
;; case-lambda (let loop-arities ([A* A0]
[(list (Function: arr1) (Function: arr2)) [arr2 arr2])
(when (null? arr1) (fail! s t)) (cond
(let loop-arities ([A* A0] [(null? arr2) A*]
[arr2 arr2]) [(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
(cond [else (fail! s t)]))]
[(null? arr2) A*] ;; recur structurally on pairs
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))] [(list (Pair: a d) (Pair: a* d*))
[else (fail! s t)]))] (let ([A1 (subtype* A0 a a*)])
;; recur structurally on pairs (and A1 (subtype* A1 d d*)))]
[(list (Pair: a d) (Pair: a* d*)) ;; quantification over two types preserves subtyping
(let ([A1 (subtype* A0 a a*)]) [(list (Poly: ns b1) (Poly: ms b2))
(and A1 (subtype* A1 d d*)))] (=> unmatch)
;; quantification over two types preserves subtyping (unless (= (length ns) (length ms))
[(list (Poly: ns b1) (Poly: ms b2)) (unmatch))
(=> unmatch) ;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
(unless (= (length ns) (length ms)) (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
(unmatch)) ;; use unification to see if we can use the polytype here
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2)) [(list (Poly: vs b) s)
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))] (=> unmatch)
;; use unification to see if we can use the polytype here (if (unify vs (list b) (list s)) A0 (unmatch))]
[(list (Poly: vs b) s) [(list s (Poly: vs b))
(=> unmatch) (=> unmatch)
(if (unify vs (list b) (list s)) A0 (unmatch))] (if (null? (fv b)) (subtype* A0 s b) (unmatch))]
[(list s (Poly: vs b)) ;; names are compared for equality:
(=> unmatch) [(list (Name: n) (Name: n*))
(if (null? (fv b)) (subtype* A0 s b) (unmatch))] (=> unmatch)
;; names are compared for equality: (if (free-identifier=? n n*)
[(list (Name: n) (Name: n*)) A0
(=> unmatch) (unmatch))]
(if (free-identifier=? n n*) ;; just unfold the recursive types
A0 [(list _ (? Mu?)) (subtype* A0 s (unfold t))]
(unmatch))] [(list (? Mu?) _) (subtype* A0 (unfold s) t)]
;; just unfold the recursive types ;; for unions, we check the cross-product
[(list _ (? Mu?)) (subtype* A0 s (unfold t))] [(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
[(list (? Mu?) _) (subtype* A0 (unfold s) t)] [(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
;; for unions, we check the cross-product ;; subtyping on immutable structs is covariant
[(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)] [(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
[(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)] (subtypes* A0 flds flds*)]
;; subtyping on immutable structs is covariant [(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
[(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _)) (subtypes* A0 (cons proc flds) (cons proc* flds*))]
(subtypes* A0 flds flds*)] ;; subtyping on structs follows the declared hierarchy
[(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _)) [(list (Struct: nm (? Type? parent) flds proc _ _ _) other)
(subtypes* A0 (cons proc flds) (cons proc* flds*))] ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
;; subtyping on structs follows the declared hierarchy (subtype* A0 parent other)]
[(list (Struct: nm (? Type? parent) flds proc _ _ _) other) ;; applications and names are structs too
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other) [(list (App: (Name: n) args stx) other)
(subtype* A0 parent other)] (let ([t (lookup-type-name n)])
;; applications and names are structs too (unless (Type? t)
[(list (App: (Name: n) args stx) other) (fail! s t))
(let ([t (lookup-type-name n)]) #;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other
(unless (Type? t) (instantiate-poly t args))
(fail! s t)) (unless (Poly? t)
#;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other (tc-error/stx stx "cannot apply non-polymorphic type ~a" t))
(instantiate-poly t args)) (match t [(Poly-unsafe: n _)
(unless (Poly? t) (unless (= n (length args))
(tc-error/stx stx "cannot apply non-polymorphic type ~a" t)) (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
(match t [(Poly-unsafe: n _) n (length args)))])
(unless (= n (length args)) (let ([v (subtype* A0 (instantiate-poly t args) other)])
(tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a" #;(printf "val: ~a~n" v)
n (length args)))]) v))]
(let ([v (subtype* A0 (instantiate-poly t args) other)]) [(list other (App: (Name: n) args stx))
#;(printf "val: ~a~n" v) (let ([t (lookup-type-name n)])
v))] (unless (Type? t)
[(list other (App: (Name: n) args stx)) (fail! s t))
(let ([t (lookup-type-name n)]) #;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other
(unless (Type? t) (instantiate-poly t args))
(fail! s t)) (unless (Poly? t)
#;(printf "subtype: 2 app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other (tc-error/stx stx "cannot apply non-polymorphic type ~a" t))
(instantiate-poly t args)) (match t [(Poly-unsafe: n _)
(unless (Poly? t) (unless (= n (length args))
(tc-error/stx stx "cannot apply non-polymorphic type ~a" t)) (tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a"
(match t [(Poly-unsafe: n _) n (length args)))])
(unless (= n (length args)) ;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args))
(tc-error/stx stx "wrong number of arguments to polymorphic type: expected ~a and got ~a" (let ([v (subtype* A0 other (instantiate-poly t args))])
n (length args)))]) #;(printf "2 val: ~a~n" v)
;(printf "about to call subtype with: ~a ~a ~n" other (instantiate-poly t args)) v))]
(let ([v (subtype* A0 other (instantiate-poly t args))]) [(list (Name: n) other)
#;(printf "2 val: ~a~n" v) (let ([t (lookup-type-name n)])
v))] ;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other)
[(list (Name: n) other) (if (Type? t)
(let ([t (lookup-type-name n)]) (subtype* A0 t other)
;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other) (fail! s t)))]
(if (Type? t) ;; Promises are covariant
(subtype* A0 t other) [(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
(fail! s t)))] ;; subtyping on values is pointwise
;; Promises are covariant [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
[(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)] ;; single values shouldn't actually happen, but they're just like the type
;; subtyping on values is pointwise [(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
;; single values shouldn't actually happen, but they're just like the type ;; subtyping on other stuff
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))] [(list (Syntax: t) (Syntax: t*))
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))] (subtype* A0 t t*)]
;; subtyping on other stuff [(list (Instance: t) (Instance: t*))
[(list (Syntax: t) (Syntax: t*)) (subtype* A0 t t*)]
(subtype* A0 t t*)] ;; otherwise, not a subtype
[(list (Instance: t) (Instance: t*)) [_ (fail! s t) #;(printf "failed")])))]))))
(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))) (and (subtype a b) (subtype b a)))
(provide subtype type-compare? subtypes/varargs subtypes) (provide subtype type-compare? subtypes/varargs subtypes)
@ -302,3 +316,6 @@
;(subtype (-> Univ B) (-> Univ Univ)) ;(subtype (-> Univ B) (-> Univ Univ))
;(subtype (make-poly '(a) (make-tvar 'a)) (make-lst N)) ;(subtype (make-poly '(a) (make-tvar 'a)) (make-lst N))
;;problem:
;; (subtype (make-Mu 'x (make-Syntax (make-Union (list (make-Base 'Number #'number?) (make-F 'x))))) (make-Syntax (make-Univ)))

235
collects/typed-scheme/private/type-abbrev.ss Normal file
View File

@ -0,0 +1,235 @@
#lang scheme
(require "../utils/utils.ss")
(require (rep type-rep effect-rep)
(utils tc-utils)
scheme/list
scheme/match
"type-effect-printer.ss"
scheme/promise
(for-syntax scheme/base stxclass)
(for-template scheme/base scheme/contract scheme/tcp))
(provide (all-defined-out))
(define top-func (make-Function (list (make-top-arr))))
(define (-vet id) (make-Var-True-Effect id))
(define (-vef id) (make-Var-False-Effect id))
(define -rem make-Remove-Effect)
(define -rest make-Restrict-Effect)
(define (var->type-eff eff)
(match eff
[(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
[(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
[_ eff]))
(define ((add-var v) eff)
(match eff
[(Latent-Var-True-Effect:) (-vet v)]
[(Latent-Var-False-Effect:) (-vef v)]
[(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
[(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
[(True-Effect:) eff]
[(False-Effect:) eff]
[_ (int-err "can't add var ~a to effect ~a" v eff)]))
(define-syntax (-> stx)
(syntax-case* stx (:) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
[(_ dom ... rng : eff1 eff2)
#'(->* (list dom ...) rng : eff1 eff2)]
[(_ dom ... rng : eff1 eff2)
#'(->* (list dom ...) rng : eff1 eff2)]
[(_ dom ... rng)
#'(->* (list dom ...) rng)]))
(define-syntax ->*
(syntax-rules (:)
[(_ dom rng)
(make-Function (list (make-arr* dom rng)))]
[(_ dom rst rng)
(make-Function (list (make-arr* dom rng rst)))]
[(_ dom rng : eff1 eff2)
(make-Function (list (make-arr* dom rng #f eff1 eff2)))]
[(_ dom rst rng : eff1 eff2)
(make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
(define-syntax ->...
(syntax-rules (:)
[(_ dom rng)
(->* dom rng)]
[(_ dom (dty dbound) rng)
(make-Function (list (make-arr* dom rng #f (cons dty 'dbound) (list) (list))))]
[(_ dom rng : eff1 eff2)
(->* dom rng : eff1 eff2)]
[(_ dom (dty dbound) rng : eff1 eff2)
(make-Function (list (make-arr* dom rng #f (cons dty 'dbound) eff1 eff2)))]))
(define-syntax cl->
(syntax-rules (:)
[(_ [(dom ...) rng] ...)
(make-Function (list (make-arr* (list dom ...) rng) ...))]
[(_ [(dom ...) rng : eff1 eff2] ...)
(make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
[(_ [(dom ...) rng rst : eff1 eff2] ...)
(make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
(define (cl->* . args)
(define (funty-arities f)
(match f
[(Function: as) as]))
(make-Function (apply append (map funty-arities args))))
(define-syntax (->key stx)
(syntax-parse stx
[(_ ty:expr ... ((k:keyword kty:expr opt:boolean)) ...* rng)
#'(make-Function
(list
(make-arr* (list ty ...)
rng
#f
#f
(list (make-Keyword 'k kty opt) ...)
null
null)))]))
(define make-arr*
(case-lambda [(dom rng) (make-arr dom rng #f #f null (list) (list))]
[(dom rng rest) (make-arr dom rng rest #f null (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest #f null eff1 eff2)]
[(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest null eff1 eff2)]
[(dom rng rest drest kws eff1 eff2)
(make-arr dom rng rest drest (sort #:key Keyword-kw kws keyword<?) eff1 eff2)]))
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #f (cons dty dbound) null null))
(define make-promise-ty
(let ([s (string->uninterned-symbol "Promise")])
(lambda (t)
(make-Struct s #f (list t) #f #f #'promise? values))))
(define N (make-Base 'Number #'number?))
(define -Integer (make-Base 'Integer #'exact-integer?))
(define B (make-Base 'Boolean #'boolean?))
(define Sym (make-Base 'Symbol #'symbol?))
(define -Void (make-Base 'Void #'void?))
(define -Bytes (make-Base 'Bytes #'bytes?))
(define -Regexp (make-Base 'Regexp #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?))))
(define -PRegexp (make-Base 'PRegexp #'(and/c pregexp? (not/c byte-pregexp?))))
(define -Byte-Regexp (make-Base 'Byte-Regexp #'(and/c byte-regexp? (not/c byte-pregexp?))))
(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp?))
(define -String (make-Base 'String #'string?))
(define -Keyword (make-Base 'Keyword #'keyword?))
(define -Char (make-Base 'Char #'char?))
(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag?))
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set?))
(define -Path (make-Base 'Path #'path?))
(define -Namespace (make-Base 'Namespace #'namespace?))
(define -Output-Port (make-Base 'Output-Port #'output-port?))
(define -Input-Port (make-Base 'Input-Port #'input-port?))
(define -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener?))
(define -Syntax make-Syntax)
(define -HT make-Hashtable)
(define -Promise make-promise-ty)
(define Univ (make-Univ))
(define Err (make-Error))
(define -Nat -Integer)
(define-syntax -v
(syntax-rules ()
[(_ x) (make-F 'x)]))
(define-syntax -poly
(syntax-rules ()
[(_ (vars ...) ty)
(let ([vars (-v vars)] ...)
(make-Poly (list 'vars ...) ty))]))
(define-syntax -polydots
(syntax-rules ()
[(_ (vars ... dotted) ty)
(let ([dotted (-v dotted)]
[vars (-v vars)] ...)
(make-PolyDots (list 'vars ... 'dotted) ty))]))
(define-syntax -mu
(syntax-rules ()
[(_ var ty)
(let ([var (-v var)])
(make-Mu 'var ty))]))
(define -values make-Values)
(define-syntax *Un
(syntax-rules ()
[(_ . args) (make-Union (list . args))]))
(define -pair make-Pair)
(define -struct make-Struct)
(define -val make-Value)
(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define -lst make-Listof)
(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
(define -Port (*Un -Input-Port -Output-Port))
(define (-lst* #:tail [tail (-val null)] . args)
(if (null? args)
tail
(-pair (car args) (apply -lst* #:tail tail (cdr args)))))
#;(define NE (-mu x (Un N (make-Listof x))))
(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
(define -Param make-Param)
(define make-pred-ty
(case-lambda
[(in out t)
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
[(t) (make-pred-ty (list Univ) B t)]))
(define -Pathlike (*Un -Path -String))
(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
(define -Byte N)
(define (-Tuple l)
(foldr -pair (-val '()) l))
(define (untuple t)
(match t
[(Value: '()) null]
[(Pair: a b) (cond [(untuple b) => (lambda (l) (cons a l))]
[else #f])]
[_ #f]))
(define -box make-Box)
(define -vec make-Vector)
(define Any-Syntax ;(-Syntax Univ)
(-mu x
(-Syntax (*Un
(-mu y (*Un (-pair x (*Un x y)) (-val '())))
(make-Vector x)
(make-Box x)
N
B
-Keyword
-String
Sym))))
(define Ident (-Syntax Sym))
;; DO NOT USE if t contains #f
(define (-opt t) (*Un (-val #f) t))

1
collects/typed-scheme/private/type-contract.ss
View File

@ -121,6 +121,7 @@
#`(syntax/c #,(t->c t)))] #`(syntax/c #,(t->c t)))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
[(Param: in out) #`(parameter/c #,(t->c out))] [(Param: in out) #`(parameter/c #,(t->c out))]
[(Hashtable: k v) #`hash?]
[else [else
(exit (fail))])))) (exit (fail))]))))

224
collects/typed-scheme/private/type-effect-convenience.ss
View File

@ -10,241 +10,23 @@
"union.ss" "union.ss"
"subtype.ss" "subtype.ss"
"type-utils.ss" "type-utils.ss"
"type-abbrev.ss"
scheme/promise scheme/promise
(for-syntax stxclass) (for-syntax stxclass)
(for-syntax scheme/base) (for-syntax scheme/base)
(for-template scheme/base scheme/contract scheme/tcp)) (for-template scheme/base scheme/contract scheme/tcp))
(provide (all-defined-out) (provide (all-defined-out)
(all-from-out "type-abbrev.ss")
;; these should all eventually go away ;; these should all eventually go away
make-Name make-ValuesDots make-Function make-Latent-Restrict-Effect make-Latent-Remove-Effect) make-Name make-ValuesDots make-Function make-Latent-Restrict-Effect make-Latent-Remove-Effect)
(define (one-of/c . args) (define (one-of/c . args)
(apply Un (map -val args))) (apply Un (map -val args)))
(define top-func (make-Function (list (make-top-arr))))
(define (-vet id) (make-Var-True-Effect id))
(define (-vef id) (make-Var-False-Effect id))
(define -rem make-Remove-Effect)
(define -rest make-Restrict-Effect)
(define (var->type-eff eff)
(match eff
[(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
[(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
[_ eff]))
(define ((add-var v) eff)
(match eff
[(Latent-Var-True-Effect:) (-vet v)]
[(Latent-Var-False-Effect:) (-vef v)]
[(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
[(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
[(True-Effect:) eff]
[(False-Effect:) eff]
[_ (int-err "can't add var ~a to effect ~a" v eff)]))
(define-syntax (-> stx)
(syntax-case* stx (:) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
[(_ dom ... rng : eff1 eff2)
#'(->* (list dom ...) rng : eff1 eff2)]
[(_ dom ... rng : eff1 eff2)
#'(->* (list dom ...) rng : eff1 eff2)]
[(_ dom ... rng)
#'(->* (list dom ...) rng)]))
(define-syntax ->*
(syntax-rules (:)
[(_ dom rng)
(make-Function (list (make-arr* dom rng)))]
[(_ dom rst rng)
(make-Function (list (make-arr* dom rng rst)))]
[(_ dom rng : eff1 eff2)
(make-Function (list (make-arr* dom rng #f eff1 eff2)))]
[(_ dom rst rng : eff1 eff2)
(make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
(define-syntax ->...
(syntax-rules (:)
[(_ dom rng)
(->* dom rng)]
[(_ dom (dty dbound) rng)
(make-Function (list (make-arr* dom rng #f (cons dty 'dbound) (list) (list))))]
[(_ dom rng : eff1 eff2)
(->* dom rng : eff1 eff2)]
[(_ dom (dty dbound) rng : eff1 eff2)
(make-Function (list (make-arr* dom rng #f (cons dty 'dbound) eff1 eff2)))]))
(define-syntax cl->
(syntax-rules (:)
[(_ [(dom ...) rng] ...)
(make-Function (list (make-arr* (list dom ...) rng) ...))]
[(_ [(dom ...) rng : eff1 eff2] ...)
(make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
[(_ [(dom ...) rng rst : eff1 eff2] ...)
(make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
(define (cl->* . args)
(define (funty-arities f)
(match f
[(Function: as) as]))
(make-Function (apply append (map funty-arities args))))
(define-syntax (->key stx)
(syntax-parse stx
[(_ ty:expr ... ((k:keyword kty:expr opt:boolean)) ...* rng)
#'(make-Function
(list
(make-arr* (list ty ...)
rng
#f
#f
(list (make-Keyword 'k kty opt) ...)
null
null)))]))
(define make-arr*
(case-lambda [(dom rng) (make-arr dom rng #f #f null (list) (list))]
[(dom rng rest) (make-arr dom rng rest #f null (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest #f null eff1 eff2)]
[(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest null eff1 eff2)]
[(dom rng rest drest kws eff1 eff2)
(make-arr dom rng rest drest (sort #:key Keyword-kw kws keyword<?) eff1 eff2)]))
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #f (cons dty dbound) null null))
(define make-promise-ty
(let ([s (string->uninterned-symbol "Promise")])
(lambda (t)
(make-Struct s #f (list t) #f #f #'promise? values))))
(define N (make-Base 'Number #'number?))
(define -Integer (make-Base 'Integer #'exact-integer?))
(define B (make-Base 'Boolean #'boolean?))
(define Sym (make-Base 'Symbol #'symbol?))
(define -Void (make-Base 'Void #'void?))
(define -Bytes (make-Base 'Bytes #'bytes?))
(define -Regexp (make-Base 'Regexp #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?))))
(define -PRegexp (make-Base 'PRegexp #'(and/c pregexp? (not/c byte-pregexp?))))
(define -Byte-Regexp (make-Base 'Byte-Regexp #'(and/c byte-regexp? (not/c byte-pregexp?))))
(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp?))
(define -String (make-Base 'String #'string?))
(define -Keyword (make-Base 'Keyword #'keyword?))
(define -Char (make-Base 'Char #'char?))
(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag?))
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set?))
(define -Path (make-Base 'Path #'path?))
(define -Namespace (make-Base 'Namespace #'namespace?))
(define -Output-Port (make-Base 'Output-Port #'output-port?))
(define -Input-Port (make-Base 'Input-Port #'input-port?))
(define -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener?))
(define -Syntax make-Syntax)
(define -HT make-Hashtable)
(define -Promise make-promise-ty)
(define Univ (make-Univ))
(define Err (make-Error))
(define -Nat -Integer)
(define-syntax -v
(syntax-rules ()
[(_ x) (make-F 'x)]))
(define-syntax -poly
(syntax-rules ()
[(_ (vars ...) ty)
(let ([vars (-v vars)] ...)
(make-Poly (list 'vars ...) ty))]))
(define-syntax -polydots
(syntax-rules ()
[(_ (vars ... dotted) ty)
(let ([dotted (-v dotted)]
[vars (-v vars)] ...)
(make-PolyDots (list 'vars ... 'dotted) ty))]))
(define-syntax -mu
(syntax-rules ()
[(_ var ty)
(let ([var (-v var)])
(make-Mu 'var ty))]))
(define -values make-Values)
(define-syntax *Un
(syntax-rules ()
[(_ . args) (make-Union (list . args))]))
(define -pair make-Pair)
(define -struct make-Struct)
(define -val make-Value)
(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define -lst make-Listof)
(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
(define -Port (*Un -Input-Port -Output-Port))
(define (-lst* #:tail [tail (-val null)] . args)
(if (null? args)
tail
(-pair (car args) (apply -lst* #:tail tail (cdr args)))))
#;(define NE (-mu x (Un N (make-Listof x))))
(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
(define (Un/eff . args) (define (Un/eff . args)
(apply Un (map tc-result-t args))) (apply Un (map tc-result-t args)))
(define -Param make-Param)
(define make-pred-ty
(case-lambda
[(in out t)
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
[(t) (make-pred-ty (list Univ) B t)]))
(define -Pathlike (*Un -Path -String))
(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
(define -Byte N)
(define (-Tuple l)
(foldr -pair (-val '()) l))
(define (untuple t)
(match t
[(Value: '()) null]
[(Pair: a b) (cond [(untuple b) => (lambda (l) (cons a l))]
[else #f])]
[_ #f]))
(define -box make-Box)
(define -vec make-Vector)
(define Any-Syntax
(-mu x
(-Syntax (*Un
(-lst x)
(-mu y (*Un x (-pair x y)))
(make-Vector x)
(make-Box x)
N
B
-String
Sym))))
(define Ident (-Syntax Sym))
;; DO NOT USE if t contains #f
(define (-opt t) (*Un (-val #f) t))
(define-syntax (make-env stx) (define-syntax (make-env stx)
(syntax-case stx () (syntax-case stx ()

7
collects/typed-scheme/private/type-utils.ss
View File

@ -5,7 +5,7 @@
(require (rep type-rep effect-rep rep-utils) (require (rep type-rep effect-rep rep-utils)
(utils tc-utils) (utils tc-utils)
(only-in (rep free-variance) combine-frees) (only-in (rep free-variance) combine-frees)
mzlib/plt-match scheme/match
scheme/list scheme/list
mzlib/trace mzlib/trace
(for-syntax scheme/base)) (for-syntax scheme/base))
@ -33,10 +33,11 @@
;; substitute : Type Name Type -> Type ;; substitute : Type Name Type -> Type
(define (substitute image name target) (define (substitute image name target #:Un [Un (get-union-maker)])
(define (sb t) (substitute image name t)) (define (sb t) (substitute image name t))
(if (hash-ref (free-vars* target) name #f) (if (hash-ref (free-vars* target) name #f)
(type-case sb target (type-case sb target
[#:Union tys (Un (map sb tys))]
[#:F name* (if (eq? name* name) image target)] [#:F name* (if (eq? name* name) image target)]
[#:arr dom rng rest drest kws thn-eff els-eff [#:arr dom rng rest drest kws thn-eff els-eff
(begin (begin
@ -141,7 +142,7 @@
;; must be applied to a Mu ;; must be applied to a Mu
(define (unfold t) (define (unfold t)
(match t (match t
[(Mu: name b) (substitute t name b)] [(Mu: name b) (substitute t name b #:Un (lambda (tys) (make-Union (sort tys < #:key Type-seq))))]
[_ (int-err "unfold: requires Mu type, got ~a" t)])) [_ (int-err "unfold: requires Mu type, got ~a" t)]))
(define (instantiate-poly t types) (define (instantiate-poly t types)

5
collects/typed-scheme/private/union.ss
View File

@ -4,7 +4,9 @@
(require (rep type-rep rep-utils) (require (rep type-rep rep-utils)
(utils tc-utils) (utils tc-utils)
"type-utils.ss"
"subtype.ss" "subtype.ss"
"type-abbrev.ss"
"type-effect-printer.ss" "type-effect-printer.ss"
"type-comparison.ss" "type-comparison.ss"
scheme/match mzlib/trace) scheme/match mzlib/trace)
@ -32,6 +34,7 @@
(define Un (define Un
(case-lambda (case-lambda
[() empty-union] [() empty-union]
[(t) t]
[args [args
;; a is a Type (not a union type) ;; a is a Type (not a union type)
;; b is a List[Type] ;; b is a List[Type]
@ -50,7 +53,7 @@
(if (andmap Values? types) (if (andmap Values? types)
(make-Values (apply map Un (map Values-types 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))] (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 null (remove-subtypes types)))]))])) [else (make-union* #;(remove-subtypes types) (foldr union2 '() (remove-subtypes types)))]))]))
#;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args) #;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)

32
collects/typed-scheme/rep/interning.ss
View File

@ -1,25 +1,25 @@
#lang scheme/base #lang scheme/base
(require syntax/boundmap) (require syntax/boundmap (for-syntax scheme/base stxclass))
(provide defintern hash-id) (provide defintern hash-id)
(define-syntax defintern (define-syntax (defintern stx)
(syntax-rules () (syntax-parse stx
[(_ name+args make-name key) [(_ name+args make-name key ([#:extra-arg e:expr]) ...*)
(defintern name+args (lambda () (make-hash #;'weak)) make-name key)] #'(defintern name+args (lambda () (make-hash #;'weak)) make-name key #:extra-arg e ...)]
[(_ (*name arg ...) make-ht make-name key-expr) [(_ (*name:id arg:id ...) make-ht make-name key-expr ([#:extra-arg e:expr]) ...*)
(define *name #'(define *name
(let ([table (make-ht)]) (let ([table (make-ht)])
(lambda (arg ...) (lambda (arg ...)
#;(all-count!) #;(all-count!)
(let ([key key-expr]) (let ([key key-expr])
(hash-ref table key (hash-ref table key
(lambda () (lambda ()
(let ([new (make-name (count!) arg ...)]) (let ([new (make-name (count!) e ... arg ...)])
(hash-set! table key new) (hash-set! table key new)
new)))))))])) new)))))))]))
(define (make-count!) (define (make-count!)

204
collects/typed-scheme/rep/rep-utils.ss
View File

@ -8,12 +8,13 @@
"interning.ss" "interning.ss"
mzlib/etc mzlib/etc
(for-syntax (for-syntax
stxclass
scheme/base scheme/base
syntax/struct syntax/struct
syntax/stx syntax/stx
(utils utils))) (rename-in (utils utils) [id mk-id])))
(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 +26,9 @@
;; all types are Type? ;; 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)))
@ -43,119 +44,88 @@
(define-syntaxes (dt de) (define-syntaxes (dt de)
(let () (let ()
(define (parse-opts opts stx) (define-syntax-class no-provide-kw
(let loop ([provide? #t] [intern? #f] [frees #t] [fold-rhs #f] [opts opts]) (pattern #:no-provide))
(cond (define-syntax-class idlist
[(null? opts) (values provide? intern? frees fold-rhs)] (pattern (i:id ...)))
[(eq? '#:no-provide (syntax-e (stx-car opts))) (define (combiner f flds)
(loop #f intern? frees fold-rhs (cdr opts))] (syntax-parse flds
[(eq? '#:no-frees (syntax-e (stx-car opts))) [() #'empty-hash-table]
(loop #f intern? #f fold-rhs (cdr opts))] [(e) #`(#,f e)]
[(not (and (stx-pair? opts) (stx-pair? (stx-car opts)))) [(e ...) #`(combine-frees (list (#,f e) ...))]))
(raise-syntax-error #f "bad options" stx)] (define-syntax-class frees-pat
[(eq? '#:intern (syntax-e (stx-car (car opts)))) #:transparent
(loop provide? (stx-car (stx-cdr (car opts))) frees fold-rhs (cdr opts))] #:attributes (f1 f2)
[(eq? '#:frees (syntax-e (stx-car (car opts)))) (pattern (f1:expr f2:expr))
(loop provide? intern? (stx-cdr (car opts)) fold-rhs (cdr opts))] (pattern (#f)
[(eq? '#:fold-rhs (syntax-e (stx-car (car opts)))) #:with f1 #'empty-hash-table
(loop provide? intern? frees (stx-cdr (car opts)) (cdr opts))] #:with f2 #'empty-hash-table))
[else (raise-syntax-error #f "bad options" stx)]))) (define-syntax-class fold-pat
#:transparent
#:attributes (e)
(pattern #:base
#:with e fold-target)
(pattern ex:expr
#:with e #'#'ex))
(define (mk par ht-stx) (define (mk par ht-stx)
(lambda (stx) (lambda (stx)
(syntax-case stx () (syntax-parse stx
[(dform nm flds . opts) [(dform nm:id flds:idlist ([[#:key key-expr:expr]] #:opt
(let*-values ([(provide? intern? frees fold-rhs) (parse-opts (syntax->list #'opts) #'opts)] [[#:intern intern?:expr]] #:opt
[(kw) (string->keyword (symbol->string (syntax-e #'nm)))]) [[#:frees . frees:frees-pat]] #:opt
(with-syntax* [[#:fold-rhs fold-rhs:fold-pat]] #:opt
([ex (id #'nm #'nm ":")] [no-provide?:no-provide-kw] #:opt) ...*)
[kw-stx kw] (with-syntax*
[parent par] ([ex (mk-id #'nm #'nm ":")]
[(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)] [kw-stx (string->keyword (symbol->string #'nm.datum))]
[(flds* ...) #'flds] [parent par]
[*maker (id #'nm "*" #'nm)] [(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)]
[**maker (id #'nm "**" #'nm)] [*maker (mk-id #'nm "*" #'nm)]
[ht-stx ht-stx] [**maker (mk-id #'nm "**" #'nm)]
[bfs-fold-rhs (cond [(and fold-rhs (eq? (syntax-e (stx-car fold-rhs)) '#:base)) [ht-stx ht-stx]
#`(lambda (tr er) #,fold-target)] [bfs-fold-rhs (cond [#'fold-rhs #`(lambda (tr er) #,#'fold-rhs.e)]
[(and fold-rhs (stx-pair? fold-rhs)) [else #'(lambda (type-rec-id effect-rec-id)
(with-syntax ([fr (stx-car fold-rhs)]) #`(*maker (#,type-rec-id flds.i) ...))])]
#'(lambda (tr er) [provides (if #'no-provide?
#'fr))] #'(begin)
[fold-rhs (raise-syntax-error fold-rhs "something went wrong")] #`(begin
[else #'(lambda (type-rec-id effect-rec-id) #`(*maker (#,type-rec-id flds*) ...))])] (provide ex pred acc ...)
[provides (if provide? (provide (rename-out [*maker maker]))))]
#`(begin [intern
(provide ex pred acc ...) (let ([mk (lambda (int) #`(defintern (**maker . flds) maker #,int #:extra-arg key-expr))])
(provide (rename-out [*maker maker]))) (syntax-parse #'flds
#'(begin))] [_ #:when #'intern?
[intern (cond (mk #'intern?)]
[(syntax? intern?) [() (mk #'#f)]
#`(defintern (**maker . flds) maker #,intern?)] [(f) (mk #'f)]
[(null? (syntax-e #'flds)) [_ (mk #'(list . flds))]))]
#'(defintern (**maker . flds) maker #f)] [frees
[(stx-null? (stx-cdr #'flds)) #'(defintern (**maker . flds) maker . flds)] (with-syntax ([(f1 f2) (if #'frees
[else #'(defintern (**maker . flds) maker (list . flds))])] #'(frees.f1 frees.f2)
[frees (cond (list (combiner #'free-vars* #'flds)
[(not frees) #'(begin)] (combiner #'free-idxs* #'flds)))])
;; we know that this has no free vars (quasisyntax/loc stx
[(and (pair? frees) (syntax? (car frees)) (not (syntax-e (car frees)))) (define (*maker . flds)
(syntax/loc stx (define v (**maker . flds))
(define (*maker . flds) (unless-in-table
(define v (**maker . flds)) var-table v
#;(printf "~a entered in #f case~n" '*maker) (define fvs f1)
(unless-in-table (define fis f2)
var-table v (hash-set! var-table v fvs)
(hash-set! var-table v empty-hash-table) (hash-set! index-table v fis))
(hash-set! index-table v empty-hash-table)) v)))])
v))] #`(begin
;; we provided an expression each for calculating the free vars and free idxs (define-struct (nm parent) flds #:inspector #f)
;; this should really be 2 expressions, one for each kind (define-match-expander ex
[(and (pair? frees) (pair? (cdr frees))) (lambda (s)
(quasisyntax/loc (syntax-parse s
stx [(_ . fs)
(define (*maker . flds) #:with pat (syntax/loc s (_ _ . fs))
(define v (**maker . flds)) (syntax/loc s (struct nm pat))])))
#;(printf "~a entered in expr case ~n~a~n~a ~n" '*maker '#,(car frees) '#,(cadr frees)) (begin-for-syntax
#, (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
(quasisyntax/loc (car frees) intern
(unless-in-table provides
var-table v frees))])))
(hash-set! var-table v #,(car frees)) (values (mk #'Type #'type-name-ht) (mk #'Effect #'effect-name-ht))))
(hash-set! index-table v #,(cadr frees))))
#;(printf "~a exited in expr case~n" '*maker)
v))]
[else
(let
([combiner
(lambda (f flds)
(syntax-case flds ()
[() #'empty-hash-table]
[(e) #`(#,f e)]
[(e ...) #`(combine-frees (list (#,f e) ...))]))])
(quasisyntax/loc stx
(define (*maker . flds)
(define v (**maker . flds))
#;(printf "~a entered in default case~n" '*maker)
(unless-in-table
var-table v
(define fvs #,(combiner #'free-vars* #'flds))
(define fis #,(combiner #'free-idxs* #'flds))
(hash-set! var-table v fvs)
(hash-set! index-table v fis))
v)))])])
#`(begin
(define-struct (nm parent) flds #:inspector #f)
(define-match-expander ex
(lambda (s)
(...
(syntax-case 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)))
intern
provides
frees)))])))
(values (mk #'Type #'type-name-ht) (mk #'Effect #'effect-name-ht))))

72
collects/typed-scheme/rep/type-rep.ss
View File

@ -13,7 +13,7 @@
;; Type is defined in rep-utils.ss ;; Type is defined in rep-utils.ss
;; t must be a Type ;; t must be a Type
(dt Scope (t)) (dt Scope (t) [#:key (Type-key t)])
;; this is ONLY used when a type error ocurrs ;; this is ONLY used when a type error ocurrs
(dt Error () [#:frees #f] [#:fold-rhs #:base]) (dt Error () [#:frees #f] [#:fold-rhs #:base])
@ -41,39 +41,52 @@
stx)]) stx)])
;; left and right are Types ;; left and right are Types
(dt Pair (left right)) (dt Pair (left right) [#:key 'pair])
;; elem is a Type ;; 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 ;; 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) ;; 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 ;; body is a Scope
(dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))] (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 ;; n is how many variables are bound here
;; body is a Scope ;; body is a Scope
(dt Poly (n body) #:no-provide (dt Poly (n body) #:no-provide
[#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:frees (free-vars* body) (without-below n (free-idxs* body))]
[#:fold-rhs (let ([body* (remove-scopes n 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 ;; n is how many variables are bound here
;; there are n-1 'normal' vars and 1 ... var ;; there are n-1 'normal' vars and 1 ... var
;; body is a Scope ;; body is a Scope
(dt PolyDots (n body) #:no-provide (dt PolyDots (n body) #:no-provide
[#:key (Type-key body)]
[#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:frees (free-vars* body) (without-below n (free-idxs* body))]
[#:fold-rhs (let ([body* (remove-scopes n body)]) [#:fold-rhs (let ([body* (remove-scopes n body)])
(*PolyDots n (add-scopes n (type-rec-id body*))))]) (*PolyDots n (add-scopes n (type-rec-id body*))))])
;; pred : identifier ;; pred : identifier
;; cert : syntax certifier ;; 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 ;; name : symbol
;; parent : Struct ;; parent : Struct
@ -92,7 +105,8 @@
(and proc (type-rec-id proc)) (and proc (type-rec-id proc))
poly? poly?
pred-id pred-id
cert)]) cert)]
[#:key (gensym)])
;; kw : keyword? ;; kw : keyword?
;; ty : Type ;; ty : Type
@ -100,7 +114,8 @@
(dt Keyword (kw ty required?) (dt Keyword (kw ty required?)
[#:frees (free-vars* ty) [#:frees (free-vars* ty)
(free-idxs* 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] ;; dom : Listof[Type]
;; rng : Type ;; rng : Type
@ -112,6 +127,7 @@
;; els-eff : Effect ;; els-eff : Effect
;; arr is NOT a Type ;; arr is NOT a Type
(dt arr (dom rng rest drest kws thn-eff els-eff) (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) [#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null)
(map Keyword-ty kws) (map Keyword-ty kws)
dom))) dom)))
@ -153,13 +169,22 @@
[#:fold-rhs (*Function (map type-rec-id arities))]) [#:fold-rhs (*Function (map type-rec-id arities))])
;; v : Scheme Value ;; 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] ;; elems : Listof[Type]
(dt Union (elems) [#:frees (combine-frees (map free-vars* elems)) (dt Union (elems) [#:frees (combine-frees (map free-vars* elems))
(combine-frees (map free-idxs* elems))] (combine-frees (map free-idxs* elems))]
[#:fold-rhs ((unbox 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]) (dt Univ () [#:frees #f] [#:fold-rhs #:base])
;; types : Listof[Type] ;; types : Listof[Type]
@ -167,23 +192,25 @@
#:no-provide #:no-provide
[#:frees (combine-frees (map free-vars* types)) [#:frees (combine-frees (map free-vars* types))
(combine-frees (map free-idxs* 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) (dt ValuesDots (types dty dbound)
[#:frees (combine-frees (map free-vars* (cons dty types))) [#:frees (combine-frees (map free-vars* (cons dty types)))
(combine-frees (map free-idxs* (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 ;; in : Type
;; out : Type ;; out : Type
(dt Param (in out)) (dt Param (in out) [#:key 'parameter])
;; key : Type ;; key : Type
;; value : Type ;; value : Type
(dt Hashtable (key value)) (dt Hashtable (key value) [#:key 'hash])
;; t : Type ;; t : Type
(dt Syntax (t)) (dt Syntax (t) [#:key 'syntax])
;; pos-flds : (Listof Type) ;; pos-flds : (Listof Type)
;; name-flds : (Listof (Tuple Symbol Type Boolean)) ;; name-flds : (Listof (Tuple Symbol Type Boolean))
@ -197,7 +224,7 @@
(map free-idxs* (append pos-flds (map free-idxs* (append pos-flds
(map cadr name-flds) (map cadr name-flds)
(map cadr methods))))] (map cadr methods))))]
[#:key 'class]
[#:fold-rhs (match (list pos-flds name-flds methods) [#:fold-rhs (match (list pos-flds name-flds methods)
[(list [(list
pos-tys pos-tys
@ -211,17 +238,18 @@
(map list mname (map type-rec-id mty)))])]) (map list mname (map type-rec-id mty)))])])
;; cls : Class ;; cls : Class
(dt Instance (cls)) (dt Instance (cls) [#:key 'instance])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Ugly hack - should use units ;; Ugly hack - should use units
(define union-maker (box #f)) (define union-maker (box (lambda args (int-err "Union not yet available"))))
(define (set-union-maker! v) (set-box! union-maker v)) (define (set-union-maker! v) (set-box! union-maker v))
(define (get-union-maker) (unbox union-maker))
(provide set-union-maker!) (provide set-union-maker! get-union-maker)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

3
collects/typed-scheme/typecheck/tc-app-unit.ss
View File

@ -548,7 +548,8 @@
#:literals (#%plain-app reverse) #:literals (#%plain-app reverse)
[c:lv-clause [c:lv-clause
#:with (#%plain-app reverse n:id) #'c.e #:with (#%plain-app reverse n:id) #'c.e
#:when (free-identifier=? name #'n) #:with (v) #'(c.v ...)
#:when (free-identifier=? name #'v)
(type-annotation #'v)] (type-annotation #'v)]
[_ #f])) [_ #f]))
(syntax-parse stx (syntax-parse stx

13
collects/typed-scheme/utils/utils.ss
View File

@ -171,11 +171,22 @@
(define print-type* (box (lambda _ (error "print-type* not yet defined")))) (define print-type* (box (lambda _ (error "print-type* not yet defined"))))
(define print-effect* (box (lambda _ (error "print-effect* 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) (define-syntax (define-struct/printer stx)
(syntax-case stx () (syntax-case stx ()
[(form name (flds ...) printer) [(form name (flds ...) printer)
#`(define-struct/properties name (flds ...) #`(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)])) #f)]))
(define (id kw . args) (define (id kw . args)