File splitting, dependency reduction.

original commit: f075ecd36e708d21c825666502290e3bb98830af
This commit is contained in:
Sam Tobin-Hochstadt 2012-06-26 13:33:18 -04:00
parent 1d2a50c63e
commit 88460e98dd
12 changed files with 185 additions and 139 deletions

View File

@ -1 +1 @@
#lang typed-scheme
#lang typed/racket/base

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@ -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?)])

View File

@ -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?))]
)