Clean up of typechecking for heterogeneous vectors and structs.

This commit is contained in:
Eric Dobson 2012-06-15 21:21:33 -07:00 committed by Sam Tobin-Hochstadt
parent dd078dcb95
commit 1df6165e9f
5 changed files with 152 additions and 221 deletions

View File

@ -229,6 +229,8 @@
[tc-e/t #(2 3 #t) (make-HeterogenousVector (list -Integer -Integer -Boolean))]
[tc-e (vector 2 "3" #t) (make-HeterogenousVector (list -Integer -String -Boolean))]
[tc-e (vector-immutable 2 "3" #t) (make-HeterogenousVector (list -Integer -String -Boolean))]
[tc-e (make-vector 4 1) (-vec -Integer)]
[tc-e (build-vector 4 (lambda (x) 1)) (-vec -Integer)]
[tc-e (range 4) (-lst -Byte)]
[tc-e (range 2 4 1) (-lst -PosByte)]
[tc-e (range 0 4 1) (-lst -Byte)]
@ -880,9 +882,9 @@
#:ret (ret -Number -true-filter))
[tc-e (let ([x 1]) (if x x (add1 x)))
#:ret (ret -One (-FS -top -top))]
[tc-e (let: ([x : (U (Vectorof Number) String) (vector 1 2 3)])
[tc-e (let: ([x : (U (Vectorof Integer) String) (vector 1 2 3)])
(if (vector? x) (vector-ref x 0) (string-length x)))
-Number]
-Integer]
[tc-e (let ()
(define: foo : (Integer * -> Integer) +)
(foo 1 2 3 4 5))

View File

@ -31,6 +31,9 @@
([cond-contracted tc/app (syntax? . -> . tc-results?)]
[cond-contracted tc/app/check (syntax? tc-results? . -> . tc-results?)]))
(define-signature tc-app-hetero^
([cond-contracted tc/app-hetero (syntax? (or/c #f tc-results?). -> . (or/c #f tc-results?))]))
(define-signature tc-apply^
([cond-contracted tc/apply (syntax? syntax? . -> . tc-results?)]))

View File

@ -30,7 +30,7 @@
(only-in racket/private/class-internal do-make-object)
(only-in syntax/location module-name-fixup)))
(import tc-expr^ tc-lambda^ tc-let^ tc-apply^)
(import tc-expr^ tc-lambda^ tc-let^ tc-apply^ tc-app-hetero^)
(export tc-app^)
@ -272,6 +272,7 @@
;; the main dispatching function
;; syntax tc-results? -> tc-results?
(define (tc/app/internal form expected)
(or (tc/app-hetero form expected)
(syntax-parse form
#:literals (#%plain-app #%plain-lambda letrec-values quote
values apply k:apply not false? list list* call-with-values
@ -308,223 +309,6 @@
Univ)))
(list (ret Univ) (single-value #'arg))
expected)])]
;; unsafe struct operations
[(#%plain-app (~and op:normal-op (~or (~literal unsafe-struct-ref) (~literal unsafe-struct*-ref))) s e:expr)
(let ([e-t (single-value #'e)])
(match (single-value #'s)
[(tc-result1:
(and t (or (Struct: _ _ (list (fld: flds _ muts) ...) _ _ _ _ _)
(? needs-resolving?
(app resolve-once
(Struct: _ _ (list (fld: flds _ muts) ...) _ _ _ _ _))))))
(let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f])
(match e-t
[(tc-result1: (Value: (? number? i))) i]
[_ #f]))])
(cond [(not ival)
(check-below e-t -Integer)
(cond-check-below (ret (apply Un flds)) expected)]
[(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length flds))))
(let ([result (if (list-ref muts ival)
(ret (list-ref flds ival))
;; FIXME - could do something with paths here
(ret (list-ref flds ival)))])
(cond-check-below result expected))]
[(not (and (integer? ival) (exact? ival)))
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"expected exact integer for struct index, but got ~a" ival)]
[(< ival 0)
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"index ~a too small for struct ~a" ival t)]
[(not (<= ival (sub1 (length flds))))
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"index ~a too large for struct ~a" ival t)]))]
[s-ty
(let ([arg-tys (list s-ty e-t)])
(tc/funapp #'op #'(s e) (single-value #'op) arg-tys expected))]))]
[(#%plain-app (~and op:normal-op (~or (~literal unsafe-struct-set!) (~literal unsafe-struct*-set!)))
s e:expr val:expr)
(let ([e-t (single-value #'e)])
(match (single-value #'s)
[(tc-result1: (and t (or (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _)
(? needs-resolving?
(app resolve-once
(Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))))
(let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f])
(match e-t
[(tc-result1: (Value: (? number? i))) i]
[_ #f]))])
(cond [(not ival)
(tc-error/expr
#:stx #'e
#:return (or expected (ret -Void))
"expected statically known index for unsafe struct mutation, but got ~a"
(match e-t [(tc-result1: t) t]))]
[(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length flds))))
(tc-expr/check #'val (ret (list-ref flds ival)))
(cond-check-below (ret -Void) expected)]
[(not (and (integer? ival) (exact? ival)))
(single-value #'val)
(tc-error/expr
#:stx #'e #:return (or expected (ret (Un)))
"expected exact integer for unsafe struct mutation, but got ~a" ival)]
[(< ival 0)
(single-value #'val)
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"index ~a too small for struct ~a" ival t)]
[(not (<= ival (sub1 (length flds))))
(single-value #'val)
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"index ~a too large for struct ~a" ival t)]))]
[s-ty
(let ([arg-tys (list s-ty e-t (single-value #'val))])
(tc/funapp #'op #'(s e val) (single-value #'op) arg-tys expected))]))]
;; vector-ref on het vectors
[(#%plain-app (~and op:normal-op (~or (~literal vector-ref)
(~literal unsafe-vector-ref)
(~literal unsafe-vector*-ref)))
v e:expr)
(let ([e-t (single-value #'e)])
(let loop ((v-t (single-value #'v)))
(match v-t
[(tc-result1: (and t (HeterogenousVector: es)))
(let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f])
(match e-t
[(tc-result1: (Value: (? number? i))) i]
[_ #f]))])
(cond [(not ival)
(check-below e-t -Integer)
(cond-check-below (ret (apply Un es)) expected)]
[(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es))))
(cond-check-below (ret (list-ref es ival)) expected)]
[(not (and (integer? ival) (exact? ival)))
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"expected exact integer for vector index, but got ~a" ival)]
[(< ival 0)
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"index ~a too small for vector ~a" ival t)]
[(not (<= ival (sub1 (length es))))
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"index ~a too large for vector ~a" ival t)]))]
[(tc-result1: (? needs-resolving? e) f o)
(loop (ret (resolve-once e) f o))]
[v-ty
(let ([arg-tys (list v-ty e-t)])
(tc/funapp #'op #'(v e) (single-value #'op) arg-tys expected))])))]
[(#%plain-app (~and op:normal-op (~or (~literal vector-set!)
(~literal unsafe-vector-set!)
(~literal unsafe-vector*-set!)))
v e:expr val:expr)
(let ([e-t (single-value #'e)])
(let loop ((v-t (single-value #'v)))
(match v-t
[(tc-result1: (and t (HeterogenousVector: es)))
(let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f])
(match e-t
[(tc-result1: (Value: (? number? i))) i]
[_ #f]))])
(cond [(not ival)
(tc-error/expr
#:stx #'e #:return (or expected (ret -Void))
"expected statically known index for heterogeneous vector, but got ~a"
(match e-t [(tc-result1: t) t]))]
[(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es))))
(tc-expr/check #'val (ret (list-ref es ival)))
(cond-check-below (ret -Void) expected)]
[(not (and (integer? ival) (exact? ival)))
(single-value #'val)
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"expected exact integer for vector index, but got ~a" ival)]
[(< ival 0)
(single-value #'val)
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"index ~a too small for vector ~a" ival t)]
[(not (<= ival (sub1 (length es))))
(single-value #'val)
(tc-error/expr #:stx #'e #:return (or expected (ret (Un)))
"index ~a too large for vector ~a" ival t)]))]
[(tc-result1: (? needs-resolving? e) f o)
(loop (ret (resolve-once e) f o))]
[v-ty
(let ([arg-tys (list v-ty e-t (single-value #'val))])
(tc/funapp #'op #'(v e val) (single-value #'op) arg-tys expected))])))]
[(#%plain-app (~and op:normal-op (~or (~literal vector-immutable) (~literal vector))) args:expr ...)
(let loop ([expected expected])
(match expected
[(tc-result1: (Vector: t))
(for ([e (in-list (syntax->list #'(args ...)))])
(tc-expr/check e (ret t)))
expected]
[(tc-result1: (HeterogenousVector: ts))
(unless (= (length ts) (length (syntax->list #'(args ...))))
(tc-error/expr "expected vector with ~a elements, but got ~a"
(length ts)
(make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...))))))
(for ([e (in-list (syntax->list #'(args ...)))]
[t (in-list ts)])
(tc-expr/check e (ret t)))
expected]
[(tc-result1: (? needs-resolving? e) f o)
(loop (ret (resolve-once e) f o))]
;; If the expected type is a union, then we examine just the parts
;; of the union that are vectors. If there's only one of those,
;; we re-run this whole algorithm with that. Otherwise, we treat
;; it like any other expected type.
[(tc-result1: (Union: ts))
(define u-ts (for/list ([t (in-list ts)]
#:when (eq? 'vector (Type-key t)))
t))
(match u-ts
[(list)
(define arg-tys (map single-value (syntax->list #'(args ...))))
(tc/funapp #'op #'(args ...) (single-value #'op) arg-tys expected)]
[(list t0)
(check-below (loop (ret t0)) expected)]
[_
(check-below
(ret (make-HeterogenousVector (map (lambda (x) (generalize (tc-expr/t x)))
(syntax->list #'(args ...)))))
expected)])]
;; since vectors are mutable, if there is no expected type,
;; we want to generalize the element type
[(or #f (tc-result1: _))
(cond-check-below
(ret (make-HeterogenousVector (map (lambda (x) (generalize (tc-expr/t x)))
(syntax->list #'(args ...)))))
expected)]
[_ (int-err "bad expected: ~a" expected)]))]
;; since vectors are mutable, if there is no expected type,
;; we want to generalize the element type
[(#%plain-app (~and op:normal-op (~literal make-vector)) n elt)
(match expected
[(tc-result1: (Vector: t))
(tc-expr/check #'n (ret -Integer))
(tc-expr/check #'elt (ret t))
expected]
[(or #f (tc-result1: _))
(tc/funapp #'op #'(n elt) (single-value #'op)
(list (single-value #'n)
(match (single-value #'elt)
[(tc-result1: t) (ret (generalize t))]))
expected)]
[_ (int-err "bad expected: ~a" expected)])]
[(#%plain-app (~and op:normal-op (~literal build-vector)) n proc)
(match expected
[(tc-result1: (Vector: t))
(tc-expr/check #'n (ret -Integer))
(tc-expr/check #'proc (ret (-NonNegFixnum . -> . t)))
expected]
[(or #f (tc-result1: _))
(tc/funapp #'op #'(n elt) (single-value #'op)
(list (single-value #'n)
(match (tc/funapp #'proc #'(1) ; valid nonnegative-fixnum
(single-value #'proc)
(list (ret -NonNegFixnum))
#f)
[(tc-result1: t) (ret (-> -NonNegFixnum (generalize t)))]))
expected)]
[_ (int-err "bad expected: ~a" expected)])]
;; call-with-values
[(#%plain-app call-with-values prod con)
(match (tc/funapp #'prod #'() (single-value #'prod) null #f)

View File

@ -0,0 +1,140 @@
#lang racket/unit
(require (rename-in "../../utils/utils.rkt" [infer r:infer])
"../signatures.rkt" "../tc-metafunctions.rkt" "../check-below.rkt"
"../tc-app-helper.rkt" "../find-annotation.rkt" "../tc-funapp.rkt"
"../tc-subst.rkt" (prefix-in c: racket/contract)
syntax/parse racket/match racket/trace scheme/list
unstable/sequence unstable/list
;; fixme - don't need to be bound in this phase - only to make tests work
scheme/bool
racket/unsafe/ops
(only-in racket/private/class-internal do-make-object)
(only-in syntax/location module-name-fixup)
(only-in '#%kernel [apply k:apply] [reverse k:reverse])
;; end fixme
(for-syntax syntax/parse scheme/base (utils tc-utils))
(private type-annotation)
(types utils abbrev union subtype resolve convenience type-table substitute)
(utils tc-utils)
(only-in srfi/1 alist-delete)
(except-in (env type-env-structs tvar-env index-env) extend)
(rep type-rep filter-rep object-rep rep-utils)
(r:infer infer)
'#%paramz
(for-template
racket/unsafe/ops racket/fixnum racket/flonum
(only-in '#%kernel [apply k:apply] [reverse k:reverse])
"../internal-forms.rkt" scheme/base scheme/bool '#%paramz
(only-in racket/private/class-internal do-make-object)
(only-in syntax/location module-name-fixup)))
(import tc-expr^ tc-lambda^ tc-let^ tc-apply^)
(export tc-app-hetero^)
(define (tc/index expr)
(syntax-parse expr
[((~literal quote) i:number)
(values (tc-literal #'i) (syntax-e #'i))]
[_
(match (tc-expr expr)
[(and type (tc-result1: (Value: (? number? i))))
(values type i)]
[type (values type #f)])]))
(define (index-error i-val i-bound expr type expected name)
(define return (or expected (ret (Un))))
(cond
[(not (and (integer? i-val) (exact? i-val)))
(tc-error/expr #:stx expr #:return return "expected exact integer for ~a index, but got ~a" name i-val)]
[(< i-val 0)
(tc-error/expr #:stx expr #:return return "index ~a too small for ~a ~a" i-val name type)]
[(not (< i-val i-bound))
(tc-error/expr #:stx expr #:return return "index ~a too large for ~a ~a" i-val name type)]))
(define (valid-index? i bound)
(and (integer? i) (exact? i) (<= 0 i (sub1 bound))))
;; FIXME - Do something with paths in the case that a structure/vector is not mutable
(define (tc/hetero-ref i-e es-t vec-t expected name)
(define-values (i-t i-val) (tc/index i-e))
(define i-bound (length es-t))
(cond
[(valid-index? i-val i-bound)
(cond-check-below (ret (list-ref es-t i-val)) expected)]
[(not i-val)
(check-below i-t -Integer)
(cond-check-below (ret (apply Un es-t)) expected)]
[else
(index-error i-val i-bound i-e vec-t expected name)]))
(define (tc/hetero-set! i-e es-t val-e vec-t expected name)
(define-values (i-t i-val) (tc/index i-e))
(define i-bound (length es-t))
(cond
[(valid-index? i-val i-bound)
(tc-expr/check val-e (ret (list-ref es-t i-val)))
(cond-check-below (ret -Void) expected)]
[(not i-val)
(single-value val-e)
(tc-error/expr
#:stx i-e #:return (or expected (ret -Void))
"expected statically known index for ~a mutation, but got ~a"
name (match i-t [(tc-result1: t) t]))]
[else
(single-value val-e)
(index-error i-val i-bound i-e vec-t expected) name]))
(define (tc/app-hetero form expected)
(syntax-parse form
#:literals (#%plain-app
vector-ref unsafe-vector-ref unsafe-vector*-ref
vector-set! unsafe-vector-set! unsafe-vector*-set!
unsafe-struct-ref unsafe-struct*-ref
unsafe-struct-set! unsafe-struct*-set!
vector-immutable vector)
;; unsafe struct-ref
[(#%plain-app (~or unsafe-struct-ref unsafe-struct*-ref) struct:expr index:expr)
(match (single-value #'struct)
[(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))
(tc/hetero-ref #'index flds struct-t expected "struct")]
[s-ty #f])]
;; vector-ref on het vectors
[(#%plain-app (~or vector-ref unsafe-vector-ref unsafe-vector*-ref) vec:expr index:expr)
(match (single-value #'vec)
[(tc-result1: (and vec-t (app resolve (HeterogenousVector: es))))
(tc/hetero-ref #'index es vec-t expected "vector")]
[v-ty #f])]
;; unsafe struct-set!
[(#%plain-app (~or unsafe-struct-set! unsafe-struct*-set!) s:expr index:expr val:expr)
(match (single-value #'s)
[(tc-result1: (and struct-t (app resolve (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))
(tc/hetero-set! #'index flds #'val struct-t expected "struct")]
[s-ty #f])]
;; vector-set! on het vectors
[(#%plain-app (~or vector-set! unsafe-vector-set! unsafe-vector*-set!) v:expr index:expr val:expr)
(match (single-value #'v)
[(tc-result1: (and vec-t (app resolve (HeterogenousVector: es))))
(tc/hetero-set! #'index es #'val vec-t expected "vector")]
[v-ty #f])]
[(#%plain-app (~or vector-immutable vector) args:expr ...)
(match expected
[(tc-result1: (app resolve (Vector: t))) #f]
[(tc-result1: (app resolve (HeterogenousVector: ts)))
(unless (= (length ts) (length (syntax->list #'(args ...))))
(tc-error/expr "expected vector with ~a elements, but got ~a"
(length ts)
(make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...))))))
(for ([e (in-list (syntax->list #'(args ...)))]
[t (in-list ts)])
(tc-expr/check e (ret t)))
expected]
;; since vectors are mutable, if there is no expected type, we want to generalize the element type
[(or #f (tc-result1: _))
(ret (make-HeterogenousVector (map (lambda (x) (generalize (tc-expr/t x)))
(syntax->list #'(args ...)))))]
[_ (int-err "bad expected: ~a" expected)])]
[_ #f]))

View File

@ -6,6 +6,7 @@
provide-signature-elements
define-values/invoke-unit/infer link)
"signatures.rkt"
"tc-app/tc-app-hetero.rkt" "signatures.rkt"
"tc-if.rkt" "tc-lambda-unit.rkt" "tc-app.rkt"
"tc-let-unit.rkt" "tc-apply.rkt"
"tc-expr-unit.rkt" "check-subforms-unit.rkt")
@ -13,4 +14,5 @@
(provide-signature-elements tc-expr^ check-subforms^)
(define-values/invoke-unit/infer
(link tc-if@ tc-lambda@ tc-app@ tc-let@ tc-expr@ check-subforms@ tc-apply@))
(link tc-if@ tc-lambda@ tc-app@ tc-let@ tc-expr@ check-subforms@ tc-apply@
tc-app-hetero@))