everything but or and implies works

original commit: 0804e64695ab0d04a8db1d1f95e1fc8f14b32217
This commit is contained in:
Sam Tobin-Hochstadt 2010-04-21 18:13:13 -04:00
commit 88ae88c901
10 changed files with 25 additions and 28 deletions

View File

@ -12,7 +12,7 @@
(only-in '#%kernel [apply kernel:apply])
scheme/promise scheme/system
(only-in string-constants/private/only-once maybe-print-message)
(only-in scheme/match/runtime match:error matchable? match-equality-test)
(only-in racket/match/runtime match:error matchable? match-equality-test)
(for-template scheme)
(rename-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Nat -Nat*]))

View File

@ -11,7 +11,7 @@
(only-in '#%kernel [apply kernel:apply])
scheme/promise scheme/system
(only-in string-constants/private/only-once maybe-print-message)
(only-in scheme/match/runtime match:error matchable? match-equality-test)
(only-in racket/match/runtime match:error matchable? match-equality-test)
(for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-ExactPositiveInteger -Pos])))
(define-for-syntax all-num-types (list -Pos -Nat -Integer -ExactRational -Flonum -Real N))

View File

@ -12,7 +12,7 @@
scheme/promise scheme/system
(only-in string-constants/private/only-once maybe-print-message)
(only-in mzscheme make-namespace)
(only-in scheme/match/runtime match:error matchable? match-equality-test)
(only-in racket/match/runtime match:error matchable? match-equality-test)
(for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])
(only-in (rep type-rep) make-HashtableTop make-MPairTop make-BoxTop make-VectorTop)))

View File

@ -7,7 +7,7 @@
(only-in scheme/list cons? take drop add-between last filter-map)
(only-in rnrs/lists-6 fold-left)
'#%paramz
(only-in scheme/match/runtime match:error)
(only-in racket/match/runtime match:error)
scheme/promise
string-constants/string-constant
;(prefix-in ce: test-engine/scheme-tests)

View File

@ -9,7 +9,7 @@
"extra-procs.ss"
"prims.ss"
"base-types.ss"
scheme/contract/regions scheme/contract/base
racket/contract/regions racket/contract/base
(for-syntax
"base-types-extra.ss"
unstable/debug

View File

@ -9,7 +9,7 @@
(private typed-renaming)
(rep type-rep)
(utils tc-utils)
scheme/contract/private/provide unstable/list
racket/contract/private/provide unstable/list
unstable/debug
unstable/syntax scheme/struct-info scheme/match
"def-binding.ss" syntax/parse)

View File

@ -8,7 +8,7 @@
unstable/sequence
;; fixme - don't need to be bound in this phase - only to make syntax/parse happy
scheme/bool
(only-in scheme/private/class-internal make-object do-make-object)
(only-in racket/private/class-internal make-object do-make-object)
(only-in '#%kernel [apply k:apply])
;; end fixme
(for-syntax syntax/parse scheme/base (utils tc-utils))
@ -22,7 +22,7 @@
(for-template
(only-in '#%kernel [apply k:apply])
"internal-forms.ss" scheme/base scheme/bool
(only-in scheme/private/class-internal make-object do-make-object)))
(only-in racket/private/class-internal make-object do-make-object)))
(import tc-expr^ tc-lambda^ tc-dots^ tc-let^)
(export tc-app^)

View File

@ -69,12 +69,12 @@
(for/fold ([Γ (replace-props env imps)]) ([f atoms])
(match f
[(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
[(ImpFilter: _ _) Γ]
[(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
(update-type/lexical (lambda (x t) (let ([new-t (update t f)])
(when (type-equal? new-t (Un))
(set-box! flag #f))
new-t))
x Γ)])))
x Γ)]
[_ Γ])))
(p/c [env+ (env? (listof Filter/c) (box/c #t). -> . env?)])

View File

@ -12,11 +12,11 @@
(except-in (utils tc-utils stxclass-util))
(env lexical-env)
(only-in (env type-environments) lookup current-tvars extend-env)
scheme/private/class-internal
racket/private/class-internal
(except-in syntax/parse id)
(only-in srfi/1 split-at))
(require (for-template scheme/base scheme/private/class-internal))
(require (for-template scheme/base racket/private/class-internal))
(import tc-if^ tc-lambda^ tc-app^ tc-let^ check-subforms^)
(export tc-expr^)

View File

@ -91,19 +91,16 @@
(provide combine-props tc-results->values)
(define (combine-props new-props old-props)
(define-values (new-atoms new-formulas)
(partition (lambda (e) (or (TypeFilter? e) (NotTypeFilter? e))) new-props))
(values new-formulas new-atoms)
#;#;
(define-values (derived-imps derived-atoms)
(for/fold
([derived-imps null]
[derived-atoms null])
([o old-props])
(match o
[(ImpFilter: as cs)
(let ([as* (remove* new-atoms as filter-equal?)])
(if (null? as*)
(values derived-imps (append cs new-atoms))
(values (cons (make-ImpFilter as* cs) derived-imps) derived-atoms)))])))
(values (append new-imps derived-imps) (append new-atoms derived-atoms)))
(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]
[derived-atoms new-atoms]
[worklist (append old-props new-formulas)])
(if (null? worklist)
(values derived-props derived-atoms)
(let ([p (car worklist)])
(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))]
[_ (loop (cons p derived-props) derived-atoms (cdr worklist))])))))