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

Remove unneccessary requires.

Browse Source 
Fix let checking to use annotations as the expected type for the RHS.
Fix bug in use of expected types in inference.

svn: r9674
This commit is contained in:
Sam Tobin-Hochstadt 2008-05-06 00:42:28 +00:00
parent 2fc38964e5
commit c6f2b2d517
10 changed files with 58 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/typed-scheme/private/base-env.ss
View File

@ -483,7 +483,7 @@
)))
(begin-for-syntax
;(printf "running base-env~n")
#;(printf "running base-env~n")
(initialize-type-env initial-env)
(initialize-others))

14
collects/typed-scheme/private/infer-ops.ss
View File

@ -271,18 +271,18 @@
;; returns a substitution
;; if R is #f, we don't care about the substituion
;; just return a boolean result
(define (infer X S T R)
(with-handlers ([exn:infer? (lambda _ #f)])
(define (infer X S T R [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)])
(let ([cs (cgen/list X null S T)])
(if R
(subst-gen cs R)
#t))))
(if (not expected)
(subst-gen cs R)
(cset-meet cs (cgen null X R expected))))))
;; like infer, but T-var is the vararg type:
(define (infer/vararg X S T T-var R)
(define (infer/vararg X S T T-var R [expected #f])
(define new-T (extend S T T-var))
(and ((length S) . >= . (length T))
(infer X S new-T R)))
(infer X S new-T R expected)))
;; Listof[A] Listof[B] B -> Listof[B]
;; pads out t to be as long as s

2
collects/typed-scheme/private/signatures.ss
View File

@ -22,7 +22,7 @@
(type-check tc-toplevel-form))
(define-signature tc-expr^
(tc-expr tc-expr/check check-below tc-literal tc-exprs tc-exprs/check tc-expr/t #;check-expr))
(tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t #;check-expr))
(define-signature check-subforms^
(check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check))

11
collects/typed-scheme/private/tc-app-unit.ss
View File

@ -195,12 +195,6 @@
[f-ty (tc-error/expr #:return (ret (Un))
"Type of argument to apply is not a function type: ~n~a" f-ty)]))))
(define (stringify l [between " "])
(define (intersperse v l)
(cond [(null? l) null]
[(null? (cdr l)) l]
[else (cons (car l) (cons v (intersperse v (cdr l))))]))
(apply string-append (intersperse between (map (lambda (s) (format "~a" s)) l))))
(define (tc/funapp f-stx args-stx ftype0 argtys expected)
(match-let* ([(list (tc-result: argtypes arg-thn-effs arg-els-effs) ...) argtys])
@ -267,8 +261,7 @@
(stringify (map stringify msg-doms) "\n") (stringify argtypes))))]
[(and (= (length (car doms*))
(length argtypes))
(infer (fv/list (car doms*)) argtypes (car doms*) (if expected #f (car rngs*)))
#;(infer/list (car doms*) argtypes vars))
(infer (fv/list (cons (car rngs*) (car doms*))) argtypes (car doms*) (car rngs*) expected))
=> (lambda (substitution)
(or expected
(let* ([s (lambda (t) (subst-all substitution t))]
@ -298,7 +291,7 @@
(unless (<= (length dom) (length argtypes))
(tc-error "incorrect number of arguments to function: ~a ~a" dom argtypes))
(let ([substitution
(infer/vararg vars argtypes dom rest (if expected #f rng))])
(infer/vararg vars argtypes dom rest rng expected)])
(cond
[(and expected substitution) expected]
[substitution

4
collects/typed-scheme/private/tc-expr-unit.ss
View File

@ -87,6 +87,10 @@
(define (tc-expr/t e) (match (tc-expr e)
[(tc-result: t) t]))
(define (tc-expr/check/t e t)
(match (tc-expr/check e t)
[(tc-result: t) t]))
(define (check-below tr1 expected)
(match (list tr1 expected)
[(list (tc-result: t1 te1 ee1) t2)

21
collects/typed-scheme/private/tc-let-unit.ss
View File

@ -24,8 +24,6 @@
(export tc-let^)
(define (do-check expr->type namess types form exprs body clauses expected)
;; just for error reporting
#;(define clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)]))
;; extend the lexical environment for checking the body
(with-lexical-env/extend
;; the list of lists of name
@ -104,16 +102,13 @@
;; if none of the names bound in the letrec are free vars of this rhs
[(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?)) (free-vars (car exprs))))
;; then check this expression separately
(let ([t (tc-expr/maybe-expected/t (car exprs) (car names))])
(with-lexical-env/extend
(list (car names))
(list (get-type/infer (car names) t))
(loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses))))]
(with-lexical-env/extend
(list (car names))
(list (get-type/infer (car names) (car exprs) (lambda (e) (tc-expr/maybe-expected/t e (car names))) tc-expr/check/t))
(loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses)))]
[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)
(match (tc-expr/check e t)
[(tc-result: t) t]))
(do-check (lambda (stx e t) (tc-expr/check/t e t))
names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)]))))
;; this is so match can provide us with a syntax property to
@ -133,12 +128,12 @@
;; all the trailing expressions - the ones actually bound to the names
[exprs (syntax->list exprs)]
;; the types of the exprs
[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
#;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
;; the annotated types of the name (possibly using the inferred types)
[types (map get-type/infer names inferred-types)]
[types (for/list ([name names] [e exprs]) (get-type/infer name e (tc-expr-t/maybe-expected expected) tc-expr/check/t))]
;; the clauses for error reporting
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
(do-check check-type names types form inferred-types body clauses expected)))
(do-check void names types form types body clauses expected)))
(define (tc/let-values/check namess exprs body form expected)
(tc/let-values/internal namess exprs body form expected))

5
collects/typed-scheme/private/tc-toplevel.ss
View File

@ -3,7 +3,7 @@
(require syntax/kerncase
mzlib/etc
mzlib/plt-match
scheme/match
"signatures.ss"
"tc-structs.ss"
"type-utils.ss"
@ -21,11 +21,8 @@
"provide-handling.ss"
"type-alias-env.ss"
"type-contract.ss"
;(only-in "prims.ss" :)
(for-template
;(only-in "prims.ss" :)
"internal-forms.ss"
"tc-utils.ss"
(lib "contract.ss")
scheme/base))

7
collects/typed-scheme/private/tc-utils.ss
View File

@ -7,6 +7,13 @@
(define orig-module-stx (make-parameter #f))
(define expanded-module-stx (make-parameter #f))
(define (stringify l [between " "])
(define (intersperse v l)
(cond [(null? l) null]
[(null? (cdr l)) l]
[else (cons (car l) (cons v (intersperse v (cdr l))))]))
(apply string-append (intersperse between (map (lambda (s) (format "~a" s)) l))))
;; helper function, not currently used
(define (find-origin stx)
(cond [(syntax-property stx 'origin) => (lambda (orig)

42
collects/typed-scheme/private/type-annotation.ss
View File

@ -1,7 +1,7 @@
#lang scheme/base
(require "type-rep.ss" "parse-type.ss" "tc-utils.ss" "subtype.ss" "utils.ss" "union.ss" "resolve-type.ss"
"type-env.ss")
"type-env.ss" "type-effect-convenience.ss")
(require (lib "plt-match.ss")
mzlib/trace)
(provide type-annotation
@ -76,22 +76,34 @@
;; get the type annotations on this list of identifiers
;; if not all identifiers have annotations, return the supplied inferred type
;; list[identifier] type -> list[type]
(define (get-type/infer stxs e-type)
(match (list stxs e-type)
[(list '() (Values: '())) (list)]
[(list (list stx ...) (Values: (list ty ...)))
(map (lambda (stx ty)
(cond [(type-annotation stx) => (lambda (ann) (check-type stx ty ann) (log/extra stx ty ann) ann)]
[else (log/noann stx ty) ty]))
stx ty)]
[(list (list stx) ty)
(define (get-type/infer stxs expr tc-expr tc-expr/check)
(match stxs
['()
(tc-expr/check expr (-values null))
(list)]
[(list stx)
(cond [(type-annotation stx #:infer #t)
=> (lambda (ann)
(check-type stx ty ann)
(log/extra stx ty ann)
(list ann))]
[else (log/noann stx ty) (list ty)])]
[else (int-err "wrong type arity - get-type/infer ~a ~a" stxs e-type)]))
(list (tc-expr/check expr ann)))]
[else (list (tc-expr expr))])]
[(list stx ...)
(let ([anns (for/list ([s stxs]) (type-annotation s #:infer #t))])
(if (for/and ([a anns]) a)
(begin (tc-expr/check expr (-values anns)) anns)
(let ([ty (tc-expr expr)])
(match ty
[(Values: tys)
(if (not (= (length stxs) (length tys)))
(tc-error/delayed #:ret (map (lambda _ (Un)) stxs)
"Expression should produce ~a values, but produces ~a values of types ~a"
(length stxs) (length tys) (stringify tys))
(map (lambda (stx ty)
(cond [(type-annotation stx #:infer #t) => (lambda (ann) (check-type stx ty ann) (log/extra stx ty ann) ann)]
[else (log/noann stx ty) ty]))
stxs tys))]
[ty (tc-error/delayed #:ret (map (lambda _ (Un)) stxs)
"Expression should produce ~a values, but produces one values of type "
(length stxs) ty)]))))]))
;; check that e-type is compatible with ty in context of stx

2
collects/typed-scheme/typed-reader.ss
View File

@ -1,7 +1,5 @@
#lang scheme/base
(require (for-template "private/prims.ss"))
;; Provides raise-read-error and raise-read-eof-error
(require syntax/readerr)