From 47dce89a2564a0655fc5cfe3957015aa9e9279be Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 23 Apr 2010 18:36:15 -0400 Subject: [PATCH] more progress towards let original commit: f7bf6d8a220e3d07eb27f6213273dcee5a585b46 --- .../tests/typed-scheme/succeed/simple-or.ss | 7 +++-- .../typed-scheme/env/type-environments.ss | 10 +++---- collects/typed-scheme/typecheck/tc-if.ss | 8 ++++-- .../typed-scheme/typecheck/tc-let-unit.ss | 27 ++++++++++++++----- .../typecheck/tc-metafunctions.ss | 27 ++++++++++++++----- 5 files changed, 55 insertions(+), 24 deletions(-) diff --git a/collects/tests/typed-scheme/succeed/simple-or.ss b/collects/tests/typed-scheme/succeed/simple-or.ss index daf71795..3e1cf4c0 100644 --- a/collects/tests/typed-scheme/succeed/simple-or.ss +++ b/collects/tests/typed-scheme/succeed/simple-or.ss @@ -1,9 +1,8 @@ #lang typed/scheme (define: x : Any 7) -#;(define: (f [x : (U String Number)]) : Number - (if (number? x) (add1 x) (string-length x))) +(define: (f [x : (U String Number)]) : Number 0) + +;(let ([tmp (number? x)]) (if tmp tmp (string? x))) -(let ([tmp (number? x)]) (if tmp tmp (string? x))) -#; (if (let ([tmp (number? x)]) (if tmp tmp (string? x))) (f x) 0) \ No newline at end of file diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss index d8a48855..6640e8e3 100644 --- a/collects/typed-scheme/env/type-environments.ss +++ b/collects/typed-scheme/env/type-environments.ss @@ -37,7 +37,7 @@ [(struct env (eq? l props)) (make-env eq? (filter f l) props)])) -(define (make-empty-env p?) (make env p? null null)) +(define (make-empty-env p?) (make-env p? null null)) ;; the initial type variable environment - empty ;; this is used in the parsing of types @@ -51,23 +51,23 @@ (r:d/c (env-map f e) ((pair? . -> . pair?) env? . -> . env?) - (make env (env-eq? e) (map f (env-l e)) (env-props e))) + (make-env (env-eq? e) (map f (env-l e)) (env-props e))) ;; extend that works on single arguments (define (extend e k v) (match e - [(struct env (f l p)) (make env f (cons (cons k v) l) p)] + [(struct env (f l p)) (make-env f (cons (cons k v) l) p)] [_ (int-err "extend: expected environment, got ~a" e)])) (define (extend-env ks vs e) (match e - [(struct env (f l p)) (make env f (append (map cons ks vs) l) p)] + [(struct env (f l p)) (make-env f (append (map cons ks vs) l) p)] [_ (int-err "extend-env: expected environment, got ~a" e)])) (define (replace-props e props) (match e [(struct env (f l p)) - (make env f l props)])) + (make-env f l props)])) (define (lookup e key fail) (match e diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss index 3134e838..86b06ae2 100644 --- a/collects/typed-scheme/typecheck/tc-if.ss +++ b/collects/typed-scheme/typecheck/tc-if.ss @@ -42,8 +42,12 @@ (match (single-value tst) [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _) (let*-values ([(flag+ flag-) (values (box #t) (box #t))]) - (match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) (list fs+) flag+) (tc thn (unbox flag+)))] - [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) (list fs-) flag-) (tc els (unbox flag-)))]) + (match-let* ([env-thn (env+ (lexical-env) (list fs+) flag+)] + [env-els (env+ (lexical-env) (list fs-) flag-)] + [new-thn-props (env-props env-thn)] + [new-els-props (env-props env-els)] + [(tc-results: ts fs2 os2) (with-lexical-env env-thn (tc thn (unbox flag+)))] + [(tc-results: us fs3 os3) (with-lexical-env env-els (tc els (unbox flag-)))]) ;; if we have the same number of values in both cases (cond [(= (length ts) (length us)) (let ([r (combine-results diff --git a/collects/typed-scheme/typecheck/tc-let-unit.ss b/collects/typed-scheme/typecheck/tc-let-unit.ss index 506c1003..61ba6194 100644 --- a/collects/typed-scheme/typecheck/tc-let-unit.ss +++ b/collects/typed-scheme/typecheck/tc-let-unit.ss @@ -5,8 +5,9 @@ (types utils convenience) (private type-annotation parse-type) (env lexical-env type-alias-env type-env type-environments) + (rep type-rep) syntax/free-vars - mzlib/trace + mzlib/trace unstable/debug scheme/match (prefix-in c: scheme/contract) (except-in scheme/contract -> ->* one-of/c) syntax/kerncase syntax/parse @@ -26,17 +27,29 @@ syntax? (listof syntax?) syntax? (listof syntax?) (or/c #f tc-results?) . c:-> . tc-results?) - (define-values (types props) - (for/lists (t p) - ([r (in-list results)]) - (match r [(tc-results: ts fs os) (values ts null)]))) - ;; extend the lexical environment for checking the body + (w/c t/p ([types (listof (listof Type/c))] + [props (listof (listof Filter?))]) + (define-values (types props) + (for/lists (t p) + ([r (in-list results)] + [names (in-list namess)]) + (match r + [(tc-results: ts (FilterSet: fs+ fs-) os) + (values ts + (for/list ([n names] + [f+ fs+] + [f- fs-]) + (-and (make-ImpFilter (make-NotTypeFilter (-val #f) null n) f+) + (make-ImpFilter (make-TypeFilter (-val #f) null n) f-))))])))) + ;; extend the lexical environment for checking the body (with-lexical-env/extend/props ;; the list of lists of name namess ;; the types types - (append (apply append props) (env-props (lexical-env))) + (w/c append-region + #:result (listof Filter?) + (append (apply append props) (env-props (lexical-env)))) (for-each expr->type clauses exprs diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index 1399f717..3cb72f67 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -6,7 +6,7 @@ [->* -->*] [one-of/c -one-of/c]) (rep type-rep filter-rep rep-utils) scheme/list - scheme/contract scheme/match unstable/match + scheme/contract scheme/match unstable/match scheme/trace (for-syntax scheme/base)) ;(provide (all-defined-out)) @@ -90,21 +90,29 @@ (provide combine-props tc-results->values) -(define (resolve atoms prop) + +(d/c (resolve atoms prop) + ((listof Filter/c) + Filter/c + . -> . + Filter/c) (for/fold ([prop prop]) ([a (in-list atoms)]) (match prop [(AndFilter: ps) (let loop ([ps ps] [result null]) (if (null? ps) - (-and result) + (apply -and result) (let ([p (car ps)]) (cond [(opposite? a p) -bot] [(implied-atomic? p a) (loop (cdr ps) result)] [else (loop (cdr ps) (cons p result))]))))] [_ prop]))) -(define (combine-props new-props old-props flag) +(d/c (combine-props new-props old-props flag) + ((listof Filter/c) (listof Filter/c) (box/c boolean?) + . -> . + (values (listof (or/c ImpFilter? OrFilter? AndFilter?)) (listof (or/c TypeFilter? NotTypeFilter?)))) (define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p))) (define-values (new-atoms new-formulas) (partition atomic-prop? new-props)) (let loop ([derived-props null] @@ -116,8 +124,11 @@ [p (resolve derived-atoms p)]) (match p [(AndFilter: ps) (loop derived-props derived-atoms (append ps (cdr worklist)))] - [(TypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))] - [(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))] + [(ImpFilter: a c) + (if (for/or ([p (append derived-props derived-atoms)]) + (implied-atomic? a p)) + (loop derived-props derived-atoms (cons c (cdr worklist))) + (loop (cons p derived-props) derived-atoms (cdr worklist)))] [(OrFilter: ps) (let ([new-or (let or-loop ([ps ps] [result null]) @@ -133,6 +144,10 @@ (if (OrFilter? new-or) (loop (cons new-or derived-props) derived-atoms (cdr worklist)) (loop derived-props derived-atoms (cons new-or (cdr worklist)))))] + [(TypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))] + [(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))] [(Top:) (loop derived-props derived-atoms (cdr worklist))] [(Bot:) (set-box! flag #f) (values derived-props derived-atoms)] [_ (loop (cons p derived-props) derived-atoms (cdr worklist))]))))) + +