From bb8d8e23d81c7f1324d1bfc8b33882fc71f94503 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Thu, 19 Jun 2008 14:57:35 -0400 Subject: [PATCH] * Split apart identifier typechecking and type instantiation * Add dotted instantiation (replacing bounds with different bounds) * Fix some macro issues, including syntax locations * Fix more effect inference --- collects/typed-scheme/private/infer-unit.ss | 14 +++- collects/typed-scheme/private/prims.ss | 23 ++++-- collects/typed-scheme/private/tc-expr-unit.ss | 82 ++++++++++++------- .../private/type-effect-convenience.ss | 8 +- collects/typed-scheme/private/type-utils.ss | 37 +++++++-- 5 files changed, 116 insertions(+), 48 deletions(-) diff --git a/collects/typed-scheme/private/infer-unit.ss b/collects/typed-scheme/private/infer-unit.ss index f1445f35e2..1f6c0a4fe2 100644 --- a/collects/typed-scheme/private/infer-unit.ss +++ b/collects/typed-scheme/private/infer-unit.ss @@ -127,7 +127,10 @@ (cgen/list X V (extend ts ss s-rest) ts)] [else (fail! S T)])] [ret-mapping (cg t s)]) - (cset-meet arg-mapping ret-mapping))] + (cset-meet* + (list arg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))] [((arr: ts t #f (cons dty dbound) t-thn-eff t-els-eff) (arr: ss s #f #f s-thn-eff s-els-eff)) (unless (memq dbound X) @@ -164,7 +167,10 @@ (let* ([arg-mapping (cgen/list X V ss ts)] [darg-mapping (cgen (cons dbound V) X s-dty t-dty)] [ret-mapping (cg t s)]) - (cset-meet* (list arg-mapping darg-mapping ret-mapping)))] + (cset-meet* + (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))] [((arr: ts t t-rest #f t-thn-eff t-els-eff) (arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff)) (unless (memq dbound X) @@ -174,7 +180,9 @@ (let* ([arg-mapping (cgen/list X V ss (extend ss ts t-rest))] [darg-mapping (move-rest-to-dmap (cgen (cons dbound V) X s-dty t-rest) dbound)] [ret-mapping (cg t s)]) - (cset-meet* (list arg-mapping darg-mapping ret-mapping))) + (cset-meet* (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff)))) ;; the hard case (let* ([num-vars (- (length ts) (length ss))] [vars (for/list ([n (in-range num-vars)]) diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index b9fdfe2e4f..2414b55290 100644 --- a/collects/typed-scheme/private/prims.ss +++ b/collects/typed-scheme/private/prims.ss @@ -124,16 +124,20 @@ This file defines two sorts of primitives. All of them are provided into any mod (define-syntax (plambda: stx) (syntax-case stx () [(plambda: (tvars ...) formals . body) - (syntax-property #'(lambda: formals . body) - 'typechecker:plambda - #'(tvars ...))])) + (quasisyntax/loc stx + (#%expression + #,(syntax-property (syntax/loc stx (lambda: formals . body)) + 'typechecker:plambda + #'(tvars ...))))])) (define-syntax (pcase-lambda: stx) (syntax-case stx () [(pcase-lambda: (tvars ...) cl ...) - (syntax-property #'(case-lambda: cl ...) - 'typechecker:plambda - #'(tvars ...))])) + (quasisyntax/loc stx + (#%expression + #,(syntax-property (syntax/loc stx (case-lambda: cl ...)) + 'typechecker:plambda + #'(tvars ...))))])) (define-syntax (pdefine: stx) (syntax-case stx (:) @@ -173,8 +177,11 @@ This file defines two sorts of primitives. All of them are provided into any mod (define-syntax (inst stx) (syntax-case stx (:) - [(_ arg : tys ...) - (syntax-property #'arg 'type-inst #'(tys ...))] + [(_ arg : . tys) + (syntax/loc stx (inst arg . tys))] + [(_ arg tys ... ty ddd b) + (eq? (syntax-e #'ddd) '...) + (syntax-property #'arg 'type-inst #'(tys ... (ty . b)))] [(_ arg tys ...) (syntax-property #'arg 'type-inst #'(tys ...))])) diff --git a/collects/typed-scheme/private/tc-expr-unit.ss b/collects/typed-scheme/private/tc-expr-unit.ss index 207774dadc..d0a4acd1ca 100644 --- a/collects/typed-scheme/private/tc-expr-unit.ss +++ b/collects/typed-scheme/private/tc-expr-unit.ss @@ -15,7 +15,9 @@ "lexical-env.ss" ;; maybe needs tests "type-annotation.ss" ;; has tests "effect-rep.ss" - scheme/private/class-internal) + (only-in "type-environments.ss" lookup current-tvars extend-env) + scheme/private/class-internal + (only-in srfi/1 split-at)) (require (for-template scheme/base scheme/private/class-internal)) @@ -49,32 +51,52 @@ [(regexp? v) -Regexp] [else Univ])) + +(define (do-inst stx ty) + (define inst (syntax-property stx 'type-inst)) + (define (split-last l) + (let-values ([(all-but last-list) (split-at l (sub1 (length l)))]) + (values all-but (car last-list)))) + (cond [(not inst) ty] + [(not (or (Poly? ty) (PolyDots? ty))) + (tc-error/expr #:return (ret (Un)) "Cannot instantiate non-polymorphic type ~a" ty)] + + [(and (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 (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)))] + [(and (PolyDots? ty) (= (length (syntax->list inst)) (PolyDots-n ty))) + ;; In this case, we need to check the last thing. If it's a dotted var, then we need to + ;; use instantiate-poly-dotted, otherwise we do the normal thing. + (let-values ([(all-but-last last-stx) (split-last (syntax->list inst))]) + (match (syntax-e last-stx) + [(cons last-ty-stx last-id-stx) + (unless (Dotted? (lookup (current-tvars) (syntax-e last-id-stx) (lambda _ #f))) + (tc-error/stx last-id-stx "~a is not a type variable bound with ..." (syntax-e last-id-stx))) + (let* ([last-id (syntax-e last-id-stx)] + [last-ty + (parameterize ([current-tvars (extend-env (list last-id) + (list (make-DottedBoth (make-F last-id))) + (current-tvars))]) + (parse-type last-ty-stx))]) + (instantiate-poly-dotted ty (map parse-type all-but-last) last-ty last-id))] + [_ + (instantiate-poly ty (map parse-type (syntax->list inst)))]))] + [else + (instantiate-poly ty (map parse-type (syntax->list inst)))])) + ;; typecheck an identifier ;; the identifier has variable effect ;; tc-id : identifier -> tc-result (define (tc-id id) - (let* ([ty (lookup-type/lexical id)] - [inst (syntax-property id 'type-inst)]) - (cond [(and inst - (not (or (Poly? ty) (PolyDots? ty)))) - (tc-error/expr #:return (ret (Un)) "Cannot instantiate non-polymorphic type ~a" ty)] - - [(and inst - (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))) - ty)]) - (ret ty* (list (make-Var-True-Effect id)) (list (make-Var-False-Effect id))))]))) + (let* ([ty (lookup-type/lexical id)]) + (ret ty (list (make-Var-True-Effect id)) (list (make-Var-False-Effect id))))) ;; typecheck an expression, but throw away the effect ;; tc-expr/t : Expr -> Type @@ -129,7 +151,7 @@ [(quote-syntax datum) (ret Any-Syntax)] ;; mutation! [(set! id val) - (match-let* ([(tc-result: id-t) (tc-id #'id)] + (match-let* ([(tc-result: id-t) (tc-expr #'id)] [(tc-result: val-t) (tc-expr #'val)]) (unless (subtype val-t id-t) (tc-error/expr "Mutation only allowed with compatible types:~n~a is not a subtype of ~a" val-t id-t)) @@ -235,7 +257,7 @@ (tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form)] ;; mutation! [(set! id val) - (match-let* ([(tc-result: id-t) (tc-id #'id)] + (match-let* ([(tc-result: id-t) (tc-expr #'id)] [(tc-result: val-t) (tc-expr #'val)]) (unless (subtype val-t id-t) (tc-error/expr "Mutation only allowed with compatible types:~n~a is not a subtype of ~a" val-t id-t)) @@ -276,9 +298,13 @@ (unless (syntax? form) (int-err "bad form input to tc-expr: ~a" form)) ;; typecheck form - (cond [(type-ascription form) => (lambda (ann) - (tc-expr/check form ann))] - [else (internal-tc-expr form)]))) + (let ([ty (cond [(type-ascription form) => (lambda (ann) + (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))])))) (define (tc/send rcvr method args [expected #f]) (match (tc-expr rcvr) diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index a0c6c81594..cf76cb5599 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -35,12 +35,12 @@ [(False-Effect:) eff] [_ (error 'internal-tc-error "can't add var to effect ~a" eff)])) -(define-syntax -> - (syntax-rules (:) +(define-syntax (-> stx) + (syntax-case* stx (:) (lambda (a b) (eq? (syntax-e a) (syntax-e b))) [(_ dom ... rng : eff1 eff2) - (->* (list dom ...) rng : eff1 eff2)] + #'(->* (list dom ...) rng : eff1 eff2)] [(_ dom ... rng) - (->* (list dom ...) rng)])) + #'(->* (list dom ...) rng)])) (define-syntax ->* (syntax-rules (:) diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index 9da1fe368c..5987266e33 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -16,6 +16,7 @@ subst ret instantiate-poly + instantiate-poly-dotted tc-result: tc-result-equal? effects-equal? @@ -52,10 +53,6 @@ (define (sb t) (substitute-dots images name t)) (if (hash-ref (free-vars* target) name #f) (type-case sb target - ;; The way I handled this in my type system is via type validity checking. Hrmm. - #;[#:F name* (if (eq? name* name) - (int-err "substitute-dots: got single variable ~a" name*) - target)] [#:F name* target] [#:arr dom rng rest drest thn-eff els-eff (if (and (pair? drest) @@ -78,6 +75,27 @@ (map (lambda (e) (sub-eff sb e)) els-eff)))]) target)) +;; implements sd from the formalism +;; substitute-dotted : Type Name Type Name -> Type +(define (substitute-dotted image image-bound name target) + (define (sb t) (substitute-dotted image image-bound name t)) + (if (hash-ref (free-vars* target) name #f) + (type-case sb target + [#:F name* + (if (eq? name* name) + image + target)] + [#:arr dom rng rest drest thn-eff els-eff + (make-arr (map sb dom) + (sb rng) + (and rest (sb rest)) + (and drest + (cons (sb (car drest)) + (if (eq? name (cdr drest)) image-bound (cdr drest)))) + (map (lambda (e) (sub-eff sb e)) thn-eff) + (map (lambda (e) (sub-eff sb e)) els-eff))]) + target)) + ;; substitute many variables ;; substitution = Listof[List[Name,Type]] ;; subst-all : substition Type -> Type @@ -105,7 +123,16 @@ [rest-tys (drop types (length fixed))] [body* (subst-all (map list fixed fixed-tys) body)]) (substitute-dots rest-tys dotted body*))] - [_ (int-err "instantiate-many: requires Poly type, got ~a" t)])) + [_ (int-err "instantiate-poly: requires Poly type, got ~a" t)])) + +(define (instantiate-poly-dotted t types image var) + (match t + [(PolyDots: (list fixed ... dotted) body) + (unless (= (length fixed) (length types)) + (int-err "instantiate-poly-dotted: wrong number of types: expected ~a, got ~a" (length fixed) (length types))) + (let ([body* (subst-all (map list fixed types) body)]) + (substitute-dotted image var dotted body*))] + [_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)])) ;; this structure represents the result of typechecking an expression