rename syntax properties

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 ...)

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+)]))

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=?])