add types for Stx-Null, Stx-Pairof, and Stx-Listof

pkgs/typed-racket-pkgs/typed-racket-more/typed/syntax/stx.rkt

@@ -2,38 +2,58 @@
 
 (require syntax/stx)
 
+(module types typed/racket/base
+  (provide Stxof
+           Stx-Null
+           Stx-Pairof
+           Stx-Listof)
+  (define-type (Stxof t)
+    (U t (Syntaxof t)))
+  (define-type Stx-Null
+    (Stxof Null))
+  (define-type (Stx-Pairof a b)
+    (Stxof (Pairof a b)))
+  (define-type (Stx-Listof a)
+    (Rec lst
+         (U Stx-Null
+            (Stx-Pairof a lst)))))
+(require 'types)
+(provide (all-from-out 'types))
+
 (begin-for-syntax
- (define (-stx-list type)
+  (define (-Stxof t)
-   (Un (-lst type) (-Syntax (-lst type)))))
+    (Un t (-Syntax t)))
+  (define -Stx-Null
+    (-Stxof -Null))
+  (define (-Stx-Pairof a b)
+    (-Stxof (-pair a b)))
+  (define (-Stx-Listof a)
+    (-mu lst
+         (Un -Stx-Null
+             (-Stx-Pairof a lst)))))
 
 (type-environment
- [stx-null? (make-pred-ty (Un -Null (-Syntax -Null)))]
+ [stx-null? (make-pred-ty -Stx-Null)]
- [stx-pair? (make-pred-ty (Un (-pair Univ Univ) (-Syntax (-pair Univ Univ))))]
+ [stx-pair? (make-pred-ty (-Stx-Pairof Univ Univ))]
- [stx-list? (make-pred-ty (-stx-list Univ))]
+ [stx-list? (make-pred-ty (-Stx-Listof Univ))]
  [stx->list (-poly (a)
-              (cl->* (-> (-lst a) (-lst a))
+              (cl->* (-> (-Stx-Listof a) (-lst a))
-                     (-> (-Syntax (-lst a)) (-lst a))
                      (-> (-Syntax Univ) (-val #f))))]
  [stx-car (-poly (a b)
             (cl->*
-             (-> (-pair a b) a)
+             (-> (-Stx-Pairof a b) a)
-             (-> (-lst a) a)
+             (-> (-Stx-Listof a) a)))]
-             (-> (-Syntax (-pair a b)) a)
-             (-> (-Syntax (-lst a)) a)))]
  [stx-cdr (-poly (a b)
             (cl->*
-             (-> (-pair a b) b)
+             (-> (-Stx-Pairof a b) b)
              (-> (-lst a) (-lst a))
-             (-> (-Syntax (-pair a (-lst b))) (-lst b))
+             (-> (-Stx-Listof a) (-Stx-Listof a))))]
-             (-> (-Syntax (-pair a b)) b)
-             (-> (-Syntax (-lst a)) (-lst a))))]
  [stx-map (-polydots (c a b)
             (cl->*
-             (-> (-> a c) (-pair a (-lst a)) (-pair c (-lst c)))
+             (-> (-> a c) (-Stx-Pairof a (-Stx-Listof a)) (-pair c (-lst c)))
-             (-> (-> a c) (-Syntax (-pair a (-lst a))) (-pair c (-lst c)))
              ((list
                ((list a) (b b) . ->... . c)
-               (Un (-lst a) (-Syntax (-lst a))))
+               (-Stx-Listof a))
-              ((Un (-lst b) (-Syntax (-lst b))) b) . ->... .(-lst c))))]
+              ((-Stx-Listof b) b) . ->... .(-lst c))))]
  [module-or-top-identifier=?
   (-> (-Syntax -Symbol) (-Syntax -Symbol) -Boolean)])

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/stx.rkt

@@ -20,6 +20,8 @@
 (ann (stx->list (list #'a #'b)) (Listof (Syntaxof Symbol)))
 (ann (stx->list (list 'a 'b)) (Listof Symbol))
 (ann (add1 (car (stx->list '(1 2 3)))) Positive-Index)
+(ann (stx->list #'(a b . (c d))) (Listof (Syntaxof Symbol)))
+(ann (stx->list (cons #'a #'(b . (c d)))) (Listof (Syntaxof Symbol)))
 
 (ann (stx-car #'(a b)) (Syntaxof 'a))
 (ann (stx-cdr #'(a b)) (List (Syntaxof 'b)))
@@ -30,6 +32,9 @@
 (ann (stx-map (λ: ([id : Symbol]) (symbol=? id 'a))
               '(a b c d))
      (Listof Boolean))
+(ann (stx-map (λ: ([id : Identifier]) (free-identifier=? id #'a))
+              (cons #'a #'(b . (c d))))
+     (Listof Boolean))
 (ann (stx-map (λ: ([x : (Syntaxof Real)] [y : (Syntaxof Real)])
                 (+ (syntax-e x) (syntax-e y)))
               #'(1 2 3)
@@ -39,6 +44,11 @@
               '(1 2 3)
               '(1 2 3))
      (Listof Real))
+(ann (stx-map (λ: ([x : (Syntaxof Real)] [y : (Syntaxof Real)])
+                (+ (syntax-e x) (syntax-e y)))
+              #'(1 . (2 3))
+              (cons #'1 #'(2 . (3))))
+     (Listof Real))
 
 (module-or-top-identifier=? #'a #'b)