From 4255e1dfabd0f4e96dade648ca7f74f2624578d8 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 29 Apr 2009 22:54:29 +0000 Subject: [PATCH] Add `single-value' function, should be used more. 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 --- collects/typed-scheme/test.ss | 14 +++++ collects/typed-scheme/typecheck/signatures.ss | 6 +-- collects/typed-scheme/typecheck/tc-app.ss | 47 +++++++++++++--- .../typed-scheme/typecheck/tc-expr-unit.ss | 6 +++ .../typed-scheme/typecheck/tc-lambda-unit.ss | 53 ++++++++++--------- .../typecheck/tc-metafunctions.ss | 2 +- collects/typed-scheme/typed-scheme.ss | 10 ++-- collects/typed-scheme/types/abbrev.ss | 23 ++++++-- collects/typed-scheme/types/printer.ss | 2 + collects/typed-scheme/types/subtype.ss | 3 -- collects/typed-scheme/types/utils.ss | 14 ++++- collects/typed-scheme/utils/utils.ss | 2 +- 12 files changed, 132 insertions(+), 50 deletions(-) diff --git a/collects/typed-scheme/test.ss b/collects/typed-scheme/test.ss index 148488a5..c9b5d7c5 100644 --- a/collects/typed-scheme/test.ss +++ b/collects/typed-scheme/test.ss @@ -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))} \ No newline at end of file diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss index 577dbd2b..366056c8 100644 --- a/collects/typed-scheme/typecheck/signatures.ss +++ b/collects/typed-scheme/typecheck/signatures.ss @@ -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?)] diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 6d1e9298..3973404b 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -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")) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index 831e0dcd..43fbcc99 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -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 diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss index ae4f4296..b0b16629 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -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)))) diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index e9ba2608..7bb32a49 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -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 diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss index 5a43f819..72053d9b 100644 --- a/collects/typed-scheme/typed-scheme.ss +++ b/collects/typed-scheme/typed-scheme.ss @@ -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))]))])) diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 165dbb6c..be209812 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -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)) \ No newline at end of file + (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)])) \ No newline at end of file diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index cc5b3673..6667f41f 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -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 ")")])) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 4c154e5c..39570982 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -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*)] diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss index 8d86e992..e37685ed 100644 --- a/collects/typed-scheme/types/utils.ss +++ b/collects/typed-scheme/types/utils.ss @@ -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)) diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss index 69a09d92..f322ad03 100644 --- a/collects/typed-scheme/utils/utils.ss +++ b/collects/typed-scheme/utils/utils.ss @@ -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