diff --git a/collects/typed-racket/typecheck/signatures.rkt b/collects/typed-racket/typecheck/signatures.rkt index 6b2035e4..0eeb9e82 100644 --- a/collects/typed-racket/typecheck/signatures.rkt +++ b/collects/typed-racket/typecheck/signatures.rkt @@ -49,6 +49,10 @@ (define-signature tc-app-objects^ ([cond-contracted tc/app-objects (syntax? (or/c #f tc-results?). -> . (or/c #f tc-results?))])) +(define-signature tc-app-eq^ + ([cond-contracted tc/app-eq (syntax? (or/c #f tc-results?). -> . (or/c #f tc-results?))])) + + (define-signature tc-apply^ ([cond-contracted tc/apply (syntax? syntax? . -> . tc-results?)])) diff --git a/collects/typed-racket/typecheck/tc-app.rkt b/collects/typed-racket/typecheck/tc-app.rkt index 6527d82b..bd73e4c7 100644 --- a/collects/typed-racket/typecheck/tc-app.rkt +++ b/collects/typed-racket/typecheck/tc-app.rkt @@ -28,56 +28,10 @@ (import tc-expr^ tc-lambda^ tc-let^ tc-apply^ tc-app-keywords^ tc-app-hetero^ tc-app-list^ tc-app-apply^ tc-app-values^ - tc-app-objects^) + tc-app-objects^ tc-app-eq^) (export tc-app^) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Comparators - -;; comparators that inform the type system -(define-syntax-class comparator - #: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) (eof-object? 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 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 - (-FS (-filter-at (-val val) o) - (-not-filter-at (-val val) o)))] - [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o)) - (ret -Boolean - (-FS (-filter-at (-val val) o) - (-not-filter-at (-val val) o)))] - [((tc-result1: t _ o) - (or (and (? (lambda _ (free-identifier=? #'member comparator))) - (tc-result1: (app untuple (list (and ts (Value: _)) ...)))) - (and (? (lambda _ (free-identifier=? #'memv comparator))) - (tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...)))) - (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) - (-FS (-filter-at ty o) - (-not-filter-at ty o))))] - [(_ _) (ret -Boolean)])) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; let loop @@ -145,6 +99,7 @@ (tc/app-values form expected) (tc/app-keywords form expected) (tc/app-objects form expected) + (tc/app-eq form expected) (syntax-parse form #:literals (#%plain-app #%plain-lambda letrec-values quote not false? list @@ -180,15 +135,6 @@ Univ))) (list (ret Univ) (single-value #'arg)) expected)])] - ;; in eq? cases, call tc/eq - [(#%plain-app eq?:comparator v1 v2) - ;; make sure the whole expression is type correct - (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 (~or false? not) arg) (match (single-value #'arg) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-eq.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-eq.rkt new file mode 100644 index 00000000..090e99d0 --- /dev/null +++ b/collects/typed-racket/typecheck/tc-app/tc-app-eq.rkt @@ -0,0 +1,69 @@ +#lang racket/unit + +(require "../../utils/utils.rkt" + syntax/parse racket/match + (typecheck signatures tc-app-helper tc-funapp check-below) + (types abbrev union utils) + (rep type-rep) + + (for-template racket/base)) + +(import tc-expr^) +(export tc-app-eq^) + +;; comparators that inform the type system +(define-syntax-class comparator + #: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)) + +(define (tc/app-eq form expected) + (syntax-parse form + #:literals (#%plain-app) + [(#%plain-app eq?:comparator v1 v2) + ;; make sure the whole expression is type correct + (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)])] + [_ #f])) + +;; 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) (eof-object? 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 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 + (-FS (-filter-at (-val val) o) + (-not-filter-at (-val val) o)))] + [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o)) + (ret -Boolean + (-FS (-filter-at (-val val) o) + (-not-filter-at (-val val) o)))] + [((tc-result1: t _ o) + (or (and (? (lambda _ (free-identifier=? #'member comparator))) + (tc-result1: (app untuple (list (and ts (Value: _)) ...)))) + (and (? (lambda _ (free-identifier=? #'memv comparator))) + (tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...)))) + (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) + (-FS (-filter-at ty o) + (-not-filter-at ty o))))] + [(_ _) (ret -Boolean)])) + + diff --git a/collects/typed-racket/typecheck/typechecker.rkt b/collects/typed-racket/typecheck/typechecker.rkt index 77f4ce55..491ab8dd 100644 --- a/collects/typed-racket/typecheck/typechecker.rkt +++ b/collects/typed-racket/typecheck/typechecker.rkt @@ -7,6 +7,7 @@ define-values/invoke-unit/infer link) "signatures.rkt" "tc-app/tc-app-apply.rkt" + "tc-app/tc-app-eq.rkt" "tc-app/tc-app-hetero.rkt" "tc-app/tc-app-keywords.rkt" "tc-app/tc-app-list.rkt" @@ -22,4 +23,4 @@ (define-values/invoke-unit/infer (link tc-if@ tc-lambda@ tc-app@ tc-let@ tc-expr@ check-subforms@ tc-apply@ tc-app-hetero@ tc-app-list@ tc-app-apply@ tc-app-values@ tc-app-keywords@ - tc-app-objects@)) + tc-app-objects@ tc-app-eq@))