Add property/c contract combinator for checking first-order properties

pkgs/racket-doc/scribblings/reference/contracts.scrbl

@@ -1091,6 +1091,33 @@ This function is a holdover from before @tech{flat contracts} could be used
 directly as predicates. It exists today for backwards compatibility.
 }
 
+@defproc[(property/c [accessor (-> any/c any/c)]
+                     [ctc flat-contract?]
+                     [#:name name any/c (object-name accessor)])
+         flat-contract?]{
+
+Constructs a @tech{flat contract} that checks that the first-order property
+accessed by @racket[accessor] satisfies @racket[ctc]. The resulting contract
+is equivalent to
+
+@racketblock[(lambda (v) (ctc (accessor v)))]
+
+except that more information is included in error messages produced by
+violations of the contract. The @racket[name] argument is used to describe the
+property being checked in error messages.
+
+@examples[#:eval (contract-eval) #:once
+  (define/contract (sum-triple lst)
+    (-> (and/c (listof number?)
+               (property/c length (=/c 3)))
+        number?)
+    (+ (first lst) (second lst) (third lst)))
+  (eval:check (sum-triple '(1 2 3)) 6)
+  (eval:error (sum-triple '(1 2)))]
+
+@history[#:added "7.3.0.11"]
+}
+
 @defproc[(suggest/c [c contract?]
                     [field string?]
                     [message string?]) contract?]{

pkgs/racket-test/tests/racket/contract/property.rkt

@@ -0,0 +1,144 @@
+#lang racket/base
+(require "test-util.rkt")
+(parameterize ([current-contract-namespace (make-full-contract-namespace)])
+  (test/spec-passed/result
+   'property/c1
+   '(contract (property/c length (=/c 3)) '(1 2 3) 'pos 'neg)
+   '(1 2 3))
+  (test/pos-blame
+   'property/c2
+   '(contract (property/c length (=/c 3)) '(1 2) 'pos 'neg))
+
+  (test-true
+   'property/c-message1
+   '(with-handlers ([exn:fail:contract:blame?
+                     (λ (exn)
+                       (and (member "the length of"
+                                    (blame-context (exn:fail:contract:blame-object exn)))
+                            #t))])
+      (contract (property/c length (=/c 3)) '(1 2) 'pos 'neg)))
+  (test-true
+   'property/c-message2
+   '(with-handlers ([exn:fail:contract:blame?
+                     (λ (exn)
+                       (and (member "the vector-length of"
+                                    (blame-context (exn:fail:contract:blame-object exn)))
+                            #t))])
+      (contract (property/c vector-length (=/c 3)) #(1 2) 'pos 'neg)))
+  (test-true
+   'property/c-message3
+   '(with-handlers ([exn:fail:contract:blame?
+                     (λ (exn)
+                       (and (member "the length of"
+                                    (blame-context (exn:fail:contract:blame-object exn)))
+                            #t))])
+      (contract (property/c vector-length (=/c 3) #:name "length") #(1 2) 'pos 'neg)))
+
+  (test/spec-passed/result
+   'property/c-message4
+   '(with-handlers ([exn:fail:contract:blame?
+                     (λ (exn)
+                       (define m (regexp-match #rx"promised:[^\n]*\n" (exn-message exn)))
+                       (and m (car m)))])
+      (contract (property/c length (=/c 3)) '(1 2) 'pos 'neg))
+   "promised: (=/c 3)\n")
+
+  (test/spec-passed/result
+   'property/c-name1
+   '(contract-name (property/c length (=/c 3)))
+   '(property/c length (=/c 3)))
+  (test/spec-passed/result
+   'property/c-name2
+   '(contract-name (property/c vector-length (=/c 3)))
+   '(property/c vector-length (=/c 3)))
+  (test/spec-passed/result
+   'property/c-name3
+   '(contract-name (property/c vector-length (=/c 3) #:name "length"))
+   '(property/c vector-length (=/c 3)))
+
+  (test/spec-passed/result
+   'property/c-stronger1
+   '(contract-stronger? (property/c length (integer-in 0 4))
+                        (property/c length (integer-in 0 4)))
+   #t)
+  (test/spec-passed/result
+   'property/c-stronger2
+   '(contract-stronger? (property/c length (integer-in 0 4))
+                        (property/c length (integer-in 1 3)))
+   #f)
+  (test/spec-passed/result
+   'property/c-stronger3
+   '(contract-stronger? (property/c length (integer-in 1 3))
+                        (property/c length (integer-in 0 4)))
+   #t)
+  (test/spec-passed/result
+   'property/c-stronger4
+   '(contract-stronger? (property/c vector-length (integer-in 0 4))
+                        (property/c length (integer-in 0 4)))
+   #f)
+  (test/spec-passed/result
+   'property/c-stronger5
+   '(contract-stronger? (property/c vector-length (integer-in 1 3))
+                        (property/c length (integer-in 0 4)))
+   #f)
+
+  (test/spec-passed/result
+   'property/c-equivalent1
+   '(contract-equivalent? (property/c length (integer-in 0 4))
+                          (property/c length (integer-in 0 4)))
+   #t)
+  (test/spec-passed/result
+   'property/c-equivalent2
+   '(contract-equivalent? (property/c length (integer-in 0 4))
+                          (property/c length (integer-in 1 3)))
+   #f)
+  (test/spec-passed/result
+   'property/c-equivalent3
+   '(contract-equivalent? (property/c length (integer-in 1 3))
+                          (property/c length (integer-in 0 4)))
+   #f)
+  (test/spec-passed/result
+   'property/c-equivalent4
+   '(contract-equivalent? (property/c vector-length (integer-in 0 4))
+                          (property/c length (integer-in 0 4)))
+   #f)
+  (test/spec-passed/result
+   'property/c-equivalent5
+   '(contract-equivalent? (property/c vector-length (integer-in 1 3))
+                          (property/c length (integer-in 0 4)))
+   #f)
+
+  (test-true
+   'property/c-generate1
+   '(let ()
+      (define generatable-length
+        (flat-named-contract
+         'generatable-length
+         length
+         (λ (fuel) (λ () '(1 2 3)))))
+      (and (contract-random-generate (property/c generatable-length (=/c 3))) #t)))
+  (test-true
+   'property/c-generate2
+   '(let ()
+      (define generatable-length
+        (flat-named-contract
+         'generatable-length
+         length
+         (λ (fuel)
+           (define seq (in-cycle (in-list '((1 2) (1 2 3)))))
+           (define-values (has-next? get-next) (sequence-generate seq))
+           get-next)))
+      (and (contract-random-generate (property/c generatable-length (=/c 3))) #t)))
+  (test/spec-passed/result
+   'property/c-generate3
+   '(let ()
+      (define generatable-length
+        (flat-named-contract
+         'generatable-length
+         length
+         (λ (fuel) (λ () '(1 2)))))
+      (contract-random-generate
+       (property/c generatable-length (=/c 3))
+       5
+       (λ (no-generator?) (if no-generator? 'no-generator 'generator-failed))))
+   'generator-failed))

racket/collects/racket/contract/base.rkt

@@ -21,7 +21,8 @@
          "private/arrow-val-first.rkt"
          "private/orc.rkt"
          "private/list.rkt"
-         "private/and.rkt")
+         "private/and.rkt"
+         "private/property.rkt")
 
 (provide
  base->?
@@ -142,6 +143,7 @@
  get/build-late-neg-projection
  get/build-val-first-projection
 
+ property/c
  suggest/c
  struct-guard/c
 

racket/collects/racket/contract/private/property.rkt

@@ -0,0 +1,74 @@
+#lang racket/base
+
+(require "guts.rkt"
+         "prop.rkt"
+         "blame.rkt"
+         "generate.rkt")
+
+(provide property/c)
+
+(struct property/c (accessor val-ctc prop-name)
+  #:constructor-name make-property/c
+  #:omit-define-syntaxes
+  #:property prop:custom-write contract-custom-write-property-proc
+  #:property prop:custom-print-quotable 'never
+  #:property prop:flat-contract
+  (build-flat-contract-property
+   #:name
+   (λ (ctc)
+     `(property/c ,(contract-name (property/c-accessor ctc))
+                  ,(contract-name (property/c-val-ctc ctc))))
+   #:first-order
+   (λ (ctc)
+     (define accessor (property/c-accessor ctc))
+     (define val-ctc-first-order (contract-first-order (property/c-val-ctc ctc)))
+     (λ (val)
+       (val-ctc-first-order (accessor val))))
+   #:late-neg-projection
+   (λ (ctc)
+     (define accessor (property/c-accessor ctc))
+     (define val-ctc-proj (contract-late-neg-projection (property/c-val-ctc ctc)))
+     (define prop-name (property/c-prop-name ctc))
+     (define ctx-str (format "the ~a of" prop-name))
+     (λ (orig-blame)
+       (define blame (blame-add-context orig-blame ctx-str))
+       (define val-ctc-proj/blame (val-ctc-proj blame))
+       (λ (val neg-party)
+         (val-ctc-proj/blame (accessor val) neg-party)
+         val)))
+   #:stronger
+   (λ (ctc-a ctc-b)
+     (and (contract-stronger? (property/c-accessor ctc-a)
+                              (property/c-accessor ctc-b))
+          (contract-stronger? (property/c-val-ctc ctc-a)
+                              (property/c-val-ctc ctc-b))))
+   #:equivalent
+   (λ (ctc-a ctc-b)
+     (and (contract-equivalent? (property/c-accessor ctc-a)
+                                (property/c-accessor ctc-b))
+          (contract-equivalent? (property/c-val-ctc ctc-a)
+                                (property/c-val-ctc ctc-b))))
+   #:generate
+   (λ (ctc)
+     ; It’s very unlikely that `accessor` will be a contract, much less a contract with a generator,
+     ; but if it is, we can try to generate values for it.
+     (define accessor (property/c-accessor ctc))
+     (define val-ctc-first-order (contract-first-order (property/c-val-ctc ctc)))
+     (λ (fuel)
+       (define sub-fuel (inexact->exact (ceiling (sqrt fuel))))
+       (define val-generate (contract-random-generate/choose accessor sub-fuel))
+       (and val-generate
+            (λ () (let loop ([i sub-fuel])
+                    (if (zero? i)
+                        contract-random-generate-fail
+                        (let ([val (accessor (val-generate))])
+                          (if (val-ctc-first-order val)
+                              val
+                              (loop (sub1 i))))))))))
+   #:list-contract?
+   (λ (ctc) (list-contract? (property/c-accessor ctc)))))
+
+(define/subexpression-pos-prop (property/c accessor ctc-v #:name [name (object-name accessor)])
+  (unless (and (procedure? accessor) (procedure-arity-includes? accessor 1))
+    (raise-argument-error 'property/c "(procedure-arity-includes/c 1)" accessor))
+  (make-property/c accessor (coerce-flat-contract 'property/c ctc-v) name))