From 4edd8ce157e0e992fd28be66299a23e28fc894d8 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Mon, 24 Mar 2014 00:44:57 -0700 Subject: [PATCH] Use filters when typechecking using tc-body. Closes PR 11920. original commit: dd8b646b0b3a0fd7905467f275f0f786eac958dd --- .../typed-racket/typecheck/tc-expr-unit.rkt | 39 ++++++++++++++----- .../typed-racket/types/filter-ops.rkt | 19 +++++++++ .../unit-tests/typecheck-tests.rkt | 28 +++++++++++++ 3 files changed, 77 insertions(+), 9 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt index 7ca43f07..6d753636 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt @@ -5,17 +5,17 @@ racket/match (prefix-in - (contract-req)) "signatures.rkt" "check-below.rkt" "tc-app-helper.rkt" "../types/kw-types.rkt" - (types utils abbrev union subtype type-table classes) + (types utils abbrev union subtype type-table classes filter-ops) (private-in parse-type type-annotation syntax-properties) (rep type-rep filter-rep object-rep) (utils tc-utils) (env lexical-env tvar-env index-env) - racket/format + racket/format racket/list racket/private/class-internal syntax/parse syntax/stx unstable/syntax (only-in racket/list split-at) - (typecheck internal-forms) + (typecheck internal-forms tc-envops) ;; Needed for current implementation of typechecking letrec-syntax+values (for-template (only-in racket/base letrec-values)) @@ -519,6 +519,23 @@ #:stx form "expected single value, got multiple (or zero) values")])) + +;; check-body-form: (All (A) (syntax? (-> A) -> A)) +;; Checks an expression and then calls the function in a context with an extended lexical environment. +;; The environment is extended with the propositions that are true if the expression returns +;; (e.g. instead of raising an error). +(define (check-body-form e k) + (define results (tc-expr/check e tc-any-results)) + (define props + (match results + [(tc-any-results:) empty] + [(tc-results: _ (FilterSet: f+ f-) _) + (map -or f+ f-)] + [(tc-results: _ (FilterSet: f+ f-) _ _ _) + (map -or f+ f-)])) + (with-lexical-env (env+ (lexical-env) props (box #t)) + (add-unconditional-prop (k) (apply -and props)))) + ;; type-check a body of exprs, producing the type of the last one. ;; if the body is empty, the type is Void. ;; syntax[list[expr]] -> tc-results/c @@ -526,14 +543,18 @@ (match (syntax->list body) [(list) (ret -Void)] [(list es ... e-final) - (for ((e es)) - (tc-expr/check e tc-any-results)) - (tc-expr e-final)])) + (define ((continue es)) + (if (empty? es) + (tc-expr e-final) + (check-body-form (first es) (continue (rest es))))) + ((continue es))])) (define (tc-body/check body expected) (match (syntax->list body) [(list) (check-below (ret -Void) expected)] [(list es ... e-final) - (for ((e es)) - (tc-expr/check e tc-any-results)) - (tc-expr/check e-final expected)])) + (define ((continue es)) + (if (empty? es) + (tc-expr/check e-final expected) + (check-body-form (first es) (continue (rest es))))) + ((continue es))])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt index c02e1bcd..6fb3ca29 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt @@ -207,6 +207,25 @@ [else (loop (cdr fs) (cons t result))])])))) +;; add-unconditional-prop: tc-results? Filter/c? -> tc-results? +;; Ands the given proposition to the filters in the tc-results. +;; Useful to express properties of the form: if this expressions returns at all, we learn this +(define (add-unconditional-prop results prop) + (match results + ;; TODO add support for filters on tc-any-results + [(tc-any-results:) results] + [(tc-results: ts (FilterSet: fs+ fs-) os) + (ret ts + (for/list ([f+ fs+] [f- fs-]) + (-FS (-and prop f+) (-and prop f-))) + os)] + [(tc-results: ts (FilterSet: fs+ fs-) os dty dbound) + (ret ts + (for/list ([f+ fs+] [f- fs-]) + (-FS (-and prop f+) (-and prop f-))) + os)])) + + ;; ands the given type filter to both sides of the given arr for each argument ;; useful to express properties of the form: if this function returns at all, ;; we learn this about its arguments (like fx primitives, or car/cdr, etc.) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index 9c791bc7..2b61b084 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -2667,6 +2667,34 @@ (number? x)) -Boolean] + [tc-e + (let () + (: g (Any -> Boolean : #:+ (Number @ 0) #:- Bot)) + (define (g x) + (or (number? x) + (g x))) + (: x Any) + (define x 0) + (g x) + (add1 x)) + -Number] + + [tc-e + (let: ([x : Any 1]) + (unless (number? x) + (error 'foo)) + (add1 x)) + -Number] + + [tc-e + (let: ([x : Any 1]) + (let () + (unless (number? x) + (error 'foo)) + #t) + (add1 x)) + -Number] + [tc-e/t (let () (: f (Number -> Number))