suzanne.soy/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
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-16 15:28:29 +00:00
parent f1840f4eeb
commit 537d267314
7 changed files with 67 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -10,13 +10,13 @@
[cnt tc-toplevel-form (syntax? . -> . any)])) [cnt tc-toplevel-form (syntax? . -> . any)]))
(define-signature tc-expr^ (define-signature tc-expr^
([cnt tc-expr (syntax? . -> . tc-result?)] ([cnt tc-expr (syntax? . -> . tc-results?)]
[cnt tc-expr/check (syntax? Type/c . -> . tc-result?)] [cnt tc-expr/check (syntax? tc-results? . -> . tc-results?)]
[cnt tc-expr/check/t (syntax? Type/c . -> . Type/c)] [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 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-literal (any/c . -> . Type/c)]
[cnt tc-exprs ((listof syntax?) . -> . tc-result?)] [cnt tc-exprs ((listof syntax?) . -> . tc-results?)]
[cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-result?)] [cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-results?)]
[cnt tc-expr/t (syntax? . -> . Type/c)])) [cnt tc-expr/t (syntax? . -> . Type/c)]))
(define-signature check-subforms^ (define-signature check-subforms^
@ -25,24 +25,24 @@
[cnt check-subforms/with-handlers/check (syntax? Type/c . -> . any)])) [cnt check-subforms/with-handlers/check (syntax? Type/c . -> . any)]))
(define-signature tc-if^ (define-signature tc-if^
([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)] ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-result?)])) [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]))
(define-signature tc-lambda^ (define-signature tc-lambda^
([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)] ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-result?)] [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)])) [cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) Type/c . -> . Type/c)]))
(define-signature tc-app^ (define-signature tc-app^
([cnt tc/app (syntax? . -> . tc-result?)] ([cnt tc/app (syntax? . -> . tc-results?)]
[cnt tc/app/check (syntax? Type/c . -> . tc-result?)] [cnt tc/app/check (syntax? tc-results? . -> . tc-results?)]
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type/c) . -> . tc-result?)])) [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-results?) (or/c #f Type/c) . -> . tc-results?)]))
(define-signature tc-let^ (define-signature tc-let^
([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-result?)] ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-result?)] [cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)] [cnt tc/let-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]
[cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)])) [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]))
(define-signature tc-dots^ (define-signature tc-dots^
([cnt tc/dots (syntax? . -> . (values Type/c symbol?))])) ([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 (rename-in "../utils/utils.ss" [private private-in]))
(require syntax/kerncase (require syntax/kerncase
scheme/match scheme/match (prefix-in - scheme/contract)
"signatures.ss" "signatures.ss"
(types utils convenience union subtype) (types utils convenience union subtype)
(private-in parse-type type-annotation) (private-in parse-type type-annotation)
@ -23,7 +23,8 @@
;; return the type of a literal value ;; return the type of a literal value
;; scheme-value -> type ;; 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 (define-syntax-class exp
(pattern i (pattern i
#:when expected #:when expected
@ -45,7 +46,7 @@
[(i ...) [(i ...)
(-Tuple (map tc-literal (syntax->list #'(i ...))))] (-Tuple (map tc-literal (syntax->list #'(i ...))))]
[i #:declare i (3d vector?) [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])) [_ Univ]))
@ -120,15 +121,20 @@
(match (tc-expr/check e t) (match (tc-expr/check e t)
[(tc-result: t) t])) [(tc-result: t) t]))
;; check-below : (/\ (Result Type -> Result) ;; check-below : (/\ (Results Type -> Result)
;; (Results Results -> Result)
;; (Type Type -> Type)) ;; (Type Type -> Type))
(define (check-below tr1 expected) (define (check-below tr1 expected)
(match (list tr1 expected) (match* (tr1 expected)
[(list (tc-result: t1 te1 ee1) t2) [((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) (unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1)) (tc-error/expr "Expected ~a, but got ~a" t2 t1))
(ret expected)] (ret expected)]
[(list t1 t2) [((? Type? t1) (? Type? t2))
(unless (subtype t1 t2) (unless (subtype t1 t2)
(tc-error/expr"Expected ~a, but got ~a" t2 t1)) (tc-error/expr"Expected ~a, but got ~a" t2 t1))
expected])) expected]))
@ -159,7 +165,9 @@
;; data ;; data
[(quote #f) (ret (-val #f) false-filter)] [(quote #f) (ret (-val #f) false-filter)]
[(quote #t) (ret (-val #t) true-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 ;; syntax
[(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))] [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))]
;; mutation! ;; mutation!
@ -314,9 +322,9 @@
(tc-expr/check form ann))] (tc-expr/check form ann))]
[else (internal-tc-expr form)])]) [else (internal-tc-expr form)])])
(match ty (match ty
[(tc-result: t eff1 eff2) [(tc-results: ts fs os)
(let ([ty* (do-inst form t)]) (let ([ts* (do-inst form ts)])
(ret ty* eff1 eff2))])))) (ret ts fs os))]))))
(define (tc/send rcvr method args [expected #f]) (define (tc/send rcvr method args [expected #f])
(match (tc-expr rcvr) (match (tc-expr rcvr)

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

@ -19,10 +19,10 @@
(import tc-expr^) (import tc-expr^)
(export tc-lambda^) (export tc-lambda^)
(d-s/c lam-result ([args (listof (list identifier? Type/c))] (d-s/c lam-result ([args (listof (list/c identifier? Type/c))]
[kws (listof (list keyword? identifier? Type/c boolean?))] [kws (listof (list/c keyword? identifier? Type/c boolean?))]
[rest (or/c #f Type/c)] [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?]) [body tc-results?])
#:transparent) #:transparent)

18
collects/typed-scheme/typecheck/tc-new-app-unit.ss Normal file
View File

@ -0,0 +1,18 @@
#lang scheme/unit
(require "signatures.ss" "../utils/utils.ss")
(require (utils tc-utils))
(import tc-expr^ tc-lambda^ tc-dots^)
(export tc-app^)
(define (tc/app . args)
(int-err "tc/app NYI"))
(define (tc/app/check . args)
(int-err "tc/app/check NYI"))
(define (tc/funapp . args)
(int-err "tc/funapp NYI"))

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

@ -161,7 +161,7 @@
[(define-values (var ...) expr) [(define-values (var ...) expr)
(let* ([vars (syntax->list #'(var ...))] (let* ([vars (syntax->list #'(var ...))]
[ts (map lookup-type vars)]) [ts (map lookup-type vars)])
(tc-expr/check #'expr (-values ts))) (tc-expr/check #'expr (ret ts)))
(void)] (void)]
;; to handle the top-level, we have to recur into begins ;; 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 mzlib/trace
(only-in scheme/unit provide-signature-elements) (only-in scheme/unit provide-signature-elements)
"signatures.ss" "tc-toplevel.ss" "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-let-unit.ss" "tc-dots-unit.ss"
"tc-expr-unit.ss" "check-subforms-unit.ss") "tc-expr-unit.ss" "check-subforms-unit.ss")
(provide-signature-elements typechecker^ tc-expr^) (provide-signature-elements typechecker^ tc-expr^)
(define-values/link-units/infer (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 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))])) [(_ 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 ;; convenience function for returning the result of typechecking an expression
(define ret (define ret
@ -214,7 +219,7 @@
[o (if (list? t) [o (if (list? t)
(listof Object?) (listof Object?)
Object?)]) Object?)])
[_ (listof tc-result?)])]) [_ tc-results?])])
(define (subst v t e) (substitute t v e)) (define (subst v t e) (substitute t v e))