Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP: more complete function application for case-> #757

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
144 changes: 47 additions & 97 deletions typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -664,22 +664,10 @@
(define abs-cases ; used both for abs and magnitude
(list
;; abs is not the identity on negative zeros.
((Un -Zero -PosReal) . -> . (Un -Zero -PosReal) : -true-propset : (-arg-path 0))
;; but we know that we at least get *some* zero, and that it preserves exactness
(map unop (list -FlonumZero -SingleFlonumZero -RealZero))
;; abs may not be closed on fixnums. (abs min-fixnum) is not a fixnum
((Un -PosInt -NegInt) . -> . -PosInt)
(-Int . -> . -Nat)
((Un -PosRat -NegRat) . -> . -PosRat)
(-Rat . -> . -NonNegRat)
((Un -PosFlonum -NegFlonum) . -> . -PosFlonum)
(-Flonum . -> . -NonNegFlonum)
((Un -PosSingleFlonum -NegSingleFlonum) . -> . -PosSingleFlonum)
(-SingleFlonum . -> . -NonNegSingleFlonum)
((Un -PosInexactReal -NegInexactReal) . -> . -PosInexactReal)
(-InexactReal . -> . -NonNegInexactReal)
((Un -PosReal -NegReal) . -> . -PosReal)
(-Real . -> . -NonNegReal)))
(-> (Un -Zero -PosReal) (Un -Zero -PosReal) : -true-propset : (-arg-path 0))
(map unop (list -RealZero -Int -Rat -Flonum -SingleFlonum))
(-> (Un -PosReal -NegReal) -PosReal)
(-> -Real -NonNegReal)))

;Check to ensure we fail fast if the flonum bindings change
(define-namespace-anchor anchor)
Expand Down Expand Up @@ -1031,65 +1019,44 @@
(commutative-case -InexactComplex (Un -InexactComplex -InexactReal -PosRat -NegRat) -InexactComplex)
(varop N))]
[+ (from-cases
(-> -Zero)
(-> N N : -true-propset : (-arg-path 0))
(binop -Zero)
(-> N -Zero N : -true-propset : (-arg-path 0))
(-> -Zero N N : -true-propset : (-arg-path 1))
(-> -PosByte -PosByte -PosIndex)
(-> -Byte -Byte -Index)
(-> -PosByte -PosByte -PosByte -PosIndex)
(-> -Byte -Byte -Byte -Index)
(commutative-binop -PosIndex -Index -PosFixnum)
(-> -PosIndex -Index -Index -PosFixnum)
(-> -Index -PosIndex -Index -PosFixnum)
(-> -Index -Index -PosIndex -PosFixnum)
(-> -Index -Index -NonNegFixnum)
(-> -Index -Index -Index -NonNegFixnum)
(commutative-binop -NegFixnum -One -NonPosFixnum)
(commutative-binop -NonPosFixnum -NonNegFixnum -Fixnum)
(commutative-case -PosInt -Nat -PosInt)
(commutative-case -NegInt -NonPosInt -NegInt)
(map varop (list -Nat -NonPosInt -Int))
(commutative-case -PosRat -NonNegRat -PosRat)
(commutative-case -NegRat -NonPosRat -NegRat)
(map varop (list -NonNegRat -NonPosRat -Rat))
;; flonum + real -> flonum
(commutative-case -PosFlonum -NonNegReal -PosFlonum)
(commutative-case -PosReal -NonNegFlonum -PosFlonum)
(commutative-case -NegFlonum -NonPosReal -NegFlonum)
(commutative-case -NegReal -NonPosFlonum -NegFlonum)
(commutative-case -NonNegFlonum -NonNegReal -NonNegFlonum)
(commutative-case -NonPosFlonum -NonPosReal -NonPosFlonum)
(commutative-case -Flonum -Real -Flonum)
(varop-1+ -Flonum)
;; single-flonum + rat -> single-flonum
(commutative-case -PosSingleFlonum (Un -NonNegRat -NonNegSingleFlonum) -PosSingleFlonum)
(commutative-case (Un -PosRat -PosSingleFlonum) -NonNegSingleFlonum -PosSingleFlonum)
(commutative-case -NegSingleFlonum (Un -NonPosRat -NonPosSingleFlonum) -NegSingleFlonum)
(commutative-case (Un -NegRat -NegSingleFlonum) -NonPosSingleFlonum -NegSingleFlonum)
(commutative-case -NonNegSingleFlonum (Un -NonNegRat -NonNegSingleFlonum) -NonNegSingleFlonum)
(commutative-case -NonPosSingleFlonum (Un -NonPosRat -NonPosSingleFlonum) -NonPosSingleFlonum)
(commutative-case -SingleFlonum (Un -Rat -SingleFlonum) -SingleFlonum)
(varop-1+ -SingleFlonum)
;; inexact-real + real -> inexact-real
(commutative-case -PosInexactReal -NonNegReal -PosInexactReal)
(commutative-case -PosReal -NonNegInexactReal -PosInexactReal)
(commutative-case -NegInexactReal -NonPosReal -NegInexactReal)
(commutative-case -NegReal -NonPosInexactReal -NegInexactReal)
(commutative-case -NonNegInexactReal -NonNegReal -NonNegInexactReal)
(commutative-case -NonPosInexactReal -NonPosReal -NonPosInexactReal)
(commutative-case -InexactReal -Real -InexactReal)
;; real
(commutative-case -PosReal -NonNegReal -PosReal)
(commutative-case -NegReal -NonPosReal -NegReal)
(map varop (list -NonNegReal -NonPosReal -Real -ExactNumber))
;; complex
(commutative-case -FloatComplex N -FloatComplex)
(commutative-case -Flonum -InexactComplex -FloatComplex)
(commutative-case -SingleFlonumComplex (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex)
(commutative-case -InexactComplex (Un -Rat -InexactReal -InexactComplex) -InexactComplex)
(varop N))]
(-> -NegFixnum -One -NonPosFixnum)
(-> -One -NegFixnum -NonPosFixnum)
(-> -NonPosFixnum -NonNegFixnum -Fixnum)
(-> -NonNegFixnum -NonPosFixnum -Fixnum)
(-> -Flonum -Real -Flonum)
(-> -Real -Flonum -Flonum)
(-> -SingleFlonum (Un -Rat -SingleFlonum) -SingleFlonum)
(-> (Un -Rat -SingleFlonum) -SingleFlonum -SingleFlonum)
(-> -InexactReal -Real -InexactReal)
(-> -Real -InexactReal -InexactReal)
(-> -FloatComplex N -FloatComplex)
(-> N -FloatComplex -FloatComplex)
(-> -Flonum -InexactComplex -FloatComplex)
(-> -InexactComplex -Flonum -FloatComplex)
(-> -SingleFlonumComplex (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex)
(-> (Un -Rat -SingleFlonum -SingleFlonumComplex) -SingleFlonumComplex -SingleFlonumComplex)
(-> -InexactComplex (Un -Rat -InexactReal -InexactComplex) -InexactComplex)
(-> (Un -Rat -InexactReal -InexactComplex) -InexactComplex -InexactComplex)
(-> -PosReal -NonNegReal -PosReal)
(-> -NonNegReal -PosReal -PosReal)
(-> -PosReal -NonNegReal -NonNegReal -PosReal)
(-> -NonNegReal -PosReal -NonNegReal -PosReal)
(-> -NonNegReal -NonNegReal -PosReal -PosReal)
(-> -NegReal -NonPosReal -NegReal)
(-> -NonPosReal -NegReal -NegReal)
(-> -NegReal -NonPosReal -NonPosReal -NegReal)
(-> -NonPosReal -NegReal -NonPosReal -NegReal)
(-> -NonPosReal -NonPosReal -NegReal -NegReal)
(map varop (list -Zero -Nat -Int -PosReal -NegReal
-NonNegReal -NonPosReal -Real -ExactNumber N))
(map varop-1+ (list -Flonum -SingleFlonum)))]

[- (from-cases
(binop -Zero)
Expand Down Expand Up @@ -1268,45 +1235,28 @@

[add1 (from-cases
(-> -Zero -One)
(-> -One -PosByte)
(-> -Byte -PosIndex)
(-> -Index -PosFixnum)
(-> -NegFixnum -NonPosFixnum)
(-> -One -Byte)
(-> -Byte -Index)
(-> -Index -Fixnum)
(-> -NonPosFixnum -Fixnum)
(-> -Nat -Pos)
(-> -NegInt -NonPosInt)
(unop -Int)
(-> -NonNegRat -PosRat)
(unop -Rat)
(-> -NonNegFlonum -PosFlonum)
(unop -Flonum)
(-> -NonNegSingleFlonum -PosSingleFlonum)
(unop -SingleFlonum)
(-> -NonNegInexactReal -PosInexactReal)
(unop -InexactReal)
(-> -NonNegReal -PosReal)
(map unop (list -Real -FloatComplex -SingleFlonumComplex -InexactComplex N)))]
(-> -InexactReal -InexactReal)
(map unop (list -Int -Rat -Flonum -SingleFlonum
-FloatComplex -SingleFlonumComplex
-Real -InexactReal -InexactComplex N)))]

[sub1 (from-cases
(-> -One -Zero)
(-> -PosByte -Byte)
(-> -PosIndex -Index)
(-> -Index -Fixnum)
(-> -PosFixnum -NonNegFixnum)
(-> -NonNegFixnum -Fixnum)
(-> -Pos -Nat)
(-> -NonPosInt -NegInt)
(unop -Int)
(-> -NonPosRat -NegRat)
(unop -Rat)
(-> -NonPosFlonum -NegFlonum)
(unop -Flonum)
(-> -NonPosSingleFlonum -NegSingleFlonum)
(unop -SingleFlonum)
(-> -NonPosInexactReal -NegInexactReal)
(unop -InexactReal)
(-> -NonPosReal -NegReal)
(map unop (list -Real -FloatComplex -SingleFlonumComplex -InexactComplex N)))]
(map unop (list -Int -Rat -Flonum -SingleFlonum
-Real -InexactReal -FloatComplex
-SingleFlonumComplex -InexactComplex
N)))]

[quotient
(from-cases
Expand Down Expand Up @@ -1498,7 +1448,7 @@
;; no positive / negative cases, possible underflow
(-NonNegReal . -> . -NonNegSingleFlonum)
(-NonPosReal . -> . -NonPosSingleFlonum)
(-Real . -> . -SingleFlonumZero))]
(-Real . -> . -SingleFlonum))]
[real->double-flonum
(from-cases (map unop all-flonum-types)
(-SingleFlonumPosZero . -> . -FlonumPosZero)
Expand Down
2 changes: 1 addition & 1 deletion typed-racket-lib/typed-racket/env/lexical-env.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@
[lookup-obj-type/lexical ((Object?) (env? #:fail (or/c #f Type? (-> any/c (or/c Type? #f))))
. ->* .
(or/c Type? #f))]
[lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))])
[lookup-alias/lexical ((identifier?) (env?) . ->* . OptObject?)])

;; used at the top level
(define (add-props-to-current-lexical! ps)
Expand Down
49 changes: 40 additions & 9 deletions typed-racket-lib/typed-racket/infer/infer-unit.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -420,6 +420,19 @@
(cgen context s t)
(cgen/seq context t-seq s-seq)))]))

(define/cond-contract (cgen/arrow-pair/arrow context s-arr-pair t-arr)
(context? (cons/c Type? Values?) Arrow? . -> . (or/c #f cset?))
(match* (s-arr-pair t-arr)
[((cons dom1 cdom1)
(Arrow: dom2 rst2 kws2 cdom2))
(and
(null? kws2)
(% cset-meet
(cgen context cdom1 cdom2)
(cgen context
(positional-domain->Tuple dom2 rst2)
dom1)))]))

(define/cond-contract (cgen/flds context flds-s flds-t)
(context? (listof fld?) (listof fld?) . -> . (or/c #f cset?))
(% cset-meet*
Expand Down Expand Up @@ -812,17 +825,35 @@
(% cset-meet (cg in2 in1) (cg out1 out2))]
[((Fun: s-arr)
(Fun: t-arr))
(define s-arrow-combinations
(let loop ([arrows s-arr]
[acc #f])
(match arrows
['() (if acc (list acc) '())]
[(cons a rst)
(define a* (if acc
(intersect-arrows a acc)
(match a
[(Arrow: dom rst kws cdom)
(and (for/and ([kw (in-list kws)])
(not (Keyword-required? kw)))
(cons (positional-domain->Tuple dom rst)
cdom))])))
(if a*
(append (loop rst a*)
(loop rst acc))
(loop rst acc))])))
(% cset-meet*
(for/list/fail
([t-arr (in-list t-arr)])
;; for each element of t-arr, we need to get at least one element of s-arr that works
(let ([results (for*/list ([s-arr (in-list s-arr)]
[v (in-value (cgen/arrow context s-arr t-arr))]
#:when v)
v)])
;; ensure that something produces a constraint set
(and (not (null? results))
(cset-join results)))))]
([t-arr (in-list t-arr)])
;; for each element of t-arr, we need to get at least one element of s-arr that works
(let ([results (for*/list ([s-arr-pair (in-list s-arrow-combinations)]
[v (in-value (cgen/arrow-pair/arrow context s-arr-pair t-arr))]
#:when v)
v)])
;; ensure that something produces a constraint set
(and (not (null? results))
(cset-join results)))))]
[(_ _)
;; nothing worked, and we fail
#f]))]))
Expand Down
3 changes: 3 additions & 0 deletions typed-racket-lib/typed-racket/infer/intersect.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -236,3 +236,6 @@
[else (internal-restrict t1 t2 '() obj)]))

(define internal-restrict (intersect-types #f))



11 changes: 10 additions & 1 deletion typed-racket-lib/typed-racket/rep/object-rep.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@
obj-seq-next
scale-obj
uninterpreted-PE?
intersect-objects
(rename-out [make-LExp* make-LExp]
[make-LExp raw-make-LExp])
(all-from-out "fme-utils.rkt"))
Expand Down Expand Up @@ -395,4 +396,12 @@
(define (add-path-to-lexp p l)
(match l
[(LExp: const terms)
(make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
(make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))


(define (intersect-objects o1 o2)
(match* (o1 o2)
[(o o) o]
[((Empty:) _) o2]
[(_ (Empty:)) o1]
[(_ _) o1]))
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@
[stx:exn-body^
(set! body-results (tc-expr/check #'stx expected))])
(define handler-results (get-handler-results))
(merge-tc-results (cons body-results handler-results)))
(union-tc-results (cons body-results handler-results)))

;; typecheck the expansion of a with-handlers form
;; syntax -> void
Expand Down
9 changes: 6 additions & 3 deletions typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,14 @@
(provide/cond-contract
[tc/funapp1
((syntax? stx-list? Arrow? (listof tc-results/c) (or/c #f tc-results/c))
(#:check boolean?)
(#:check boolean? #:tooltip? boolean?)
. ->* . full-tc-results/c)])
(define (tc/funapp1 f-stx args-stx ftype0 arg-ress expected #:check [check? #t])
(define (tc/funapp1 f-stx args-stx ftype0 arg-ress expected
#:check [check? #t]
#:tooltip? [tooltip? #t])
;; update tooltip-table with inferred function type
(add-typeof-expr f-stx (ret (make-Fun (list ftype0))))
(when tooltip?
(add-typeof-expr f-stx (ret (make-Fun (list ftype0)))))
(match* (ftype0 arg-ress)
;; we check that all kw args are optional
[((Arrow: dom rst (list (Keyword: _ _ #f) ...) rng)
Expand Down
48 changes: 34 additions & 14 deletions typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
(utils tc-utils identifier)
(env tvar-env lexical-env)
(for-syntax syntax/parse racket/base)
(types utils subtype resolve abbrev
(types utils subtype resolve abbrev type-table
substitute classes prop-ops)
(typecheck tc-metafunctions tc-app-helper tc-subst tc-envops
check-below)
Expand Down Expand Up @@ -115,17 +115,14 @@
;; check there are no RestDots
#:when (not (for/or ([a (in-list arrows)])
(RestDots? (Arrow-rst a))))
(cond
;; find the first function where the argument types match
[(ormap (match-lambda
[(and a (Arrow: dom rst _ _))
(and (subtypes/varargs argtys dom rst) a)])
arrows)
=> (λ (a)
;; then typecheck here -- we call the separate function so that we get
;; the appropriate props/objects
(tc/funapp1 f-stx args-stx a args-res expected #:check #f))]
[else
(define applicable-arrows
(filter (match-lambda
[(Arrow: dom rst _ _)
(subtypes/varargs argtys dom rst)])
arrows))

(match applicable-arrows
[(list)
;; if nothing matched, error
(match arrows
[(list (Arrow: doms rsts _ rngs) ...)
Expand All @@ -135,7 +132,30 @@
#:msg-thunk (lambda (dom)
(string-append
"No function domains matched in function application:\n"
dom)))])])]
dom)))])]
[(list a) (tc/funapp1 f-stx args-stx a args-res expected #:check #f)]
[_
;; call a separate function so that we get
;; the appropriate props/objects
(define app-result
(intersect-tc-results
(for/list ([a (in-list applicable-arrows)])
(tc/funapp1 f-stx args-stx a args-res expected
#:check #f
#:tooltip? #f))))
(define applicable-domain
;; gather and intersect applicable domains to report to user
;; generally what class of inputs produces the resulting output
(for/fold ([domtys (build-list (length argtys) (λ (_) Univ))])
([a (in-list applicable-arrows)])
(match a
[(Arrow: dom rst _ _) (for/list ([domty (in-list domtys)]
[idx (in-naturals)])
(intersect domty (dom+rst-ref dom rst idx)))])))
(add-typeof-expr
f-stx
(ret (make-Fun (list (-Arrow applicable-domain (tc-results->values app-result))))))
app-result])]
;; any kind of dotted polymorphic function without mandatory keyword args
[(PolyDots: (list fixed-vars ... dotted-var)
(Fun: arrows))
Expand Down Expand Up @@ -308,7 +328,7 @@
;; a union of functions can be applied if we can apply all of the elements
[(Union: (? Bottom?) ts) #:when (for/and ([t (in-list ts)])
(subtype t top-func))
(merge-tc-results
(union-tc-results
(for/list ([fty (in-list ts)])
(tc/funapp f-stx args-stx fty args-res expected)))]
;; bottom or error type is a perfectly good fcn type
Expand Down
Loading