diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt index 8fd9d29..15bb030 100644 --- a/tapl/fomega.rkt +++ b/tapl/fomega.rkt @@ -53,17 +53,19 @@ (define (normalize τ) (syntax-parse τ [x:id #'x] - [((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...) + [((~literal #%plain-app) + ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...) (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] [((~literal #%plain-lambda) (x ...) . bodys) #:with bodys_norm (stx-map normalize #'bodys) - (syntax-track-origin #'(#%plain-lambda (x ...) . bodys_norm) τ #'plain-lambda)] + (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)] [((~literal #%plain-app) x:id . args) #:with args_norm (stx-map normalize #'args) - (syntax-track-origin #'(#%plain-app x . args_norm) τ #'#%plain-app)] + (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)] [((~literal #%plain-app) . args) #:with args_norm (stx-map normalize #'args) - (syntax-track-origin (normalize #'(#%plain-app . args_norm)) τ #'#%plain-app)] + #:with res (normalize #'(#%plain-app . args_norm)) + (transfer-stx-props #'res τ #:ctx τ)] [_ τ])) (define old-eval (current-type-eval)) @@ -123,4 +125,4 @@ (format "Expected: ~a arguments with type(s): " (stx-length #'(k_in ...))) (string-join (stx-map type->str #'(k_in ...)) ", ")) - (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]) \ No newline at end of file + (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]) diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt index 5640f5d..a6468c3 100644 --- a/tapl/fomega2.rkt +++ b/tapl/fomega2.rkt @@ -47,17 +47,18 @@ (define (normalize τ) (syntax-parse τ [x:id #'x] - [((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...) + [((~literal #%plain-app) + ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...) (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] [((~literal #%plain-lambda) (x ...) . bodys) #:with bodys_norm (stx-map normalize #'bodys) - (syntax-track-origin #'(#%plain-lambda (x ...) . bodys_norm) τ #'plain-lambda)] + (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)] [((~literal #%plain-app) x:id . args) #:with args_norm (stx-map normalize #'args) - (syntax-track-origin #'(#%plain-app x . args_norm) τ #'#%plain-app)] + (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)] [((~literal #%plain-app) . args) #:with args_norm (stx-map normalize #'args) - (syntax-track-origin (normalize #'(#%plain-app . args_norm)) τ #'#%plain-app)] + (transfer-stx-props (normalize #'(#%plain-app . args_norm)) τ #:ctx τ)] [_ τ])) (define old-eval (current-type-eval)) @@ -91,4 +92,4 @@ (type-error #:src t #:msg "not a valid type: ~a" t))) #'(τ ...) #'(k_τ ...)) #:when (typechecks? #'(k_τ ...) #'(k ...)) - (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]) \ No newline at end of file + (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]) diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt index 694c731..c496706 100644 --- a/tapl/stx-utils.rkt +++ b/tapl/stx-utils.rkt @@ -70,6 +70,10 @@ (define (generate-temporariesss stx) (stx-map generate-temporariess stx)) +;; transfers properties and src loc from orig to new +(define (transfer-stx-props new orig #:ctx [ctx new]) + (datum->syntax ctx (syntax-e new) orig orig)) + ;; set-stx-prop/preserved : Stx Any Any -> Stx ;; Returns a new syntax object with the prop property set to val. If preserved ;; syntax properties are supported, this also marks the property as preserved. diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 7522e84..82fc3b0 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -754,23 +754,13 @@ (free-identifier=? #'actual #'lit)) fail-msg) this-syntax))]))) - (define (merge-type-tags stx) - (define t (syntax-property stx 'type)) - (or (and (pair? t) - (identifier? (car t)) (identifier? (cdr t)) - (free-identifier=? (car t) (cdr t)) - (set-stx-prop/preserved stx 'type (car t))) - stx)) ; subst τ for y in e, if (bound-id=? x y) (define (subst τ x e [cmp bound-identifier=?]) (syntax-parse e - [y:id #:when (cmp e x) - ; use syntax-track-origin to transfer 'orig - ; but may transfer multiple #%type tags, so merge - (merge-type-tags (syntax-track-origin τ #'y #'y))] + [y:id #:when (cmp e x) (transfer-stx-props τ e)] [(esub ...) - #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1 cmp)) #'(esub ...)) - (syntax-track-origin (syntax/loc e (esub_subst ...)) e x)] + #:with res (stx-map (λ (e1) (subst τ x e1 cmp)) #'(esub ...)) + (transfer-stx-props #'res e #:ctx e)] [_ e])) (define (substs τs xs e [cmp bound-identifier=?])