From a3b9cbc712dc5136046638cc5c6947a507a6999b Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 10 Sep 2015 14:29:23 -0400 Subject: [PATCH] fix define-type-constructor to properly error if used at runtime --- tapl/stlc+lit.rkt | 3 ++ tapl/stlc+rec-iso.rkt | 6 +++- tapl/stlc.rkt | 10 +++++- tapl/tests/rackunit-typechecking.rkt | 4 +-- tapl/typecheck.rkt | 50 +++++++++++++++++++--------- 5 files changed, 54 insertions(+), 19 deletions(-) diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt index b24be01..a675b7d 100644 --- a/tapl/stlc+lit.rkt +++ b/tapl/stlc+lit.rkt @@ -26,6 +26,9 @@ #:with op/tc (generate-temporary #'op) #'(begin (provide (rename-out [op/tc op])) + #;(define-syntax op/tc (make-rename-transformer (assign-type #'op #'τ))) + ; rename transformer doesnt seem to expand at the right time + ; - op still has no type in #%app (define-syntax (op/tc stx) (syntax-parse stx [f:id (⊢ #,(syntax/loc stx op) : τ)] ; HO case diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt index 4d70e0c..e204578 100644 --- a/tapl/stlc+rec-iso.rkt +++ b/tapl/stlc+rec-iso.rkt @@ -26,8 +26,12 @@ ; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1)) ; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2)) (syntax-parse (list τ1 τ2) - [(((~literal #%plain-lambda) (x:id ...) k1 ... t1) + [#;(((~literal #%plain-lambda) (x:id ...) k1 ... t1) ((~literal #%plain-lambda) (y:id ...) k2 ... t2)) + (((~literal #%plain-app) tycon1 ((~literal #%plain-lambda) (x:id ...) k1 ... t1)) + ((~literal #%plain-app) tycon2 ((~literal #%plain-lambda) (y:id ...) k2 ... t2))) + #:when ((current-type=?) #'tycon1 #'tycon2) + #:when (types=? #'(k1 ...) #'(k2 ...)) #:when (= (stx-length #'(x ...)) (stx-length #'(y ...))) #:with (z ...) (generate-temporaries #'(x ...)) ((current-type=?) (substs #'(z ...) #'(x ...) #'t1) diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index c705b99..bed5fe7 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -39,7 +39,15 @@ ;; type=? : Type Type -> Boolean ;; Two types are equivalent when structurally free-identifier=? ;; - assumes canonical (ie expanded) representation - (define (type=? τ1 τ2) + (define (type=? t1 t2) + ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum t1)) + ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum t2)) + (or (and (identifier? t1) (identifier? t2) (free-identifier=? t1 t2)) + (and (stx-null? t1) (stx-null? t2)) + (and (stx-pair? t1) (stx-pair? t2) + (with-syntax ([(ta ...) t1][(tb ...) t2]) + (types=? #'(ta ...) #'(tb ...)) #;(types=? t1 t2))))) + #;(define (type=? τ1 τ2) ; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1)) ; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2)) (syntax-parse (list τ1 τ2) diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt index 241eebb..f998de2 100644 --- a/tapl/tests/rackunit-typechecking.rkt +++ b/tapl/tests/rackunit-typechecking.rkt @@ -22,9 +22,9 @@ #:fail-when (typecheck? #'τ ((current-type-eval) #'not-τ)) (format - "(~a:~a) Expression ~a should not have type ~a" + "(~a:~a) Expression ~a has type ~a; should not typecheck with ~a" (syntax-line stx) (syntax-column stx) - (syntax->datum #'e) (type->str #'τ)) + (syntax->datum #'e) (type->str #'τ) (type->str #'not-τ)) #'(void)])) (define-syntax (typecheck-fail stx) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 2470ca2..bea2c16 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -93,10 +93,13 @@ "~a (~a:~a): Expected expression ~s to have ~a type, got: ~a" (syntax-source #'e) (syntax-line #'e) (syntax-column #'e) (syntax->datum #'e) 'tycon (type->str #'τ_e)) - (if (stx-pair? #'τ_e) + #;(if (stx-pair? #'τ_e) (syntax-parse #'τ_e [(τ-expander . args) #'(e- args)]) - #'e-)])])) + #'e-) + (syntax-parse #'τ_e + [(τ-expander . args) #'(e- args)] + [_ #'e-])])])) (define-syntax (⇑s stx) (syntax-parse stx #:datum-literals (as) [(_ es as tycon) @@ -117,10 +120,13 @@ ;#:with args (τ-get #'τ_e) #:with res (stx-map (λ (e t) - (if (stx-pair? t) + #;(if (stx-pair? t) (syntax-parse t [(τ-expander . args) #`(#,e #'args)]) - e)) + e) + (syntax-parse t + [(τ-expander . args) #`(#,e #'args)] + [_ e])) #'(e- (... ...)) #'(τ_e (... ...))) #'res])])) @@ -170,7 +176,12 @@ (assign-type #'tv #'k) #'ok #:tag '#,tag))] ...) (λ (x ...) - (let-syntax ([x (make-rename-transformer + (let-syntax ([x (syntax-parser [_:id (assign-type #'x #'τ)] + [(o . rst) ; handle if x used in fn position + #:with app (datum->syntax #'o '#%app) + #`(app #,(assign-type #'x #'τ) . rst)] + #;[(_ . rst) #`(#,(assign-type #'x #'τ) . rst)]) + #;(make-rename-transformer (assign-type #'x #'τ))] ...) (#%expression e) ... void))))) (list #'tvs+ #'xs+ #'(e+ ...) @@ -270,7 +281,9 @@ #'(begin (provide τ (for-syntax τ? τ-expander)) (begin-for-syntax - (define (τ? t) (and (identifier? t) (free-identifier=? t #'τ-internal))) + (define (τ? t) ;(and (identifier? t) (free-identifier=? t #'τ-internal))) + (syntax-parse t + [((~literal #%plain-app) (~literal τ-internal)) #t][_ #f])) (define (inferτ+erase e) (syntax-parse (infer+erase e) #:context e [(e- e_τ) @@ -283,16 +296,18 @@ (define-syntax τ-expander (pattern-expander (syntax-parser - [ty:id #'(~literal τ-internal)] - [(_ . rst) - #'((~literal τ-internal) . rst)])))) + ;[ty:id #'(~literal τ-internal)] + [ty:id #'((~literal #%plain-app) (~literal τ-internal))] + ;[(_ . rst) #'((~literal τ-internal) . rst)])))) + [(_ . rst) #'(((~literal #%plain-app) (~literal τ-internal)) . rst)])))) (define τ-internal (λ () (raise (exn:fail:type:runtime (format "~a: Cannot use type at run time" 'τ) (current-continuation-marks))))) (define-syntax τ (syntax-parser - [(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))])) + ;[(~var _ id) (add-orig (assign-type #'τ-internal #'kind) #'τ)])))])) + [(~var _ id) (add-orig (assign-type #'(τ-internal) #'kind) #'τ)])))])) ; I use identifiers "τ" and "kind" but this form is not restricted to them. ; E.g., τ can be #'★ and kind can be #'#%kind (★'s type) @@ -317,14 +332,16 @@ (pattern-expander (syntax-parser [(_ . pat:id) - #'(~and ((~literal #%plain-lambda) bvs + #'(~and #;((~literal #%plain-lambda) bvs ((~literal #%plain-app) (~literal τ-internal) . rst)) + ((~literal #%plain-app) (~literal τ-internal) ((~literal #%plain-lambda) bvs (~literal void) . rst)) #,(if (attribute has-bvs?) #'(~parse pat #'(bvs rst)) #'(~parse pat #'rst)))] [(_ (~optional (~and (~fail #:unless #,(attribute has-bvs?)) bvs-pat) #:defaults ([bvs-pat #'()])) . pat) - #'((~literal #%plain-lambda) bvs-pat + #'((~literal #%plain-app) (~literal τ-internal) ((~literal #%plain-lambda) bvs-pat (~literal void) . pat)) + #;((~literal #%plain-lambda) bvs-pat ((~literal #%plain-app) (~literal τ-internal) . pat))]))) (define-syntax τ-expander* (pattern-expander @@ -342,8 +359,10 @@ (define (τ? t) (and (stx-pair? t) (syntax-parse t - [((~literal #%plain-lambda) bvs ((~literal #%plain-app) (~literal τ-internal) . _)) - #t #;(typecheck? #'tycon #'τ-internal)] + #;[((~literal #%plain-lambda) bvs ((~literal #%plain-app) (~literal τ-internal) . _)) + #t] + [((~literal #%plain-app) (~literal τ-internal) . _) + #t] [_ #f])))) (define τ-internal (λ _ (raise (exn:fail:type:runtime @@ -364,7 +383,8 @@ (infers/ctx+erase #'([bv : #%kind] (... ...)) #'args #:expand (current-type-eval)) #:with (~! (~var _ kind) (... ...)) #'τs- - (assign-type #'(λ bvs- (τ-internal . τs-)) #'#%kind)] + ;(assign-type #'(λ bvs- (τ-internal . τs-)) #'#%kind) + (assign-type #'(τ-internal (λ bvs- void . τs-)) #'#%kind)] ;; else fail with err msg [_ (type-error #:src stx