Rename -no-obj and -no-filter to -empty-obj and -top-filter.
This commit is contained in:
Eric Dobson
parent
07bde5063b
commit
d401a398cd
|
|
@ -388,9 +388,7 @@
|
||||||
[new-tys (for/list ([var (in-list vars)])
|
[new-tys (for/list ([var (in-list vars)])
|
||||||
;; must be a Result since we are matching these against
|
;; must be a Result since we are matching these against
|
||||||
;; the contents of the `Values`, which are Results
|
;; the contents of the `Values`, which are Results
|
||||||
(make-Result
|
(-result (substitute (make-F var) dbound s-dty)))]
|
||||||
(substitute (make-F var) dbound s-dty)
|
|
||||||
-no-filter -no-obj))]
|
|
||||||
;; generate constraints on the prefixes, and on the dummy types
|
;; generate constraints on the prefixes, and on the dummy types
|
||||||
[new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)])
|
[new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)])
|
||||||
;; now take all the dummy types, and use them to constrain dbound appropriately
|
;; now take all the dummy types, and use them to constrain dbound appropriately
|
||||||
|
|
@ -404,9 +402,7 @@
|
||||||
;; see comments for last case, this case swaps `s` and `t` order
|
;; see comments for last case, this case swaps `s` and `t` order
|
||||||
(let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))]
|
(let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))]
|
||||||
[new-tys (for/list ([var (in-list vars)])
|
[new-tys (for/list ([var (in-list vars)])
|
||||||
(make-Result
|
(-result (substitute (make-F var) dbound t-dty)))]
|
||||||
(substitute (make-F var) dbound t-dty)
|
|
||||||
-no-filter -no-obj))]
|
|
||||||
[new-cset (cgen/list V (append vars X) Y ss (append ts new-tys))])
|
[new-cset (cgen/list V (append vars X) Y ss (append ts new-tys))])
|
||||||
(move-vars-to-dmap new-cset dbound vars))]
|
(move-vars-to-dmap new-cset dbound vars))]
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -241,7 +241,7 @@
|
||||||
(define-syntax-class object
|
(define-syntax-class object
|
||||||
#:attributes (object)
|
#:attributes (object)
|
||||||
(pattern e:expr
|
(pattern e:expr
|
||||||
#:attr object -no-obj))
|
#:attr object -empty-obj))
|
||||||
|
|
||||||
(define-splicing-syntax-class (full-latent doms)
|
(define-splicing-syntax-class (full-latent doms)
|
||||||
#:description "latent propositions and object"
|
#:description "latent propositions and object"
|
||||||
|
|
@ -250,7 +250,7 @@
|
||||||
(~optional (~seq #:object o:object)))
|
(~optional (~seq #:object o:object)))
|
||||||
#:attr positive (apply -and (attribute p+.prop))
|
#:attr positive (apply -and (attribute p+.prop))
|
||||||
#:attr negative (apply -and (attribute p-.prop))
|
#:attr negative (apply -and (attribute p-.prop))
|
||||||
#:attr object (or (attribute o.object) -no-obj)))
|
#:attr object (or (attribute o.object) -empty-obj)))
|
||||||
|
|
||||||
(define (parse-types stx-list)
|
(define (parse-types stx-list)
|
||||||
(stx-map parse-type stx-list))
|
(stx-map parse-type stx-list))
|
||||||
|
|
|
||||||
|
|
@ -29,8 +29,8 @@
|
||||||
((Values: (list (Result: t-r _ _) ...)) (ret t-r))
|
((Values: (list (Result: t-r _ _) ...)) (ret t-r))
|
||||||
((ValuesDots: (list (Result: t-r _ _) ...) dty dbound)
|
((ValuesDots: (list (Result: t-r _ _) ...) dty dbound)
|
||||||
(ret t-r
|
(ret t-r
|
||||||
(make-list (length t-r) -no-filter)
|
(make-list (length t-r) -top-filter)
|
||||||
(make-list (length t-r) -no-obj)
|
(make-list (length t-r) -empty-obj)
|
||||||
dty dbound))))
|
dty dbound))))
|
||||||
(cond [(and (not rest) (not (= (length dom) (length t-a))))
|
(cond [(and (not rest) (not (= (length dom) (length t-a))))
|
||||||
(tc-error/expr #:return error-ret
|
(tc-error/expr #:return error-ret
|
||||||
|
|
@ -47,9 +47,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) -no-obj)]
|
[oa (in-sequence-forever (in-list o-a) -empty-obj)]
|
||||||
[ta (in-sequence-forever (in-list t-a) -Bottom)])
|
[ta (in-sequence-forever (in-list t-a) -Bottom)])
|
||||||
(values (if (>= nm dom-count) -no-obj oa)
|
(values (if (>= nm dom-count) -empty-obj oa)
|
||||||
ta))])
|
ta))])
|
||||||
(match rng
|
(match rng
|
||||||
((AnyValues:) tc-any-results)
|
((AnyValues:) tc-any-results)
|
||||||
|
|
|
||||||
|
|
@ -18,7 +18,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)]) -no-obj)
|
(for/list ([t (in-list ts)]) -empty-obj)
|
||||||
dty dbound)]
|
dty dbound)]
|
||||||
[_ (int-err "do-ret fails: ~a" t)]))
|
[_ (int-err "do-ret fails: ~a" t)]))
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -81,15 +81,15 @@
|
||||||
(let ([filter
|
(let ([filter
|
||||||
(match* (f2 f3)
|
(match* (f2 f3)
|
||||||
[((NoFilter:) _)
|
[((NoFilter:) _)
|
||||||
-no-filter]
|
-top-filter]
|
||||||
[(_ (NoFilter:))
|
[(_ (NoFilter:))
|
||||||
-no-filter]
|
-top-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 -no-obj)])
|
[object (if (object-equal? o2 o3) o2 -empty-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
|
||||||
|
|
|
||||||
|
|
@ -65,7 +65,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 -no-obj #t))))])
|
(proc s nm -empty-obj #t))))])
|
||||||
(define (run res)
|
(define (run res)
|
||||||
(match res
|
(match res
|
||||||
[(tc-any-results:) res]
|
[(tc-any-results:) res]
|
||||||
|
|
|
||||||
|
|
@ -121,7 +121,7 @@
|
||||||
(define-lookup: lookup: ids keys)
|
(define-lookup: lookup: ids keys)
|
||||||
(match o
|
(match o
|
||||||
[(Path: p (lookup: idx)) (make-Path p idx)]
|
[(Path: p (lookup: idx)) (make-Path p idx)]
|
||||||
[_ -no-obj]))
|
[_ -empty-obj]))
|
||||||
|
|
||||||
;; Abstract all given id objects into index objects (keys) in
|
;; Abstract all given id objects into index objects (keys) in
|
||||||
;; the given filter set
|
;; the given filter set
|
||||||
|
|
@ -130,7 +130,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:) -no-filter]))
|
[(NoFilter:) -top-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)
|
||||||
|
|
|
||||||
|
|
@ -42,7 +42,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))]
|
||||||
[_ -no-filter]))
|
[_ -top-filter]))
|
||||||
|
|
||||||
;; Substitution of objects into a type
|
;; Substitution of objects into a type
|
||||||
;; This is essentially t [o/x] from the paper
|
;; This is essentially t [o/x] from the paper
|
||||||
|
|
@ -81,9 +81,9 @@
|
||||||
[(Path: p i)
|
[(Path: p i)
|
||||||
(if (name-ref=? i k)
|
(if (name-ref=? i k)
|
||||||
(match o
|
(match o
|
||||||
[(Empty:) -no-obj]
|
[(Empty:) -empty-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:) -no-obj]
|
[(NoObject:) -empty-obj]
|
||||||
[(Path: p* i*) (make-Path (append p p*) i*)])
|
[(Path: p* i*) (make-Path (append p p*) i*)])
|
||||||
t)]))
|
t)]))
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -101,15 +101,15 @@
|
||||||
(make-Mu 'var ty))]))
|
(make-Mu 'var ty))]))
|
||||||
|
|
||||||
;; Results
|
;; Results
|
||||||
(define/cond-contract (-result t [f -no-filter] [o -no-obj])
|
(define/cond-contract (-result t [f -top-filter] [o -empty-obj])
|
||||||
(c:->* (Type/c) (FilterSet? Object?) Result?)
|
(c:->* (Type/c) (FilterSet? Object?) Result?)
|
||||||
(make-Result t f o))
|
(make-Result t f o))
|
||||||
|
|
||||||
;; Filters
|
;; Filters
|
||||||
(define/decl -top (make-Top))
|
(define/decl -top (make-Top))
|
||||||
(define/decl -bot (make-Bot))
|
(define/decl -bot (make-Bot))
|
||||||
(define/decl -no-filter (make-FilterSet -top -top))
|
(define/decl -top-filter (make-FilterSet -top -top))
|
||||||
(define/decl -no-obj (make-Empty))
|
(define/decl -empty-obj (make-Empty))
|
||||||
|
|
||||||
(define/cond-contract (-FS + -)
|
(define/cond-contract (-FS + -)
|
||||||
(c:-> Filter/c Filter/c FilterSet?)
|
(c:-> Filter/c Filter/c FilterSet?)
|
||||||
|
|
@ -145,7 +145,7 @@
|
||||||
;; Function types
|
;; Function types
|
||||||
(define/cond-contract (make-arr* dom rng
|
(define/cond-contract (make-arr* dom rng
|
||||||
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
|
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
|
||||||
#:filters [filters -no-filter] #:object [obj -no-obj])
|
#:filters [filters -top-filter] #:object [obj -empty-obj])
|
||||||
(c:->* ((c:listof Type/c) (c:or/c SomeValues/c Type/c))
|
(c:->* ((c:listof Type/c) (c:or/c SomeValues/c Type/c))
|
||||||
(#:rest (c:or/c #f Type/c)
|
(#:rest (c:or/c #f Type/c)
|
||||||
#:drest (c:or/c #f (c:cons/c Type/c symbol?))
|
#:drest (c:or/c #f (c:cons/c Type/c symbol?))
|
||||||
|
|
|
||||||
|
|
@ -4,7 +4,7 @@
|
||||||
racket/match racket/set
|
racket/match racket/set
|
||||||
racket/lazy-require
|
racket/lazy-require
|
||||||
(contract-req)
|
(contract-req)
|
||||||
(only-in (types base-abbrev) -lst* -result -no-filter -no-obj)
|
(only-in (types base-abbrev) -lst* -result)
|
||||||
(rep type-rep rep-utils)
|
(rep type-rep rep-utils)
|
||||||
(utils tc-utils)
|
(utils tc-utils)
|
||||||
(rep free-variance)
|
(rep free-variance)
|
||||||
|
|
@ -109,10 +109,7 @@
|
||||||
;; We need to recur first, just to expand out any dotted usages of this.
|
;; We need to recur first, just to expand out any dotted usages of this.
|
||||||
(let ([expanded (sb dty)])
|
(let ([expanded (sb dty)])
|
||||||
(for/list ([img (in-list images)])
|
(for/list ([img (in-list images)])
|
||||||
(make-Result
|
(-result (substitute img name expanded))))))
|
||||||
(substitute img name expanded)
|
|
||||||
-no-filter
|
|
||||||
-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)
|
||||||
|
|
|
||||||
|
|
@ -70,17 +70,17 @@
|
||||||
(case-lambda [(t)
|
(case-lambda [(t)
|
||||||
(make-tc-results
|
(make-tc-results
|
||||||
(cond [(Type/c? t)
|
(cond [(Type/c? t)
|
||||||
(list (make-tc-result t -no-filter -no-obj))]
|
(list (make-tc-result t -top-filter -empty-obj))]
|
||||||
[else
|
[else
|
||||||
(for/list ([i (in-list t)])
|
(for/list ([i (in-list t)])
|
||||||
(make-tc-result i -no-filter -no-obj))])
|
(make-tc-result i -top-filter -empty-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 -no-obj))
|
(list (make-tc-result t f -empty-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 -no-obj)))
|
(make-tc-result i f -empty-obj)))
|
||||||
#f)]
|
#f)]
|
||||||
[(t f o)
|
[(t f o)
|
||||||
(make-tc-results
|
(make-tc-results
|
||||||
|
|
|
||||||
|
|
@ -68,8 +68,8 @@
|
||||||
(check-prints-as? (-mu x (-lst x)) "(Rec x (Listof x))")
|
(check-prints-as? (-mu x (-lst x)) "(Rec x (Listof x))")
|
||||||
(check-prints-as? (-seq -String -Symbol) "(Sequenceof String Symbol)")
|
(check-prints-as? (-seq -String -Symbol) "(Sequenceof String Symbol)")
|
||||||
(check-prints-as? (-poly (a) (-> a -Void)) "(All (a) (-> a Void))")
|
(check-prints-as? (-poly (a) (-> a -Void)) "(All (a) (-> a Void))")
|
||||||
(check-prints-as? (-> -Input-Port (make-Values (list (-result -String (-FS -top -bot) -no-obj)
|
(check-prints-as? (-> -Input-Port (make-Values (list (-result -String (-FS -top -bot) -empty-obj)
|
||||||
(-result -String (-FS -top -bot) -no-obj))))
|
(-result -String (-FS -top -bot) -empty-obj))))
|
||||||
"(-> Input-Port (values (String : (Top | Bot)) (String : (Top | Bot))))")
|
"(-> Input-Port (values (String : (Top | Bot)) (String : (Top | Bot))))")
|
||||||
;; this case tests that the Number union is printed with its name
|
;; this case tests that the Number union is printed with its name
|
||||||
;; rather than its expansion (a former bug)
|
;; rather than its expansion (a former bug)
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user