progress towards let

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)

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)

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
+(define-syntax-rule (with-lexical-env e . b)
-  (syntax-rules ()
+  (parameterize ([lexical-env e]) . b))
-    [(_ e . b) (parameterize ([lexical-env e]) . b)]))
 
 ;; run code in an extended env
-(define-syntax with-lexical-env/extend
+(define-syntax-rule (with-lexical-env/extend is ts . b)
-  (syntax-rules ()
+  (with-lexical-env (extend/values is ts (lexical-env)) . b))
-    [(_ is ts . b) (parameterize ([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

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))) Γ)]

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)))

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) 
+                  (get-type/infer name e (tc-expr-t/maybe-expected expected) 
-                                         tc-expr/check)
+                                         tc-expr/check))]
-                    [(tc-results: ts) ts]))]
          ;; 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)))
 
 

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))
@@ -110,10 +137,7 @@
         (match result
           [(list) -bot]
           [(list f) f]
-          [(or (list f1 (AndFilter: fs))
+          [_ (distribute (compact result))])
-               (list (AndFilter: fs) f1))
-           (apply -and (for/list ([f (in-list fs)]) (-or f1 f)))]
-          [_ (distribute result)])
         (match (car fs)
           [(and t (Top:)) t]
           [(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]