Check function kws against expected before tc-expr

This checks that the given lambda has the right keywords
wrt to the expected type. Doing this should avoid the bad
arity errors that result from the kw protocol encoding.

Closes PR 13898
This commit is contained in:
Asumu Takikawa 2014-05-19 22:04:30 -04:00
parent 9c05eff875
commit 2d81c9667c
6 changed files with 129 additions and 16 deletions

View File

@ -7,6 +7,20 @@
(for-label "colon.rkt"))
(provide (all-defined-out))
;; Data definitions
;; ----------------
;;
;; A LambdaKeywords is a
;; (lambda-kws (Listof Keyword) (Listof Keyword))
(struct lambda-kws (mand opt))
;; interp.
;; - the first list contains the mandatory keywords
;; - the second list contains the optional keywords
;;
;; The TR lambda form sets this as a syntax property on lambda expansions
;; to allow TR to check for missing keywords.
(define-literal-set colon #:for-label (:))
(define-splicing-syntax-class annotated-name
@ -240,7 +254,24 @@
(~and (mand:mand-formal ... opt:opt-formal ...)
(~bind [rest.form #'()])))
#:attr kw-property
(ormap values (append (attribute mand.kw) (attribute opt.kw)))
;; separate raw keywords into mandatory and optional and
;; put them in a struct for later use by tc-expr
(let ([kws (append (attribute mand.kw)
(attribute opt.kw))]
[opt?s (append (attribute mand.default)
(attribute opt.default))])
(define-values (mand-kws opt-kws)
(for/fold ([mand-kws '()]
[opt-kws '()])
([kw (in-list kws)]
[opt? (in-list opt?s)]
#:when kw)
(if opt?
(values mand-kws (cons (syntax-e kw) opt-kws))
(values (cons (syntax-e kw) mand-kws) opt-kws))))
(and (or (not (null? mand-kws))
(not (null? opt-kws)))
(lambda-kws mand-kws opt-kws)))
#:attr opt-property
(list (length (attribute mand)) (length (attribute opt)))
#:attr erased

View File

@ -57,7 +57,7 @@
(lookup-type/lexical orig env
#:fail (lambda (i) (lookup-fail i) #f)))
(define t (if pre-t
(kw-convert pre-t)
(kw-convert pre-t #f)
Err))
(register-type i t)
t)]

View File

@ -175,12 +175,14 @@
(tc/send #'find-app #'rcvr #'meth #'(args ...) expected)]
;; kw function def
;; TODO simplify this case
[(~and (let-values ([(f) fun]) . body) _:kw-lambda^)
[(~and (let-values ([(f) fun]) . body) kw:kw-lambda^)
#:when expected
(match expected
[(tc-result1: (and f (or (Function: _)
(Poly: _ (Function: _)))))
(tc-expr/check/type #'fun (kw-convert f #:split #t))
(define actual-kws (attribute kw.value))
(check-kw-arity actual-kws f)
(tc-expr/check/type #'fun (kw-convert f actual-kws #:split #t))
(ret f -true-filter)]
[(or (tc-results: _) (tc-any-results: _))
(tc-expr/check form #f)])]

View File

@ -2,8 +2,10 @@
(require "abbrev.rkt" "../rep/type-rep.rkt"
"../utils/tc-utils.rkt"
"../base-env/annotate-classes.rkt"
"tc-result.rkt"
racket/list racket/set racket/dict racket/match
racket/format racket/string
syntax/parse)
;; convert : [Listof Keyword] [Listof Type] [Listof Type] [Option Type]
@ -128,23 +130,50 @@
(dict-set d prefix (arg-diff prefix e))
(dict-set d e empty))))
(define (inner-kw-convert arrs split?)
;; handle-extra-or-missing-kws : (Listof Keyword) LambdaKeywords
;; -> (Listof Keyword)
;; Remove keywords in the given list that aren't in the actual lambda
;; keywords list. This allows the typechecker to check some branches of the
;; type that match the actual kws. Add extra actual mandatory keywords
;; with Bottom type.
(define (handle-extra-or-missing-kws kws actual-kws)
(match-define (lambda-kws actual-mands actual-opts) actual-kws)
(define expected-mands (map Keyword-kw (filter Keyword-required? kws)))
(define missing-removed
(filter
(λ (kw) (or (member (Keyword-kw kw) actual-mands)
(member (Keyword-kw kw) actual-opts)))
kws))
(append missing-removed
(for/list ([kw (in-list (set-subtract actual-mands expected-mands))])
(make-Keyword kw -Bottom #t))))
;; inner-kw-convert : (Listof arr) (Option LambdaKeywords) Boolean -> Type
;; Helper function that converts each arr to a Function type and then
;; merges them into a single Function type.
(define (inner-kw-convert arrs actual-kws split?)
(define table (find-prefixes arrs))
(define fns
(for/set ([(k v) (in-dict table)])
(match k
[(arr: mand rng rest drest kws)
(convert kws mand v rng rest drest split?)])))
(define kws* (if actual-kws
(handle-extra-or-missing-kws kws actual-kws)
kws))
(convert kws* mand v rng rest drest split?)])))
(apply cl->* (set->list fns)))
(define (kw-convert ft #:split [split? #f])
(match ft
[(Function: arrs)
(inner-kw-convert arrs split?)]
[(Poly-names: names f)
(make-Poly names (kw-convert f #:split split?))]
[(PolyDots-names: names f)
(make-PolyDots names (kw-convert f #:split split?))]))
;; kw-convert : Type (Option LambdaKeywords) [Boolean] -> Type
;; Given an ordinary function type, convert it to a type that matches the keyword
;; function protocol
(define (kw-convert ft actual-kws #:split [split? #f])
(match ft
[(Function: arrs)
(inner-kw-convert arrs actual-kws split?)]
[(Poly-names: names f)
(make-Poly names (kw-convert f actual-kws #:split split?))]
[(PolyDots-names: names f)
(make-PolyDots names (kw-convert f actual-kws #:split split?))]))
;; kw-unconvert : Type (Listof Syntax) (Listof Keyword) (Listof Keyword) -> Type
;; Given a type for a core keyword function, unconvert it to a
@ -219,6 +248,42 @@
[else (int-err "unsupported arrs in keyword function type")])]
[_ (int-err "unsupported keyword function type")]))
;; check-kw-arity : LambdaKeywords Type -> Void
;;
;; Check if the TR lambda property listing the keywords matches up with
;; the type that we've given. Allows for better error messages than just
;; relying on tc-expr. Return #f if the function shouldn't be checked.
(define (check-kw-arity kw-prop f-type)
(match-define (lambda-kws actual-mands actual-opts) kw-prop)
(define arrs
(match f-type
[(AnyPoly-names: _ _ (Function: arrs)) arrs]))
(for/and ([arr (in-list arrs)])
(match-define (arr: _ _ _ _ kws) arr)
(define-values (mand-kw-types opt-kw-types) (partition-kws kws))
(define mand-kws (map Keyword-kw mand-kw-types))
(define opt-kws (map Keyword-kw opt-kw-types))
(define missing-kws (set-union (set-subtract mand-kws actual-mands)
(set-subtract opt-kws actual-opts)))
;; extra optional keywords are okay
(define extra-kws (set-subtract actual-mands mand-kws))
(unless (set-empty? missing-kws)
(tc-error/fields
#:delayed? #t
"type mismatch"
#:more "function is missing keyword arguments"
"missing keywords"
(string-join (map ~a missing-kws))
"expected type" f-type))
(unless (set-empty? extra-kws)
(tc-error/fields
#:delayed? #t
"type mismatch"
#:more "function has too many mandatory keyword arguments"
"extra keywords"
(string-join (map ~a extra-kws))
"expected type" f-type))))
;; compute-kws : (Listof Keyword) (Listof Keyword) (Listof Type)
;; -> (Listof make-Keyword)
;; Computes the keyword types for an arr in kw-unconvert
@ -325,4 +390,5 @@
(define (partition-kws kws)
(partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws))
(provide kw-convert kw-unconvert opt-convert opt-unconvert partition-kws)
(provide kw-convert kw-unconvert opt-convert opt-unconvert partition-kws
check-kw-arity)

View File

@ -11,7 +11,7 @@
(define-syntax-rule (t arg expected)
(begin
(test-equal? (format "~a" '(arg expected))
(kw-convert arg)
(kw-convert arg #f)
expected)))
(define (extract-arrs t)

View File

@ -3066,6 +3066,20 @@
#:ret (ret (-lst* (-lst* -String)))
#:expected (ret (-lst* (-lst* -String)))]
;; PR 13898
[tc-err
(let ()
(: f ([#:foo Any] -> (Option Natural)))
(tr:define (f #:foo x) 0)
(error "dummy"))
#:msg #rx"missing keyword arguments.*#:foo"]
[tc-err
(let ()
(: f (-> [#:foo Any] Zero))
(tr:define (f #:foo [foo 'foo] #:bar bar) 0)
(error "dummy"))
#:msg #rx"too many mandatory keyword arguments.*#:foo"]
)
(test-suite