From c21c00e3128faa3b26f412545db9d8037730503b Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Mon, 20 Jun 2016 15:04:32 -0400 Subject: [PATCH] rename syntax properties --- tapl/fsub.rkt | 7 +++---- tapl/lam-testing.rkt | 6 +++--- tapl/typecheck.rkt | 43 ++++++++++++++++++++++--------------------- 3 files changed, 28 insertions(+), 28 deletions(-) diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt index b7ca58e..ea4b80c 100644 --- a/tapl/fsub.rkt +++ b/tapl/fsub.rkt @@ -24,7 +24,7 @@ (begin-for-syntax (define (expose t) (cond [(identifier? t) - (define sub (typeof t #:tag 'sub)) + (define sub (typeof t #:tag '<:)) (if sub (expose sub) t)] [else t])) (current-promote expose) @@ -75,11 +75,10 @@ (define-typed-syntax Λ #:datum-literals (<:) [(Λ ([tv:id <: τsub:type] ...) e) ;; NOTE: store the subtyping relation of tv and τsub in another - ;; "environment", ie, a syntax property with another tag: 'sub + ;; "environment", ie, a syntax property with another tag: '<: ;; The "expose" function looks for this tag to enforce the bound, ;; as in TaPL (fig 28-1) - #:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type] ...) - #:octx #'([tv : τsub] ...) #:tag 'sub) + #:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type <: τsub] ...)) (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))]) (define-typed-syntax inst [(inst e τ:type ...) diff --git a/tapl/lam-testing.rkt b/tapl/lam-testing.rkt index 2be3869..a1c3eda 100644 --- a/tapl/lam-testing.rkt +++ b/tapl/lam-testing.rkt @@ -12,11 +12,11 @@ (local-expand #'(λ (x y) (let-syntax -; ([x (λ (sx) (syntax-parse sx [z:id (syntax-property #'y 'type 100)]))]) - ([x (make-rename-transformer (syntax-property #'x 'type 100))]) +; ([x (λ (sx) (syntax-parse sx [z:id (syntax-property #'y ': 100)]))]) + ([x (make-rename-transformer (syntax-property #'x ': 100))]) e)) 'expression null) #:when (printf "~a\n" #'e+) - #:when (printf "~a\n" (syntax-property #'e+ 'type)) + #:when (printf "~a\n" (syntax-property #'e+ ':)) #'(λ xs e+)])) \ No newline at end of file diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index e339cf6..0f129d8 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -26,7 +26,7 @@ ;; type checking functions/forms ;; General type checking strategy: -;; - Each (expanded) syntax object has a 'type syntax property that is the type +;; - Each (expanded) syntax object has a ': syntax property that is the type ;; of the surface form. ;; - To typecheck a surface form, it local-expands each subterm in order to get ;; their types. @@ -167,7 +167,7 @@ ;; - eval here so all types are stored in canonical form ;; - syntax-local-introduce fixes marks on types ;; which didnt get marked bc they were syntax properties - (define (assign-type e τ #:tag [tag 'type]) + (define (assign-type e τ #:tag [tag ':]) (set-stx-prop/preserved e tag (syntax-local-introduce ((current-type-eval) τ)))) (define (add-expected-type e τ) @@ -181,7 +181,7 @@ ;; typeof : Syntax -> Type or #f ;; Retrieves type of given stx, or #f if input has not been assigned a type. - (define (typeof stx #:tag [tag 'type]) + (define (typeof stx #:tag [tag ':]) (define ty (syntax-property stx tag)) (if (cons? ty) (car ty) ty)) @@ -276,12 +276,10 @@ ;; tvctx = tyvars and their kinds ;; octx + tag = some other context (and an associated tag) ;; eg bounded quantification in Fsub - (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] - #:octx [octx tvctx] #:tag [tag 'unused]) + (define (infer es #:ctx [ctx null] #:tvctx [tvctx null]) (syntax-parse ctx #:datum-literals (:) [([x : τ] ...) ; dont expand yet bc τ may have references to tvs - #:with ([tv : k] ...) tvctx - #:with ([_ : ok] ...) octx + #:with ([tv (~seq sep:id tvk) ...] ...) tvctx #:with (e ...) es #:with ; old expander pattern @@ -302,9 +300,10 @@ #`(λ (tv ...) (let-syntax ([tv (make-rename-transformer (set-stx-prop/preserved - (assign-type - (assign-type #'tv #'k) - #'ok #:tag '#,tag) + (for/fold ([tv-id #'tv]) + ([s (in-list (list 'sep ...))] + [k (in-list (list #'tvk ...))]) + (assign-type tv-id k #:tag s)) 'tyvar #t))] ...) (λ (x ...) (let-syntax @@ -380,7 +379,7 @@ ;; term expansion ;; expand/df : Syntax -> Syntax ;; Local expands the given syntax object. - ;; The result always has a type (ie, a 'type stx-prop). + ;; The result always has a type (ie, a ': stx-prop). ;; Note: ;; local-expand must expand all the way down, ie stop-ids == null ;; If stop-ids is #f, then subexpressions won't get expanded and thus won't @@ -598,11 +597,10 @@ #'τ #'any))))]))) (define arg-variances arg-variances-stx) (define (τ? t) - (and (stx-pair? t) - (syntax-parse t - [((~literal #%plain-app) (~literal τ-internal) . _) - #t] - [_ #f])))) + (syntax-parse t + [(~Any/bvs (~literal τ-internal) _ . _) + #t] + [_ #f]))) (define τ-internal (λ _ (raise (exn:fail:type:runtime (format "~a: Cannot use ~a at run time" 'τ 'kind) @@ -747,9 +745,12 @@ (pattern-expander (syntax-parser [(_ tycons bvs . rst) - #'((~literal #%plain-app) tycons - ((~literal #%plain-lambda) bvs - skipped-extra-info . rst))]))) + #'(~and ty + (~parse + ((~literal #%plain-app) tycons + ((~literal #%plain-lambda) bvs + skipped-extra-info . rst)) + ((current-promote) #'ty)))]))) (define-syntax ~Any (pattern-expander (syntax-parser @@ -766,11 +767,11 @@ fail-msg) stx))]))) (define (merge-type-tags stx) - (define t (syntax-property stx 'type)) + (define t (syntax-property stx ':)) (or (and (pair? t) (identifier? (car t)) (identifier? (cdr t)) (free-identifier=? (car t) (cdr t)) - (set-stx-prop/preserved stx 'type (car t))) + (set-stx-prop/preserved stx ': (car t))) stx)) ; subst τ for y in e, if (bound-id=? x y) (define (subst τ x e [cmp bound-identifier=?])