fix case lambda (#620)
fix case-lambda checking when no expected type Not we will check each clause against the other applicable arrows that are derived during type synthesis for soundness sake. At a future date, if we instead compute a more complete "intersection" of these arrows and then check against that intersection, that would admit more correct programs.
This commit is contained in:
Andrew Kent
GitHub
parent
ffcf5afe92
commit
2ef852ae91
|
|
@ -2,7 +2,7 @@
|
|||
|
||||
(require "../utils/utils.rkt"
|
||||
racket/list syntax/parse syntax/stx
|
||||
racket/match syntax/private/id-table racket/set
|
||||
racket/match syntax/private/id-table
|
||||
racket/sequence
|
||||
(contract-req)
|
||||
(rep type-rep object-rep rep-utils)
|
||||
|
|
@ -41,6 +41,26 @@
|
|||
#:attr mapping (make-immutable-free-id-table)
|
||||
#:attr flag-mapping (make-immutable-free-id-table)))
|
||||
|
||||
;; positional: (listof identifier?)
|
||||
;; rest: id or #f
|
||||
;; syntax: syntax? - the improper syntax list of identifiers
|
||||
;; (i.e. (append positional (or id '())) but syntax)
|
||||
(struct formals (positional rest syntax) #:transparent)
|
||||
|
||||
(define (make-formals stx)
|
||||
(let loop ([s stx] [acc null])
|
||||
(cond
|
||||
[(pair? s) (loop (cdr s) (cons (car s) acc))]
|
||||
[(null? s) (formals (reverse acc) #f stx)]
|
||||
[(pair? (syntax-e s)) (loop (stx-cdr s) (cons (stx-car s) acc))]
|
||||
[(null? (syntax-e s)) (formals (reverse acc) #f stx)]
|
||||
[else (formals (reverse acc) s stx)])))
|
||||
|
||||
;; Currently no support for objects representing the rest argument
|
||||
(define (formals->objects f)
|
||||
(for/list ([i (in-list (formals-positional f))])
|
||||
(make-Path null i)))
|
||||
|
||||
(define (expected-str tys-len rst arg-len rest-id)
|
||||
(format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a"
|
||||
tys-len
|
||||
|
|
@ -52,7 +72,8 @@
|
|||
(if (= arg-len 1) "" "s")
|
||||
(if rest-id " and a rest arg" "")))
|
||||
|
||||
;; tc-lambda-body: Typechecks the body with the given args and names and returns the resulting arr?.
|
||||
;; tc-lambda-body: Typechecks the body with the given args and names
|
||||
;; and returns the resulting Arrow?.
|
||||
;; arg-names: The identifiers of the positional args
|
||||
;; arg-types: The types of the positional args
|
||||
;; rest-arg+type: Either #f for no rest argument or (cons rest-id rest-type)
|
||||
|
|
@ -154,14 +175,15 @@
|
|||
|
||||
;; typecheck a single lambda, with argument list and body
|
||||
;; drest-ty and drest-bound are both false or not false
|
||||
;; tc/lambda-clause/check: formals syntax listof[Type?] tc-result
|
||||
;; option[Type?] option[(cons Type? symbol)] -> arr?
|
||||
(define (tc/lambda-clause/check formals body arg-tys ret-ty rst)
|
||||
(check-clause (formals-positional formals) (formals-rest formals) body arg-tys rst ret-ty))
|
||||
(define/cond-contract (tc/lambda-clause/check f body arg-tys ret-ty rst)
|
||||
(-> formals? syntax? (listof Type?) (or/c tc-results/c #f) (or/c #f Type? RestDots?)
|
||||
Arrow?)
|
||||
(check-clause (formals-positional f) (formals-rest f) body arg-tys rst ret-ty))
|
||||
|
||||
;; typecheck a single opt-lambda clause with argument list and body
|
||||
;; tc/opt-lambda-clause: listof[identifier] syntax -> listof[arr?]
|
||||
(define (tc/opt-lambda-clause arg-list body aux-table flag-table)
|
||||
(define/cond-contract (tc/opt-lambda-clause arg-list body aux-table flag-table)
|
||||
(-> (listof identifier?) syntax? free-id-table? free-id-table?
|
||||
(listof Arrow?))
|
||||
;; arg-types: Listof[Type?]
|
||||
(define arg-types
|
||||
(for/list ([a (in-list arg-list)])
|
||||
|
|
@ -191,27 +213,27 @@
|
|||
(for/list ([arg-types (in-list new-arg-types)])
|
||||
(tc-lambda-body arg-list arg-types body)))
|
||||
|
||||
;; restrict-to-arity : arr? nat -> (or/c #f arr?)
|
||||
;; restrict-to-arity : Arrow? nat -> (or/c #f Arrow?)
|
||||
;; either produces a new arrow which is a subtype of arr with arity n,
|
||||
;; or #f is that is not possible
|
||||
(define (restrict-to-arity arr n)
|
||||
(match arr
|
||||
(define (restrict-Arrow-to-arity arrow n)
|
||||
(match arrow
|
||||
;; currently does not handle rest arguments
|
||||
[(Arrow: args #f '() _)
|
||||
#:when (= n (length args))
|
||||
arr]
|
||||
arrow]
|
||||
[_ #f]))
|
||||
|
||||
;; formals syntax -> listof[arr?]
|
||||
(define (tc/lambda-clause formals body)
|
||||
(define/cond-contract (tc/lambda-clause f body)
|
||||
(-> formals? syntax? (listof Arrow?))
|
||||
(define-values (aux-table flag-table)
|
||||
(syntax-parse body
|
||||
[(b:rebuild-let*) (values (attribute b.mapping) (attribute b.flag-mapping))]
|
||||
[_ (values (make-immutable-free-id-table)
|
||||
(make-immutable-free-id-table))]))
|
||||
|
||||
(define arg-list (formals-positional formals))
|
||||
(define rest-id (formals-rest formals))
|
||||
(define arg-list (formals-positional f))
|
||||
(define rest-id (formals-rest f))
|
||||
|
||||
(define eta-expanded?
|
||||
(syntax-parse body
|
||||
|
|
@ -251,11 +273,14 @@
|
|||
;; but we can't return anything but a (listof arr?) here
|
||||
;; FIXME: misses optimization opportunities in this code
|
||||
(match (tc-expr eta-expanded?)
|
||||
[(tc-result1: (Fun: arrs))
|
||||
(define possibles (for*/list ([arr (in-list arrs)]
|
||||
[restricted (in-value (restrict-to-arity arr (length arg-list)))]
|
||||
#:when restricted)
|
||||
restricted))
|
||||
[(tc-result1: (Fun: arrows))
|
||||
(define possibles
|
||||
(for*/list ([arrow (in-list arrows)]
|
||||
[restricted (in-value (restrict-Arrow-to-arity
|
||||
arrow
|
||||
(length arg-list)))]
|
||||
#:when restricted)
|
||||
restricted))
|
||||
(if (null? possibles)
|
||||
#f
|
||||
possibles)]
|
||||
|
|
@ -271,67 +296,174 @@
|
|||
body))])]))
|
||||
|
||||
|
||||
;; positional: (listof identifier?)
|
||||
;; rest: id or #f
|
||||
;; syntax: syntax? - the improper syntax list of identifiers
|
||||
;; (i.e. (append positional (or id '())) but syntax)
|
||||
(struct formals (positional rest syntax) #:transparent)
|
||||
|
||||
(define (make-formals stx)
|
||||
(let loop ([s stx] [acc null])
|
||||
(cond
|
||||
[(pair? s) (loop (cdr s) (cons (car s) acc))]
|
||||
[(null? s) (formals (reverse acc) #f stx)]
|
||||
[(pair? (syntax-e s)) (loop (stx-cdr s) (cons (stx-car s) acc))]
|
||||
[(null? (syntax-e s)) (formals (reverse acc) #f stx)]
|
||||
[else (formals (reverse acc) s stx)])))
|
||||
|
||||
;; Currently no support for objects representing the rest argument
|
||||
(define (formals->objects formals)
|
||||
(for/list ([i (in-list (formals-positional formals))])
|
||||
(make-Path null i)))
|
||||
|
||||
|
||||
;; An arity is a list (List Natural Boolean), with the number of positional
|
||||
;; arguments and whether there is a rest argument.
|
||||
;; case-arities
|
||||
;; a description of the supported arities for a case-lambda
|
||||
;; we have seen thus far while checking a case-lambda (recall
|
||||
;; that, for Function types and type checking purposes, all
|
||||
;; functions are case-lambdas)
|
||||
;; fixed-arities : (listof natural?)
|
||||
;; supported unique options so far for fixed argument counts,
|
||||
;; where for each element n, n < rest-pos, and the list should
|
||||
;; not contain duplicates
|
||||
;; (NOTE: once we encounter a rest arg at position rest-pos, we
|
||||
;; _remove_ arity counts that the rest encompasses (i.e.
|
||||
;; when n >= rest-pos) -- see example below of
|
||||
;; checking a case-lambda)
|
||||
;; rest-pos : (or/c natural? +inf.0)
|
||||
;; at what position would an argument be in the rest argument
|
||||
;;
|
||||
;; An arities-seen is a list (List (Listof Natural) (U Natural Infinity)),
|
||||
;; with the list of positional only arities seen and the least number of
|
||||
;; positional arguments on an arity with a rest argument seen.
|
||||
(define (formals->arity formals)
|
||||
(list
|
||||
(length (formals-positional formals))
|
||||
(and (formals-rest formals) #t)))
|
||||
;; We construct these specs _while_ we are parsing and checking
|
||||
;; case-lambdas to help us know if a clause is dead code,
|
||||
;; which Arrow types we should type check a particular case-lambda
|
||||
;; clause at, etc
|
||||
;;
|
||||
;; e.g. after each step of looking at the below case-lambda,
|
||||
;; we would have the following case-arity-spec (i.e. after
|
||||
;; using `add-to-arities` to update the case-arities):
|
||||
;; (case-lambda
|
||||
;; [(x) ...] ; ==> (case-arities '(1) +inf.0)
|
||||
;; [(x y) ...] ; ==> (case-arities '(1 2) +inf.0)
|
||||
;; [(x y z) ...] ; ==> (case-arities '(1 2 3) +inf.0)
|
||||
;; [(x y . rst) ...] ; ==> (case-arities '(1 2) 2)
|
||||
;; [l ...]) ; ==> (case-arities '() 0)
|
||||
(struct case-arities (fixed-arities rest-pos) #:transparent)
|
||||
|
||||
(define initial-arities-seen (list empty +inf.0))
|
||||
;; initially, we have seen no fixed arities and it is impossible for
|
||||
;; an argument to be in a rest argument from a previous clause
|
||||
(define initial-case-arities (case-arities '() +inf.0))
|
||||
|
||||
;; arities-seen-add : arities-seen? arity? -> arities-seen?
|
||||
;; Adds the arity to the arities encoded in the arity-seen.
|
||||
(define (arities-seen-add arities-seen arity)
|
||||
(match-define (list positionals min-rest) arities-seen)
|
||||
(match-define (list new-positional new-rest) arity)
|
||||
(define new-min-rest
|
||||
(if new-rest
|
||||
(min new-positional min-rest)
|
||||
min-rest))
|
||||
(list
|
||||
(filter (λ (n) (< n new-min-rest)) (cons new-positional positionals))
|
||||
new-min-rest))
|
||||
;; Adds the arity described by formals 'f' to the arities
|
||||
;; described by 'arities'. See above example near `case-arities`
|
||||
;; definition.
|
||||
(define/cond-contract (add-to-arities arities f)
|
||||
(-> case-arities? formals? case-arities?)
|
||||
(match* (arities f)
|
||||
[((case-arities fixed-arities rest-pos)
|
||||
(formals positional rst _))
|
||||
(define arity (length positional))
|
||||
(define new-rest-pos
|
||||
(if rst (min rest-pos arity) rest-pos))
|
||||
(define new-fixed-arities
|
||||
(cond
|
||||
[(eqv? +inf.0 new-rest-pos) (cons arity fixed-arities)]
|
||||
[else (for/list ([i (in-list (cons arity fixed-arities))]
|
||||
#:when (< i new-rest-pos))
|
||||
i)]))
|
||||
(case-arities new-fixed-arities new-rest-pos)]))
|
||||
|
||||
|
||||
;; arities-seen-seen-before? : arities-seen? arity? -> boolean?
|
||||
;; Determines if the arity would have been covered by an existing arity in the arity-seen
|
||||
(define (arities-seen-seen-before? arities-seen arity)
|
||||
(match-define (list positionals min-rest) arities-seen)
|
||||
(match-define (list new-positional new-rest) arity)
|
||||
(or (>= new-positional min-rest)
|
||||
(and (member new-positional positionals) (not new-rest))))
|
||||
;; Determines if the given formals would be
|
||||
;; covered by a supported arity in arities
|
||||
(define/cond-contract (in-arities? arities f-or-arrow)
|
||||
(-> case-arities? (or/c formals? Arrow?) boolean?)
|
||||
(match* (arities f-or-arrow)
|
||||
[((case-arities fixed-arities rest-pos)
|
||||
(or (formals (app length arity) rst _)
|
||||
(Arrow: (app length arity) rst _ _)))
|
||||
(or (>= arity rest-pos)
|
||||
(and (not rst) (memv arity fixed-arities) #t))]))
|
||||
|
||||
|
||||
|
||||
;; Returns a list of Arrows where the list contains all the valid Arrows
|
||||
;; from 'arrows' that could apply to a clause with formals 'f', given we
|
||||
;; have already seen case-arities 'seen'.
|
||||
(define/cond-contract (arrows-matching-seen+formals arrows seen f)
|
||||
(-> (listof Arrow?) case-arities? formals? (listof Arrow?))
|
||||
(match-define (formals formals-positionals formals-rest? _) f)
|
||||
(define pos-count (length formals-positionals))
|
||||
(for*/list ([arrow (in-list arrows)]
|
||||
[dom (in-value (Arrow-dom arrow))]
|
||||
[rst (in-value (Arrow-rst arrow))]
|
||||
#:unless (in-arities? seen arrow)
|
||||
#:when (cond
|
||||
[formals-rest?
|
||||
(or (Type? rst) (>= (length dom) pos-count))]
|
||||
[rst (<= (length dom) pos-count)]
|
||||
[else (= (length dom) pos-count)]))
|
||||
arrow))
|
||||
|
||||
|
||||
|
||||
;; For each clause (i.e. each elem in formals+bodies) we figure out which
|
||||
;; of the expected arrows it needs to type check at and which clauses
|
||||
;; are dead code.
|
||||
;;
|
||||
;; Returns the association list mapping clauses to the arrows they need
|
||||
;; to type check at.
|
||||
(define/cond-contract (create-to-check-list formals+bodies expected-arrows)
|
||||
(-> (listof (cons/c formals? syntax?))
|
||||
(listof Arrow?)
|
||||
(listof (cons/c (cons/c formals? syntax?)
|
||||
(listof Arrow?))))
|
||||
;; arities we have seen so far while checking case-lambda clauses
|
||||
(define seen initial-case-arities)
|
||||
(for*/list ([f+b (in-list formals+bodies)]
|
||||
[clause-formals (in-value (car f+b))]
|
||||
[clause-body (in-value (cdr f+b))])
|
||||
(define matching-arrows
|
||||
(arrows-matching-seen+formals expected-arrows
|
||||
seen
|
||||
clause-formals))
|
||||
(when (or (in-arities? seen clause-formals)
|
||||
(null? matching-arrows))
|
||||
(warn-unreachable clause-body)
|
||||
(add-dead-lambda-branch (formals-syntax clause-formals)))
|
||||
(set! seen (add-to-arities seen clause-formals))
|
||||
(cons f+b matching-arrows)))
|
||||
|
||||
|
||||
;; formals+bodies : formals and bodies to check
|
||||
;; expected-arrows : expected arrow types for the overall case-lambda
|
||||
;; orig-arrows : an association list recording if any formals and bodies
|
||||
;; have _already_ been checked at a certain Arrow type
|
||||
(define/cond-contract
|
||||
(check-mono-lambda/expected formals+bodies expected-arrows orig-arrows)
|
||||
(-> (listof (cons/c formals? syntax?))
|
||||
(listof Arrow?)
|
||||
(listof (cons/c (cons/c formals? syntax?)
|
||||
(listof Arrow?)))
|
||||
(listof Arrow?))
|
||||
|
||||
|
||||
(define to-check-list (create-to-check-list formals+bodies expected-arrows))
|
||||
|
||||
(cond
|
||||
[(and (andmap (λ (f+b+arrows) (null? (cdr f+b+arrows)))
|
||||
to-check-list)
|
||||
;; If the empty function is expected, then don't error out
|
||||
(not (null? expected-arrows)))
|
||||
;; TODO improve error message.
|
||||
(tc-error/expr #:return (list (-Arrow null -Bottom #:rest Univ))
|
||||
"Expected a function of type ~a, but got a function with the wrong arity"
|
||||
(make-Fun expected-arrows))]
|
||||
[else
|
||||
(for*/list ([(f+b arrows-to-check-against) (in-assoc to-check-list)]
|
||||
[clause-formals (in-value (car f+b))]
|
||||
[clause-body (in-value (cdr f+b))]
|
||||
[orig-arrows (in-value (assoc-ref orig-arrows f+b '()))]
|
||||
[arrow (in-list arrows-to-check-against)])
|
||||
;; NOTE!!! checking clauses against all applicable arrows is sound, but
|
||||
;; less complete than actually intersecting all of the arrow types and
|
||||
;; then checking clauses against the result
|
||||
(match arrow
|
||||
;; if this clause has an orig-arrow, we already checked it once and that
|
||||
;; was it's arrow type -- we don't want to check it again at the same arrow
|
||||
[_ #:when (member arrow orig-arrows) arrow]
|
||||
[(Arrow: dom rst '() rng)
|
||||
(define expected
|
||||
(values->tc-results rng (formals->objects clause-formals)))
|
||||
(tc/lambda-clause/check
|
||||
clause-formals clause-body dom expected rst)]))]))
|
||||
|
||||
|
||||
;; tc/mono-lambda : (listof (list formals syntax?)) (or/c #f tc-results) -> (listof arr?)
|
||||
;; typecheck a sequence of case-lambda clauses
|
||||
(define (tc/mono-lambda formals+bodies expected)
|
||||
(define expected-type
|
||||
(define/cond-contract (tc/mono-lambda formals+bodies expected)
|
||||
(-> (listof (cons/c formals? syntax?))
|
||||
(or/c #f tc-results/c)
|
||||
(listof Arrow?))
|
||||
(define expected-arrows
|
||||
(match expected
|
||||
[(tc-result1: t)
|
||||
(define resolved (resolve t))
|
||||
|
|
@ -339,78 +471,75 @@
|
|||
[(Fun: arrows)
|
||||
#:when (for/and ([arr (in-list arrows)])
|
||||
(null? (Arrow-kws arr)))
|
||||
resolved]
|
||||
arrows]
|
||||
[_ #f])]
|
||||
[_ #f]))
|
||||
|
||||
;; find-matching-arrs: (list/c natural? boolean?) arities-seen? -> (or #f Listof[arr?])
|
||||
;; Returns a list when we know the expected type, and the list contains all the valid arrs that the
|
||||
;; clause needs to type as.
|
||||
;; Returns false if there is not enough information in the expected type to propogate down to the
|
||||
;; clause
|
||||
(define (find-matching-arrs formal-arity arities-seen)
|
||||
(match-define (list formal-positionals formal-rest) formal-arity)
|
||||
(match expected-type
|
||||
[(Fun: arrows)
|
||||
#:when (for/and ([arr (in-list arrows)])
|
||||
(null? (Arrow-kws arr)))
|
||||
(for*/list ([a (in-list arrows)]
|
||||
[dom (in-value (Arrow-dom a))]
|
||||
[rst (in-value (Arrow-rst a))]
|
||||
#:unless (arities-seen-seen-before? arities-seen (list (length dom) rst))
|
||||
#:when (cond
|
||||
[formal-rest
|
||||
(or (Type? rst) (>= (length dom) formal-positionals))]
|
||||
[else ((if rst <= =) (length dom) formal-positionals)]))
|
||||
a)]
|
||||
[_ #f]))
|
||||
|
||||
|
||||
;; For each clause we figure out which arrs it needs to typecheck as,
|
||||
;; and also which clauses are dead code.
|
||||
(define-values (used-formals+bodies+arrs arities-seen)
|
||||
(for/fold ([formals+bodies+arrs* empty]
|
||||
[arities-seen initial-arities-seen])
|
||||
([formal+body (in-list formals+bodies)])
|
||||
(match formal+body
|
||||
[(list formal body)
|
||||
(define arity (formals->arity formal))
|
||||
(define matching-arrs (find-matching-arrs arity arities-seen))
|
||||
(values
|
||||
(cons
|
||||
(cond
|
||||
[(or (arities-seen-seen-before? arities-seen arity)
|
||||
(null? matching-arrs))
|
||||
(warn-unreachable body)
|
||||
(add-dead-lambda-branch (formals-syntax formal))
|
||||
(list formal body null)]
|
||||
[else (list formal body matching-arrs)])
|
||||
formals+bodies+arrs*)
|
||||
(arities-seen-add arities-seen arity))])))
|
||||
|
||||
(cond
|
||||
[(and (andmap (λ (f-b-arr) (empty? (third f-b-arr)))
|
||||
used-formals+bodies+arrs)
|
||||
;; If the empty function is expected, then don't error out
|
||||
(match expected-type
|
||||
[(Fun: (list)) #f]
|
||||
[_ #t]))
|
||||
;; TODO improve error message.
|
||||
(tc-error/expr #:return (list (-Arrow null -Bottom #:rest Univ))
|
||||
"Expected a function of type ~a, but got a function with the wrong arity"
|
||||
expected-type)]
|
||||
[expected-arrows
|
||||
;; if we have expected Arrows, proceed with checking against them
|
||||
(check-mono-lambda/expected formals+bodies expected-arrows '())]
|
||||
[else
|
||||
(apply append
|
||||
(for/list ([fb* (in-list used-formals+bodies+arrs)])
|
||||
(match-define (list f* b* t*) fb*)
|
||||
(cond
|
||||
[(not t*) (tc/lambda-clause f* b*)]
|
||||
[else
|
||||
(for/list ([arrow (in-list t*)])
|
||||
(match arrow
|
||||
[(Arrow: dom rst '() rng)
|
||||
(tc/lambda-clause/check
|
||||
f* b* dom (values->tc-results rng (formals->objects f*)) rst)]))])))]))
|
||||
;; if we don't have expected Arrows, we may need to re-check some
|
||||
;; of the bodies against Arrow types derived while checking the
|
||||
;; bodies for soundness sake, so first we will check their bodies
|
||||
;; with no expected type and then use check-mono-lambda/expected
|
||||
;; to perform any re-checking that is needed
|
||||
|
||||
;; arities we have seen so far while checking case-lambda clauses
|
||||
(define seen initial-case-arities)
|
||||
;; clauses that are unreachable because of the formals and ordering
|
||||
;; of the case-lambda clauses
|
||||
(define unreachable-clauses '())
|
||||
;; now we typecheck the bodies, recording their arrows (resulting-arrows)
|
||||
;; and the mapping of which formals+body produced which Arrow (already-checked),
|
||||
;; all while updating which arities we have seen and which, if any, case-lambda
|
||||
;; clauses are in fact unreachable
|
||||
(define-values (resulting-arrowss already-checked)
|
||||
(for*/lists (_1 _2)
|
||||
([f+b (in-list formals+bodies)]
|
||||
[f (in-value (car f+b))]
|
||||
[b (in-value (cdr f+b))]
|
||||
#:unless (let ([unreachable? (in-arities? seen f)])
|
||||
(when unreachable?
|
||||
(warn-unreachable b)
|
||||
(add-dead-lambda-branch (formals-syntax f))
|
||||
(set! unreachable-clauses
|
||||
(cons f+b unreachable-clauses)))
|
||||
unreachable?))
|
||||
(set! seen (add-to-arities seen f))
|
||||
(define resulting-arrow (tc/lambda-clause f b))
|
||||
(values resulting-arrow
|
||||
(cons f+b resulting-arrow))))
|
||||
|
||||
(define resulting-arrows (apply append resulting-arrowss))
|
||||
|
||||
;; if there was more than one live case-lambda clause, we may need
|
||||
;; to recheck some clauses against some of the arrows generated
|
||||
;; during checking for soundness sake,
|
||||
;; e.g.
|
||||
;; if we naively check (case-lambda
|
||||
;; [([x : Num] . [rst : Num *]) x]
|
||||
;; [[rst : Num *] 0]
|
||||
;; we get (case-> (-> Num Num * Num)
|
||||
;; (-> Num * Zero))
|
||||
;; which is unsound (i.e. we can upcast an intersection to either
|
||||
;; type, namely in this case to (-> Num * Zero), and then call
|
||||
;; it as the identity function on any number, which does not
|
||||
;; always produce the constant 0). In other words, our `case->`
|
||||
;; is really an UNORDERED intersection that we just don't work
|
||||
;; super hard to check function application with, it is not
|
||||
;; truly an ordered intersection, and thus if some function `f`
|
||||
;; has type `A ∧ B` it must be checked at both `A` and `B`.
|
||||
(cond
|
||||
[(> (- (length formals+bodies)
|
||||
(length unreachable-clauses))
|
||||
1)
|
||||
(check-mono-lambda/expected (remove* unreachable-clauses
|
||||
formals+bodies)
|
||||
resulting-arrows
|
||||
already-checked)]
|
||||
[else
|
||||
resulting-arrows])]))
|
||||
|
||||
(define (tc/dep-lambda formalss-stx bodies-stx dep-fun-ty)
|
||||
(parameterize ([with-refinements? #t])
|
||||
|
|
@ -450,8 +579,9 @@
|
|||
(tc/dep-lambda formalss bodies dep-fun-ty)]
|
||||
[_ (make-Fun
|
||||
(tc/mono-lambda
|
||||
(for/list ([f (in-syntax formalss)] [b (in-syntax bodies)])
|
||||
(list (make-formals f) b))
|
||||
(for/list ([f (in-syntax formalss)]
|
||||
[b (in-syntax bodies)])
|
||||
(cons (make-formals f) b))
|
||||
expected))]))
|
||||
|
||||
(define (plambda-prop stx)
|
||||
|
|
@ -459,13 +589,13 @@
|
|||
(and d (car (flatten d))))
|
||||
|
||||
(define (has-poly-annotation? form)
|
||||
(or (plambda-prop form) (cons? (lookup-scoped-tvar-layer form))))
|
||||
(or (plambda-prop form) (pair? (lookup-scoped-tvar-layer form))))
|
||||
|
||||
(define (remove-poly-layer tvarss)
|
||||
(filter cons? (map rest tvarss)))
|
||||
(filter pair? (map rest tvarss)))
|
||||
|
||||
(define (get-poly-layer tvarss)
|
||||
(map first tvarss))
|
||||
(map car tvarss))
|
||||
|
||||
(define (get-poly-tvarss form)
|
||||
(let ([plambda-tvars
|
||||
|
|
@ -506,7 +636,7 @@
|
|||
;; and make both annotated and declared type variables point to the
|
||||
;; same actual type variables (the fresh names)
|
||||
(define (extend-and-loop form ns formals bodies expected)
|
||||
(let loop ((tvarss tvarss))
|
||||
(let loop ([tvarss tvarss])
|
||||
(match tvarss
|
||||
[(list) (maybe-loop form formals bodies expected)]
|
||||
[(cons (list (list tvars ...) dotted) rest-tvarss)
|
||||
|
|
@ -522,8 +652,8 @@
|
|||
[(tc-result1: (app resolve (and t (Poly-fresh: ns fresh-ns expected*))))
|
||||
;; make sure the declared and annotated type variable arities match up
|
||||
;; with the expected type variable arity
|
||||
(for ((tvars (in-list tvarss)))
|
||||
(when (and (cons? tvars) (list? (first tvars)))
|
||||
(for ([tvars (in-list tvarss)])
|
||||
(when (and (pair? tvars) (list? (car tvars)))
|
||||
(tc-error
|
||||
"Expected a polymorphic function without ..., but given function/annotation had ..."))
|
||||
(unless (= (length tvars) (length fresh-ns))
|
||||
|
|
@ -540,11 +670,11 @@
|
|||
(tc-error "Expected ~a non-dotted type variables, but given ~a"
|
||||
(length ns) (length vars)))]
|
||||
[else
|
||||
(tc-error "Expected a polymorphic function with ..., but function/annotation had no ...")]))
|
||||
(tc-error "Expected a polymorphic function with ..., but function/annotation had no ...")]))
|
||||
(make-PolyDots (append ns (list dvar)) (extend-and-loop form ns formals bodies (ret expected*)))]
|
||||
[(tc-result1: (app resolve (and t (PolyRow-fresh: ns fresh-ns constraints expected*))))
|
||||
(for ((tvars (in-list tvarss)))
|
||||
(when (and (cons? tvars) (list? (first tvars)))
|
||||
(when (and (pair? tvars) (list? (car tvars)))
|
||||
(tc-error
|
||||
"Expected a polymorphic function without ..., but given function/annotation had ..."))
|
||||
(unless (= (length tvars) 1)
|
||||
|
|
@ -558,28 +688,30 @@
|
|||
formals bodies (ret expected*)))]
|
||||
[_
|
||||
(define lengths
|
||||
(for/set ((tvars (in-list tvarss)))
|
||||
(match tvars
|
||||
[(list (list vars ...) dotted)
|
||||
(length vars)]
|
||||
[(list vars ...)
|
||||
(length vars)])))
|
||||
(remove-duplicates
|
||||
(for/list ([tvars (in-list tvarss)])
|
||||
(match tvars
|
||||
[(list (list vars ...) dotted)
|
||||
(length vars)]
|
||||
[(list vars ...)
|
||||
(length vars)]))))
|
||||
(define dots
|
||||
(for/set ((tvars (in-list tvarss)))
|
||||
(match tvars
|
||||
[(list (list vars ...) dotted) #t]
|
||||
[(list vars ...) #f])))
|
||||
(unless (= 1 (set-count lengths))
|
||||
(tc-error "Expected annotations to have the same number of type variables, but given ~a"
|
||||
(set->list lengths)))
|
||||
(unless (= 1 (set-count dots))
|
||||
(tc-error "Expected annotations to all have ... or none to have ..., but given both"))
|
||||
(define dotted (and (set-first dots) (second (first tvarss))))
|
||||
(define ns (build-list (set-first lengths) (lambda (_) (gensym))))
|
||||
(remove-duplicates
|
||||
(for/list ([tvars (in-list tvarss)])
|
||||
(match tvars
|
||||
[(list (list vars ...) dotted) #t]
|
||||
[(list vars ...) #f]))))
|
||||
(unless (= 1 (length lengths))
|
||||
(tc-error "Expected annotations to have the same number of type variables, but given ~a"
|
||||
lengths))
|
||||
(unless (= 1 (length dots))
|
||||
(tc-error "Expected annotations to all have ... or none to have ..., but given both"))
|
||||
(define dotted (and (car dots) (second (car tvarss))))
|
||||
(define ns (build-list (car lengths) (lambda (_) (gensym))))
|
||||
(define results (extend-and-loop form ns formals bodies expected))
|
||||
(if dotted
|
||||
(make-PolyDots (append ns (list dotted)) results)
|
||||
(make-Poly #:original-names (first tvarss) ns results))]))
|
||||
(make-Poly #:original-names (car tvarss) ns results))]))
|
||||
|
||||
;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
|
||||
;; tc/lambda : syntax syntax-list syntax-list (or/c tc-results #f) -> tc-results
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#;
|
||||
(exn-pred 2)
|
||||
(exn-pred 3)
|
||||
#lang typed-scheme
|
||||
|
||||
(plambda: (a ...) ([z : String] . [w : Number *])
|
||||
|
|
|
|||
|
|
@ -12,11 +12,21 @@
|
|||
(apply (lambda: ([x : Number] . [y : Number *]) x)
|
||||
1 w))
|
||||
|
||||
(plambda: (a ...) ([z : String] . [w : Number *])
|
||||
(apply (case-lambda: (([x : Number] . [y : Number ... a]) x)
|
||||
(([x : String] [y : String] . [z : String *]) 0)
|
||||
([y : Number *] 0))
|
||||
w))
|
||||
|
||||
; the next lambda fails currently because we are incomplete in our
|
||||
; checking of case-lambdas. Specifically, since it is unannotated
|
||||
; we check each clause and get an arrow type:
|
||||
; (-> Number Number ... a Number)
|
||||
; (-> String String String * Zero)
|
||||
; (-> Number * Zero)
|
||||
; and we cannot _naively_ intersect these (i.e. just put them in a
|
||||
; case->), we would need to intersect them in a more complex way
|
||||
; that ensured soundness.
|
||||
;(plambda: (a ...) ([z : String] . [w : Number *])
|
||||
; (apply (case-lambda: (([x : Number] . [y : Number ... a]) x)
|
||||
; (([x : String] [y : String] . [z : String *]) 0)
|
||||
; ([y : Number *] 0))
|
||||
; w))
|
||||
|
||||
;; */*/poly
|
||||
(plambda: (a ...) ([z : String] . [w : Number *])
|
||||
|
|
|
|||
|
|
@ -4324,6 +4324,40 @@
|
|||
(void))
|
||||
#:ret (ret -Void #f #f)
|
||||
#:msg #rx"given: String"]
|
||||
[tc-err
|
||||
(let ()
|
||||
(ann ((tr:case-lambda (([x : Number] . [y : Number *]) x)
|
||||
(([x : String] [y : String] . [z : String *]) 0)
|
||||
([y : Number *] 0))
|
||||
42)
|
||||
Zero) ;; ==> actually returns 42
|
||||
(void))
|
||||
#:ret (ret -Void #f #f)
|
||||
#:msg #rx"type mismatch"]
|
||||
[tc-err
|
||||
(let ()
|
||||
(ann ((plambda: (a ...) ([z : String] . [w : Number *])
|
||||
(apply (case-lambda: (([x : Number] . [y : Number ... a]) x)
|
||||
(([x : String] [y : String] . [z : String *]) 0)
|
||||
([y : Number *] 0))
|
||||
w))
|
||||
"Hello" 42)
|
||||
Zero) ;; ==> actually returns 42
|
||||
(void))
|
||||
#:ret (ret -Void #f #f)
|
||||
#:msg #rx"type mismatch"]
|
||||
[tc-err
|
||||
(let ()
|
||||
(ann ((tr:case-lambda
|
||||
#:∀ (A)
|
||||
[([a : A])
|
||||
(ann a A)]
|
||||
[[rest : A *]
|
||||
(ann rest (Listof A))]) 1)
|
||||
(Listof One)) ;; ==> actually returns 1
|
||||
(void))
|
||||
#:ret (ret -Void #f #f)
|
||||
#:msg #rx"type mismatch"]
|
||||
)
|
||||
|
||||
(test-suite
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user