commit a3b9cbc712dc5136046638cc5c6947a507a6999b
parent d1814cb57acb142c2cd63c1b53cf95eba89b06d1
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 10 Sep 2015 14:29:23 -0400
fix define-type-constructor to properly error if used at runtime
Diffstat:
5 files changed, 54 insertions(+), 19 deletions(-)
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
