diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/lengths.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/lengths.rkt index b8d13d71..2f1d000a 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/lengths.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/lengths.rkt @@ -6,47 +6,30 @@ (require "../structures.rkt" + "../terminal.rkt" "simple.rkt" racket/match + (except-in racket/contract recursive-contract) (for-template racket/base)) (provide - list-length/sc - vector-length/sc - empty-list/sc - empty-vector/sc) + (contract-out + [rename list-length/sc* list-length/sc (natural-number/c . -> . static-contract?)] + [vector-length/sc (natural-number/c . -> . static-contract?)] + [empty-list/sc static-contract?] + [empty-vector/sc static-contract?])) +(define-terminal-sc list-length/sc (n) #:flat + #`(λ (l) (and (list? l) (= #,n (length l))))) -(define (length-contract-write-proc v port mode) - (match-define (length-contract name length stx) v) - (define-values (open close) - (if (equal? mode 0) - (values "(" ")") - (values "#<" ">"))) - (display open port) - (fprintf port "~a/sc" name) - (display " " port) - (write length port) - (display close port)) +(define-terminal-sc vector-length/sc (n) #:flat + #`(λ (l) (and (vector? l) (= #,n (vector-length l))))) - -(struct length-contract static-contract (name length syntax) - #:methods gen:sc - [(define (sc-map v f) v) - (define (sc->contract v f) (length-contract-syntax v)) - (define (sc->constraints v f) 'flat)] - #:methods gen:terminal-sc - [(define (terminal-sc-kind v) 'flat)] - #:methods gen:custom-write [(define write-proc length-contract-write-proc)]) - -(define (list-length/sc n) - (if (equal? 0 n) +(define (list-length/sc* n) + (if (zero? n) empty-list/sc - (length-contract 'length n - #`(λ (l) (and (list? l) (= #,n (length l))))))) -(define empty-list/sc (flat/sc #'null?)) + empty-vector/sc)) -(define (vector-length/sc n) - (length-contract 'vector-length n - #`(λ (l) (and (vector? l) (= #,n (vector-length l)))))) + +(define empty-list/sc (flat/sc #'null?)) (define empty-vector/sc (vector-length/sc 0)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/terminal.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/terminal.rkt new file mode 100644 index 00000000..386528e2 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/terminal.rkt @@ -0,0 +1,36 @@ +#lang racket/base + +;; Utilities for defining static contracts that have internal structure but have no sub static +;; contracts. Example: (length/sc 1). + +(require + "structures.rkt" + "constraints.rkt" + racket/match + (for-syntax + racket/base + syntax/parse)) + +(provide + define-terminal-sc) + +(begin-for-syntax + (define-syntax-class kind-keyword + [pattern #:flat #:with sym 'flat] + [pattern #:chaperone #:with sym 'chaperone] + [pattern #:impersonator #:with sym 'impersonator])) + + +(define-syntax (define-terminal-sc stx) + (syntax-parse stx + [(_ name:id (args:id ...) kind:kind-keyword body:expr) + #'(struct name static-contract (args ...) + #:transparent + #:methods gen:sc + [(define (sc-map v f) v) + (define (sc->contract v unused-f) + (match-define (name args ...) v) + body) + (define (sc->constraints v f) (simple-contract-restrict 'kind.sym))] + #:methods gen:terminal-sc + [(define (terminal-sc-kind v) 'kind.sym)])]))