From e912818f866d6bcbeb43e4567ba9d0f1d58d6e3c Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 10 Jun 2008 14:10:40 -0400 Subject: [PATCH] Instantiation appears to work. --- collects/typed-scheme/private/base-env.ss | 14 ++++++++++++++ collects/typed-scheme/private/extra-procs.ss | 6 +++++- collects/typed-scheme/private/tc-expr-unit.ss | 11 +++++++++-- .../typed-scheme/private/type-effect-printer.ss | 4 +++- collects/typed-scheme/private/type-rep.ss | 3 ++- collects/typed-scheme/private/type-utils.ss | 2 +- collects/typed-scheme/private/utils.ss | 2 +- 7 files changed, 35 insertions(+), 7 deletions(-) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 898796f66f..0b8695a31e 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -498,6 +498,20 @@ [syntax? (make-pred-ty (-Syntax Univ))] [syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a)) (-> (-Syntax Univ) Univ Univ)))] + + ;; experimental + + [map* (make-PolyDots + (list 'a 'b 'c) + (make-Function + (list + (make-arr-dots + (list (make-Function (list (make-arr-dots (list (-v b)) (-v a) (-v c) 'c))) + (-lst (-v b))) + (-lst (-v a)) + (-lst (-v c)) + 'c))))] + ))) (begin-for-syntax diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss index b8b87b6c44..428b5eaf5e 100644 --- a/collects/typed-scheme/private/extra-procs.ss +++ b/collects/typed-scheme/private/extra-procs.ss @@ -1,7 +1,11 @@ #lang scheme/base -(provide assert) +(provide assert map*) (define (assert v) (unless v (error "Assertion failed - value was #f")) v) + +(define map* map) + + diff --git a/collects/typed-scheme/private/tc-expr-unit.ss b/collects/typed-scheme/private/tc-expr-unit.ss index b9a48725c7..67bf815853 100644 --- a/collects/typed-scheme/private/tc-expr-unit.ss +++ b/collects/typed-scheme/private/tc-expr-unit.ss @@ -69,13 +69,20 @@ (let* ([ty (lookup-type/lexical id)] [inst (syntax-property id 'type-inst)]) (cond [(and inst - (not (Poly? ty))) + (not (or (Poly? ty) (PolyDots? ty)))) (tc-error/expr #:return (ret (Un)) "Cannot instantiate non-polymorphic type ~a" ty)] + [(and inst - (not (= (length (syntax->list inst)) (Poly-n ty)))) + (Poly? ty) + (not (= (length (syntax->list inst)) (Poly-n ty)))) (tc-error/expr #:return (ret (Un)) "Wrong number of type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a" ty (Poly-n ty) (length (syntax->list inst)))] + [(and inst (PolyDots? ty) (not (>= (length (syntax->list inst)) (sub1 (PolyDots-n ty))))) + ;; we can provide 0 arguments for the ... var + (tc-error/expr #:return (ret (Un)) + "Wrong number of type arguments to polymorphic type ~a:~nexpected at least: ~a~ngot: ~a" + ty (sub1 (PolyDots-n ty)) (length (syntax->list inst)))] [else (let ([ty* (if inst (instantiate-poly ty (map parse-type (syntax->list inst))) diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss index c2a2d940db..2a5dac4dcd 100644 --- a/collects/typed-scheme/private/type-effect-printer.ss +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -52,7 +52,7 @@ (when rest (fp "~a* " rest)) (when drest - (fp "~a ..." drest)) + (fp "~a ... ~a " (car drest) (cdr drest))) (fp "-> ~a" rng) (unless (and (null? thn-eff) (null? els-eff)) (fp " : ~a ~a" thn-eff els-eff)) @@ -115,6 +115,8 @@ [(Poly-names: names body) #;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body)) (fp "(All ~a ~a)" names body)] + [(PolyDots-names: (list names ... dotted) body) + (fp "(All ~a ~a)" (append names (list dotted '...)) body)] #; [(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)] [(Mu: x (Syntax: (Union: (list diff --git a/collects/typed-scheme/private/type-rep.ss b/collects/typed-scheme/private/type-rep.ss index ce8583d49e..b15df1cbd4 100644 --- a/collects/typed-scheme/private/type-rep.ss +++ b/collects/typed-scheme/private/type-rep.ss @@ -337,7 +337,7 @@ (if rest (sb rest) #f) (if drest (cons (sb (car drest)) - (if (= (cdr drest) (+ count outer)) (F-n image) (cdr drest))) + (if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest))) #f) (map (lambda (e) (sub-eff sb e)) thn-eff) (map (lambda (e) (sub-eff sb e)) els-eff))] @@ -526,6 +526,7 @@ [PolyDots:* PolyDots:] [Mu* make-Mu] [Poly* make-Poly] + [PolyDots* make-PolyDots] [Mu-body* Mu-body] [Poly-body* Poly-body] [PolyDots-body* PolyDots-body])) diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index ead27eea21..621f6aabbd 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -33,7 +33,7 @@ (begin (when (and (pair? drest) (eq? name (cdr drest))) - (int-err "substitute used on ... variable ~a" name)) + (int-err "substitute used on ... variable ~a in type ~a" name target)) (make-arr (map sb dom) (sb rng) (and rest (sb rest)) diff --git a/collects/typed-scheme/private/utils.ss b/collects/typed-scheme/private/utils.ss index efdc4da4d1..1d3275c9a7 100644 --- a/collects/typed-scheme/private/utils.ss +++ b/collects/typed-scheme/private/utils.ss @@ -99,7 +99,7 @@ [(_ val) #'(? (lambda (x) (equal? val x)))]))) -(define-for-syntax printing? #f) +(define-for-syntax printing? #t) (define print-type* (box (lambda _ (error "print-type* not yet defined")))) (define print-effect* (box (lambda _ (error "print-effect* not yet defined"))))