From 88460e98ddbc3ff7e7673bf3ae4d89aebcb7fb07 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 26 Jun 2012 13:33:18 -0400 Subject: [PATCH] File splitting, dependency reduction. original commit: f075ecd36e708d21c825666502290e3bb98830af --- .../typed-racket/succeed/null-program.rkt | 2 +- .../typed-racket/unit-tests/test-utils.rkt | 3 +- collects/typed-racket/base-env/base-types.rkt | 2 +- .../typed-racket/base-env/type-env-lang.rkt | 10 +- collects/typed-racket/core.rkt | 2 +- collects/typed-racket/infer/infer-unit.rkt | 2 +- .../typed-racket/private/type-annotation.rkt | 2 +- collects/typed-racket/typecheck/tc-app.rkt | 3 +- .../typed-racket/typecheck/tc-expr-unit.rkt | 3 +- collects/typed-racket/types/generalize.rkt | 48 +++++++ collects/typed-racket/types/tc-result.rkt | 116 ++++++++++++++++ collects/typed-racket/types/utils.rkt | 131 +----------------- 12 files changed, 185 insertions(+), 139 deletions(-) create mode 100644 collects/typed-racket/types/generalize.rkt create mode 100644 collects/typed-racket/types/tc-result.rkt diff --git a/collects/tests/typed-racket/succeed/null-program.rkt b/collects/tests/typed-racket/succeed/null-program.rkt index 3297b32c..5b678dfa 100644 --- a/collects/tests/typed-racket/succeed/null-program.rkt +++ b/collects/tests/typed-racket/succeed/null-program.rkt @@ -1 +1 @@ -#lang typed-scheme +#lang typed/racket/base diff --git a/collects/tests/typed-racket/unit-tests/test-utils.rkt b/collects/tests/typed-racket/unit-tests/test-utils.rkt index 673ae4c0..f8353210 100644 --- a/collects/tests/typed-racket/unit-tests/test-utils.rkt +++ b/collects/tests/typed-racket/unit-tests/test-utils.rkt @@ -6,7 +6,8 @@ scheme/gui/dynamic typed-racket/utils/utils (for-syntax scheme/base) - (types comparison utils) + (types utils) + (rep type-rep) rackunit rackunit/text-ui) (provide private typecheck (rename-out [infer r:infer]) utils env rep types base-env) diff --git a/collects/typed-racket/base-env/base-types.rkt b/collects/typed-racket/base-env/base-types.rkt index 97153e6d..312e401b 100644 --- a/collects/typed-racket/base-env/base-types.rkt +++ b/collects/typed-racket/base-env/base-types.rkt @@ -153,7 +153,7 @@ [False (-val #f)] [True (-val #t)] [Null (-val null)] -[Nothing (Un)] +[Nothing (*Un)] [Futureof (-poly (a) (-future a))] [Pairof (-poly (a b) (-pair a b))] [MPairof (-poly (a b) (-mpair a b))] diff --git a/collects/typed-racket/base-env/type-env-lang.rkt b/collects/typed-racket/base-env/type-env-lang.rkt index a7c01097..6458823b 100644 --- a/collects/typed-racket/base-env/type-env-lang.rkt +++ b/collects/typed-racket/base-env/type-env-lang.rkt @@ -1,10 +1,10 @@ #lang racket/base -(require "../utils/utils.rkt" - (for-syntax (env init-envs) +(require "../utils/utils.rkt" + (for-syntax "../env/global-env.rkt" racket/base syntax/parse (except-in (rep filter-rep type-rep) make-arr) - (rename-in (types union convenience) [make-arr* make-arr]))) + (rename-in (types numeric-tower abbrev convenience)))) (define-syntax (#%module-begin stx) (syntax-parse stx #:literals (require provide) @@ -25,7 +25,7 @@ (provide #%module-begin require (all-from-out racket/base) - (for-syntax - (types-out convenience union) + (for-syntax (rep-out type-rep) + (types-out numeric-tower abbrev convenience) (all-from-out racket/base))) diff --git a/collects/typed-racket/core.rkt b/collects/typed-racket/core.rkt index 7eb3b962..3959c27c 100644 --- a/collects/typed-racket/core.rkt +++ b/collects/typed-racket/core.rkt @@ -6,7 +6,7 @@ (private with-types type-contract parse-type) (except-in syntax/parse id) racket/match racket/syntax unstable/match racket/list - (types utils convenience) + (types utils convenience generalize) (typecheck provide-handling tc-toplevel tc-app-helper) (rep type-rep) (for-template (only-in (base-env prims) :type :print-type :query-result-type)) diff --git a/collects/typed-racket/infer/infer-unit.rkt b/collects/typed-racket/infer/infer-unit.rkt index 69fc411f..1e472ef2 100644 --- a/collects/typed-racket/infer/infer-unit.rkt +++ b/collects/typed-racket/infer/infer-unit.rkt @@ -6,7 +6,7 @@ (utils tc-utils) (rep free-variance type-rep filter-rep rep-utils) (types utils convenience union subtype remove-intersect resolve - substitute) + substitute generalize) (env type-name-env index-env tvar-env)) make-env -> ->* one-of/c) "constraint-structs.rkt" diff --git a/collects/typed-racket/private/type-annotation.rkt b/collects/typed-racket/private/type-annotation.rkt index e6ac2e56..f28c91e9 100644 --- a/collects/typed-racket/private/type-annotation.rkt +++ b/collects/typed-racket/private/type-annotation.rkt @@ -4,7 +4,7 @@ (rep type-rep) (utils tc-utils) (env global-env) - (except-in (types subtype union convenience resolve utils comparison) -> ->* one-of/c) + (except-in (types subtype union convenience resolve utils generalize comparison) -> ->* one-of/c) (private parse-type) (contract-req) racket/match) diff --git a/collects/typed-racket/typecheck/tc-app.rkt b/collects/typed-racket/typecheck/tc-app.rkt index 13c872eb..83c0aaa4 100644 --- a/collects/typed-racket/typecheck/tc-app.rkt +++ b/collects/typed-racket/typecheck/tc-app.rkt @@ -15,7 +15,8 @@ ;; end fixme (for-syntax syntax/parse racket/base (utils tc-utils)) (private type-annotation) - (types utils abbrev union subtype resolve convenience type-table substitute) + (types utils abbrev union subtype resolve convenience + type-table substitute generalize) (utils tc-utils) (only-in srfi/1 alist-delete) (except-in (env type-env-structs tvar-env index-env) extend) diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index c0348796..58973053 100644 --- a/collects/typed-racket/typecheck/tc-expr-unit.rkt +++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt @@ -5,7 +5,8 @@ racket/match (prefix-in - racket/contract) "signatures.rkt" "tc-envops.rkt" "tc-metafunctions.rkt" "tc-subst.rkt" "check-below.rkt" "tc-funapp.rkt" "tc-app-helper.rkt" "../types/kw-types.rkt" - (types utils convenience union subtype remove-intersect type-table filter-ops) + (types utils convenience union subtype remove-intersect + type-table filter-ops generalize) (private-in parse-type type-annotation) (rep type-rep) (only-in (infer infer) restrict) diff --git a/collects/typed-racket/types/generalize.rkt b/collects/typed-racket/types/generalize.rkt new file mode 100644 index 00000000..39bf8ad9 --- /dev/null +++ b/collects/typed-racket/types/generalize.rkt @@ -0,0 +1,48 @@ +#lang racket/base + +(require "../utils/utils.rkt" + (rep type-rep filter-rep object-rep rep-utils) + (utils tc-utils) + (only-in racket/contract current-blame-format) + "abbrev.rkt" "numeric-tower.rkt" "subtype.rkt" "substitute.rkt" "union.rkt" + racket/match + (for-syntax syntax/parse racket/base) + syntax/id-table racket/dict) + +(provide generalize) + +;; used to produce a more general type for loop variables, vectors, etc. +;; generalize : Type -> Type +(define (generalize t) + (let/ec exit + (let loop ([t* t]) + (match t* + [(Value: '()) (-lst Univ)] + [(Value: 0) -Int] + [(List: ts) (-lst (apply Un ts))] + [(? (lambda (t) (subtype t -Int))) -Int] + [(? (lambda (t) (subtype t -Rat))) -Rat] + [(? (lambda (t) (subtype t -Flonum))) -Flonum] + [(? (lambda (t) (subtype t -SingleFlonum))) -SingleFlonum] + [(? (lambda (t) (subtype t -InexactReal))) -InexactReal] + [(? (lambda (t) (subtype t -Real))) -Real] + [(? (lambda (t) (subtype t -ExactNumber))) -ExactNumber] + [(? (lambda (t) (subtype t -FloatComplex))) -FloatComplex] + [(? (lambda (t) (subtype t -SingleFlonumComplex))) -SingleFlonumComplex] + [(? (lambda (t) (subtype t -Number))) -Number] + [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*] + [(Pair: t1 (Value: '())) (-lst t1)] + [(MPair: t1 (Value: '())) (-mlst t1)] + [(or (Pair: t1 t2) (MPair: t1 t2)) + (let ([t-new (loop t2)]) + (if (type-equal? ((match t* + [(Pair: _ _) -lst] + [(MPair: _ _) -mlst]) + t1) + t-new) + t-new + (exit t)))] + [(ListDots: t bound) (-lst (substitute Univ bound t))] + [(? (lambda (t) (subtype t -Symbol))) -Symbol] + [(Value: #t) -Boolean] + [_ (exit t)])))) \ No newline at end of file diff --git a/collects/typed-racket/types/tc-result.rkt b/collects/typed-racket/types/tc-result.rkt new file mode 100644 index 00000000..b5896e2e --- /dev/null +++ b/collects/typed-racket/types/tc-result.rkt @@ -0,0 +1,116 @@ +#lang racket/base + +(require "../utils/utils.rkt" + (rep free-variance type-rep filter-rep object-rep rep-utils) + (utils tc-utils) + racket/match + (contract-req)) + +;; this structure represents the result of typechecking an expression +(define-struct/cond-contract tc-result + ([t Type/c] [f FilterSet/c] [o Object?]) + #:transparent) +(define-struct/cond-contract tc-results + ([ts (listof tc-result?)] [drest (or/c (cons/c Type/c symbol?) #f)]) + #:transparent) + +(define-match-expander tc-result: + (syntax-rules () + [(_ tp fp op) (struct tc-result (tp fp op))] + [(_ tp) (struct tc-result (tp _ _))])) + +(define-match-expander tc-results: + (syntax-rules () + [(_ tp fp op) + (struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) + #f))] + [(_ tp fp op dty dbound) + (struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) + (cons dty dbound)))] + [(_ tp) + (struct tc-results ((list (struct tc-result (tp _ _)) (... ...)) + #f))])) + +(define-match-expander tc-result1: + (syntax-rules () + [(_ tp fp op) (struct tc-results ((list (struct tc-result (tp fp op))) + #f))] + [(_ tp) (struct tc-results ((list (struct tc-result (tp _ _))) + #f))])) + +(define (tc-results-t tc) + (match tc + [(tc-results: t) t])) + +(define-match-expander Result1: + (syntax-rules () + [(_ tp) (Values: (list (Result: tp _ _)))] + [(_ tp fp op) (Values: (list (Result: tp fp op)))])) + +(define-match-expander Results: + (syntax-rules () + [(_ tp) (Values: (list (Result: tp _ _) (... ...)))] + [(_ tp fp op) (Values: (list (Result: tp fp op) (... ...)))])) + +;; convenience function for returning the result of typechecking an expression +(define ret + (case-lambda [(t) + (let ([mk (lambda (t) (make-FilterSet (make-Top) (make-Top)))]) + (make-tc-results + (cond [(Type? t) + (list (make-tc-result t (mk t) (make-Empty)))] + [else + (for/list ([i t]) + (make-tc-result i (mk t) (make-Empty)))]) + #f))] + [(t f) + (make-tc-results + (if (Type? t) + (list (make-tc-result t f (make-Empty))) + (for/list ([i t] [f f]) + (make-tc-result i f (make-Empty)))) + #f)] + [(t f o) + (make-tc-results + (if (and (list? t) (list? f) (list? o)) + (map make-tc-result t f o) + (list (make-tc-result t f o))) + #f)] + [(t f o dty) + (int-err "ret used with dty without dbound")] + [(t f o dty dbound) + (make-tc-results + (if (and (list? t) (list? f) (list? o)) + (map make-tc-result t f o) + (list (make-tc-result t f o))) + (cons dty dbound))])) + +;(trace ret) + +(provide/cond-contract + [ret + (->i ([t (or/c Type/c (listof Type/c))]) + ([f (t) (if (list? t) + (listof FilterSet/c) + FilterSet/c)] + [o (t) (if (list? t) + (listof Object?) + Object?)] + [dty Type/c] + [dbound symbol?]) + [res tc-results?])]) + +(define (combine-results tcs) + (match tcs + [(list (tc-result1: t f o) ...) + (ret t f o)])) + +(define tc-result-equal? equal?) + +(provide tc-result: tc-results: tc-result1: Result1: Results:) +(provide/cond-contract + [combine-results ((listof tc-results?) . -> . tc-results?)] + [tc-result? (any/c . -> . boolean?)] + [tc-result-t (tc-result? . -> . Type/c)] + [tc-result-equal? (tc-result? tc-result? . -> . boolean?)] + [tc-results? (any/c . -> . boolean?)]) \ No newline at end of file diff --git a/collects/typed-racket/types/utils.rkt b/collects/typed-racket/types/utils.rkt index de5899ce..3edd8fcc 100644 --- a/collects/typed-racket/types/utils.rkt +++ b/collects/typed-racket/types/utils.rkt @@ -3,16 +3,15 @@ (require "../utils/utils.rkt" (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) - "substitute.rkt" + "substitute.rkt" "tc-result.rkt" (only-in (rep free-variance) combine-frees) (env index-env tvar-env) racket/match racket/list - racket/contract - (for-syntax racket/base syntax/parse)) + racket/contract) -(provide effects-equal?) ;;Never Used +(provide (all-from-out "tc-result.rkt")) ;; unfold : Type -> Type @@ -55,119 +54,6 @@ [_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)])) -;; this structure represents the result of typechecking an expression -(define-struct/cond-contract tc-result - ([t Type/c] [f FilterSet/c] [o Object?]) - #:transparent) -(define-struct/cond-contract tc-results - ([ts (listof tc-result?)] [drest (or/c (cons/c Type/c symbol?) #f)]) - #:transparent) - -(define-match-expander tc-result: - (syntax-parser - [(_ tp fp op) #'(struct tc-result (tp fp op))] - [(_ tp) #'(struct tc-result (tp _ _))])) - -(define-match-expander tc-results: - (syntax-parser - [(_ tp fp op) - #'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) - #f))] - [(_ tp fp op dty dbound) - #'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) - (cons dty dbound)))] - [(_ tp) - #'(struct tc-results ((list (struct tc-result (tp _ _)) (... ...)) - #f))])) - -(define-match-expander tc-result1: - (syntax-parser - [(_ tp fp op) #'(struct tc-results ((list (struct tc-result (tp fp op))) - #f))] - [(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _))) - #f))])) - -(define (tc-results-t tc) - (match tc - [(tc-results: t) t])) - -(provide tc-result: tc-results: tc-result1: Result1: Results:) - -(define-match-expander Result1: - (syntax-parser - [(_ tp) #'(Values: (list (Result: tp _ _)))] - [(_ tp fp op) #'(Values: (list (Result: tp fp op)))])) - -(define-match-expander Results: - (syntax-parser - [(_ tp) #'(Values: (list (Result: tp _ _) (... ...)))] - [(_ tp fp op) #'(Values: (list (Result: tp fp op) (... ...)))])) - -;; convenience function for returning the result of typechecking an expression -(define ret - (case-lambda [(t) - (let ([mk (lambda (t) (make-FilterSet (make-Top) (make-Top)))]) - (make-tc-results - (cond [(Type? t) - (list (make-tc-result t (mk t) (make-Empty)))] - [else - (for/list ([i t]) - (make-tc-result i (mk t) (make-Empty)))]) - #f))] - [(t f) - (make-tc-results - (if (Type? t) - (list (make-tc-result t f (make-Empty))) - (for/list ([i t] [f f]) - (make-tc-result i f (make-Empty)))) - #f)] - [(t f o) - (make-tc-results - (if (and (list? t) (list? f) (list? o)) - (map make-tc-result t f o) - (list (make-tc-result t f o))) - #f)] - [(t f o dty) - (int-err "ret used with dty without dbound")] - [(t f o dty dbound) - (make-tc-results - (if (and (list? t) (list? f) (list? o)) - (map make-tc-result t f o) - (list (make-tc-result t f o))) - (cons dty dbound))])) - -;(trace ret) - -(provide/cond-contract - [ret - (->i ([t (or/c Type/c (listof Type/c))]) - ([f (t) (if (list? t) - (listof FilterSet/c) - FilterSet/c)] - [o (t) (if (list? t) - (listof Object?) - Object?)] - [dty Type/c] - [dbound symbol?]) - [res tc-results?])]) - -(define (combine-results tcs) - (match tcs - [(list (tc-result1: t f o) ...) - (ret t f o)])) - - -;; type comparison - -;; equality - good - -(define tc-result-equal? equal?) -(define (effects-equal? fs1 fs2) - (and - (= (length fs1) (length fs2)) - (andmap eq? fs1 fs2))) - - ;; fv : Type -> Listof[Symbol] (define (fv t) (hash-map (free-vars* t) (lambda (k v) k))) (define (fi t) (for/list ([(k v) (in-hash (free-idxs* t))]) k)) @@ -217,21 +103,14 @@ [unfold (Mu? . -> . Type/c)] [instantiate-poly ((or/c Poly? PolyDots?) (listof Type/c) . -> . Type/c)] [instantiate-poly-dotted - (PolyDots? (listof Type/c) Type/c symbol? . -> . Type/c)] - [tc-result? (any/c . -> . boolean?)] - [tc-result-t (tc-result? . -> . Type/c)] - [tc-result-equal? (tc-result? tc-result? . -> . boolean?)] - [tc-results? (any/c . -> . boolean?)] + (PolyDots? (listof Type/c) Type/c symbol? . -> . Type/c)] [tc-error/expr ((string?) (#:return any/c #:stx syntax?) #:rest (listof any/c) . ->* . any/c)] - [fv (Rep? . -> . (listof symbol?))] [fi (Rep? . -> . (listof symbol?))] [fv/list ((listof Type/c) . -> . (listof symbol?))] [lookup-fail (identifier? . -> . Type/c)] - [lookup-type-fail (identifier? . -> . Type/c)] - [combine-results ((listof tc-results?) . -> . tc-results?)] + [lookup-type-fail (identifier? . -> . Type/c)] [current-poly-struct (parameter/c (or/c #f poly?))] - )