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

disable application checking, `3' now typechecks

Browse Source 
svn: r14128

original commit: 537d267314bbf5e74230460874b9af89a43bfacf
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-16 15:28:29 +00:00
commit d8ac05e077
11 changed files with 92 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
collects/tests/typed-scheme/fail/struct-provide.ss Normal file
View File

@ -0,0 +1,11 @@
#;
(exn-pred exn:fail:syntax? #rx".*typed module.*")
#lang scheme/load
(module m typed-scheme
(define-struct: q ())
(provide (all-defined-out)))
(module n scheme
(require 'm)
q)

14
collects/tests/typed-scheme/succeed/rts-prov.ss Normal file
View File

@ -0,0 +1,14 @@
#lang scheme/load
(module l scheme
(define-struct q ())
(provide (all-defined-out)))
(module m typed-scheme
(require-typed-struct q () 'l)
(provide (all-defined-out)))
(module n typed-scheme
(require 'm)
(: f q)
(define f (make-q)))

7
collects/typed-scheme/env/type-name-env.ss vendored
View File

@ -3,12 +3,15 @@
(require syntax/boundmap
mzlib/trace
(env type-alias-env)
(utils tc-utils)
(rep type-rep)
(types utils))
(provide register-type-name
lookup-type-name
register-type-names
add-alias
type-name-env-map)
;; a mapping from id -> type (where id is the name of the type)
@ -42,3 +45,7 @@
;; (id type -> T) -> listof[T]
(define (type-name-env-map f)
(module-identifier-mapping-map the-mapping f))
(define (add-alias from to)
(when (lookup-type-name to (lambda () #f))
(register-resolved-type-alias from (make-Name to))))

5
collects/typed-scheme/typecheck/provide-handling.ss
View File

@ -3,6 +3,7 @@
(require (except-in "../utils/utils.ss" extend))
(require (only-in srfi/1/list s:member)
syntax/kerncase syntax/boundmap
(env type-name-env type-alias-env)
mzlib/trace
(private type-contract)
(rep type-rep)
@ -73,7 +74,9 @@
#`(begin
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(begin
(add-alias #'export-id #'id)
(make-rename-transformer #'id))
(lambda (stx)
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
(provide (rename-out [export-id out-id]))))))]

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

@ -10,13 +10,13 @@
[cnt tc-toplevel-form (syntax? . -> . any)]))
(define-signature tc-expr^
([cnt tc-expr (syntax? . -> . tc-result?)]
[cnt tc-expr/check (syntax? Type/c . -> . tc-result?)]
([cnt tc-expr (syntax? . -> . tc-results?)]
[cnt tc-expr/check (syntax? tc-results? . -> . tc-results?)]
[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/c . -> . tc-result?)]
[cnt check-below (->d ([s (or/c Type/c tc-results?)] [t (or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])]
;[cnt tc-literal (any/c . -> . Type/c)]
[cnt tc-exprs ((listof syntax?) . -> . tc-results?)]
[cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-results?)]
[cnt tc-expr/t (syntax? . -> . Type/c)]))
(define-signature check-subforms^
@ -25,24 +25,24 @@
[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/c . -> . tc-result?)]))
([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]))
(define-signature tc-lambda^
([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-result?)]
([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]
[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/c . -> . tc-result?)]
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type/c) . -> . tc-result?)]))
([cnt tc/app (syntax? . -> . tc-results?)]
[cnt tc/app/check (syntax? tc-results? . -> . tc-results?)]
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-results?) (or/c #f Type/c) . -> . tc-results?)]))
(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/c . -> . tc-result?)]
[cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)]))
([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/let-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]
[cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]))
(define-signature tc-dots^
([cnt tc/dots (syntax? . -> . (values Type/c symbol?))]))

30
collects/typed-scheme/typecheck/tc-expr-unit.ss
View File

@ -3,7 +3,7 @@
(require (rename-in "../utils/utils.ss" [private private-in]))
(require syntax/kerncase
scheme/match
scheme/match (prefix-in - scheme/contract)
"signatures.ss"
(types utils convenience union subtype)
(private-in parse-type type-annotation)
@ -23,7 +23,8 @@
;; return the type of a literal value
;; scheme-value -> type
(define (tc-literal v-stx [expected #f])
(d/c (tc-literal v-stx [expected #f])
(-->* (syntax?) ((-or/c #f Type/c)) Type/c)
(define-syntax-class exp
(pattern i
#:when expected
@ -45,7 +46,7 @@
[(i ...)
(-Tuple (map tc-literal (syntax->list #'(i ...))))]
[i #:declare i (3d vector?)
(make-Vector (apply Un (map tc-literal (vector->list #'i.datum))))]
(make-Vector (apply Un (map tc-literal (vector->list #'i.datum))))]
[_ Univ]))
@ -120,15 +121,20 @@
(match (tc-expr/check e t)
[(tc-result: t) t]))
;; check-below : (/\ (Result Type -> Result)
;; check-below : (/\ (Results Type -> Result)
;; (Results Results -> Result)
;; (Type Type -> Type))
(define (check-below tr1 expected)
(match (list tr1 expected)
[(list (tc-result: t1 te1 ee1) t2)
(match* (tr1 expected)
[((tc-results: t1) (tc-results: t2))
(unless (andmap subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
(ret expected)]
[((tc-result1: t1) (? Type? t2))
(unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
(ret expected)]
[(list t1 t2)
[((? Type? t1) (? Type? t2))
(unless (subtype t1 t2)
(tc-error/expr"Expected ~a, but got ~a" t2 t1))
expected]))
@ -159,7 +165,9 @@
;; data
[(quote #f) (ret (-val #f) false-filter)]
[(quote #t) (ret (-val #t) true-filter)]
[(quote val) (ret (tc-literal #'val expected))]
[(quote val) (match expected
[(tc-result1: t)
(ret (tc-literal #'val t))])]
;; syntax
[(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))]
;; mutation!
@ -314,9 +322,9 @@
(tc-expr/check form ann))]
[else (internal-tc-expr form)])])
(match ty
[(tc-result: t eff1 eff2)
(let ([ty* (do-inst form t)])
(ret ty* eff1 eff2))]))))
[(tc-results: ts fs os)
(let ([ts* (do-inst form ts)])
(ret ts fs os))]))))
(define (tc/send rcvr method args [expected #f])
(match (tc-expr rcvr)

6
collects/typed-scheme/typecheck/tc-lambda-unit.ss
View File

@ -19,10 +19,10 @@
(import tc-expr^)
(export tc-lambda^)
(d-s/c lam-result ([args (listof (list identifier? Type/c))]
[kws (listof (list keyword? identifier? Type/c boolean?))]
(d-s/c lam-result ([args (listof (list/c identifier? Type/c))]
[kws (listof (list/c keyword? identifier? Type/c boolean?))]
[rest (or/c #f Type/c)]
[drest (or/c #f (cons symbol? Type/c))]
[drest (or/c #f (cons/c symbol? Type/c))]
[body tc-results?])
#:transparent)

12
collects/typed-scheme/typecheck/tc-structs.ss
View File

@ -131,11 +131,13 @@
(map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent)
null)))
(register-type-name nm (wrapper sty))
(for/list ([e bindings])
(let ([nm (car e)]
[t (cdr e)])
(register-type nm t)
(make-def-binding nm t))))
(cons
(make-def-stx-binding nm)
(for/list ([e bindings])
(let ([nm (car e)]
[t (cdr e)])
(register-type nm t)
(make-def-binding nm t)))))
;; check and register types for a polymorphic define struct
;; tc/poly-struct : Listof[identifier] (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void

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

@ -161,7 +161,7 @@
[(define-values (var ...) expr)
(let* ([vars (syntax->list #'(var ...))]
[ts (map lookup-type vars)])
(tc-expr/check #'expr (-values ts)))
(tc-expr/check #'expr (ret ts)))
(void)]
;; to handle the top-level, we have to recur into begins

4
collects/typed-scheme/typecheck/typechecker.ss
View File

@ -5,11 +5,11 @@
mzlib/trace
(only-in scheme/unit provide-signature-elements)
"signatures.ss" "tc-toplevel.ss"
"tc-if-unit.ss" "tc-lambda-unit.ss" "tc-app-unit.ss"
"tc-new-if.ss" "tc-lambda-unit.ss" "tc-new-app-unit.ss"
"tc-let-unit.ss" "tc-dots-unit.ss"
"tc-expr-unit.ss" "check-subforms-unit.ss")
(provide-signature-elements typechecker^ tc-expr^)
(define-values/link-units/infer
tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@)
tc-toplevel@ tc-new-if@ tc-lambda@ tc-dots@ tc-new-app@ tc-let@ tc-expr@ check-subforms@)

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

@ -180,7 +180,12 @@
[(_ tp fp op dty dbound) #'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) (cons dty dbound)))]
[(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _)) (... ...)) #f))]))
(provide tc-result: tc-results: tc-result? tc-results?)
(define-match-expander tc-result1:
(syntax-parser
[(_ tp fp op) #'(struct tc-results ((list (struct tc-result (tp fp op))) #f))]
[(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _))) #f))]))
(provide tc-result: tc-results: tc-result1: tc-result? tc-results?)
;; convenience function for returning the result of typechecking an expression
(define ret
@ -214,7 +219,7 @@
[o (if (list? t)
(listof Object?)
Object?)])
[_ (listof tc-result?)])])
[_ tc-results?])])
(define (subst v t e) (substitute t v e))