Use abbreviations for filters.
This commit is contained in:
parent
09ff5cafd4
commit
a76d57fa88
|
@ -491,12 +491,12 @@
|
||||||
(-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) -top))
|
(-> -FlonumZero -Flonum B : (-FS (-filter -PosFlonum 1) -top))
|
||||||
(-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) -top))
|
(-> -Flonum -FlonumZero B : (-FS (-filter -NegFlonum 0) -top))
|
||||||
(-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
|
(-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
|
||||||
(-> -Flonum -PosFlonum B : (-FS -top -top))
|
(-> -Flonum -PosFlonum B)
|
||||||
(-> -NonNegFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
|
(-> -NonNegFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
|
||||||
(-> -Flonum -NonNegFlonum B : (-FS -top -top))
|
(-> -Flonum -NonNegFlonum B)
|
||||||
(-> -NegFlonum -Flonum B : (-FS -top -top))
|
(-> -NegFlonum -Flonum B)
|
||||||
(-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top))
|
(-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top))
|
||||||
(-> -NonPosFlonum -Flonum B : (-FS -top -top))
|
(-> -NonPosFlonum -Flonum B)
|
||||||
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NegFlonum 0) -top))
|
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NegFlonum 0) -top))
|
||||||
(comp -Flonum))))
|
(comp -Flonum))))
|
||||||
(define fl>-type
|
(define fl>-type
|
||||||
|
@ -504,14 +504,14 @@
|
||||||
(from-cases
|
(from-cases
|
||||||
(-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) -top))
|
(-> -FlonumZero -Flonum B : (-FS (-filter -NegFlonum 1) -top))
|
||||||
(-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) -top))
|
(-> -Flonum -FlonumZero B : (-FS (-filter -PosFlonum 0) -top))
|
||||||
(-> -PosFlonum -Flonum B : (-FS -top -top))
|
(-> -PosFlonum -Flonum B)
|
||||||
(-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top))
|
(-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top))
|
||||||
(-> -NonNegFlonum -Flonum B : (-FS -top -top))
|
(-> -NonNegFlonum -Flonum B)
|
||||||
(-> -Flonum -NonNegFlonum B : (-FS (-filter -PosFlonum 0) -top))
|
(-> -Flonum -NonNegFlonum B : (-FS (-filter -PosFlonum 0) -top))
|
||||||
(-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
|
(-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
|
||||||
(-> -Flonum -NegFlonum B : (-FS -top -top))
|
(-> -Flonum -NegFlonum B)
|
||||||
(-> -NonPosFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
|
(-> -NonPosFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
|
||||||
(-> -Flonum -NonPosFlonum B : (-FS -top -top))
|
(-> -Flonum -NonPosFlonum B)
|
||||||
(comp -Flonum))))
|
(comp -Flonum))))
|
||||||
(define fl<=-type
|
(define fl<=-type
|
||||||
(lambda ()
|
(lambda ()
|
||||||
|
@ -519,12 +519,12 @@
|
||||||
(-> -FlonumZero -Flonum B : (-FS (-filter -NonNegFlonum 1) -top))
|
(-> -FlonumZero -Flonum B : (-FS (-filter -NonNegFlonum 1) -top))
|
||||||
(-> -Flonum -FlonumZero B : (-FS (-filter -NonPosFlonum 0) -top))
|
(-> -Flonum -FlonumZero B : (-FS (-filter -NonPosFlonum 0) -top))
|
||||||
(-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
|
(-> -PosFlonum -Flonum B : (-FS (-filter -PosFlonum 1) -top))
|
||||||
(-> -Flonum -PosFlonum B : (-FS -top -top))
|
(-> -Flonum -PosFlonum B)
|
||||||
(-> -NonNegFlonum -Flonum B : (-FS (-filter -NonNegFlonum 1) -top))
|
(-> -NonNegFlonum -Flonum B : (-FS (-filter -NonNegFlonum 1) -top))
|
||||||
(-> -Flonum -NonNegFlonum B : (-FS -top -top))
|
(-> -Flonum -NonNegFlonum B)
|
||||||
(-> -NegFlonum -Flonum B : (-FS -top -top))
|
(-> -NegFlonum -Flonum B)
|
||||||
(-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top))
|
(-> -Flonum -NegFlonum B : (-FS (-filter -NegFlonum 0) -top))
|
||||||
(-> -NonPosFlonum -Flonum B : (-FS -top -top))
|
(-> -NonPosFlonum -Flonum B)
|
||||||
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top))
|
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top))
|
||||||
(comp -Flonum))))
|
(comp -Flonum))))
|
||||||
(define fl>=-type
|
(define fl>=-type
|
||||||
|
@ -532,13 +532,13 @@
|
||||||
(from-cases
|
(from-cases
|
||||||
(-> -FlonumZero -Flonum B : (-FS (-filter -NonPosFlonum 1) -top))
|
(-> -FlonumZero -Flonum B : (-FS (-filter -NonPosFlonum 1) -top))
|
||||||
(-> -Flonum -FlonumZero B : (-FS (-filter -NonNegFlonum 0) -top))
|
(-> -Flonum -FlonumZero B : (-FS (-filter -NonNegFlonum 0) -top))
|
||||||
(-> -PosFlonum -Flonum B : (-FS -top -top))
|
(-> -PosFlonum -Flonum B)
|
||||||
(-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top))
|
(-> -Flonum -PosFlonum B : (-FS (-filter -PosFlonum 0) -top))
|
||||||
(-> -NonNegFlonum -Flonum B : (-FS -top -top))
|
(-> -NonNegFlonum -Flonum B)
|
||||||
(-> -Flonum -NonNegFlonum B : (-FS (-filter -NonNegFlonum 0) -top))
|
(-> -Flonum -NonNegFlonum B : (-FS (-filter -NonNegFlonum 0) -top))
|
||||||
(-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
|
(-> -NegFlonum -Flonum B : (-FS (-filter -NegFlonum 1) -top))
|
||||||
(-> -Flonum -NegFlonum B : (-FS -top -top))
|
(-> -Flonum -NegFlonum B)
|
||||||
(-> -NonPosFlonum -Flonum B : (-FS -top -top))
|
(-> -NonPosFlonum -Flonum B)
|
||||||
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top))
|
(-> -Flonum -NonPosFlonum B : (-FS (-filter -NonPosFlonum 0) -top))
|
||||||
(comp -Flonum))))
|
(comp -Flonum))))
|
||||||
(define flmin-type
|
(define flmin-type
|
||||||
|
|
|
@ -41,9 +41,9 @@
|
||||||
(let-values
|
(let-values
|
||||||
([(o-a t-a) (for/lists (os ts)
|
([(o-a t-a) (for/lists (os ts)
|
||||||
([nm (in-range arg-count)]
|
([nm (in-range arg-count)]
|
||||||
[oa (in-sequence-forever (in-list o-a) (make-Empty))]
|
[oa (in-sequence-forever (in-list o-a) -no-obj)]
|
||||||
[ta (in-sequence-forever (in-list t-a) (Un))])
|
[ta (in-sequence-forever (in-list t-a) -Bottom)])
|
||||||
(values (if (>= nm dom-count) (make-Empty) oa)
|
(values (if (>= nm dom-count) -no-obj oa)
|
||||||
ta))])
|
ta))])
|
||||||
(match rng
|
(match rng
|
||||||
((AnyValues:) tc-any-results)
|
((AnyValues:) tc-any-results)
|
||||||
|
|
|
@ -21,7 +21,7 @@
|
||||||
[(ValuesDots: (list (Result: ts _ _) ...) dty dbound)
|
[(ValuesDots: (list (Result: ts _ _) ...) dty dbound)
|
||||||
(ret ts
|
(ret ts
|
||||||
(for/list ([t (in-list ts)]) (make-NoFilter))
|
(for/list ([t (in-list ts)]) (make-NoFilter))
|
||||||
(for/list ([t (in-list ts)]) (make-Empty))
|
(for/list ([t (in-list ts)]) -no-obj)
|
||||||
dty dbound)]
|
dty dbound)]
|
||||||
[_ (int-err "do-ret fails: ~a" t)]))
|
[_ (int-err "do-ret fails: ~a" t)]))
|
||||||
|
|
||||||
|
|
|
@ -89,15 +89,15 @@
|
||||||
(let ([filter
|
(let ([filter
|
||||||
(match* (f2 f3)
|
(match* (f2 f3)
|
||||||
[((NoFilter:) _)
|
[((NoFilter:) _)
|
||||||
(-FS -top -top)]
|
-no-filter]
|
||||||
[(_ (NoFilter:))
|
[(_ (NoFilter:))
|
||||||
(-FS -top -top)]
|
-no-filter]
|
||||||
[((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
|
[((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
|
||||||
;(printf "f2- ~a f+ ~a\n" f2- fs+)
|
;(printf "f2- ~a f+ ~a\n" f2- fs+)
|
||||||
(-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props))
|
(-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props))
|
||||||
(-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])]
|
(-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])]
|
||||||
[type (Un t2 t3)]
|
[type (Un t2 t3)]
|
||||||
[object (if (object-equal? o2 o3) o2 (make-Empty))])
|
[object (if (object-equal? o2 o3) o2 -no-obj)])
|
||||||
;(printf "result filter is: ~a\n" filter)
|
;(printf "result filter is: ~a\n" filter)
|
||||||
(ret type filter object))))]
|
(ret type filter object))))]
|
||||||
;; special case if one of the branches is unreachable
|
;; special case if one of the branches is unreachable
|
||||||
|
|
|
@ -71,7 +71,7 @@
|
||||||
(for/list ([i (in-list lst)])
|
(for/list ([i (in-list lst)])
|
||||||
(for/fold ([s i])
|
(for/fold ([s i])
|
||||||
([nm (in-list (apply append abstract namess))])
|
([nm (in-list (apply append abstract namess))])
|
||||||
(proc s nm (make-Empty) #t))))])
|
(proc s nm -no-obj #t))))])
|
||||||
(define (run res)
|
(define (run res)
|
||||||
(match res
|
(match res
|
||||||
[(tc-any-results:) res]
|
[(tc-any-results:) res]
|
||||||
|
|
|
@ -35,7 +35,7 @@
|
||||||
[(_ i) (app lookup (? values i))]))
|
[(_ i) (app lookup (? values i))]))
|
||||||
(match o
|
(match o
|
||||||
[(Path: p (lookup: idx)) (make-Path p idx)]
|
[(Path: p (lookup: idx)) (make-Path p idx)]
|
||||||
[_ (make-Empty)]))
|
[_ -no-obj]))
|
||||||
|
|
||||||
|
|
||||||
(define/cond-contract (abstract-filter ids keys fs)
|
(define/cond-contract (abstract-filter ids keys fs)
|
||||||
|
@ -43,7 +43,7 @@
|
||||||
(match fs
|
(match fs
|
||||||
[(FilterSet: f+ f-)
|
[(FilterSet: f+ f-)
|
||||||
(-FS (abo ids keys f+) (abo ids keys f-))]
|
(-FS (abo ids keys f+) (abo ids keys f-))]
|
||||||
[(NoFilter:) (-FS -top -top)]))
|
[(NoFilter:) -no-filter]))
|
||||||
|
|
||||||
(define/cond-contract (abo xs idxs f)
|
(define/cond-contract (abo xs idxs f)
|
||||||
((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c)
|
((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c)
|
||||||
|
|
|
@ -34,7 +34,7 @@
|
||||||
[(FilterSet: f+ f-)
|
[(FilterSet: f+ f-)
|
||||||
(-FS (subst-filter (add-extra-filter f+) k o polarity)
|
(-FS (subst-filter (add-extra-filter f+) k o polarity)
|
||||||
(subst-filter (add-extra-filter f-) k o polarity))]
|
(subst-filter (add-extra-filter f-) k o polarity))]
|
||||||
[_ (-FS -top -top)]))
|
[_ -no-filter]))
|
||||||
|
|
||||||
(define/cond-contract (subst-type t k o polarity)
|
(define/cond-contract (subst-type t k o polarity)
|
||||||
(-> Type/c name-ref/c Object? boolean? Type/c)
|
(-> Type/c name-ref/c Object? boolean? Type/c)
|
||||||
|
@ -64,9 +64,9 @@
|
||||||
[(Path: p i)
|
[(Path: p i)
|
||||||
(if (name-ref=? i k)
|
(if (name-ref=? i k)
|
||||||
(match o
|
(match o
|
||||||
[(Empty:) (make-Empty)]
|
[(Empty:) -no-obj]
|
||||||
;; the result is not from an annotation, so it isn't a NoObject
|
;; the result is not from an annotation, so it isn't a NoObject
|
||||||
[(NoObject:) (make-Empty)]
|
[(NoObject:) -no-obj]
|
||||||
[(Path: p* i*) (make-Path (append p p*) i*)])
|
[(Path: p* i*) (make-Path (append p p*) i*)])
|
||||||
t)]))
|
t)]))
|
||||||
|
|
||||||
|
|
|
@ -4,7 +4,7 @@
|
||||||
racket/match racket/set racket/function unstable/function
|
racket/match racket/set racket/function unstable/function
|
||||||
racket/lazy-require
|
racket/lazy-require
|
||||||
(contract-req)
|
(contract-req)
|
||||||
(only-in (types base-abbrev) -lst* -result)
|
(only-in (types base-abbrev) -lst* -result -no-filter -no-obj)
|
||||||
(rep type-rep filter-rep object-rep rep-utils)
|
(rep type-rep filter-rep object-rep rep-utils)
|
||||||
(utils tc-utils)
|
(utils tc-utils)
|
||||||
(rep free-variance)
|
(rep free-variance)
|
||||||
|
@ -111,8 +111,8 @@
|
||||||
(for/list ([img (in-list images)])
|
(for/list ([img (in-list images)])
|
||||||
(make-Result
|
(make-Result
|
||||||
(substitute img name expanded)
|
(substitute img name expanded)
|
||||||
(make-FilterSet (make-Top) (make-Top))
|
-no-filter
|
||||||
(make-Empty))))))
|
-no-obj)))))
|
||||||
(make-ValuesDots (map sb types) (sb dty) dbound))]
|
(make-ValuesDots (map sb types) (sb dty) dbound))]
|
||||||
[#:arr dom rng rest drest kws
|
[#:arr dom rng rest drest kws
|
||||||
(if (and (pair? drest)
|
(if (and (pair? drest)
|
||||||
|
|
|
@ -3,6 +3,7 @@
|
||||||
(require "../utils/utils.rkt"
|
(require "../utils/utils.rkt"
|
||||||
(rep free-variance type-rep filter-rep object-rep rep-utils)
|
(rep free-variance type-rep filter-rep object-rep rep-utils)
|
||||||
(utils tc-utils)
|
(utils tc-utils)
|
||||||
|
(types base-abbrev)
|
||||||
racket/match
|
racket/match
|
||||||
(contract-req))
|
(contract-req))
|
||||||
|
|
||||||
|
@ -67,20 +68,19 @@
|
||||||
;; convenience function for returning the result of typechecking an expression
|
;; convenience function for returning the result of typechecking an expression
|
||||||
(define ret
|
(define ret
|
||||||
(case-lambda [(t)
|
(case-lambda [(t)
|
||||||
(let ([mk (lambda (t) (make-FilterSet (make-Top) (make-Top)))])
|
|
||||||
(make-tc-results
|
(make-tc-results
|
||||||
(cond [(Type/c? t)
|
(cond [(Type/c? t)
|
||||||
(list (make-tc-result t (mk t) (make-Empty)))]
|
(list (make-tc-result t -no-filter -no-obj))]
|
||||||
[else
|
[else
|
||||||
(for/list ([i (in-list t)])
|
(for/list ([i (in-list t)])
|
||||||
(make-tc-result i (mk t) (make-Empty)))])
|
(make-tc-result i -no-filter -no-obj))])
|
||||||
#f))]
|
#f)]
|
||||||
[(t f)
|
[(t f)
|
||||||
(make-tc-results
|
(make-tc-results
|
||||||
(if (Type/c? t)
|
(if (Type/c? t)
|
||||||
(list (make-tc-result t f (make-Empty)))
|
(list (make-tc-result t f -no-obj))
|
||||||
(for/list ([i (in-list t)] [f (in-list f)])
|
(for/list ([i (in-list t)] [f (in-list f)])
|
||||||
(make-tc-result i f (make-Empty))))
|
(make-tc-result i f -no-obj)))
|
||||||
#f)]
|
#f)]
|
||||||
[(t f o)
|
[(t f o)
|
||||||
(make-tc-results
|
(make-tc-results
|
||||||
|
|
Loading…
Reference in New Issue
Block a user