From 6b89062d6a2e6b35fb24c71d7f0fb839d49546b1 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 5 May 2009 16:27:18 +0000 Subject: [PATCH] Various constants are true. Remove useless code. `combine-filter' now handles producing the new type/object in appropriate cases. Move student expansion later in pattern match. Print out top-level tc-results. svn: r14721 --- .../typed-scheme/typecheck/tc-expr-unit.ss | 9 +++--- .../typed-scheme/typecheck/tc-lambda-unit.ss | 2 +- .../typecheck/tc-metafunctions.ss | 22 +++++++------- collects/typed-scheme/typecheck/tc-new-if.ss | 12 ++++---- collects/typed-scheme/typed-scheme.ss | 5 ++-- collects/typed-scheme/types/utils.ss | 30 +++++++++++-------- 6 files changed, 42 insertions(+), 38 deletions(-) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index 468aa19dee..03baae8c33 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -188,9 +188,9 @@ [(quote #t) (ret (-val #t) true-filter)] [(quote val) (match expected [(tc-result1: t) - (ret (tc-literal #'val t))])] + (ret (tc-literal #'val t) true-filter)])] ;; syntax - [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))] + [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) true-filter)] ;; mutation! [(set! id val) (match-let* ([(tc-result: id-t) (tc-expr #'id)] @@ -273,9 +273,9 @@ [(quote #f) (ret (-val #f) false-filter)] [(quote #t) (ret (-val #t) true-filter)] - [(quote val) (ret (tc-literal #'val))] + [(quote val) (ret (tc-literal #'val) true-filter)] ;; syntax - [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))] + [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) true-filter)] ;; w-c-m [(with-continuation-mark e1 e2 e3) (begin (tc-expr/check/type #'e1 Univ) @@ -315,7 +315,6 @@ ;; application [(#%plain-app . _) (tc/app form)] ;; if - [(if tst body) (tc/if-twoarm #'tst #'body #'(#%app void))] [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els)] diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss index 1e255f0f44..6119c29fc5 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -277,7 +277,7 @@ (define (tc/lambda/internal form formals bodies expected) (if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected)) (ret (tc/plambda form formals bodies expected)) - (ret (tc/mono-lambda/type formals bodies expected)))) + (ret (tc/mono-lambda/type formals bodies expected) true-filter))) ;; tc/lambda : syntax syntax-list syntax-list -> tc-result (define (tc/lambda form formals bodies) diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index d0dfda98b6..1a7ca3b9e9 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -118,28 +118,30 @@ (define-match-expander F-FS: (lambda (stx) #'(FilterSet: (list (Bot:)) _))) -(d/c (combine-filter f1 f2 f3) - (FilterSet? FilterSet? FilterSet? . -> . FilterSet?) +(d/c (combine-filter f1 f2 f3 t2 t3 o2 o3) + (FilterSet? FilterSet? FilterSet? Type? Type? Object? Object? . -> . tc-results?) + (define (mk f) (ret (Un t2 t3) f (make-Empty))) (match* (f1 f2 f3) - [(f (T-FS:) (F-FS:)) f] ;; the student expansion - [((T-FS:) f _) f] - [((F-FS:) _ f) f] + [((T-FS:) f _) (ret t2 f o2)] + [((F-FS:) _ f) (ret t3 f o3)] ;; skipping the general or/predicate rule because it's really complicated ;; or/predicate special case for one elem lists ;; note that we are relying on equal? on identifiers here [((FilterSet: (list (TypeFilter: t pi x)) (list (NotTypeFilter: t pi x))) (T-FS:) (FilterSet: (list (TypeFilter: s pi x)) (list (NotTypeFilter: s pi x)))) - (make-FilterSet (list (make-TypeFilter (Un t s) pi x)) (list (make-NotTypeFilter (Un t s) pi x)))] + (mk (make-FilterSet (list (make-TypeFilter (Un t s) pi x)) (list (make-NotTypeFilter (Un t s) pi x))))] ;; or - [((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (combine null (append f1- f3-))] + [((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (mk (combine null (append f1- f3-)))] ;; and [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:)) - (combine (append f1+ f2+) null)] - [(f f* f*) f*] + (mk (combine (append f1+ f2+) null))] + [(f f* f*) (mk f*)] + ;; the student expansion + [(f (T-FS:) (F-FS:)) (mk f)] [(_ _ _) ;; could intersect f2 and f3 here - (make-FilterSet null null)])) + (mk (make-FilterSet null null))])) ;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results? (define (values->tc-results tc formals) diff --git a/collects/typed-scheme/typecheck/tc-new-if.ss b/collects/typed-scheme/typecheck/tc-new-if.ss index 6970804c43..6d6bc87be9 100644 --- a/collects/typed-scheme/typecheck/tc-new-if.ss +++ b/collects/typed-scheme/typecheck/tc-new-if.ss @@ -20,15 +20,15 @@ (define (tc/if-twoarm tst thn els [expected #f]) (define (tc e) (if expected (tc-expr/check e expected) (tc-expr e))) - (match (tc-expr tst) + (match (single-value tst) [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _) - (match-let ([(tc-results: ts fs2 _) (with-lexical-env (env+ (lexical-env) fs+) (tc thn))] - [(tc-results: us fs3 _) (with-lexical-env (env+ (lexical-env) fs-) (tc els))]) + (match-let ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+) (tc thn))] + [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs-) (tc els))]) ;; if we have the same number of values in both cases (cond [(= (length ts) (length us)) - (ret (for/list ([t ts] [u us]) (Un t u)) - (for/list ([f2 fs2] [f3 fs3]) - (combine-filter f1 f2 f3)))] + (combine-results + (for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3]) + (combine-filter f1 f2 f3 t u o2 o3)))] [else (tc-error/expr #:return (ret Err) "Expected the same number of values from both branches of if expression, but got ~a and ~a" diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss index 72053d9b05..49d1ea97cf 100644 --- a/collects/typed-scheme/typed-scheme.ss +++ b/collects/typed-scheme/typed-scheme.ss @@ -130,9 +130,8 @@ body2] [_ (let ([ty-str (match type [(tc-result1: (? (lambda (t) (type-equal? t -Void)))) #f] - [(tc-result1: t) - (format "- : ~a\n" t)] - [(tc-results: ts) (format "- : ~a\n" (cons 'values ts))] + [(tc-results: t) + (format "- : ~a\n" type)] [x (int-err "bad type result: ~a" x)])]) (if #'ty-str #`(let ([type '#,ty-str]) diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss index b7ad8b71de..da45eab2f5 100644 --- a/collects/typed-scheme/types/utils.ss +++ b/collects/typed-scheme/types/utils.ss @@ -30,7 +30,8 @@ just-Dotted? tc-error/expr lookup-fail - lookup-type-fail) + lookup-type-fail + combine-results) ;; substitute : Type Name Type -> Type @@ -190,17 +191,15 @@ ;; convenience function for returning the result of typechecking an expression (define ret - (case-lambda [(t) - (make-tc-results - (cond [(Type? t) - (list (make-tc-result t (make-FilterSet null null) (make-Empty)))] - [(or (Values? t) (ValuesDots? t)) - (int-err "Values in ret: ~a" t) - #;(values->tc-results t)] - [else - (for/list ([i t]) - (make-tc-result i (make-FilterSet null null) (make-Empty)))]) - #f)] + (case-lambda [(t) + (let ([mk (lambda (t) (make-FilterSet null null))]) + (make-tc-results + (cond [(Type? t) + (list (make-tc-result t (mk t) (make-Empty)))] + [else + (for/list ([i t]) + (make-tc-result i (mk t) (make-Empty)))]) + #f))] [(t f) (make-tc-results (if (Type? t) @@ -225,7 +224,7 @@ (p/c [ret - (->d ([t (or/c Type/c (listof Type/c) Values? ValuesDots?)]) + (->d ([t (or/c Type/c (listof Type/c))]) ([f (if (list? t) (listof FilterSet?) FilterSet?)] @@ -236,6 +235,11 @@ [dbound symbol?]) [_ tc-results?])]) +(define (combine-results tcs) + (match tcs + [(list (tc-result1: t f o) ...) + (ret t f o)])) + (define (subst v t e) (substitute t v e))