Make environments much lazier about computing types; remove useless requires.

Allow duplicate type annotations when they are the same type.

original commit: 3e1eb67336617150b546841a0c1c3d2793385b06
This commit is contained in:
Sam Tobin-Hochstadt 2011-08-29 19:58:56 -04:00
parent bb11c93478
commit 0550dd15d2
21 changed files with 89 additions and 92 deletions

View File

@ -1,5 +1,5 @@
#;
(exn-pred 4)
(exn-pred 2)
#lang typed/racket
(: bar : (String -> String))
(: bar : (Number -> Number))

View File

@ -1,24 +1,17 @@
#lang racket
#lang racket/base
(require
"../utils/utils.rkt"
(for-template '#%paramz racket/base racket/list
racket/tcp
(only-in rnrs/lists-6 fold-left)
'#%paramz
(only-in '#%kernel [apply kernel:apply])
racket/promise racket/system
(only-in string-constants/private/only-once maybe-print-message)
(only-in racket/match/runtime match:error matchable? match-equality-test)
racket/unsafe/ops racket/flonum)
(utils tc-utils)
(types union convenience)
(rename-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]))
(for-template racket/base racket/list racket/unsafe/ops racket/flonum)
(utils tc-utils)
(rename-in (types union convenience abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]))
(provide indexing)
(define-syntax-rule (make-env* [i t] ...) (make-env [i (λ () t)] ...))
(define-syntax-rule (indexing index-type)
(make-env
(make-env*
[build-list (-poly (a) (index-type (-Index . -> . a) . -> . (-lst a)))]
[make-list (-poly (a) (index-type a . -> . (-lst a)))]
@ -129,7 +122,7 @@
[N index-type]
[?N (-opt index-type)]
[-Input (Un -String -Input-Port -Bytes -Path)])
(-Pattern -Input [N ?N ?outp -Bytes] . ->opt . -Boolean))]
(-Pattern -Input [N ?N ?outp -Bytes] . ->opt . B))]

View File

@ -18,10 +18,12 @@
(define-syntax (define-initial-env stx)
(syntax-parse stx
[(_ initialize-env [id-expr ty] ...)
[(_ initialize-env [id-expr ty] ... #:middle [id-expr* ty*] ...)
#`(begin
(define initial-env (make-env [id-expr ty] ...))
(define (initialize-env) (initialize-type-env initial-env))
(define initial-env (make-env [id-expr (λ () ty)] ... ))
(do-time "finished local-expand types")
(define initial-env* (make-env [id-expr* (λ () ty*)] ...))
(define (initialize-env) (initialize-type-env initial-env) (initialize-type-env initial-env*))
(provide initialize-env))]))
(define-initial-env initialize-special
@ -185,6 +187,7 @@
;; below here: keyword-argument functions from the base environment
;; FIXME: abstraction to remove duplication here
#:middle
[((kw-expander-proc (syntax-local-value #'file->string)))
(->key -Pathlike #:mode (one-of/c 'binary 'text) #f -String)]

View File

@ -98,5 +98,4 @@
(define-hierarchy exn:fail:user (#:kernel-maker k:exn:fail:user) ())))
;; cce: adding exn:break would require a generic type for continuations
(void))

View File

@ -23,7 +23,7 @@
extra
(define e
(parameterize ([infer-param infer])
(make-env [id ty] ...)))
(make-env [id (λ () ty)] ...)))
(define (init)
(initialize-type-env e))
(provide init)))]

View File

@ -5,8 +5,9 @@
(require "../utils/utils.rkt"
syntax/id-table
(rep type-rep)
(utils tc-utils)
(types utils))
(types utils comparison))
(provide register-type register-type-if-undefined
finish-register-type
@ -31,18 +32,24 @@
(define (register-type-if-undefined id type)
(cond [(free-id-table-ref the-mapping id (lambda _ #f))
=> (lambda (e)
(tc-error/expr #:stx id "Duplicate type annotation for ~a" (syntax-e id))
(define t (if (box? e) (unbox e) e))
(unless (and (Type? t) (type-equal? t type))
(tc-error/expr #:stx id "Duplicate type annotation of ~a for ~a, previous was ~a" type (syntax-e id) t))
(when (box? e)
(free-id-table-set! the-mapping id (unbox e))))]
(free-id-table-set! the-mapping id t)))]
[else (register-type id type)]))
;; add a single type to the mapping
;; identifier type -> void
(define (register-type/undefined id type)
;(printf "register-type/undef ~a\n" (syntax-e id))
(if (free-id-table-ref the-mapping id (lambda _ #f))
(void (tc-error/expr #:stx id "Duplicate type annotation for ~a" (syntax-e id)))
(free-id-table-set! the-mapping id (box type))))
(cond [(free-id-table-ref the-mapping id (lambda _ #f))
=>
(λ (t) ;; it's ok to annotate with the same type
(define t* (if (box? t) (unbox t) t))
(unless (and (Type? t*) (type-equal? type t*))
(void (tc-error/expr #:stx id "Duplicate type annotation of ~a for ~a, previous was ~a" type (syntax-e id) t*))))]
[else (free-id-table-set! the-mapping id (box type))]))
;; add a bunch of types to the mapping
;; listof[id] listof[type] -> void
@ -52,9 +59,11 @@
;; given an identifier, return the type associated with it
;; if none found, calls lookup-fail
;; identifier -> type
(define (lookup-type id [fail-handler (lambda () (lookup-type-fail id))])
(let ([v (free-id-table-ref the-mapping id fail-handler)])
(if (box? v) (unbox v) v)))
(define (lookup-type id [fail-handler (λ () (lookup-type-fail id))])
(define v (free-id-table-ref the-mapping id fail-handler))
(cond [(box? v) (unbox v)]
[(procedure? v) (define t (v)) (register-type id t) t]
[else v]))
(define (maybe-finish-register-type id)
(let ([v (free-id-table-ref the-mapping id)])

View File

@ -1,12 +1,11 @@
#lang scheme/base
#lang racket/base
(require (except-in "../utils/utils.rkt" infer))
(require "infer-unit.rkt" "constraints.rkt" "dmap.rkt" "signatures.rkt"
"restrict.rkt" "promote-demote.rkt"
mzlib/trace
(only-in scheme/unit provide-signature-elements
define-values/invoke-unit/infer link)
(utils unit-utils))
racket/trace
(only-in racket/unit provide-signature-elements
define-values/invoke-unit/infer link))
(provide-signature-elements restrict^ infer^)

View File

@ -1,7 +1,6 @@
#lang racket/base
(require racket/unit racket/contract racket/require
"constraint-structs.rkt"
(path-up "utils/utils.rkt" "utils/unit-utils.rkt" "rep/type-rep.rkt"))
"constraint-structs.rkt" (path-up "utils/utils.rkt" "rep/type-rep.rkt"))
(provide (all-defined-out))
(define-signature dmap^

View File

@ -1,12 +1,12 @@
#lang scheme/base
#lang racket/base
(require "../utils/utils.rkt"
(rep type-rep)
(utils tc-utils)
(env global-env)
(except-in (types subtype union convenience resolve utils) -> ->*)
(except-in (types subtype union convenience resolve utils comparison) -> ->*)
(private parse-type)
(only-in scheme/contract listof ->)
(contract-req)
racket/match mzlib/trace)
(provide type-annotation
get-type
@ -38,10 +38,12 @@
(define (type-annotation stx #:infer [let-binding #f])
(define (pt prop)
(when (and (identifier? stx)
let-binding
(lookup-type stx (lambda () #f)))
(maybe-finish-register-type stx)
(tc-error/expr #:stx stx "Duplicate type annotation for ~a" (syntax-e stx)))
let-binding)
(define t1 (parse-type/id stx prop))
(define t2 (lookup-type stx (lambda () #f)))
(when (and t2 (not (type-equal? t1 t2)))
(maybe-finish-register-type stx)
(tc-error/expr #:stx stx "Duplicate type annotation of ~a for ~a, previous was ~a" t1 (syntax-e stx) t2)))
(if (syntax? prop)
(parse-type prop)
(parse-type/id stx prop)))

View File

@ -1,7 +1,6 @@
#lang scheme/base
#lang racket/base
(require racket/match scheme/contract)
(require "rep-utils.rkt" "free-variance.rkt")
(require "rep-utils.rkt" "free-variance.rkt" racket/contract/base)
(define (Filter/c-predicate? e)
(and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e))))

View File

@ -1,8 +1,5 @@
#lang scheme/base
(require "../utils/utils.rkt"
(for-syntax scheme/base)
(utils tc-utils) scheme/list
mzlib/etc scheme/contract)
#lang racket/base
(require "../utils/utils.rkt" (for-syntax racket/base) (contract-req))
(provide Covariant Contravariant Invariant Constant Dotted
combine-frees flip-variances without-below unless-in-table
@ -52,10 +49,10 @@
;; frees -> frees
(define (flip-variances vs)
(for/hasheq ([(k v) (in-hash vs)])
(values k (evcase v
[Covariant Contravariant]
[Contravariant Covariant]
[v v]))))
(values k
(cond [(eq? v Covariant) Contravariant]
[(eq? v Contravariant) Covariant]
[else v]))))
(define (make-invariant vs)
(for/hasheq ([(k v) (in-hash vs)])

View File

@ -1,6 +1,6 @@
#lang scheme/base
#lang racket/base
(require racket/match scheme/contract "rep-utils.rkt" "free-variance.rkt" "filter-rep.rkt")
(require "rep-utils.rkt" "free-variance.rkt" "filter-rep.rkt" "../utils/utils.rkt" (contract-req))
(provide object-equal?)
(def-pathelem CarPE () [#:fold-rhs #:base])

View File

@ -1,13 +1,11 @@
#lang scheme/base
(require "../utils/utils.rkt")
(require mzlib/struct mzlib/pconvert
(require mzlib/pconvert
racket/match
syntax/boundmap
"free-variance.rkt"
"interning.rkt"
racket/syntax unstable/match unstable/struct
mzlib/etc
unstable/match unstable/struct
racket/stxparam
scheme/contract
(for-syntax
@ -17,7 +15,6 @@
(except-in syntax/parse id identifier keyword)
scheme/base
syntax/struct
syntax/stx
scheme/contract
racket/syntax
(rename-in (except-in (utils utils stxclass-util) bytes byte-regexp regexp byte-pregexp pregexp)

View File

@ -1,9 +1,6 @@
#lang scheme/base
(require scheme/unit scheme/contract
"../utils/utils.rkt"
(rep type-rep)
(utils unit-utils)
(types utils))
#lang racket/base
(require racket/unit racket/contract
"../utils/utils.rkt" (rep type-rep) (types utils))
(provide (all-defined-out))
(define-signature tc-expr^

View File

@ -25,7 +25,7 @@
(require (for-template scheme/base
"internal-forms.rkt"))
(provide tc/struct tc/poly-struct names-of-struct tc/builtin-struct d-s)
(provide tc/struct tc/poly-struct names-of-struct d-s)
(define (names-of-struct stx)
(define (parent? stx)
@ -284,20 +284,17 @@
;; register a struct type
;; convenience function for built-in structs
;; tc/builtin-struct : identifier Maybe[identifier] Listof[identifier] Listof[Type] Maybe[identifier] Listof[Type] -> void
(define/cond-contract (tc/builtin-struct nm parent flds tys kernel-maker #;parent-tys)
;; FIXME - figure out how to make this lots lazier
(define/cond-contract (tc/builtin-struct nm parent flds tys kernel-maker)
(c-> identifier? (or/c #f identifier?) (listof identifier?)
(listof Type/c) (or/c #f identifier?) #;(listof fld?)
(listof Type/c) (or/c #f identifier?)
any/c)
(define parent-name (if parent (make-Name parent) #f))
(define parent-flds (if parent (get-parent-flds parent-name) null))
(define parent-tys (map fld-t parent-flds))
(define defs (mk/register-sty nm flds parent-name parent-flds tys #:mutable #t))
(if kernel-maker
(let* ([result-type (lookup-type-name nm)]
[ty (->* (append parent-tys tys) result-type)])
(register-type kernel-maker ty)
(cons (make-def-binding kernel-maker ty) defs))
defs))
(when kernel-maker
(register-type kernel-maker (λ () (->* (append parent-tys tys) (lookup-type-name nm))))))
;; syntax for tc/builtin-struct

View File

@ -1,9 +1,8 @@
#lang scheme/base
#lang racket/base
(require "../utils/utils.rkt")
(require (utils unit-utils)
mzlib/trace
(only-in scheme/unit
(require "../utils/utils.rkt"
racket/trace
(only-in racket/unit
provide-signature-elements
define-values/invoke-unit/infer link)
"signatures.rkt"

View File

@ -1,6 +1,6 @@
#lang scheme/base
#lang racket/base
(require racket/match scheme/vector scheme/contract)
(require racket/match racket/vector racket/contract/base racket/contract/combinator)
(define-struct any-wrap (val)
#:property prop:custom-write

View File

@ -4,7 +4,6 @@
syntax/location
(for-syntax scheme/base
syntax/parse
racket/syntax
(prefix-in tr: "../private/typed-renaming.rkt")))
(provide require/contract define-ignored)

View File

@ -1,8 +1,8 @@
#lang scheme/base
#lang racket/base
(require (except-in syntax/parse id keyword)
(for-syntax syntax/parse
scheme/base
racket/base
(only-in racket/syntax generate-temporary)))
(provide (except-out (all-defined-out) id keyword)

View File

@ -1,4 +1,4 @@
#lang scheme/base
#lang racket/base
#|
This file is for utilities that are only useful for Typed Racket, but
@ -7,7 +7,7 @@ don't depend on any other portion of the system
(provide (all-defined-out))
(require "syntax-traversal.rkt" racket/dict
syntax/parse (for-syntax scheme/base syntax/parse) racket/match)
syntax/parse (for-syntax racket/base syntax/parse) racket/match)
;; a parameter representing the original location of the syntax being
;; currently checked

View File

@ -6,7 +6,7 @@ at least theoretically.
|#
(require (for-syntax racket/base syntax/parse racket/string)
racket/contract racket/require-syntax
racket/contract/base racket/require-syntax
racket/provide-syntax racket/unit (prefix-in d: unstable/debug)
racket/struct-info racket/pretty mzlib/pconvert syntax/parse)
@ -104,7 +104,7 @@ at least theoretically.
#'(void)))
;; some macros to do some timing, only when `timing?' is #t
(define-for-syntax timing? #f)
(define-for-syntax timing? #t)
(define last-time #f) (define initial-time #f)
(define (set!-initial-time t) (set! initial-time t))
@ -178,8 +178,16 @@ at least theoretically.
cond-contracted
define-struct/cond-contract
define/cond-contract
contract-req
define/cond-contract/provide)
(define-require-syntax contract-req
(if enable-contracts?
(syntax-rules ()
[(_) racket/contract])
(syntax-rules ()
[(_) (combine-in)])))
(define-syntax-rule (define/cond-contract/provide (name . args) c . body)
(begin (define/cond-contract name c
(begin