Split filter operations into their own file.
Take into account the type of arguments in filter generation.
This commit is contained in:
Sam Tobin-Hochstadt
parent
35f090cde8
commit
27b0c01cdd
|
|
@ -4,7 +4,7 @@
|
|||
(prefix-in r: "../utils/utils.ss")
|
||||
scheme/match (r:rep filter-rep rep-utils type-rep) unstable/struct
|
||||
(except-in (r:utils tc-utils) make-env)
|
||||
(r:typecheck tc-metafunctions))
|
||||
#;(r:typecheck tc-metafunctions))
|
||||
|
||||
(provide current-tvars
|
||||
extend
|
||||
|
|
|
|||
|
|
@ -748,15 +748,19 @@
|
|||
(parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
|
||||
;(printf "got to here 2 ~a ~a ~a ~n" dom names o-a)
|
||||
(let* ([dom-count (length dom)]
|
||||
[arg-count (+ dom-count (if rest 1 0) (length kws))]
|
||||
[o-a (for/list ([nm (in-range arg-count)]
|
||||
[oa (in-sequence-forever (in-list o-a) (make-Empty))])
|
||||
(if (>= nm dom-count) (make-Empty) oa))])
|
||||
[arg-count (+ dom-count (if rest 1 0) (length kws))])
|
||||
(let-values
|
||||
([(o-a t-a) (for/lists (os ts)
|
||||
([nm (in-range arg-count)]
|
||||
[oa (in-sequence-forever (in-list o-a) (make-Empty))]
|
||||
[ta (in-sequence-forever (in-list t-a) (Un))])
|
||||
(values (if (>= nm dom-count) (make-Empty) oa)
|
||||
ta))])
|
||||
(define-values (t-r f-r o-r)
|
||||
(for/lists (t-r f-r o-r)
|
||||
([r (in-list results)])
|
||||
(open-Result r o-a)))
|
||||
(ret t-r f-r o-r))]
|
||||
(open-Result r o-a t-a)))
|
||||
(ret t-r f-r o-r)))]
|
||||
[((arr: _ _ _ drest '()) _)
|
||||
(int-err "funapp with drest args NYI")]
|
||||
[((arr: _ _ _ _ kws) _)
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
(require (rename-in "../utils/utils.ss" [infer r:infer]))
|
||||
(require "signatures.ss"
|
||||
(rep type-rep filter-rep object-rep)
|
||||
(rename-in (types convenience subtype union utils comparison remove-intersect abbrev)
|
||||
(rename-in (types convenience subtype union utils comparison remove-intersect abbrev filter-ops)
|
||||
[remove *remove])
|
||||
(env lexical-env type-environments)
|
||||
(r:infer infer)
|
||||
|
|
@ -53,6 +53,7 @@
|
|||
;(printf "old els-props: ~a\n" (env-props (lexical-env)))
|
||||
;(printf "fs-: ~a~n" fs-)
|
||||
;(printf "els-props: ~a~n" (env-props env-els))
|
||||
;(printf "thn-props: ~a~n" (env-props env-thn))
|
||||
;(printf "new-els-props: ~a~n" new-els-props)
|
||||
;; if we have the same number of values in both cases
|
||||
(cond [(= (length ts) (length us))
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require "../utils/utils.ss")
|
||||
(require (rename-in (types subtype convenience remove-intersect union utils)
|
||||
(require (rename-in (types subtype convenience remove-intersect union utils filter-ops)
|
||||
[-> -->]
|
||||
[->* -->*]
|
||||
[one-of/c -one-of/c])
|
||||
|
|
@ -146,7 +146,9 @@
|
|||
(if (OrFilter? new-or)
|
||||
(loop (cons new-or derived-props) derived-atoms (cdr worklist))
|
||||
(loop derived-props derived-atoms (cons new-or (cdr worklist)))))]
|
||||
[(TypeFilter: (== (Un) type-equal?) _ _) (set-box! flag #f) (values derived-props derived-atoms)]
|
||||
[(TypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
|
||||
[(NotTypeFilter: (== Univ type-equal?) _ _) (set-box! flag #f) (values derived-props derived-atoms)]
|
||||
[(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
|
||||
[(Top:) (loop derived-props derived-atoms (cdr worklist))]
|
||||
[(Bot:) (set-box! flag #f) (values derived-props derived-atoms)]
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require "../utils/utils.ss")
|
||||
(require (rename-in (types subtype convenience remove-intersect union utils)
|
||||
(require (rename-in (types subtype convenience remove-intersect union utils filter-ops)
|
||||
[-> -->]
|
||||
[->* -->*]
|
||||
[one-of/c -one-of/c])
|
||||
|
|
@ -16,28 +16,23 @@
|
|||
(begin (d/c (name . args) c . body)
|
||||
(p/c [name c])))
|
||||
|
||||
(define (name-ref=? a b)
|
||||
(or (eq? a b)
|
||||
(and (identifier? a)
|
||||
(identifier? b)
|
||||
(free-identifier=? a b))))
|
||||
|
||||
(d/c/p (open-Result r objs)
|
||||
(-> Result? (listof Object?) (values Type/c FilterSet? Object?))
|
||||
(d/c/p (open-Result r objs ts)
|
||||
(-> Result? (listof Object?) (listof Type/c) (values Type/c FilterSet? Object?))
|
||||
(match r
|
||||
[(Result: t fs old-obj)
|
||||
(for/fold ([t t] [fs fs] [old-obj old-obj])
|
||||
([(o k) (in-indexed (in-list objs))])
|
||||
([(o k) (in-indexed (in-list objs))]
|
||||
[arg-ty (in-list ts)])
|
||||
(values (subst-type t k o #t)
|
||||
(subst-filter-set fs k o #t)
|
||||
(subst-filter-set fs k o #t arg-ty)
|
||||
(subst-object old-obj k o #t)))]))
|
||||
|
||||
(d/c/p (subst-filter-set fs k o polarity)
|
||||
(-> FilterSet? name-ref/c Object? boolean? FilterSet?)
|
||||
(d/c/p (subst-filter-set fs k o polarity t)
|
||||
(-> FilterSet? name-ref/c Object? boolean? Type/c FilterSet?)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(combine (subst-filter f+ k o polarity)
|
||||
(subst-filter f- k o polarity))]))
|
||||
(combine (subst-filter (-and (make-TypeFilter t null k) f+) k o polarity)
|
||||
(subst-filter (-and (make-TypeFilter t null k) f-) k o polarity))]))
|
||||
|
||||
(d/c/p (subst-type t k o polarity)
|
||||
(-> Type/c name-ref/c Object? boolean? Type/c)
|
||||
|
|
|
|||
|
|
@ -71,115 +71,3 @@
|
|||
|
||||
(define Ident (-Syntax -Symbol))
|
||||
|
||||
(define (atomic-filter? e)
|
||||
(or (TypeFilter? e) (NotTypeFilter? e)))
|
||||
|
||||
(define (opposite? f1 f2)
|
||||
(match* (f1 f2)
|
||||
[((TypeFilter: t1 p1 i1)
|
||||
(NotTypeFilter: t2 p1 i2))
|
||||
(and (free-identifier=? i1 i2)
|
||||
(subtype t1 t2))]
|
||||
[((NotTypeFilter: t2 p1 i2)
|
||||
(TypeFilter: t1 p1 i1))
|
||||
(and (free-identifier=? i1 i2)
|
||||
(subtype t1 t2))]
|
||||
[(_ _) #f]))
|
||||
|
||||
;; is f1 implied by f2?
|
||||
(define (implied-atomic? f1 f2)
|
||||
(if (filter-equal? f1 f2)
|
||||
#t
|
||||
(match* (f1 f2)
|
||||
[((TypeFilter: t1 p1 i1)
|
||||
(TypeFilter: t2 p1 i2))
|
||||
(and (free-identifier=? i1 i2)
|
||||
(subtype t1 t2))]
|
||||
[((NotTypeFilter: t2 p1 i2)
|
||||
(NotTypeFilter: t1 p1 i1))
|
||||
(and (free-identifier=? i1 i2)
|
||||
(subtype t1 t2))]
|
||||
[(_ _) #f])))
|
||||
|
||||
;; props : propositions to compress
|
||||
;; or? : is this or OrFilter (alternative is AndFilter)
|
||||
(define (compact props or?)
|
||||
(define tf-map (make-hash))
|
||||
(define ntf-map (make-hash))
|
||||
(let loop ([props props] [others null])
|
||||
(if (null? props)
|
||||
(append others
|
||||
(for/list ([v (in-dict-values tf-map)]) v)
|
||||
(for/list ([v (in-dict-values ntf-map)]) v))
|
||||
(match (car props)
|
||||
[(and p (TypeFilter: t1 f1 x) (? (lambda _ or?)))
|
||||
(hash-update! tf-map
|
||||
(list f1 (hash-id x))
|
||||
(match-lambda [(TypeFilter: t2 _ _) (make-TypeFilter (Un t1 t2) f1 x)]
|
||||
[p (int-err "got something that isn't a typefilter ~a" p)])
|
||||
p)
|
||||
(loop (cdr props) others)]
|
||||
[(and p (NotTypeFilter: t1 f1 x) (? (lambda _ (not or?))))
|
||||
(hash-update! ntf-map
|
||||
(list f1 (hash-id x))
|
||||
(match-lambda [(NotTypeFilter: t2 _ _) (make-NotTypeFilter (Un t1 t2) f1 x)]
|
||||
[p (int-err "got something that isn't a nottypefilter ~a" p)])
|
||||
p)
|
||||
(loop (cdr props) others)]
|
||||
[p (loop (cdr props) (cons p others))]))))
|
||||
|
||||
(define (-or . args)
|
||||
(define mk
|
||||
(case-lambda [() -bot]
|
||||
[(f) f]
|
||||
[fs (make-OrFilter fs)]))
|
||||
(define (distribute args)
|
||||
(define-values (ands others) (partition AndFilter? args))
|
||||
(if (null? ands)
|
||||
(apply mk others)
|
||||
(match-let ([(AndFilter: elems) (car ands)])
|
||||
(apply -and (for/list ([a (in-list elems)])
|
||||
(apply -or a (append (cdr ands) others)))))))
|
||||
(let loop ([fs args] [result null])
|
||||
(if (null? fs)
|
||||
(match result
|
||||
[(list) -bot]
|
||||
[(list f) f]
|
||||
[_ (distribute (compact result #t))])
|
||||
(match (car fs)
|
||||
[(and t (Top:)) t]
|
||||
[(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]
|
||||
[(Bot:) (loop (cdr fs) result)]
|
||||
[t
|
||||
(cond [(for/or ([f (in-list (append (cdr fs) result))])
|
||||
(opposite? f t))
|
||||
-top]
|
||||
[(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? f t)))
|
||||
(loop (cdr fs) result)]
|
||||
[else
|
||||
(loop (cdr fs) (cons t result))])]))))
|
||||
|
||||
(define (-and . args)
|
||||
(let loop ([fs (remove-duplicates args filter-equal?)] [result null])
|
||||
(if (null? fs)
|
||||
(match result
|
||||
[(list) -top]
|
||||
[(list f) f]
|
||||
;; don't think this is useful here
|
||||
[(list f1 f2) (if (opposite? f1 f2)
|
||||
-bot
|
||||
(if (filter-equal? f1 f2)
|
||||
f1
|
||||
(make-AndFilter (compact (list f1 f2) #f))))]
|
||||
[_ (make-AndFilter (compact result #f))])
|
||||
(match (car fs)
|
||||
[(and t (Bot:)) t]
|
||||
[(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
|
||||
[(Top:) (loop (cdr fs) result)]
|
||||
[t (cond [(for/or ([f (in-list (append (cdr fs) result))])
|
||||
(opposite? f t))
|
||||
-bot]
|
||||
[(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? t f)))
|
||||
(loop (cdr fs) result)]
|
||||
[else
|
||||
(loop (cdr fs) (cons t result))])]))))
|
||||
|
|
|
|||
156
collects/typed-scheme/types/filter-ops.ss
Normal file
156
collects/typed-scheme/types/filter-ops.ss
Normal file
|
|
@ -0,0 +1,156 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require "../utils/utils.ss"
|
||||
(rep type-rep filter-rep object-rep rep-utils)
|
||||
(utils tc-utils) (only-in (infer infer) restrict)
|
||||
"abbrev.ss" (only-in scheme/contract current-blame-format [-> -->] listof)
|
||||
(types comparison printer union subtype utils remove-intersect)
|
||||
scheme/list scheme/match scheme/promise
|
||||
(for-syntax syntax/parse scheme/base)
|
||||
unstable/debug syntax/id-table scheme/dict
|
||||
scheme/trace
|
||||
(for-template scheme/base))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define (atomic-filter? e)
|
||||
(or (TypeFilter? e) (NotTypeFilter? e)))
|
||||
|
||||
(define (opposite? f1 f2)
|
||||
(match* (f1 f2)
|
||||
[((TypeFilter: t1 p1 i1)
|
||||
(NotTypeFilter: t2 p1 i2))
|
||||
(and (name-ref=? i1 i2)
|
||||
(subtype t1 t2))]
|
||||
[((NotTypeFilter: t2 p1 i2)
|
||||
(TypeFilter: t1 p1 i1))
|
||||
(and (name-ref=? i1 i2)
|
||||
(subtype t1 t2))]
|
||||
[(_ _) #f]))
|
||||
|
||||
|
||||
(define (name-ref=? a b)
|
||||
(or (eq? a b)
|
||||
(and (identifier? a)
|
||||
(identifier? b)
|
||||
(free-identifier=? a b))))
|
||||
|
||||
;; is f1 implied by f2?
|
||||
(define (implied-atomic? f1 f2)
|
||||
(if (filter-equal? f1 f2)
|
||||
#t
|
||||
(match* (f1 f2)
|
||||
[((TypeFilter: t1 p1 i1)
|
||||
(TypeFilter: t2 p1 i2))
|
||||
(and (name-ref=? i1 i2)
|
||||
(subtype t1 t2))]
|
||||
[((NotTypeFilter: t2 p1 i2)
|
||||
(NotTypeFilter: t1 p1 i1))
|
||||
(and (name-ref=? i1 i2)
|
||||
(subtype t1 t2))]
|
||||
[(_ _) #f])))
|
||||
|
||||
(define (hash-name-ref i)
|
||||
(if (identifier? i) (hash-id i) i))
|
||||
|
||||
;; compact : (Listof prop) bool -> (Listof prop)
|
||||
;; props : propositions to compress
|
||||
;; or? : is this an OrFilter (alternative is AndFilter)
|
||||
(d/c (compact props or?)
|
||||
((listof Filter/c) boolean? . --> . (listof Filter/c))
|
||||
(define tf-map (make-hash))
|
||||
(define ntf-map (make-hash))
|
||||
(let loop ([props props] [others null])
|
||||
(if (null? props)
|
||||
(append others
|
||||
(for/list ([v (in-dict-values tf-map)]) v)
|
||||
(for/list ([v (in-dict-values ntf-map)]) v))
|
||||
(match (car props)
|
||||
[(and p (TypeFilter: t1 f1 x) (? (lambda _ or?)))
|
||||
(hash-update! tf-map
|
||||
(list f1 (hash-name-ref x))
|
||||
(match-lambda [(TypeFilter: t2 _ _) (make-TypeFilter (Un t1 t2) f1 x)]
|
||||
[p (int-err "got something that isn't a typefilter ~a" p)])
|
||||
p)
|
||||
(loop (cdr props) others)]
|
||||
[(and p (TypeFilter: t1 f1 x) (? (lambda _ (not or?))))
|
||||
(match (hash-ref tf-map (list f1 (hash-name-ref x)) #f)
|
||||
[(TypeFilter: (? (lambda (t2) (not (overlap t1 t2)))) _ _)
|
||||
;; we're in an And, and we got two types for the same path that do not overlap
|
||||
(list -bot)]
|
||||
[(TypeFilter: t2 _ _)
|
||||
(hash-set! tf-map (list f1 (hash-name-ref x))
|
||||
(make-TypeFilter (restrict t1 t2) f1 x))
|
||||
(loop (cdr props) others)]
|
||||
[#f
|
||||
(hash-set! tf-map (list f1 (hash-name-ref x))
|
||||
(make-TypeFilter t1 f1 x))
|
||||
(loop (cdr props) others)])]
|
||||
[(and p (NotTypeFilter: t1 f1 x) (? (lambda _ (not or?))))
|
||||
(hash-update! ntf-map
|
||||
(list f1 (hash-name-ref x))
|
||||
(match-lambda [(NotTypeFilter: t2 _ _) (make-NotTypeFilter (Un t1 t2) f1 x)]
|
||||
[p (int-err "got something that isn't a nottypefilter ~a" p)])
|
||||
p)
|
||||
(loop (cdr props) others)]
|
||||
[p (loop (cdr props) (cons p others))]))))
|
||||
|
||||
(define (-or . args)
|
||||
(define mk
|
||||
(case-lambda [() -bot]
|
||||
[(f) f]
|
||||
[fs (make-OrFilter fs)]))
|
||||
(define (distribute args)
|
||||
(define-values (ands others) (partition AndFilter? args))
|
||||
(if (null? ands)
|
||||
(apply mk others)
|
||||
(match-let ([(AndFilter: elems) (car ands)])
|
||||
(apply -and (for/list ([a (in-list elems)])
|
||||
(apply -or a (append (cdr ands) others)))))))
|
||||
(let loop ([fs args] [result null])
|
||||
(if (null? fs)
|
||||
(match result
|
||||
[(list) -bot]
|
||||
[(list f) f]
|
||||
[_ (distribute (compact result #t))])
|
||||
(match (car fs)
|
||||
[(and t (Top:)) t]
|
||||
[(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]
|
||||
[(Bot:) (loop (cdr fs) result)]
|
||||
[t
|
||||
(cond [(for/or ([f (in-list (append (cdr fs) result))])
|
||||
(opposite? f t))
|
||||
-top]
|
||||
[(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? f t)))
|
||||
(loop (cdr fs) result)]
|
||||
[else
|
||||
(loop (cdr fs) (cons t result))])]))))
|
||||
|
||||
(define (-and . args)
|
||||
(define mk
|
||||
(case-lambda [() -top]
|
||||
[(f) f]
|
||||
[fs (make-AndFilter fs)]))
|
||||
(let loop ([fs (remove-duplicates args filter-equal?)] [result null])
|
||||
(if (null? fs)
|
||||
(match result
|
||||
[(list) -top]
|
||||
[(list f) f]
|
||||
;; don't think this is useful here
|
||||
[(list f1 f2) (if (opposite? f1 f2)
|
||||
-bot
|
||||
(if (filter-equal? f1 f2)
|
||||
f1
|
||||
(apply mk (compact (list f1 f2) #f))))]
|
||||
[_ (apply mk (compact result #f))])
|
||||
(match (car fs)
|
||||
[(and t (Bot:)) t]
|
||||
[(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
|
||||
[(Top:) (loop (cdr fs) result)]
|
||||
[t (cond [(for/or ([f (in-list (append (cdr fs) result))])
|
||||
(opposite? f t))
|
||||
-bot]
|
||||
[(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? t f)))
|
||||
(loop (cdr fs) result)]
|
||||
[else
|
||||
(loop (cdr fs) (cons t result))])]))))
|
||||
Loading…
Reference in New Issue
Block a user