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

Add `single-value' function, should be used more.

Browse Source 
Construct returns correctly in lam-result->type
Add typechecking for `values' applications.
Extend `ret' to handle dty/dbound.
Define conversions from/to values <-> results
Handle multiple values at the repl.

svn: r14665

original commit: 91f5c269642ec9ecc62efabcc83131db539fcedd
This commit is contained in:
Sam Tobin-Hochstadt 2009-04-29 22:54:29 +00:00
parent e79d66e9b8
commit 4255e1dfab
12 changed files with 132 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
collects/typed-scheme/test.ss
View File

@ -73,3 +73,17 @@ xxx6-y
(begin 1 1 1)
(#%expression (begin 1 1 1))
(values 1)
(values 1 1)
(values)
(: ff (Number -> Number))
(define (ff x) x)
(lambda: ([y : String][x : Number]) (values 1 x 1))
(lambda: ([x : Number]) (values 1 x 1))
(lambda () (values 1 1))
(lambda () 1)
#{(lambda (x) x) :: (Number -> Number)}
;; BUG - this should work
{ann (values (lambda (x) x) (lambda (x) x)) (values (Number -> Number) (String -> String))}

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

@ -14,10 +14,10 @@
[cnt tc-expr/check (syntax? tc-results? . -> . tc-results?)]
[cnt tc-expr/check/t (syntax? tc-results? . -> . Type/c)]
[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?) tc-results? . -> . tc-results?)]
[cnt tc-expr/t (syntax? . -> . Type/c)]))
[cnt tc-expr/t (syntax? . -> . Type/c)]
[cnt single-value ((syntax?) ((or/c tc-results? #f)) . ->* . tc-results?)]))
(define-signature check-subforms^
([cnt check-subforms/ignore (syntax? . -> . any)]
@ -36,7 +36,7 @@
(define-signature tc-app^
([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?)]))
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-results?) (or/c #f tc-results?) . -> . tc-results?)]))
(define-signature tc-let^
([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]

47
collects/typed-scheme/typecheck/tc-app.ss
View File

@ -2,19 +2,52 @@
(require (rename-in "../utils/utils.ss" [infer r:infer])
"signatures.ss"
stxclass
stxclass scheme/match mzlib/trace
(for-syntax stxclass)
(rep type-rep filter-rep object-rep))
(types utils)
(rep type-rep filter-rep object-rep)
(for-template
(only-in '#%kernel [apply k:apply])
"internal-forms.ss" scheme/base
(only-in scheme/private/class-internal make-object do-make-object)))
(import tc-expr^ tc-lambda^ tc-dots^ tc-let^)
(export tc-app^)
;; syntax tc-results? -> tc-results?
(define (tc/app/internal form expected)
(syntax-parse form
#:literals (#%plain-app #%plain-lambda letrec-values
values apply k:apply not list list* call-with-values do-make-object make-object cons
andmap ormap)
[(#%plain-app values arg) (single-value #'arg expected)]
[(#%plain-app values . args)
(match expected
[(tc-results: ets efs eos)
(match-let ([(list (tc-result1: ts fs os) ...)
(for/list ([arg (syntax->list #'args)]
[et ets] [ef efs] [eo eos])
(single-value arg (ret et ef eo)))])
(if (= (length ts) (length ets) (length (syntax->list #'args)))
(ret ts fs os)
(tc-error/expr #:return expected "wrong number of values: expected ~a but got ~a"
(length ets) (length (syntax->list #'args)))))]
[_ (match-let ([(list (tc-result1: ts fs os) ...)
(for/list ([arg (syntax->list #'args)])
(single-value arg))])
(ret ts fs os))])]))
(define (tc/app . args)
(error "tc/app NYI"))
;(trace tc/app/internal)
(define (tc/app/check . args)
(error "tc/app/check NYI"))
;; syntax -> tc-results
(define (tc/app form) (tc/app/internal form #f))
;; syntax tc-results? -> tc-results?
(define (tc/app/check form expected)
(define t (tc/app/internal form expected))
(check-below t expected)
expected)
(define (tc/funapp . args)
;; syntax? syntax? tc-result? (listof tc-results?) (or/c #f tc-results) -> tc-results?
(define (tc/funapp f-stx args-stx ftype0 argtys expected)
(error "tc/funapp NYI"))

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

@ -361,6 +361,12 @@
[(tc-result: t) (int-err "non-symbol methods not supported by Typed Scheme: ~a" t)])]
[(tc-result: t) (tc-error/expr #:return (or expected (ret (Un))) "send: expected a class instance, got ~a" t)]))
(define (single-value form [expected #f])
(define t (if expected (tc-expr/check form expected) (tc-expr form)))
(match t
[(tc-result1: _ _ _) t]
[_ (tc-error/stx form "expected single value, got multiple (or zero) values")]))
;; type-check a list of exprs, producing the type of the last one.
;; if the list is empty, the type is Void.
;; list[syntax[expr]] -> tc-result

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

@ -1,7 +1,7 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [infer r:infer] [extend r:extend]))
(require "signatures.ss"
(require (rename-in "../utils/utils.ss" [infer r:infer] [extend r:extend])
"signatures.ss"
"tc-metafunctions.ss"
mzlib/trace
scheme/list
@ -11,6 +11,7 @@
(rename-in (types convenience utils union)
[make-arr* make-arr])
(private type-annotation)
(types abbrev)
(env type-environments lexical-env)
(utils tc-utils)
mzlib/plt-match)
@ -29,13 +30,14 @@
(define (lam-result->type lr)
(match lr
[(struct lam-result ((list (list arg-ids arg-tys) ...) (list (list kw kw-id kw-ty req?) ...) rest drest body))
(make-arr arg-tys
(abstract-filters (append (for/list ([i (in-naturals)] [_ arg-ids]) i) kw)
(append arg-ids kw-id)
body)
#:kws (map make-Keyword kw kw-ty req?)
#:rest rest
#:drest drest)]))
(make-arr/values
arg-tys
(abstract-filters (append (for/list ([i (in-naturals)] [_ arg-ids]) i) kw)
(append arg-ids kw-id)
body)
#:kws (map make-Keyword kw kw-ty req?)
#:rest rest
#:drest drest)]))
(define (expected-str tys-len rest-ty drest arg-len rest)
(format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a"
@ -49,7 +51,7 @@
(if (= arg-len 1) "" "s")
(if rest " and a rest arg" "")))
;; listof[id] option[id] block listof[type] option[type] option[(cons type var)] type -> lam-result
;; listof[id] option[id] block listof[type] option[type] option[(cons type var)] tc-result -> lam-result
(define (check-clause arg-list rest body arg-tys rest-ty drest ret-ty)
(let* ([arg-len (length arg-list)]
[tys-len (length arg-tys)]
@ -60,12 +62,13 @@
[(< arg-len tys-len) (take arg-tys arg-len)]
[(> arg-len tys-len) (append arg-tys
(map (lambda _ (or rest-ty (Un)))
(drop arg-list tys-len)))]))])
(drop arg-list tys-len)))]))])
(define (check-body)
(with-lexical-env/extend
arg-list arg-types
(make lam-result (map list arg-list arg-types) null rest-ty drest
(tc-exprs/check (syntax->list body) ret-ty))))
(printf "arg-types old new: ~a ~a~n" arg-tys arg-types)
(when (or (not (= arg-len tys-len))
(and rest (and (not rest-ty)
(not drest))))
@ -96,7 +99,7 @@
;; typecheck a single lambda, with argument list and body
;; drest-ty and drest-bound are both false or not false
;; syntax-list[id] block listof[type] type option[type] option[(cons type var)] -> lam-result
;; syntax-list[id] block listof[type] tc-result option[type] option[(cons type var)] -> lam-result
(define (tc/lambda-clause/check args body arg-tys ret-ty rest-ty drest)
(syntax-case args ()
[(args* ...)
@ -188,18 +191,20 @@
(cons (car formals) formals*)
(cons (car bodies) bodies*)
(cons (syntax-len (car formals)) nums-seen))]))
(if (and expected
(= 1 (length (syntax->list formals))))
;; special case for not-case-lambda
(let loop ([expected expected])
(match expected
[(Mu: _ _) (loop (unfold expected))]
[(Function: (list (arr: argss rets rests drests '()) ...))
(for/list ([args argss] [ret rets] [rest rests] [drest drests])
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest drest))]
;; FIXME - is this right?
[_ (go (syntax->list formals) (syntax->list bodies) null null null)]))
(go (syntax->list formals) (syntax->list bodies) null null null)))
(cond
;; special case for not-case-lambda
[(and expected
(= 1 (length (syntax->list formals))))
(let loop ([expected expected])
(match expected
[(tc-result1: (Mu: _ _)) (loop (unfold expected))]
[(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...)))
(printf "expe: ~a~n" expected)
(for/list ([args argss] [ret rets] [rest rests] [drest drests])
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args (values->tc-results ret) rest drest))]
[_ (go (syntax->list formals) (syntax->list bodies) null null null)]))]
;; otherwise
[else (go (syntax->list formals) (syntax->list bodies) null null null)]))
(define (tc/mono-lambda/type formals bodies expected)
(define t (make-Function (map lam-result->type (tc/mono-lambda formals bodies expected))))

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

@ -28,7 +28,7 @@
[else (make-FilterSet l1 l2)]))
(d/c (abstract-filters keys ids results)
(-> (listof index/c) (listof identifier?) tc-results? (or/c Values? ValuesDots?))
((listof index/c) (listof identifier?) tc-results? . -> . (or/c Values? ValuesDots?))
(define (mk l [drest #f])
(if drest (make-ValuesDots l (car drest) (cdr drest)) (make-Values l)))
(match results

10
collects/typed-scheme/typed-scheme.ss
View File

@ -129,15 +129,15 @@
[(head:invis-kw . _)
body2]
[_ (let ([ty-str (match type
[(tc-result1: (? (lambda (t) (type-equal? t -Void)))) #f]
[(tc-result1: t)
(if (type-equal? t -Void)
#f
(format "- : ~a\n" t))]
(format "- : ~a\n" t)]
[(tc-results: ts) (format "- : ~a\n" (cons 'values ts))]
[x (int-err "bad type result: ~a" x)])])
(if #'ty-str
#`(let ([v #,body2] [type '#,ty-str])
#`(let ([type '#,ty-str])
(begin0
v
#,body2
(printf type)))
body2))]))]))

23
collects/typed-scheme/types/abbrev.ss
View File

@ -3,7 +3,7 @@
(require "../utils/utils.ss")
(require (rep type-rep object-rep filter-rep)
"printer.ss"
"printer.ss" "utils.ss"
(utils tc-utils)
scheme/list
scheme/match
@ -173,8 +173,8 @@
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
#:filters [filters -no-lfilter] #:object [obj -no-lobj])
(c:->* ((listof Type/c) (or/c ValuesDots? Values?))
(#:rest Type/c
#:drest (cons/c Type/c symbol?)
(#:rest (or/c Type/c #f)
#:drest (or/c (cons/c Type/c symbol?) #f)
#:kws (listof Keyword?)
#:filters LFilterSet?
#:object LatentObject?)
@ -262,4 +262,19 @@
(make-Function (list (make-arr* (append args (take opt-args i)) result))))))
(define-syntax-rule (->opt args ... [opt ...] res)
(opt-fn (list args ...) (list opt ...) res))
(opt-fn (list args ...) (list opt ...) res))
(define (tc-results->values tc)
(match tc
[(tc-results: ts fs os dty dbound)
(make-ValuesDots (map -result ts fs os) dty dbound)]
[(tc-results: ts fs os)
(make-Values (map -result ts fs os))]))
;; FIXME - this should really be a new metafunction like abstract-filter
(define (values->tc-results tc)
(match tc
[(ValuesDots: (list (Result: ts fs os)) dty dbound)
(int-err "values->tc-results NYI for Dots")]
[(Values: (list (Result: ts fs os)))
(ret ts)]))

2
collects/typed-scheme/types/printer.ss
View File

@ -90,12 +90,14 @@
(when drest
(fp "~a ... ~a " (car drest) (cdr drest)))
(match rng
#|
[(Values: (list (Result: t (LFilterSet: (list) (list)) (LEmpty:))))
(fp "-> ~a" t)]
[(Values: (list (Result: t fs (LEmpty:))))
(fp "-> ~a : ~a" t fs)]
[(Values: (list (Result: t lf lo)))
(fp "-> ~a : ~a ~a" t lf lo)]
|#
[_
(fp "-> ~a" rng)])
(fp ")")]))

3
collects/typed-scheme/types/subtype.ss
View File

@ -310,9 +310,6 @@
;; we can ignore interesting results
[(list (Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:)))
(subtype* A0 t t*)]
;; single values shouldn't actually happen, but they're just like the type
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
;; subtyping on other stuff
[(list (Syntax: t) (Syntax: t*))
(subtype* A0 t t*)]

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

@ -209,7 +209,15 @@
(if (and (list? t) (list? f) (list? o))
(map make-tc-result t f o)
(list (make-tc-result t f o)))
#f)]))
#f)]
[(t f o dty)
(int-err "ret used with dty without dbound")]
[(t f o dty dbound)
(make-tc-results
(if (and (list? t) (list? f) (list? o))
(map make-tc-result t f o)
(list (make-tc-result t f o)))
(cons dty dbound))]))
(p/c
[ret
@ -219,7 +227,9 @@
FilterSet?)]
[o (if (list? t)
(listof Object?)
Object?)])
Object?)]
[dty Type/c]
[dbound symbol?])
[_ tc-results?])])
(define (subst v t e) (substitute t v e))

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

@ -266,7 +266,7 @@ at least theoretically.
(define (extend s t extra)
(append t (build-list (- (length s) (length t)) (lambda _ extra))))
(define-for-syntax enable-contracts? #f)
(define-for-syntax enable-contracts? #t)
(provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c)
(define-syntax p/c