Added typed version of stx-cons.

This commit is contained in:
Georges Dupéron 2016-01-20 20:36:04 +01:00
parent 600683d832
commit 832d1ed9cf

View File

@ -1017,18 +1017,60 @@
(module m-stx-untyped racket
(require syntax/stx)
(provide stx-cons stx-drop-last)
(provide stx-cons #;stx-drop-last)
;(: stx-cons (∀ (A B) (→ A B (Syntaxof (Pairof A B)))))
(define (stx-cons a b) #`(#,a . #,b))
;(: stx-drop-last (∀ (A) (→ (Syntaxof (Listof A)) (Syntaxof (Listof A)))))
(define (stx-drop-last l)
#;(define (stx-drop-last l)
(if (and (stx-pair? l) (stx-pair? (stx-cdr l)))
(stx-cons (stx-car l) (stx-drop-last (stx-cdr l)))
#'())))
(require 'm-stx-untyped)
;; stx-cons
(module m-stx-typed typed/racket
(require typed/racket/unsafe)
(unsafe-require/typed (submod ".." m-stx-untyped)
[stx-cons ( (A B)
( (Syntaxof A)
(Syntaxof B)
(Syntaxof (Pairof (Syntaxof A)
(Syntaxof B)))))])
(provide stx-cons))
(module+ test
(require ;(submod "..")
typed/rackunit)
(check-equal? (syntax->datum
(ann (stx-cons #'a #'(b c))
(Syntaxof (Pairof (Syntaxof 'a)
(Syntaxof (List (Syntaxof 'b)
(Syntaxof 'c)))))))
'(a b c))
(check-equal? (syntax->datum
(ann (stx-cons #'1 (ann #'2 (Syntaxof 2)))
(Syntaxof (Pairof (Syntaxof 1)
(Syntaxof 2)))))
'(1 . 2)))
(require/provide 'm-stx-typed)
;; stx-pair?
(: stx-pair? ( Any Boolean : (Syntaxof Any)))
(define (stx-pair? x) (if (syntax? x) #t #f))
;; stx-drop-last
(: stx-drop-last ( (A) ( (Syntaxof (Listof A)) (Syntaxof (Listof A)))))
(define (stx-drop-last l)
(if (and (stx-pair? l) (stx-pair? (stx-cdr l)))
(stx-cons (stx-car l) (stx-drop-last (stx-cdr l)))
#'()))
; (require/typed racket/base [(assoc assoc3)
; (∀ (a b) (→ Any (Listof (Pairof a b))