more progress towards let

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
+(define: (f [x : (U String Number)]) : Number 0)
-  (if (number? x) (add1 x) (string-length x)))
+
+;(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)

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

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+)))]
+       (match-let* ([env-thn (env+ (lexical-env) (list fs+) flag+)]
-                    [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) (list fs-) flag-) (tc els (unbox 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

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)
+     (w/c t/p ([types (listof (listof Type/c))]
-       (for/lists (t p) 
+               [props (listof (listof Filter?))])
-         ([r (in-list results)])
+          (define-values (types props)
-         (match r [(tc-results: ts fs os) (values ts null)])))     
+            (for/lists (t p) 
-  ;; extend the lexical environment for checking the body
+              ([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 

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))]
+            [(ImpFilter: a c)
-            [(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
+             (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))])))))
+
+