commit dcfb3ff9874dc46ea4b37d9d3c55df254dce867f
parent c89285f39b2bcfe41f61b3317504e303051a6909
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Fri, 5 May 2017 03:30:42 +0200
Improved contract→type
Diffstat:
4 files changed, 146 insertions(+), 32 deletions(-)
diff --git a/contracts-to-types.rkt b/contracts-to-types.rkt
@@ -4,40 +4,103 @@
(rename-out [c→t contract→type]
[c→t contract->type]
[:contract→type :contract->type]))
-(require racket/contract/base
- (for-syntax syntax/parse
+(require (prefix-in c: (combine-in racket/base racket/contract/base))
+ (for-syntax racket/base
+ syntax/parse
+ syntax/parse/experimental/template
type-expander/expander))
+(begin-for-syntax
+ (define-syntax-class arrow
+ (pattern {~or {~literal ->} {~literal →} {~literal c:->}}))
+ (define-syntax-class arrow*
+ (pattern {~or {~literal ->*} {~literal c:->*}})))
+
(define-type-expander c→t
(syntax-parser
- [(_ ({~literal or/c} alt ...)) #'(U (c→t alt) ...)]
- [(_ ({~literal and/c} alt ...)) #'(∩ (c→t alt) ...)]
- [(_ ({~literal listof} c)) #'(Listof (c→t c))]
- [(_ ({~literal list/c} c ...)) #'(List (c→t c) ...)]
- [(_ ({~literal *list/c} prefix suffix ...)) #'(Rec R (U (Pairof prefix R)
- (List suffix ...)))]
- [(_ ({~literal vectorof} c)) #'(Vectorof (c→t c))]
- [(_ ({~literal vector/c} c ...)) #'(Vector (c→t c) ...)]
- [(_ ({~literal cons/c} a d)) #'(Pairof (c→t a) (c→t d))]
- [(_ {~literal integer?}) #'Integer]
- [(_ {~literal string?}) #'String]
- [(_ {~literal symbol?}) #'Symbol]
- [(_ {~literal exact-nonnegative-integer?}) #'Exact-Nonnegative-Integer]
- [(_ {~literal exact-positive-integer?}) #'Exact-Positive-Integer]
+ [(_ ({~literal c:or/c} alt ...)) #'(U (c→t alt) ...)]
+ [(_ ({~literal c:and/c} alt ...)) #'(∩ (c→t alt) ...)]
+ [(_ ({~literal c:listof} c)) #'(Listof (c→t c))]
+ [(_ ({~literal c:list/c} c ...)) #'(List (c→t c) ...)]
+ [(_ ({~literal c:*list/c} prefix suffix ...))
+ #'(Rec R (U (Pairof (c→t prefix) R)
+ (List (c→t suffix) ...)))]
+ [(_ ({~literal c:vectorof} c)) #'(Vectorof (c→t c))]
+ [(_ ({~literal c:vector/c} c ...)) #'(Vector (c→t c) ...)]
+ [(_ ({~literal c:cons/c} a d)) #'(Pairof (c→t a) (c→t d))]
+ [(_ {~literal c:number?}) #'Number]
+ [(_ {~literal c:integer?}) #'Integer]
+ [(_ {~literal c:string?}) #'String]
+ [(_ {~literal c:symbol?}) #'Symbol]
+ [(_ {~literal c:char?}) #'Char]
+ [(_ {~literal c:boolean?}) #'Boolean]
+ [(_ {~literal c:bytes?}) #'Bytes]
+ [(_ {~literal c:void?}) #'Void]
+ [(_ {~literal c:exact-nonnegative-integer?}) #'Exact-Nonnegative-Integer]
+ [(_ {~literal c:exact-positive-integer?}) #'Exact-Positive-Integer]
+ [(_ ({~literal c:syntax/c} τ)) #'(Syntaxof (c→t τ))]
+ [(_ ({~literal c:parameter/c} in)) #'(Parameterof (c→t in))]
+ [(_ ({~literal c:parameter/c} in out)) #'(Parameterof (c→t in) (c→t out))]
+ [(_ ({~literal c:promise/c} τ)) #'(Promise (c→t τ))]
+ [(_ ({~literal c:suggest/c} τ)) #'(c→t τ)]
+ [(_ ({~literal c:flat-rec-contract} R alt ...))
+ #`(Rec R (U (c→t alt) ...))]
+ [(_ (a:arrow {~seq {~optional kw:keyword}
+ {~and arg {~not {~literal ...}}}}
+ ...
+ rest {~and {~literal ...} ooo}
+ result))
+ #:with rest-kw (datum->syntax #'here '#:rest #'ooo)
+ #:with a* (datum->syntax #'here '->* #'a)
+ (template (a* ((?@ (?? kw) (c→t arg)) ...)
+ rest-kw (c→t rest)
+ (c→t result)))]
+ [(_ (a:arrow {~seq {~optional kw:keyword}
+ {~and arg {~not {~literal ...}}}}
+ ...
+ result))
+ (template (a (?@ (?? kw) (c→t arg)) ... (c→t result)))]
+ [(_ (a*:arrow* ({~seq {~optional mandatory-kw:keyword}
+ mandatory-arg}
+ ...)
+ {~optional
+ {~and opt
+ ({~seq {~optional optional-kw:keyword}
+ optional-arg}
+ ...)}}
+ {~optional {~seq #:rest ({~literal c:listof} rest)}}
+ result))
+ (quasitemplate (a* ((?@ (?? mandatory-kw) (c→t mandatory-arg)) ...)
+ #,@(if (attribute opt)
+ (template
+ {((?@ (?? optional-kw) (c→t optional-arg))
+ ...)})
+ #'{})
+ (?? (?@ #:rest (c→t rest)))
+ (c→t result)))]
+ [(_ {~literal c:any}) #'AnyValues]
+ [(_ ({~literal c:values} v ...)) #'(Values (c→t v) ...)]
[(_ {~and τ ({~literal quote} _)}) #'τ]
- [(_ {~and τ {~or :number :str :id}}) #''τ]
+ [(_ {~and τ {~or :number :str :char :boolean}}) #''τ]
+ [(_ {~and τ}) #:when (bytes? (syntax-e #'τ)) #''τ]
+ [(_ {~and τ}) #:when (regexp? (syntax-e #'τ)) #''τ]
+ [(_ {~and τ}) #:when (byte-regexp? (syntax-e #'τ)) #''τ]
[(_ {~and τ ({~literal quasiquote} _)}) #'τ]
[(_ ({~literal unquote} τ)) #'τ]
+ [(_ v:id)
+ ;; TODO: this is a terrible implementation. type-expander should provide
+ ;; a way to attach information to an identifier, so that we can know that
+ ;; v is a variable bound by flat-rec-contract.
+ #'v]
[(_ c) (raise-syntax-error
- 'contract→type
- (string-append
- "I cannot convert this contract to a type automatically."
- " Please fill in an issue at"
- " https://github.com/jsmaniac/type-expander/issues if the translation"
- " can easily be done automatically, or do the translation manually "
- " otherwise. "
- (format "~a" (syntax->datum #'c)))
- #'c)]))
+ 'contract→type
+ (string-append
+ "I cannot convert this contract to a type automatically."
+ " Please fill in an issue at"
+ " https://github.com/jsmaniac/type-expander/issues if the"
+ " translation can easily be done automatically, or do the"
+ " translation manually otherwise. ")
+ #'c)]))
(define-syntax (:contract→type stx)
(syntax-case stx ()
diff --git a/scribblings/contracts-to-types.scrbl b/scribblings/contracts-to-types.scrbl
@@ -14,10 +14,15 @@
following are supported: @racket[or/c], @racket[and/c] (the translation may
produce a type too complex for Typed/Racket to understand properly, though),
@racket[listof], @racket[list/c], @racket[*list/c], @racket[vectorof],
- @racket[vector/c], @racket[cons/c], @racket[integer?], @racket[string?],
- @racket[symbol?], @racket[exact-nonnegative-integer?],
- @racket[exact-positive-integer?], @racket['quoted-datum],
- @racket[`quasiquoted-datum-with-unquoted-types].
+ @racket[vector/c], @racket[cons/c], @racket[number?], @racket[integer?],
+ @racket[string?], @racket[symbol?], @racket[char?], @racket[boolean?],
+ @racket[bytes?], @racket[void?], @racket[exact-nonnegative-integer?],
+ @racket[exact-positive-integer?], @racket[syntax/c], @racket[parameter/c],
+ @racket[promise/c], @racket[suggest/c], @racket[flat-rec-contract], some uses
+ of @racket[->] and @racket[->*], @racket['quoted-datum],
+ @racket[`quasiquoted-datum-with-unquoted-types]. Literal data (numbers,
+ strings, characters, booleans, byte strings, regular expressions and byte
+ regular expressions) are also interpreted as singleton types.
Furthermore, using @racket[,_τ] anywhere outside of a quoted datum will leave
the type @racket[_τ] unchaged, allowing the user to manually convert to types
diff --git a/scribblings/type-expander.scrbl b/scribblings/type-expander.scrbl
@@ -255,9 +255,9 @@ used in many of @racketmodname[typed/racket]'s forms.
@racketblock[
(define-type three-ints (HomogeneousList 3 Integer))
- (define (incr3 [x : three-ints]) : HomogeneousList
+ (define (incr3 [x : three-ints]) : (HomogeneousList 3 Integer)
(map add1 x))
- (ann (incr3 '(1 2 3)) HomogeneousList)]
+ (ann (incr3 '(1 2 3)) (HomogeneousList 3 Integer))]
Type expanders can produce types which may contain other
uses of type expanders, much in the same way as macros can
diff --git a/test/test-contracts-to-types.rkt b/test/test-contracts-to-types.rkt
@@ -0,0 +1,45 @@
+#lang type-expander
+(require racket/contract/base
+ type-expander/contracts-to-types
+ typed/rackunit)
+(define-syntax-rule (check-written=? a b)
+ (check-equal? (with-output-to-string (λ () a)) (format "~s\n" b)))
+(check-written=? (:contract→type (list/c 1 2 "str" (or/c integer? string?)))
+ '(List 1 2 "str" (U Integer String)))
+(check-written=? (:contract→type
+ (list/c integer? string? boolean? char? bytes?))
+ '(List Integer String Boolean Char Bytes))
+(check-written=? (:contract→type (*list/c integer? string? boolean?))
+ '(Rec R (U (Pairof Integer R) (List String Boolean))))
+(check-written=? (:contract→type (-> integer? boolean? string? symbol?))
+ '(-> Integer Boolean String Symbol))
+(check-written=? (:contract→type (-> integer? boolean? string? ... symbol?))
+ '(->* (Integer Boolean) #:rest String Symbol))
+(check-written=? (:contract→type (->* (integer? boolean?)
+ (char?)
+ #:rest (listof string?)
+ symbol?))
+ '(->* (Integer Boolean) (Char) #:rest String Symbol))
+(check-written=? (:contract→type (->* (integer? boolean?)
+ ()
+ #:rest (listof string?)
+ symbol?))
+ '(->* (Integer Boolean) () #:rest String Symbol))
+(check-written=? (:contract→type (->* (integer? boolean?)
+ #:rest (listof string?)
+ symbol?))
+ '(->* (Integer Boolean) #:rest String Symbol))
+(check-written=? (:contract→type (->* (integer? boolean?)
+ symbol?))
+ '(->* (Integer Boolean) Symbol))
+(check-written=? (:contract→type (->* (integer? boolean?)
+ (char?)
+ symbol?))
+ '(->* (Integer Boolean) (Char) Symbol))
+(check-written=? (:contract→type (->* (integer? boolean?)
+ ()
+ symbol?))
+ '(->* (Integer Boolean) () Symbol))
+(check-written=? (:contract→type
+ (flat-rec-contract W (cons/c W W) number? string?))
+ '(Rec W (U (Pairof W W) Number String)))
+\ No newline at end of file
