From dcfb3ff9874dc46ea4b37d9d3c55df254dce867f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Fri, 5 May 2017 03:30:42 +0200 Subject: [PATCH] =?UTF-8?q?Improved=20contract=E2=86=92type?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- contracts-to-types.rkt | 115 +++++++++++++++++++++------ scribblings/contracts-to-types.scrbl | 13 ++- scribblings/type-expander.scrbl | 4 +- test/test-contracts-to-types.rkt | 45 +++++++++++ 4 files changed, 145 insertions(+), 32 deletions(-) create mode 100644 test/test-contracts-to-types.rkt diff --git a/contracts-to-types.rkt b/contracts-to-types.rkt index 5c4b0fe..053fb70 100644 --- 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 index b5660b0..e198ed5 100644 --- 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 index 42d7722..c029d56 100644 --- 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 new file mode 100644 index 0000000..90a8c89 --- /dev/null +++ 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