improve contract-stronger for list-related contracts

also bring listof in line with the present
best practices of the contract library

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

@@ -3,8 +3,9 @@
 
 (parameterize ([current-contract-namespace
                 (make-basic-contract-namespace 'racket/contract
+                                               'racket/list
                                                'racket/class)])
-
+  
   (contract-eval '(define-contract-struct couple (hd tl)))
   (contract-eval '(define-contract-struct triple (a b c)))
   
@@ -56,7 +57,7 @@
   (let ([c (contract-eval '(->i () () any))])
     (test #t (contract-eval 'contract-stronger?) c c))
 
-  (ctest #f contract-stronger? 
+  (ctest #f contract-stronger?
          (->* () #:pre (zero? (random 10)) any) 
          (->* () #:pre (zero? (random 10)) any))
   (ctest #f contract-stronger? 
@@ -135,7 +136,15 @@
   
   (ctest #t contract-stronger? (cons/c boolean? integer?) (cons/c boolean? integer?))
   (ctest #f contract-stronger? (cons/c boolean? integer?) (cons/c integer? boolean?))
-  
+  (ctest #t contract-stronger? (cons/c number? (listof number?)) (non-empty-listof number?))
+  (ctest #t contract-stronger? (non-empty-listof number?) (cons/c number? (listof number?)))
+  (ctest #t contract-stronger? (cons/c number? (list/c number? number?)) (non-empty-listof number?))
+  (ctest #t contract-stronger? (cons/c number? (cons/c number? (listof number?))) (listof number?))
+  (ctest #t contract-stronger? 
+         (cons/c (<=/c 1) (cons/c (<=/c 2) (listof (<=/c 3)))) 
+         (listof (<=/c 4)))
+  (ctest #f contract-stronger? (listof number?) (cons/c number? (cons/c number? (listof any/c))))
+    
   (contract-eval
    `(let ()
       (define x (flat-rec-contract x (or/c (cons/c x '()) '())))
@@ -161,6 +170,15 @@
   (ctest #t contract-stronger? 
          (flat-named-contract 'name2 (regexp "x"))
          (flat-named-contract 'name2 (regexp "x")))
+  (ctest #t contract-stronger? (listof (<=/c 3)) (listof (<=/c 5)))
+  (ctest #t contract-stronger? (list/c (<=/c 3) (<=/c 3)) (list/c (<=/c 3) (<=/c 3)))
+  (ctest #f contract-stronger? (list/c (<=/c 3) (<=/c 3)) (list/c (<=/c 3) (<=/c 3) (<=/c 3)))
+  (ctest #f contract-stronger? (list/c (<=/c 3) (<=/c 3) (<=/c 3)) (list/c (<=/c 3) (<=/c 3)))
+  (ctest #t contract-stronger? (list/c (<=/c 3) (<=/c 3)) (listof (<=/c 5)))
+  (ctest #t contract-stronger? (list/c (<=/c 3) (<=/c 3)) (non-empty-listof (<=/c 5)))
+  (ctest #t contract-stronger? (list/c (<=/c 3)) (non-empty-listof (<=/c 5)))
+  (ctest #f contract-stronger? (list/c) (non-empty-listof (<=/c 5)))
+  (ctest #t contract-stronger? (list/c) (listof (<=/c 5)))
   
   (contract-eval
    `(let ([c (class/c (m (-> any/c integer?)))])

racket/collects/racket/contract/private/misc.rkt

@@ -413,126 +413,224 @@
      (build-compound-type-name 'not/c ctc)
      (λ (x) (not (pred x))))))
 
-(define (listof-generate elem-ctc)
+(define (listof-generate ctc)
   (λ (fuel)
-    (define eg (generate/choose elem-ctc fuel))
+    (define eg (generate/choose (listof-ctc-elem-c ctc) fuel))
     (if eg
         (λ ()
-          (let loop ([so-far '()])
+          (let loop ([so-far (if (pe-listof-ctc? ctc)
+                                 '()
+                                 (list eg))])
             (rand-choice
              [1/5 so-far]
              [else (loop (cons (eg) so-far))])))
-        (λ () '()))))
+        (if (pe-listof-ctc? ctc)
+            (λ () '())
+            #f))))
 
-(define (non-empty-listof-generate elem-ctc)
+(define (listof-exercise ctc) 
-  (λ (fuel)
+  (cond
-    (define eg (generate/choose elem-ctc fuel))
+    [(pe-listof-ctc? ctc)
-    (if eg
+     (λ (fuel) (values void '()))]
-        (λ ()
+    [else
-          (let loop ([so-far (list (eg))])
+     (define elem-ctc (listof-ctc-elem-c ctc))
-            (rand-choice
+     (λ (fuel)
-             [1/5 so-far]
+       (define env (generate-env))
-             [else (loop (cons (eg) so-far))])))
+       (values
-        #f)))
+        (λ (lst)
+          (env-stash env elem-ctc (oneof lst)))
+        (list elem-ctc)))]))
 
-(define (non-empty-listof-exercise elem-ctc)
+(define (listof-stronger this that)
-  (λ (fuel)
+  (define this-elem (listof-ctc-elem-c this))
-    (define env (generate-env))
+  (cond
-    (values
+    [(listof-ctc? that)
-     (λ (lst)
+     (define that-elem (listof-ctc-elem-c that))
-       (env-stash env elem-ctc (oneof lst)))
+     (and (if (pe-listof-ctc? this)
-     (list elem-ctc))))
+              (pe-listof-ctc? that)
+              #t)
+          (contract-stronger? this-elem that-elem))]
+    [(the-cons/c? that)
+     (define hd-ctc (the-cons/c-hd-ctc that))
+     (define tl-ctc (the-cons/c-tl-ctc that))
+     (and (ne-listof-ctc? this)
+          (contract-stronger? this-elem hd-ctc)
+          (contract-stronger? (ne->pe-ctc this) tl-ctc))]
+    [else #f]))
+           
+(define (raise-listof-blame-error blame val empty-ok? neg-party)
+  (raise-blame-error blame #:missing-party neg-party val
+                     '(expected: "~s" given: "~e")
+                     (if empty-ok?
+                         "list?"
+                         (format "~s" `(and/c list? pair?)))
+                     val))
 
-(define (*-listof predicate? name generate exercise)
+(define (blame-add-listof-context blame) (blame-add-context blame "an element of"))
-  (λ (input)
-    (define ctc (coerce-contract name input))
-    (define ctc-name (build-compound-type-name name ctc))
-    (define proj (contract-projection ctc))
-    (define ((listof-*-ho-check check-all) blame)
-      (let ([p-app (proj (blame-add-listof-*-context blame))])
-        (λ (val)
-          (unless (predicate? val)
-            ((listof-*/fail blame val predicate?) #f))
-          (check-all p-app val))))
-    
-    (define (fo-check x)
-      (and (predicate? x) 
-           (for/and ([v (in-list x)])
-             (contract-first-order-passes? ctc v))))
-    (cond
-      [(flat-contract? ctc)
-       (make-flat-contract
-        #:name ctc-name
-        #:first-order fo-check
-        #:projection (listof-*-ho-check (λ (p v) (for-each p v) v))
-        #:val-first-projection (listof-*-val-first-flat-proj predicate? ctc)
-        #:generate (generate ctc)
-        #:exercise (exercise ctc)
-        #:list-contract? #t)]
-      [(chaperone-contract? ctc)
-       (make-chaperone-contract
-        #:name ctc-name
-        #:first-order fo-check
-        #:projection (listof-*-ho-check (λ (p v) (map p v)))
-        #:val-first-projection (listof-*-val-first-ho-proj predicate? ctc)
-        #:generate (generate ctc)
-        #:exercise (exercise ctc)
-        #:list-contract? #t)]
-      [else
-       (make-contract
-        #:name ctc-name
-        #:first-order fo-check
-        #:val-first-projection (listof-*-val-first-ho-proj predicate? ctc)
-        #:projection (listof-*-ho-check (λ (p v) (map p v)))
-        #:exercise (exercise ctc)
-        #:list-contract? #t)])))
-
-(define (listof-*-val-first-flat-proj predicate? ctc)
-  (define vf-proj (get/build-val-first-projection ctc))
-  (λ (blame)
-    (define p-app (vf-proj (blame-add-listof-*-context blame)))
-    (λ (val)
-      (cond
-        [(predicate? val)
-         (λ (neg-party)
-           (for ([ele (in-list val)])
-             ((p-app ele) neg-party))
-           val)]
-        [else
-         (listof-*/fail blame val predicate?)]))))
-
-(define (listof-*-val-first-ho-proj predicate? ctc)
-  (define vf-proj (get/build-val-first-projection ctc))
-  (λ (blame)
-    (define p-app (vf-proj (blame-add-listof-*-context blame)))
-    (λ (val)
-      (cond
-        [(predicate? val)
-         (λ (neg-party)
-           (for/list ([ele (in-list val)])
-             ((p-app ele) neg-party)))]
-        [else
-         (listof-*/fail blame val predicate?)]))))
-
-(define (listof-*/fail blame val predicate?)
-  (λ (neg-party)
-    (raise-blame-error blame #:missing-party neg-party val
-                       '(expected: "~s" given: "~e")
-                       (object-name predicate?)
-                       val)))
-
-(define (blame-add-listof-*-context blame) (blame-add-context blame "an element of"))
 (define (non-empty-list? x) (and (pair? x) (list? x)))
 
-(define (no-exercise ctc) (λ (size) (values void '())))
+(define (list-name ctc)
-(define listof-func (*-listof list? 'listof listof-generate no-exercise))
+  (build-compound-type-name (if (pe-listof-ctc? ctc)
-(define/subexpression-pos-prop (listof x) (listof-func x))
+                                'listof
+                                'non-empty-listof)
+                            (listof-ctc-elem-c ctc)))
+
+(define (list-fo-check ctc)
+  (define elem-fo? (contract-first-order (listof-ctc-elem-c ctc)))
+  (cond
+    [(pe-listof-ctc? ctc)
+     (λ (v)
+       (and (list? v)
+            (for/and ([e (in-list v)])
+              (elem-fo? e))))]
+    [(ne-listof-ctc? ctc)
+     (λ (v)
+       (and (list? v)
+            (pair? v)
+            (for/and ([e (in-list v)])
+              (elem-fo? e))))]))
+     
+(define (listof-projection ctc)
+  (define elem-proj (contract-projection (listof-ctc-elem-c ctc)))
+  (define pred? (if (pe-listof-ctc? ctc)
+                    list?
+                    non-empty-list?))
+  (λ (blame)
+    (define elem-proj+blame (elem-proj (blame-add-listof-context blame)))
+    (cond
+      [(flat-listof-ctc? ctc)
+       (λ (val)
+         (if (pred? val)
+             (begin
+               (for ([x (in-list val)])
+                 (elem-proj+blame x))
+               val)
+             (raise-listof-blame-error blame val (pe-listof-ctc? ctc) #f)))]
+      [else
+       (λ (val)
+         (if (pred? val)
+             (for/list ([x (in-list val)])
+               (elem-proj+blame x))
+             (raise-listof-blame-error blame val (pe-listof-ctc? ctc) #f)))])))
+
+(define (listof-val-first-projection ctc)
+  (define elem-proj (contract-val-first-projection (listof-ctc-elem-c ctc)))
+  (define pred? (if (pe-listof-ctc? ctc)
+                    list?
+                    non-empty-list?))
+  (λ (blame)
+    (define elem-proj+blame (elem-proj (blame-add-listof-context blame)))
+    (cond
+      [(flat-listof-ctc? ctc)
+       (λ (val)
+         (if (pred? val)
+             (λ (neg-party)
+               (for ([x (in-list val)])
+                 ((elem-proj+blame x) neg-party))
+               val)
+             (λ (neg-party)
+               (raise-listof-blame-error blame val (pe-listof-ctc? ctc) neg-party))))]
+      [else
+       (λ (val)
+         (if (pred? val)
+             (λ (neg-party)
+               (for/list ([x (in-list val)])
+                 ((elem-proj+blame x) neg-party)))
+             (λ (neg-party)
+               (raise-listof-blame-error blame val (pe-listof-ctc? ctc) neg-party))))])))
+
+(define flat-prop
+  (build-flat-contract-property
+   #:name list-name
+   #:first-order list-fo-check
+   #:projection listof-projection
+   #:val-first-projection listof-val-first-projection
+   #:generate listof-generate
+   #:exercise listof-exercise
+   #:stronger listof-stronger
+   #:list-contract? (λ (c) #t)))
+(define chap-prop
+  (build-chaperone-contract-property
+   #:name list-name
+   #:first-order list-fo-check
+   #:projection listof-projection
+   #:val-first-projection listof-val-first-projection
+   #:generate listof-generate
+   #:exercise listof-exercise
+   #:stronger listof-stronger
+   #:list-contract? (λ (c) #t)))
+(define full-prop
+  (build-contract-property
+   #:name list-name
+   #:first-order list-fo-check
+   #:projection listof-projection
+   #:val-first-projection listof-val-first-projection
+   #:generate listof-generate
+   #:exercise listof-exercise
+   #:stronger listof-stronger
+   #:list-contract? (λ (c) #t)))
+
+(struct listof-ctc (elem-c))
+
+;; possibly-empty lists
+(struct pe-listof-ctc listof-ctc ())
+
+;; possibly-empty, flat
+(struct pef-listof-ctc pe-listof-ctc ()
+  #:property prop:flat-contract flat-prop
+  #:property prop:custom-write custom-write-property-proc)
+;; possibly-empty, chaperone
+(struct pec-listof-ctc pe-listof-ctc ()
+  #:property prop:chaperone-contract chap-prop
+  #:property prop:custom-write custom-write-property-proc)
+;; possibly-empty, impersonator
+(struct pei-listof-ctc pe-listof-ctc ()
+  #:property prop:contract full-prop
+  #:property prop:custom-write custom-write-property-proc)
+
+;; non-empty lists
+(struct ne-listof-ctc listof-ctc ())
+
+;; non-empty, flat
+(struct nef-listof-ctc ne-listof-ctc ()
+  #:property prop:custom-write custom-write-property-proc
+  #:property prop:flat-contract flat-prop)
+;; non-empty, chaperone
+(struct nec-listof-ctc ne-listof-ctc ()
+  #:property prop:custom-write custom-write-property-proc
+  #:property prop:chaperone-contract chap-prop)
+;; non-empty, impersonator
+(struct nei-listof-ctc ne-listof-ctc ()
+  #:property prop:custom-write custom-write-property-proc
+  #:property prop:contract full-prop)
+
+(define (flat-listof-ctc? x)
+  (or (pef-listof-ctc? x)
+      (nef-listof-ctc? x)))
+
+(define (ne->pe-ctc ne-ctc)
+  (define elem-ctc (listof-ctc-elem-c ne-ctc))
+  (cond
+    [(nef-listof-ctc? ne-ctc)
+     (pef-listof-ctc elem-ctc)]
+    [(nef-listof-ctc? ne-ctc)
+     (pef-listof-ctc elem-ctc)]
+    [(nei-listof-ctc? ne-ctc)
+     (pei-listof-ctc elem-ctc)]))
+
+(define/subexpression-pos-prop (non-empty-listof raw-c)
+  (define c (coerce-contract 'non-empty-listof raw-c))
+  (cond
+    [(flat-contract? c) (nef-listof-ctc c)]
+    [(chaperone-contract? c) (nec-listof-ctc c)]
+    [else (nei-listof-ctc c)]))
+(define/subexpression-pos-prop (listof raw-c)
+  (define c (coerce-contract 'non-empty-listof raw-c))
+  (cond
+    [(flat-contract? c) (pef-listof-ctc c)]
+    [(chaperone-contract? c) (pec-listof-ctc c)]
+    [else (pei-listof-ctc c)]))
 
-(define non-empty-listof-func (*-listof non-empty-list? 
-                                        'non-empty-listof
-                                        non-empty-listof-generate
-                                        non-empty-listof-exercise))
-(define/subexpression-pos-prop (non-empty-listof a) (non-empty-listof-func a))
 
 (define (blame-add-car-context blame) (blame-add-context blame "the car of"))
 (define (blame-add-cdr-context blame) (blame-add-context blame "the cdr of"))
@@ -581,11 +679,24 @@
   (build-compound-type-name 'cons/c ctc-car ctc-cdr))
 
 (define (cons/c-stronger? this that) 
-  (and (the-cons/c? that)
+  (define this-hd (the-cons/c-hd-ctc this))
-       (contract-stronger? (the-cons/c-hd-ctc this)
+  (define this-tl (the-cons/c-tl-ctc this))
-                           (the-cons/c-hd-ctc that))
+  (cond
-       (contract-stronger? (the-cons/c-tl-ctc this)
+    [(the-cons/c? that)
-                           (the-cons/c-tl-ctc that))))
+     (define that-hd (the-cons/c-hd-ctc that))
+     (define that-tl (the-cons/c-tl-ctc that))
+     (and (contract-stronger? this-hd that-hd)
+          (contract-stronger? this-tl that-tl))]
+    [(ne-listof-ctc? that)
+     (define elem-ctc (listof-ctc-elem-c that))
+     (and (contract-stronger? this-hd elem-ctc)
+          (contract-stronger? this-tl (ne->pe-ctc that)))]
+    [(pe-listof-ctc? that)
+     (define elem-ctc (listof-ctc-elem-c that))
+     (and (contract-stronger? this-hd elem-ctc)
+          (contract-stronger? this-tl that))]
+    [else #f]))
+
 
 (define (cons/c-generate ctc)
   (define ctc-car (the-cons/c-hd-ctc ctc))
@@ -690,6 +801,23 @@
 (define (list/c-exercise ctc)
   (multi-exercise (generic-list/c-args ctc)))
 
+(define (list/c-stronger this that)
+  (cond
+    [(generic-list/c? that)
+     (and (= (length (generic-list/c-args this))
+             (length (generic-list/c-args that)))
+          (for/and ([this-s (in-list (generic-list/c-args this))]
+                    [that-s (in-list (generic-list/c-args this))])
+            (contract-stronger? this-s that-s)))]
+    [(listof-ctc? that)
+     (define that-elem-ctc (listof-ctc-elem-c that))
+     (define this-elem-ctcs (generic-list/c-args this))
+     (and (or (pair? this-elem-ctcs)
+              (pe-listof-ctc? that))
+          (for/and ([this-s (in-list this-elem-ctcs)])
+            (contract-stronger? this-s that-elem-ctc)))]
+    [else #f]))
+
 (struct generic-list/c (args))
 
 (struct flat-list/c generic-list/c ()
@@ -700,6 +828,7 @@
    #:first-order list/c-first-order
    #:generate list/c-generate
    #:exercise list/c-exercise
+   #:stronger list/c-stronger
    #:val-first-projection
    (λ (c) 
      (λ (blame) 
@@ -840,6 +969,7 @@
      #:first-order list/c-first-order
      #:generate list/c-generate
      #:exercise list/c-exercise
+     #:stronger list/c-stronger
      #:projection list/c-chaperone/other-projection
      #:val-first-projection list/c-chaperone/other-val-first-projection
      #:list-contract? (λ (c) #t))))
@@ -852,6 +982,7 @@
    #:first-order list/c-first-order
    #:generate list/c-generate
    #:exercise list/c-exercise
+   #:stronger list/c-stronger
    #:projection list/c-chaperone/other-projection
    #:val-first-projection list/c-chaperone/other-val-first-projection
    #:list-contract? (λ (c) #t)))