suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

use of member, memq, memv as predicates working properly

Browse Source 
svn: r17568

original commit: 05a0e722f9b64d0d53fb5b168181b467a4711ec7
This commit is contained in:
Sam Tobin-Hochstadt 2010-01-08 15:55:32 +00:00
parent 9e17eab6d8
commit 9364f5b9cc
2 changed files with 48 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
collects/tests/typed-scheme/succeed/member-pred.ss
View File

@ -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))

46
collects/typed-scheme/typecheck/tc-app.ss
View File

@ -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)