more progress towards let

original commit: f7bf6d8a220e3d07eb27f6213273dcee5a585b46
This commit is contained in:
Sam Tobin-Hochstadt 2010-04-23 18:36:15 -04:00
parent f50ace2729
commit 47dce89a25
5 changed files with 55 additions and 24 deletions

View File

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

View File

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

View File

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

View File

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

View File

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