From 9364f5b9cc6daab31d197fa29b0782a01b029c33 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 8 Jan 2010 15:55:32 +0000 Subject: [PATCH] use of member, memq, memv as predicates working properly svn: r17568 original commit: 05a0e722f9b64d0d53fb5b168181b467a4711ec7 --- .../tests/typed-scheme/succeed/member-pred.ss | 15 +++++- collects/typed-scheme/typecheck/tc-app.ss | 46 ++++++++++++++----- 2 files changed, 48 insertions(+), 13 deletions(-) diff --git a/collects/tests/typed-scheme/succeed/member-pred.ss b/collects/tests/typed-scheme/succeed/member-pred.ss index 20d3b987..d1de089e 100644 --- a/collects/tests/typed-scheme/succeed/member-pred.ss +++ b/collects/tests/typed-scheme/succeed/member-pred.ss @@ -1,8 +1,19 @@ #lang typed/scheme (: foo : Any -> (U 'x 'y)) - (define (foo x) - (if (member x '(x y)) + (ann + (if (member x '(x y)) + x + 'x) + (U 'x 'y)) + + (ann + (if (memv x '(x y)) + x + 'x) + (U 'x 'y)) + + (if (memq x '(x y)) x 'x)) diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index fe5522df..834a05ac 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -32,30 +32,52 @@ ;; comparators that inform the type system (define-syntax-class comparator - #:literals (eq? equal? eqv? = string=? symbol=? memq member) - (pattern eq?) (pattern equal?) (pattern eqv?) (pattern =) (pattern string=?) (pattern symbol=?) (pattern member)) + #:literals (eq? equal? eqv? = string=? symbol=? memq member memv) + (pattern eq?) (pattern equal?) (pattern eqv?) (pattern =) (pattern string=?) (pattern symbol=?) + (pattern member) (pattern memq) (pattern memv)) ;; typecheck eq? applications ;; identifier expr expr -> tc-results (define (tc/eq comparator v1 v2) + (define (eq?-able e) (or (boolean? e) (keyword? e) (symbol? e))) + (define (eqv?-able e) (or (eq?-able e) (number? e))) + (define (equal?-able e) #t) (define (ok? val) (define-syntax-rule (alt nm pred ...) (and (free-identifier=? #'nm comparator) (or (pred val) ...))) (or (alt symbol=? symbol?) (alt string=? string?) (alt = number?) - (alt eq? boolean? keyword? symbol?) - (alt eqv? boolean? keyword? symbol? number?) - (alt equal? (lambda (x) #t)))) + (alt eq? eq?-able) + (alt eqv? eqv?-able) + (alt equal? equal?-able))) (match* ((single-value v1) (single-value v2)) [((tc-result1: t _ o) (tc-result1: (Value: (? ok? val)))) (ret -Boolean (apply-filter (make-LFilterSet (list (make-LTypeFilter (-val val) null 0)) (list (make-LNotTypeFilter (-val val) null 0))) t o))] [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o)) (ret -Boolean (apply-filter (make-LFilterSet (list (make-LTypeFilter (-val val) null 0)) (list (make-LNotTypeFilter (-val val) null 0))) t o))] [((tc-result1: t _ o) - (and (? (lambda _ (free-identifier=? #'member comparator))) - (tc-result1: (app untuple (list ts ...))))) + (and (? (lambda _ (free-identifier=? #'member comparator))) + (tc-result1: (app untuple (list (and ts (Value: _)) ...))))) (let ([ty (apply Un ts)]) - (ret -Boolean + (ret (Un (-val #f) t) + (apply-filter + (make-LFilterSet (list (make-LTypeFilter ty null 0)) + (list (make-LNotTypeFilter ty null 0))) + t o)))] + [((tc-result1: t _ o) + (and (? (lambda _ (free-identifier=? #'memv comparator))) + (tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...))))) + (let ([ty (apply Un ts)]) + (ret (Un (-val #f) t) + (apply-filter + (make-LFilterSet (list (make-LTypeFilter ty null 0)) + (list (make-LNotTypeFilter ty null 0))) + t o)))] + [((tc-result1: t _ o) + (and (? (lambda _ (free-identifier=? #'memq comparator))) + (tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...))))) + (let ([ty (apply Un ts)]) + (ret (Un (-val #f) t) (apply-filter (make-LFilterSet (list (make-LTypeFilter ty null 0)) (list (make-LNotTypeFilter ty null 0))) @@ -394,9 +416,11 @@ ;; in eq? cases, call tc/eq [(#%plain-app eq?:comparator v1 v2) ;; make sure the whole expression is type correct - (tc/funapp #'eq? #'(v1 v2) (single-value #'eq?) (map single-value (syntax->list #'(v1 v2))) expected) - ;; check thn and els with the eq? info - (tc/eq #'eq? #'v1 #'v2)] + (match* ((tc/funapp #'eq? #'(v1 v2) (single-value #'eq?) (map single-value (syntax->list #'(v1 v2))) expected) + ;; check thn and els with the eq? info + (tc/eq #'eq? #'v1 #'v2)) + [((tc-result1: t) (tc-result1: t* f o)) + (ret t f o)])] ;; special-case for not - flip the filters [(#%plain-app not arg) (match (single-value #'arg)