From 336b6ea1f342aeece909ee4d515e22c5018a057e Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 20 Aug 2015 14:49:33 -0400 Subject: [PATCH] fix bugs in fomega2 --- tapl/fomega2.rkt | 45 +++++++++++++++++++++++++++------------------ tapl/stlc.rkt | 4 +++- tapl/typecheck.rkt | 12 ++++++++---- 3 files changed, 38 insertions(+), 23 deletions(-) diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt index 8969497..b25c6b3 100644 --- a/tapl/fomega2.rkt +++ b/tapl/fomega2.rkt @@ -27,32 +27,37 @@ (define-syntax define-type-alias (syntax-parser [(_ alias:id τ) - #:with (τ- k_τ) (infer+erase #'τ) + ;#:with (τ- k_τ) (infer+erase #'τ) + #:with τ+ ((current-type-eval) #'τ) + #:with k_τ (typeof #'τ+) #:fail-unless (kind? #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ)) - #'(define-syntax alias (syntax-parser [x:id #'τ-]))])) + #'(define-syntax alias + (syntax-parser [x:id #'τ+] [(_ . rst) #'(τ+ . rst)]))])) (begin-for-syntax ;; extend type-eval to handle tyapp ;; - requires manually handling all other forms (define (type-eval τ) + (beta (sysf:type-eval τ))) + (define (beta τ) (syntax-parse τ [((~literal #%plain-app) τ_fn τ_arg ...) - #:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn) - #:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...)) - (substs #'(τ_arg+ ...) #'(tv ...) #'τ_body)] - [((~literal ∀) _ ...) ((current-type-eval) (sysf:type-eval τ))] - [((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))] + #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'τ_fn + ;#:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...)) + ((current-type-eval) (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] + ;[((~literal ∀) _ ...) ((current-type-eval) (sysf:type-eval τ))] + ;[((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))] ; [((~literal ⇒) _ ...) ((current-type-eval) (sysf:type-eval τ))] ; [((~literal λ/tc) _ ...) (sysf:type-eval τ)] ; [((~literal app/tc) _ ...) ((current-type-eval) (sysf:type-eval τ))] - [((~literal #%plain-lambda) (x ...) τ_body ...) - #:with (τ_body+ ...) (stx-map (current-type-eval) #'(τ_body ...)) - (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'plain-lambda)] + #;[((~literal #%plain-lambda) (x ...) τ_body ...) + #:with (τ_body+ ...) (stx-map beta #'(τ_body ...)) + (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)] [((~literal #%plain-app) arg ...) - #:with (arg+ ...) (stx-map (current-type-eval) #'(arg ...)) + #:with (arg+ ...) (stx-map beta #'(arg ...)) (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)] ;[(τ ...) (stx-map (current-type-eval) #'(τ ...))] - [_ (sysf:type-eval τ)])) + [_ τ])) (current-type-eval type-eval)) (define-basic-checked-id-stx ★ : #%kind) @@ -69,13 +74,15 @@ (define-syntax (tycon stx) (syntax-parse stx [(_ τ ... τ_res) - #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res)) + ;#:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res)) + #:with (τ+ ...) (stx-map (current-type-eval) #'(τ ... τ_res)) + #:with (k ... k_res) (stx-map typeof #'(τ+ ...)) #:when (or ; when used as → (and (or (★? #'k_res) (#%kind? #'k_res)) (same-types? #'(k ... k_res)))) (if (★? #'k_res) - (⊢ (tycon-internal τ- ... τ_res-) : ★) - (⊢ (tycon-internal τ- ... τ_res-) : #%kind))]))))])) + (⊢ (tycon-internal τ+ ...) : ★) + (⊢ (tycon-internal τ+ ...) : #%kind))]))))])) (define-multi →) (define-syntax (∀ stx) @@ -93,7 +100,9 @@ (define-syntax (inst stx) (syntax-parse stx [(_ e τ ...) - #:with ([τ- k_τ] ...) (infers+erase #'(τ ...)) + ;#:with ([τ- k_τ] ...) (infers+erase #'(τ ...)) + #:with (τ+ ...) (stx-map (current-type-eval) #'(τ ...)) + #:with (k_τ ...) (stx-map typeof #'(τ+ ...)) #:when (stx-andmap (λ (t k) (or (kind? k) @@ -103,7 +112,7 @@ #:with (e- ∀τ) (infer+erase #'e) #:with ((~literal #%plain-lambda) (tv ...) k_tv ... τ_body) #'∀τ #:when (typechecks? #'(k_τ ...) #'(k_tv ...)) - (⊢ e- : #,(substs #'(τ ...) #'(tv ...) #'τ_body))])) + (⊢ e- : #,((current-type-eval) (substs #'(τ+ ...) #'(tv ...) #'τ_body)))])) #;(define-syntax (inst stx) (syntax-parse stx [(_ e τ:type ...) @@ -140,7 +149,7 @@ (define-syntax (app/tc stx) (syntax-parse stx [(_ e_fn e_arg ...) - #:with [e_fn- ((~literal #%plain-lambda) _ τ_in ... τ_out)] (infer+erase #'e_fn) + #:with [e_fn- ((~literal #%plain-app) _ τ_in ... τ_out)] (infer+erase #'e_fn) #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...)) #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) (string-append diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index 82604e1..46cd56b 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -21,7 +21,7 @@ ;; - may require some caution when mixing expanded and unexpanded types to ;; create other types (define (type-eval τ) - (or (expanded-type? τ) ; don't expand if already expanded + (or #;(expanded-type? τ) ; don't expand if already expanded (add-orig (expand/df τ) τ))) (current-type-eval type-eval) @@ -47,6 +47,8 @@ (define current-type=? (make-parameter type=?)) (current-typecheck-relation type=?)) +;(define-syntax-category type) + (define-basic-checked-stx → #:arity >= 1) #;(define-type-constructor (→ τ_in ... τ_out) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 56c7e44..372af5e 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -287,7 +287,7 @@ (define (bracket? stx) (define paren-shape/#f (syntax-property stx 'paren-shape)) (and paren-shape/#f (char=? paren-shape/#f #\[))) - (define-syntax-class bound-vars + #;(define-syntax-class bound-vars (pattern (~and stx [[x:id ...]] #;[[(~and x:id (~not (~literal ...))) ... (~optional (~literal ...))]]) @@ -297,7 +297,7 @@ (define (bracket? stx) (define paren-shape/#f (syntax-property stx 'paren-shape)) (and paren-shape/#f (char=? paren-shape/#f #\[))) - (define-syntax-class bound-vars + #;(define-syntax-class bound-vars (pattern (~and stx [[x:id ...]] #;[[(~and x:id (~not (~literal ...))) ... (~optional (~literal ...))]]) @@ -901,17 +901,21 @@ #:with #%tag? (mk-? #'#%tag) #:with name? (mk-? #'name) #:with named-binding (format-id #'name "~aed-binding" #'name) + #:with current-name? (format-id #'name? "current-~a" #'name?) #'(begin (define #%tag void) (begin-for-syntax (define (#%tag? t) (typecheck? t #'#%tag)) (define (name? t) (#%tag? (typeof t))) + (define current-name? (make-parameter name?)) (define-syntax-class name #:attributes (norm) (pattern τ #:with norm ((current-type-eval) #'τ) #:with k (typeof #'norm) #:fail-unless (#%tag? #'k) + ;#:fail-unless ((current-name?) #'norm) + ;#:fail-unless ((current-name?) #'norm) (format "~a (~a:~a) not a valid ~a: ~a" (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ) 'name (type->str #'τ)))) @@ -1009,7 +1013,7 @@ (stx-fold subst e τs xs)) ; subst τ for y in e, if (equal? (syntax-e x) (syntax-e y)) - (define-for-syntax (subst-datum-lit τ x e) + #;(define-for-syntax (subst-datum-lit τ x e) (syntax-parse e [y:id #:when (equal? (syntax-e e) (syntax-e x)) τ] [(esub ...) @@ -1017,7 +1021,7 @@ (syntax-track-origin #'(esub_subst ...) e x)] [_ e])) - (define-for-syntax (subst-datum-lits τs xs e) + #;(define-for-syntax (subst-datum-lits τs xs e) (stx-fold subst-datum-lit e τs xs)))