suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add provides

Browse Source 
Use Type/c instead fo Type? in contracts
New if typechecking.
match expanders for tc-result.

svn: r13996

original commit: 2dbd82e587a87663afacefc5524553c4fc2246ed
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-06 22:25:19 +00:00
parent b33c622891
commit ad00361e3a
5 changed files with 77 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
collects/typed-scheme/typecheck/signatures.ss
View File

@ -11,39 +11,39 @@
(define-signature tc-expr^
([cnt tc-expr (syntax? . -> . tc-result?)]
[cnt tc-expr/check (syntax? Type? . -> . tc-result?)]
[cnt tc-expr/check/t (syntax? Type? . -> . Type?)]
[cnt check-below (->d ([s (or/c Type? tc-result?)] [t Type?]) () [_ (if (Type? s) Type? tc-result?)])]
[cnt tc-literal (any/c . -> . Type?)]
[cnt tc-expr/check (syntax? Type/c . -> . tc-result?)]
[cnt tc-expr/check/t (syntax? Type/c . -> . Type/c)]
[cnt check-below (->d ([s (or/c Type/c tc-result?)] [t Type/c]) () [_ (if (Type/c s) Type/c tc-result?)])]
[cnt tc-literal (any/c . -> . Type/c)]
[cnt tc-exprs ((listof syntax?) . -> . tc-result?)]
[cnt tc-exprs/check ((listof syntax?) Type? . -> . tc-result?)]
[cnt tc-expr/t (syntax? . -> . Type?)]))
[cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-result?)]
[cnt tc-expr/t (syntax? . -> . Type/c)]))
(define-signature check-subforms^
([cnt check-subforms/ignore (syntax? . -> . any)]
[cnt check-subforms/with-handlers (syntax? . -> . any)]
[cnt check-subforms/with-handlers/check (syntax? Type? . -> . any)]))
[cnt check-subforms/with-handlers/check (syntax? Type/c . -> . any)]))
(define-signature tc-if^
([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/if-twoarm/check (syntax? syntax? syntax? Type? . -> . tc-result?)]))
[cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-result?)]))
(define-signature tc-lambda^
([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/lambda/check (syntax? syntax? syntax? Type? . -> . tc-result?)]
[cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type?) Type? . -> . Type?)]))
[cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-result?)]
[cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) Type/c . -> . Type/c)]))
(define-signature tc-app^
([cnt tc/app (syntax? . -> . tc-result?)]
[cnt tc/app/check (syntax? Type? . -> . tc-result?)]
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type?) . -> . tc-result?)]))
[cnt tc/app/check (syntax? Type/c . -> . tc-result?)]
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type/c) . -> . tc-result?)]))
(define-signature tc-let^
([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]
[cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]))
[cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)]
[cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)]))
(define-signature tc-dots^
([cnt tc/dots (syntax? . -> . (values Type? symbol?))]))
([cnt tc/dots (syntax? . -> . (values Type/c symbol?))]))

2
collects/typed-scheme/typecheck/tc-envops.ss
View File

@ -12,6 +12,8 @@
stxclass/util
(for-syntax scheme/base))
(provide env+)
(define (replace-nth l i f)
(cond [(null? l) (error 'replace-nth "list not long enough" l i f)]
[(zero? i) (cons (f (car l)) (cdr l))]

4
collects/typed-scheme/typecheck/tc-metafunctions.ss
View File

@ -1,7 +1,7 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (rename-in (types subtype convenience remove-intersect)
(require (rename-in (types subtype convenience remove-intersect union)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
@ -10,6 +10,8 @@
stxclass/util
(for-syntax scheme/base))
(provide combine-filter apply-filter abstract-filter)
;; this implements the sequence invariant described on the first page relating to Bot
(define (lcombine l1 l2)
(cond [(memq (make-LBot) l1)

39
collects/typed-scheme/typecheck/tc-new-if.ss Normal file
View File

@ -0,0 +1,39 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [infer r:infer]))
(require "signatures.ss"
(rep type-rep filter-rep object-rep)
(rename-in (types convenience subtype union utils comparison remove-intersect)
[remove *remove])
(env lexical-env)
(r:infer infer)
(utils tc-utils mutated-vars)
(typecheck tc-envops tc-metafunctions)
syntax/kerncase
mzlib/trace
mzlib/plt-match)
;; if typechecking
(import tc-expr^)
(export tc-if^)
(define (tc/if-twoarm tst thn els [expected #f])
(define (tc e) (if expected (tc-expr/check e expected) (tc-expr e)))
(match (tc-expr tst)
[(list (tc-result: _ (and f1 (FilterSet: fs+ fs-)) _))
(match-let ([(tc-results: ts fs2 _) (with-lexical-env (env+ (lexical-env) fs+) (tc thn))]
[(tc-results: us fs3 _) (with-lexical-env (env+ (lexical-env) fs-) (tc els))])
;; if we have the same number of values in both cases
(cond [(= (length ts) (length us))
(for/list ([t ts] [u us] [f2 fs2] [f3 fs3])
(ret (Un t u) (combine-filter f1 f2 f2)))]
[else
(tc-error/expr #:ret (ret Err)
"Expected the same number of values from both branches of if expression, but got ~a and ~a"
(length ts) (length us))]))]
[(tc-results: t _ _)
(tc-error/expr #:ret (ret (or expected Err))
"Test expression expects one value, given ~a" t)]))
(define tc/if-twoarm/check tc/if-twoarm)

24
collects/typed-scheme/types/utils.ss
View File

@ -167,6 +167,17 @@
;; this structure represents the result of typechecking an expression
(d-s/c tc-result ([t Type/c] [f FilterSet?] [o Object?]) #:transparent)
(define-struct tc-result (t f o) #:transparent #:omit-define-values)
(define-match-expander tc-result:
(syntax-parser
[(_ tp fp op) #'(struct tc-result (tp fp op))]))
(define-match-expander tc-results:
(syntax-parser
[(_ tp fp op) #'(list (struct tc-result (tp fp op)) (... ...))]))
(provide tc-result: tc-results:)
;; convenience function for returning the result of typechecking an expression
(define ret
@ -175,7 +186,10 @@
(list (make-tc-result t (make-FilterSet null null) (make-Empty)))
(for/list ([i t])
(make-tc-result i (make-FilterSet null null) (make-Empty))))]
[(t f) (error 'ret "two arguments not supported")]
[(t f) (if (Type? t)
(list (make-tc-result t f (make-Empty)))
(for/list ([i t] [f f])
(make-tc-result i f (make-Empty))))]
[(t f o)
(if (and (list? t) (list? f) (list? o))
(map make-tc-result t f o)
@ -187,11 +201,9 @@
([f (if (list? t)
(listof FilterSet?)
FilterSet?)]
[o (if (or (list? f) (FilterSet? f))
(if (list? t)
(listof Object?)
Object?)
(lambda (e) (eq? e f)))])
[o (if (list? t)
(listof Object?)
Object?)])
[_ (listof tc-result?)])])
(define (subst v t e) (substitute t v e))