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