From 788630d26a479363f8abe244f70a9b36c107ebab Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 23 Apr 2010 16:40:05 -0400 Subject: [PATCH] progress towards let --- .../typed-scheme/succeed/simple-fake-or.ss | 10 +++++ .../tests/typed-scheme/succeed/simple-or.ss | 5 ++- collects/typed-scheme/env/lexical-env.ss | 17 +++++---- collects/typed-scheme/typecheck/tc-envops.ss | 2 +- collects/typed-scheme/typecheck/tc-if.ss | 2 +- .../typed-scheme/typecheck/tc-let-unit.ss | 30 ++++++++++----- collects/typed-scheme/types/convenience.ss | 38 +++++++++++++++---- 7 files changed, 77 insertions(+), 27 deletions(-) create mode 100644 collects/tests/typed-scheme/succeed/simple-fake-or.ss diff --git a/collects/tests/typed-scheme/succeed/simple-fake-or.ss b/collects/tests/typed-scheme/succeed/simple-fake-or.ss new file mode 100644 index 0000000000..5621e8cd25 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/simple-fake-or.ss @@ -0,0 +1,10 @@ +#lang typed/scheme + +(define: x : Any 7) +(define: (f [x : (U String Number)]) : Number + (if (number? x) (add1 x) (string-length x))) +(if (if (number? x) + #t + (string? x)) + (f x) + 0) diff --git a/collects/tests/typed-scheme/succeed/simple-or.ss b/collects/tests/typed-scheme/succeed/simple-or.ss index c7504a951d..daf71795be 100644 --- a/collects/tests/typed-scheme/succeed/simple-or.ss +++ b/collects/tests/typed-scheme/succeed/simple-or.ss @@ -1,6 +1,9 @@ #lang typed/scheme (define: x : Any 7) -(define: (f [x : (U String Number)]) : Number +#;(define: (f [x : (U String Number)]) : Number (if (number? x) (add1 x) (string-length 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/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss index cd3d896c6e..a48332d665 100644 --- a/collects/typed-scheme/env/lexical-env.ss +++ b/collects/typed-scheme/env/lexical-env.ss @@ -10,7 +10,8 @@ (typecheck tc-metafunctions) (except-in (types utils convenience) -> ->*)) -(provide lexical-env with-lexical-env with-lexical-env/extend with-update-type/lexical) +(provide lexical-env with-lexical-env with-lexical-env/extend with-update-type/lexical + with-lexical-env/extend/props) (p/c [lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))] [update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (env?) . ->* . env?)]) @@ -19,14 +20,16 @@ (define lexical-env (make-parameter (make-empty-env free-identifier=?))) ;; run code in a new env -(define-syntax with-lexical-env - (syntax-rules () - [(_ e . b) (parameterize ([lexical-env e]) . b)])) +(define-syntax-rule (with-lexical-env e . b) + (parameterize ([lexical-env e]) . b)) ;; run code in an extended env -(define-syntax with-lexical-env/extend - (syntax-rules () - [(_ is ts . b) (parameterize ([lexical-env (extend/values is ts (lexical-env))]) . b)])) +(define-syntax-rule (with-lexical-env/extend is ts . b) + (with-lexical-env (extend/values is ts (lexical-env)) . b)) + +;; run code in an extended env and with replaced props +(define-syntax-rule (with-lexical-env/extend/props is ts ps . b) + (with-lexical-env (replace-props (extend/values is ts (lexical-env)) ps) . b)) ;; find the type of identifier i, looking first in the lexical env, then in the top-level env ;; identifer -> Type diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index e3d94c7d6b..9b4a315d29 100644 --- a/collects/typed-scheme/typecheck/tc-envops.ss +++ b/collects/typed-scheme/typecheck/tc-envops.ss @@ -65,7 +65,7 @@ ;; sets the flag box to #f if anything becomes (U) (d/c (env+ env fs flag) (env? (listof Filter/c) (box/c #t). -> . env?) - (define-values (imps atoms) (debug combine-props fs (env-props env) flag)) + (define-values (imps atoms) (combine-props fs (env-props env) flag)) (for/fold ([Γ (replace-props env imps)]) ([f atoms]) (match f [(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)] diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss index 9dd2af54ca..3134e838e4 100644 --- a/collects/typed-scheme/typecheck/tc-if.ss +++ b/collects/typed-scheme/typecheck/tc-if.ss @@ -60,7 +60,7 @@ [type (Un t2 t3)] [object (if (object-equal? o2 o3) o2 (make-Empty))]) ;(printf "result filter is: ~a\n" filter) - (ret type filter object))))]) + (debug ret type filter object))))]) (if expected (check-below r expected) r))] ;; special case if one of the branches is unreachable [(and (= 1 (length us)) (type-equal? (car us) (Un))) diff --git a/collects/typed-scheme/typecheck/tc-let-unit.ss b/collects/typed-scheme/typecheck/tc-let-unit.ss index 513d50e766..506c10035d 100644 --- a/collects/typed-scheme/typecheck/tc-let-unit.ss +++ b/collects/typed-scheme/typecheck/tc-let-unit.ss @@ -4,10 +4,11 @@ (require "signatures.ss" "tc-metafunctions.ss" (types utils convenience) (private type-annotation parse-type) - (env lexical-env type-alias-env type-env) + (env lexical-env type-alias-env type-env type-environments) syntax/free-vars mzlib/trace - scheme/match + scheme/match (prefix-in c: scheme/contract) + (except-in scheme/contract -> ->* one-of/c) syntax/kerncase syntax/parse (for-template scheme/base @@ -19,17 +20,27 @@ (import tc-expr^) (export tc-let^) -(define (do-check expr->type namess types form exprs body clauses expected) +(d/c (do-check expr->type namess results form exprs body clauses expected) + ((syntax? syntax? tc-results? . c:-> . any/c) + (listof (listof identifier?)) (listof tc-results?) + 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 - (with-lexical-env/extend + (with-lexical-env/extend/props ;; the list of lists of name namess ;; the types types + (append (apply append props) (env-props (lexical-env))) (for-each expr->type clauses exprs - (map ret types)) + results) (if expected (tc-exprs/check (syntax->list body) expected) (tc-exprs (syntax->list body))))) @@ -85,7 +96,7 @@ [else ;(for-each (lambda (vs) (for-each (lambda (v) (printf/log "Letrec Var: ~a~n" (syntax-e v))) vs)) names) (do-check (lambda (stx e t) (tc-expr/check e t)) - names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)])))) + names (map (lambda (l) (map (compose ret get-type) l)) names) form exprs body clauses expected)])))) ;; this is so match can provide us with a syntax property to ;; say that this binding is only called in tail position @@ -108,11 +119,10 @@ #;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)] ;; the annotated types of the name (possibly using the inferred types) [types (for/list ([name names] [e exprs]) - (match (get-type/infer name e (tc-expr-t/maybe-expected expected) - tc-expr/check) - [(tc-results: ts) ts]))] + (get-type/infer name e (tc-expr-t/maybe-expected expected) + tc-expr/check))] ;; the clauses for error reporting [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])]) - (do-check void names types form types body clauses expected))) + (do-check void names types form exprs body clauses expected))) diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss index 357276a0f5..09ca8fe00d 100644 --- a/collects/typed-scheme/types/convenience.ss +++ b/collects/typed-scheme/types/convenience.ss @@ -1,12 +1,13 @@ #lang scheme/base (require "../utils/utils.ss" - (rep type-rep filter-rep object-rep) + (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) "abbrev.ss" (only-in scheme/contract current-blame-format) (types comparison printer union subtype utils) scheme/list scheme/match scheme/promise (for-syntax syntax/parse scheme/base) - unstable/debug + unstable/debug syntax/id-table scheme/dict + scheme/trace (for-template scheme/base)) (provide (all-defined-out) @@ -97,6 +98,32 @@ (subtype t1 t2))] [(_ _) #f]))) +(define (compact props) + (define tf-map (make-hash)) + (define ntf-map (make-hash)) + (let loop ([props props] [others null]) + (if (null? props) + (append others + (for/list ([v (in-dict-values tf-map)]) v) + (for/list ([v (in-dict-values ntf-map)]) v)) + (match (car props) + [(and p (TypeFilter: t1 f1 x)) + (hash-update! tf-map + (list f1 (hash-id x)) + (match-lambda [(TypeFilter: t2 _ _) (make-TypeFilter (Un t1 t2) f1 x)] + [p (int-err "got something that isn't a typefilter ~a" p)]) + p) + (loop (cdr props) others)] + #; + [(and p (NotTypeFilter: t1 f1 x)) + (hash-update! ntf-map + (list f1 (hash-id x)) + (match-lambda [(NotTypeFilter: t2 _ _) (make-NotTypeFilter (restrict t1 t2) f1 x)] + [p (int-err "got something that isn't a nottypefilter ~a" p)]) + p) + (loop (cdr props) others)] + [p (loop (cdr props) (cons p others))])))) + (define (-or . args) (define (distribute args) (define-values (ands others) (partition AndFilter? args)) @@ -104,16 +131,13 @@ (make-OrFilter others) (match-let ([(AndFilter: elems) (car ands)]) (apply -and (for/list ([a (in-list elems)]) - (apply -or a (append (cdr ands) others))))))) + (apply -or a (append (cdr ands) others))))))) (let loop ([fs args] [result null]) (if (null? fs) (match result [(list) -bot] [(list f) f] - [(or (list f1 (AndFilter: fs)) - (list (AndFilter: fs) f1)) - (apply -and (for/list ([f (in-list fs)]) (-or f1 f)))] - [_ (distribute result)]) + [_ (distribute (compact result))]) (match (car fs) [(and t (Top:)) t] [(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]