From b5f6842ab05d2063cfc9e39e8f00c54724f225ab Mon Sep 17 00:00:00 2001
From: Burke Fetscher <bfetscher@racket-lang.org>
Date: Fri, 6 Sep 2013 14:47:49 -0500
Subject: [PATCH] Add #:satisfying to redex-check.

This adds the ability to generate terms satisfying
judgment-forms and metafunctions to redex-check.
---
 .../redex-doc/redex/scribblings/ref.scrbl     |  62 +++-
 .../redex-lib/redex/private/generate-term.rkt | 346 ++++++++++++------
 .../redex-test/redex/tests/gen-test.rkt       | 128 ++++++-
 3 files changed, 400 insertions(+), 136 deletions(-)

diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
index d35959436f..78e3106e91 100644
--- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
+++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
@@ -1837,8 +1837,13 @@ repeating as necessary. The optional keyword argument @racket[retries-expr]
 @racket[exn:fail:redex:generation-failure?].
 }
 
-@defform/subs[(redex-check language @#,ttpattern property-expr kw-arg ...)
-              ([kw-arg (code:line #:attempts attempts-expr)
+@defform/subs[(redex-check template property-expr kw-arg ...)
+              ([template (code:line language @#,ttpattern)
+                         (code:line language #:satisfying
+                            (judgment-form-id @#,ttpattern ...))
+                         (code:line language #:satisfying 
+                            (metafunction-id @#,ttpattern ...) = @#,ttpattern)]
+              [kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:source metafunction)
                        (code:line #:source relation-expr)
                        (code:line #:retries retries-expr)
@@ -1854,11 +1859,24 @@ repeating as necessary. The optional keyword argument @racket[retries-expr]
                            [prepare-expr (-> any/c any/c)])]{
 Searches for a counterexample to @racket[property-expr], interpreted
 as a predicate universally quantified over the pattern variables
-bound by @racket[pattern]. @racket[redex-check] constructs and tests 
-a candidate counterexample by choosing a random term @math{t} that 
-matches @racket[pattern] then evaluating @racket[property-expr]
+bound by the @racket[pattern](s) in @racket[template].
+@racket[redex-check] constructs and tests 
+a candidate counterexample by choosing a random term @math{t} based 
+on @racket[template] and then evaluating @racket[property-expr]
 using the @racket[match-bindings] produced by @racket[match]ing
-@math{t} against @racket[pattern].
+@math{t} against @racket[pattern]. The form of @racket[template] controls
+how @math{t} is generated:
+@itemlist[
+          @item{@racket[language @#,ttpattern]:
+                 In this case, redex-check generates terms that match
+                 @racket[pattern].}
+          @item{@racket[language #:satisfying (judgment-form-id @#,ttpattern ...)]:
+                  Generates terms that match @racket[pattern] and satisfy 
+                  the judgment form.}
+          @item{@racket[language #:satisfying (metafunction-id @#,ttpattern ...) = @#,ttpattern]:
+                  Generates terms matching the two @racket[pattern]s, such that
+                  if the first is the argument to the metafunction, the
+                  second will be the result.}]
 
 @racket[redex-check] generates at most @racket[attempts-expr] (default @racket[(default-check-attempts)])
 random terms in its search. The size and complexity of these terms tend to increase 
@@ -1882,14 +1900,19 @@ generated example before @racket[redex-check] checks @racket[property-expr].
 This keyword may be useful when @racket[property-expr] takes the form
 of a conditional, and a term chosen freely from the grammar is unlikely to
 satisfy the conditional's hypothesis. In some such cases, the @racket[prepare] 
-keyword  can be used to increase the probability that an example satifies the
+keyword  can be used to increase the probability that an example satisfies the
 hypothesis.
 
+The @racket[#:retries] keyword behaves identically as in @racket[generate-term],
+controlling the number of times the generation of any pattern will be
+reattempted. It can't be used together with @racket[#:satisfying].
+
 When passed a metafunction or reduction relation via the optional @racket[#:source]
 argument, @racket[redex-check] distributes its attempts across the left-hand sides
 of that metafunction/relation by using those patterns, rather than @racket[pattern],
 as the basis of its generation. It is an error if any left-hand side generates a
-term that does not match @racket[pattern].}
+term that does not match @racket[pattern]. @racket[#:source] cannot be used
+with @racket[#:satisfying].}
 
 @examples[
 #:eval redex-eval
@@ -1939,7 +1962,28 @@ term that does not match @racket[pattern].}
         #:prepare (λ (n)
                     (printf "preparing ~s; " n)
                     (add1 (abs n)))
-        #:attempts 3)]
+        #:attempts 3)
+                     
+       (define-language L
+         (nat ::= Z (S nat)))
+       (define-judgment-form L
+         #:mode (sum I I O)
+         [---------------
+          (sum Z nat nat)]
+         [(sum nat_1 nat_2 nat_3)
+          -------------------------------
+          (sum (S nat_1) nat_2 (S nat_3))])
+       (redex-check L
+                    #:satisfying
+                    (sum nat_1 nat_2 nat_3)
+                    (equal? (judgment-holds
+                             (sum nat_1 nat_2 nat_4) nat_4)
+                            (term (nat_3)))
+                    #:attempts 100)
+       (redex-check L
+                    #:satisfying
+                    (sum nat_1 nat_2 nat_3)
+                    (equal? (term nat_1) (term nat_2)))]
 
 @defform/subs[(redex-generator language-id satisfying size-expr)
               ([satisfying (judgment-form-id @#,ttpattern ...)
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
index 4c36024e18..bb3aca4c80 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
@@ -15,6 +15,7 @@
          racket/match
          racket/pretty
          (for-syntax racket/base
+                     racket/set
                      syntax/stx
                      setup/path-to-relative
                      "rewrite-side-conditions.rkt"
@@ -82,75 +83,187 @@
         (list (if lists? #'(-> list? list?) #'(-> any/c any/c)) 
               "#:prepare argument")))
 
+(define-for-syntax satisfying-disallowed-kws
+  (set '#:source '#:retries))
+
 (define-syntax (redex-check stx)
-  (syntax-case stx ()
+  (define valid-kws 
+    (cons '#:satisfying (map car (list attempts-keyword
+                                       source-keyword
+                                       retries-keyword
+                                       print?-keyword
+                                       attempt-size-keyword
+                                       (prepare-keyword #f)))))
+  (define used-kws
+    (for/fold ([kws (set)])
+              ([maybe-kw-stx (in-list (syntax->list stx))])
+      (define maybe-kw (syntax-e maybe-kw-stx))
+      (cond 
+        [(keyword? maybe-kw)
+         (unless (member maybe-kw valid-kws)
+           (raise-syntax-error 'redex-check "unknown keyword" stx maybe-kw-stx))
+         (set-add kws maybe-kw)]
+        [else kws])))
+  (define bad-kws (set-intersect used-kws satisfying-disallowed-kws))
+  (syntax-case stx (=)
+    [(form lang #:satisfying (mf-id . args) = res property . kw-args)
+     (unless (set-empty? bad-kws)
+       (raise-syntax-error 'redex-check (format "~s cannot be used with #:satisfying" (car (set->list bad-kws))) stx))
+     (redex-check/mf stx #'form #'lang #'mf-id #'args #'res #'property #'kw-args)]
+    [(form lang #:satisfying (jform-id . pats) property . kw-args)
+     (unless (set-empty? bad-kws)
+       (raise-syntax-error 'redex-check (format "~s cannot be used with #:satisfying" (car (set->list bad-kws))) stx))
+     (redex-check/jf stx #'form #'lang #'jform-id #'pats #'property #'kw-args)]
+    [(form lang #:satisfying . rest)
+     (raise-syntax-error 'redex-check "#:satisfying expected judgment form or metafunction syntax followed by a property" stx #'rest)]
     [(form lang pat property . kw-args)
-     (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...))
-                    (rewrite-side-conditions/check-errs 
-                     #'lang
-                     'redex-check #t #'pat)]
-                   [show (show-message stx)])
-     (let-values ([(attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
-                   (apply values
-                          (parse-kw-args (list attempts-keyword
-                                               source-keyword
-                                               retries-keyword
-                                               print?-keyword
-                                               attempt-size-keyword
-                                               (prepare-keyword #f))
-                                         (syntax kw-args)
-                                         stx
-                                         (syntax-e #'form)))])
-         (with-syntax ([property (syntax
-                                  (bind-prop
-                                   (λ (bindings)
-                                     (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
-                                               property))))])
-           (quasisyntax/loc stx
-             (let ([att #,attempts-stx]
-                   [ret #,retries-stx]
-                   [print? #,print?-stx]
-                   [fix #,fix-stx]
-                   [term-match (λ (generated)
-                                 (cond [(test-match lang pat generated) => values]
-                                       [else (redex-error 'redex-check "~s does not match ~s" generated 'pat)]))])
-               syncheck-exp
-               (parameterize ([attempt->size #,size-stx])
-               #,(if source-stx
-                     #`(let-values ([(metafunc/red-rel num-cases) 
-                                     #,(cond [(metafunc source-stx)
-                                              => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))]
-                                             [else
-                                              #`(let ([r #,(apply-contract #'reduction-relation? source-stx 
-                                                                           "#:source argument" (syntax-e #'form))])
-                                                  (values r (length (reduction-relation-make-procs r))))])])
-                         (check-lhs-pats
-                          lang
-                          metafunc/red-rel
-                          property
-                          (max 1 (floor (/ att num-cases)))
-                          ret
-                          'redex-check
-                          (and print? show)
-                          fix
-                          #:term-match term-match))
-                     #`(check-one
-                        #,(term-generator #'lang #'pattern 'redex-check)
-                        property att ret (and print? show) fix (and fix term-match)))))))))]))
+     (redex-check/pat stx #'form #'lang #'pat #'property #'kw-args)]))
+
+(define-struct gen-fail ())
+
+(define-for-syntax (redex-check/jf orig-stx form lang jf-id pats property kw-args)
+  (define-values (attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
+    (parse-redex-check-kw-args kw-args orig-stx form))
+  (define nts (definition-nts lang orig-stx 'redex-check))
+  (unless (judgment-form-id? jf-id)
+    (raise-syntax-error 'redex-check "expected a judgment-form" jf-id))
+  (define j-f (lookup-judgment-form-id jf-id))
+  (define clauses (judgment-form-gen-clauses j-f))
+  (define relation? (judgment-form-relation? j-f))
+  (define args-stx (if relation?
+                       (syntax/loc #'args #`(#,pats))
+                       pats))
+  (with-syntax* ([(syncheck-exp pattern (names ...) (names/ellipses ...))
+                  (rewrite-side-conditions/check-errs lang 'redex-check #t args-stx)]
+                 [show (show-message orig-stx)]
+                 [res-term-stx #`(#,jf-id #,@args-stx)]
+                 [property #`(bind-prop
+                               (λ (bindings)
+                                 (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
+                                           #,property)))])
+                (quasisyntax/loc orig-stx
+                  (let ([term-match (λ (generated)
+                                      (cond [(test-match #,lang res-term-stx generated) => values]
+                                            [else (redex-error 'redex-check "~s does not match ~s" generated 'res-term-stx)]))])
+                    syncheck-exp
+                    (let ([default-attempt-size (λ (s) (add1 (default-attempt-size s)))])
+                      (parameterize ([attempt->size #,size-stx])
+                        (check-one
+                         (λ (size _1 _2)
+                           (values
+                            (match ((make-jf-gen/proc '#,jf-id #,clauses #,lang 'pattern size))
+                              [(and res (? values)) res]
+                              [else (gen-fail)])
+                            #f))
+                         property #,attempts-stx 0 (and #,print?-stx show) #,fix-stx term-match)))))))
+
+(define-for-syntax (redex-check/mf orig-stx form lang mf-id args-stx res-stx property kw-args)
+  (define-values (attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
+    (parse-redex-check-kw-args kw-args orig-stx form))
+  (define nts (definition-nts lang orig-stx 'redex-check))
+  (define m (metafunc mf-id))
+  (unless m (raise-syntax-error 'generate-term "expected a metafuction" mf-id))
+  (define mf (syntax-local-value mf-id (λ () #f)))
+  (with-syntax* ([(lhs-syncheck-exp lhs-pat (lhs-names ...) (lhs-names/ellipses ...))
+                  (rewrite-side-conditions/check-errs lang 'redex-check #t args-stx)]
+                 [(rhs-syncheck-exp rhs-pat (rhs-names ...) (rhs-names/ellipses ...))
+                  (rewrite-side-conditions/check-errs lang 'redex-check #t res-stx)]
+                 [res-term-stx #`((#,mf-id #,@args-stx) = #,res-stx)]
+                 [mf-id (term-fn-get-id mf)]
+                 [show (show-message orig-stx)]
+                 [property #`(bind-prop
+                               (λ (bindings)
+                                 (term-let ([lhs-names/ellipses (lookup-binding bindings 'lhs-names)] ...
+                                            [rhs-names/ellipses (lookup-binding bindings 'rhs-names)] ...)
+                                           #,property)))])
+                (quasisyntax/loc orig-stx
+                  (let ([term-match (λ (generated)
+                                      (cond [(test-match #,lang res-term-stx generated) => values]
+                                            [else (redex-error 'redex-check "~s does not match ~s" generated 'res-term-stx)]))])
+                    lhs-syncheck-exp
+                    rhs-syncheck-exp
+                    (let ([default-attempt-size (λ (s) (add1 (default-attempt-size s)))])
+                      (parameterize ([attempt->size #,size-stx])
+                        (check-one
+                         (λ (size _1 _2)
+                           (values
+                            (match ((make-mf-gen/proc 'mf-id mf-id #,lang 'lhs-pat 'rhs-pat size))
+                              [(and res (? values)) res]
+                              [else (gen-fail)])
+                            #f))
+                         property #,attempts-stx 0 (and #,print?-stx show) #,fix-stx term-match)))))))
+
+(define-for-syntax (redex-check/pat orig-stx form lang pat property kw-args)
+  (with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...))
+                 (rewrite-side-conditions/check-errs 
+                  lang
+                  'redex-check #t pat)]
+                [show (show-message orig-stx)])
+    (define-values (attempts-stx source-stx retries-stx print?-stx size-stx fix-stx)
+      (parse-redex-check-kw-args kw-args orig-stx form)) 
+    (with-syntax ([property #`(bind-prop
+                               (λ (bindings)
+                                 (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
+                                           #,property)))])
+      (quasisyntax/loc orig-stx
+        (let ([att #,attempts-stx]
+              [ret #,retries-stx]
+              [print? #,print?-stx]
+              [fix #,fix-stx]
+              [term-match (λ (generated)
+                            (cond [(test-match #,lang #,pat generated) => values]
+                                  [else (redex-error 'redex-check "~s does not match ~s" generated '#,pat)]))])
+          syncheck-exp
+          (parameterize ([attempt->size #,size-stx])
+            #,(if source-stx
+                  #`(let-values ([(metafunc/red-rel num-cases) 
+                                  #,(cond [(metafunc source-stx)
+                                           => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))]
+                                          [else
+                                           #`(let ([r #,(apply-contract #'reduction-relation? source-stx 
+                                                                        "#:source argument" (syntax-e form))])
+                                               (values r (length (reduction-relation-make-procs r))))])])
+                      (check-lhs-pats
+                       #,lang
+                       metafunc/red-rel
+                       property
+                       (max 1 (floor (/ att num-cases)))
+                       ret
+                       'redex-check
+                       (and print? show)
+                       fix
+                       #:term-match term-match))
+                  #`(check-one
+                     #,(term-generator lang #'pattern 'redex-check)
+                     property att ret (and print? show) fix (and fix term-match)))))))))
+
+(define-for-syntax (parse-redex-check-kw-args kw-args orig-stx form-name)
+  (apply values
+         (parse-kw-args (list attempts-keyword
+                              source-keyword
+                              retries-keyword
+                              print?-keyword
+                              attempt-size-keyword
+                              (prepare-keyword #f))
+                        kw-args
+                        orig-stx
+                        (syntax-e form-name))))
 
 (define (format-attempts a)
   (format "~a attempt~a" a (if (= 1 a) "" "s")))
 
 (define (check-one generator property attempts retries show term-fix term-match) 
-  (let ([c (check generator property attempts retries show 
-                  #:term-fix term-fix
-                  #:term-match term-match)])
-    (if (counterexample? c)
-        (unless show c) ; check printed it
-        (if show
-            (show (format "no counterexamples in ~a\n"
-                          (format-attempts attempts)))
-            #t))))
+  (define c (check generator property attempts retries show 
+                   #:term-fix term-fix
+                   #:term-match term-match))
+  (cond 
+    [(counterexample? c)
+     (unless show c)] ; check printed it
+    [show
+     (show (format "no counterexamples in ~a\n"
+                   (format-attempts attempts)))]
+    [else
+     #t]))
 
 (define-struct (exn:fail:redex:test exn:fail:redex) (source term))
 (define-struct counterexample (term) #:transparent)
@@ -164,49 +277,54 @@
                #:term-match [term-match #f]
                #:skip-term? [skip-term? (λ (x) #f)])
   (let loop ([remaining attempts])
-    (if (zero? remaining)
-        #t
-        (let ([attempt (add1 (- attempts remaining))])
-          (let-values ([(term bindings) (generator ((attempt->size) attempt) attempt retries)]
-                       [(handler) 
-                        (λ (action term)
-                          (λ (exn)
-                            (let ([msg (format "~a ~s raises an exception" action term)])
-                              (when show (show (format "~a\n" msg)))
-                              (raise 
-                               (if show
-                                   exn
-                                   (make-exn:fail:redex:test
-                                    (format "~a:\n~a" msg (exn-message exn))
-                                    (current-continuation-marks)
-                                    exn
-                                    term))))))])
-            (let ([term (with-handlers ([exn:fail? (handler "fixing" term)])
-                          (if term-fix (term-fix term) term))])
-              (cond
-                [(skip-term? term) (loop (- remaining 1))]
-                [else
-                 (if (if term-match
-                         (let ([bindings (make-bindings 
-                                          (match-bindings
-                                           (pick-from-list (term-match term))))])
-                           (with-handlers ([exn:fail? (handler "checking" term)])
-                             (match property
-                               [(term-prop pred) (pred term)]
-                               [(bind-prop pred) (pred bindings)])))
-                         (with-handlers ([exn:fail? (handler "checking" term)])
-                           (match (cons property term-fix)
-                             [(cons (term-prop pred) _) (pred term)]
-                             [(cons (bind-prop pred) #f) (pred bindings)])))
-                     (loop (sub1 remaining))
-                     (begin
-                       (when show
-                         (show
-                          (format "counterexample found after ~a~a:\n"
-                                  (format-attempts attempt)
-                                  (if source (format " with ~a" source) "")))
-                         (pretty-write term (current-output-port)))
-                       (make-counterexample term)))])))))))
+    (cond 
+      [(zero? remaining)
+       #t]
+      [else
+       (define attempt (add1 (- attempts remaining)))
+       (define-values (raw-term bindings) (generator ((attempt->size) attempt) attempt retries))
+       (cond
+         [(gen-fail? raw-term)
+          (loop (sub1 remaining))]
+         [else
+          (define handler 
+            (λ (action term)
+              (λ (exn)
+                (define msg (format "~a ~s raises an exception" action term))
+                (when show (show (format "~a\n" msg)))
+                (raise 
+                 (if show
+                     exn
+                     (make-exn:fail:redex:test
+                      (format "~a:\n~a" msg (exn-message exn))
+                      (current-continuation-marks)
+                      exn
+                      term))))))
+          (define term (with-handlers ([exn:fail? (handler "fixing" raw-term)])
+                         (if term-fix (term-fix raw-term) raw-term)))
+          (cond
+            [(skip-term? term) (loop (- remaining 1))]
+            [(if term-match
+                 (let ([bindings (make-bindings 
+                                  (match-bindings
+                                   (pick-from-list (term-match term))))])
+                   (with-handlers ([exn:fail? (handler "checking" term)])
+                     (match property
+                       [(term-prop pred) (pred term)]
+                       [(bind-prop pred) (pred bindings)])))
+                 (with-handlers ([exn:fail? (handler "checking" term)])
+                   (match (cons property term-fix)
+                     [(cons (term-prop pred) _) (pred term)]
+                     [(cons (bind-prop pred) #f) (pred bindings)])))
+             (loop (sub1 remaining))]
+            [else
+             (when show
+               (show
+                (format "counterexample found after ~a~a:\n"
+                        (format-attempts attempt)
+                        (if source (format " with ~a" source) "")))
+               (pretty-write term (current-output-port)))
+             (make-counterexample term)])])])))
 
 (define (check-lhs-pats lang mf/rr prop attempts retries what show term-fix
                         #:term-match [term-match #f])
@@ -328,7 +446,7 @@
   (define (parse-keyword-args args)
     (define attempt-num #f)
     (define retries #f)
-
+    
     (let loop ([args args])
       (syntax-case args ()
         [() 
@@ -443,9 +561,9 @@
        (language-id-nts #'language 'generate-term) ;; for the error side-effect
        (unless (judgment-form-id? #'jf-id)
          (raise-syntax-error 'generate-term "expected a judgment-form" #'jf-id))
-        (syntax-case #'size-maybe ()
-          [() #`(λ (size) (generate-jf-pat language (jf-id . args) size))]
-          [(size) #'(generate-jf-pat language (jf-id . args) size)]))]))
+       (syntax-case #'size-maybe ()
+         [() #`(λ (size) (generate-jf-pat language (jf-id . args) size))]
+         [(size) #'(generate-jf-pat language (jf-id . args) size)]))]))
 
 (define-syntax (generate-term/source stx)
   (syntax-case stx ()
@@ -512,7 +630,7 @@
   (syntax-case stx ()
     [(g-m-p lang-id (mf-name . lhs-pats) rhs-pat size)
      #`(parameterize ([unsupported-pat-err-name 'generate-term])
-        ((make-redex-generator lang-id (mf-name . lhs-pats) = rhs-pat size)))]))
+         ((make-redex-generator lang-id (mf-name . lhs-pats) = rhs-pat size)))]))
 
 (define-syntax (generate-jf-pat stx)
   (syntax-case stx ()
@@ -583,9 +701,9 @@
     [(_ not-lang-id . rest)
      (not (identifier? #'not-lang-id))
      (raise-syntax-error 'redex-generator
-                            "expected an identifier in the language position"
-                            stx
-                            #'not-lang-id)]))
+                         "expected an identifier in the language position"
+                         stx
+                         #'not-lang-id)]))
 
 (define (make-jf-gen/proc jf-id mk-clauses lang pat size)
   (define gen (search/next (mk-clauses) pat size lang))
@@ -617,7 +735,7 @@
   (λ ()
     (parameterize ([current-logger generation-logger])
       (termify (gen)))))
-  
+
 (provide redex-check
          generate-term
          check-reduction-relation
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt
index b78c81fd53..29b30f88b3 100644
--- a/pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt
+++ b/pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt
@@ -15,6 +15,11 @@
 (define-syntax-rule (is-false e)
   (test e #f))
 
+(define-syntax-rule (no-counterexample e)
+  (test
+   (counterexample? e)
+   #f))
+
 (define-language L0)
 
 (let ()
@@ -87,7 +92,7 @@
   (test (generate-term nats #:satisfying (sum z z (s z)) 5)
               #f)
   
-  (for ([_ 100])
+  (for ([_ 50])
     (match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5)
       [`(sum ,l ,r ,res)
        (test (judgment-holds (sum ,l ,r n) n)
@@ -95,7 +100,26 @@
     (match (generate-term nats #:satisfying (r-sum n_1 n_2 n_3) 5)
       [`(r-sum ,l ,r ,res)
        (test (term (r-sum ,l ,r ,res))
-                   #t)])))
+                   #t)]))
+  (no-counterexample
+   (redex-check nats
+                #:satisfying
+                (sum n_1 n_2 n_3)
+                (equal? (car (judgment-holds
+                              (sum n_1 n_2 n_4) n_4))
+                        (term n_3))
+                #:attempts 50
+                #:print? #f))
+  
+  (no-counterexample
+   (redex-check nats
+                #:satisfying
+                (r-sum n_1 n_2 n_3)
+                (judgment-holds
+                 (sum n_1 n_2 n_3))
+                #:attempts 50
+                #:print? #f))
+  )
 
 (let ()
   
@@ -131,14 +155,24 @@
    (not (generate-term lists #:satisfying (not-in a (b (c (d (e (f ())))))) +inf.0))
    #f)
   
-  (for/and ([_ 100])
+  (for/and ([_ 50])
     (match (generate-term lists #:satisfying (not-in a l) 5)
       [`(not-in a ,l)
        (unless (judgment-holds (not-in a ,l)) (printf "l: ~s\n" l))
        (test (judgment-holds (not-in a ,l))
                    #t)]
       [#f
-       (void)])))
+       (void)]))
+  
+  (no-counterexample
+   (redex-check lists
+                #:satisfying
+                (not-in x l)
+                (judgment-holds (not-in x l))
+                #:attempts 50
+                #:print? #f))
+                
+  )
 
 (let ()
   
@@ -174,7 +208,7 @@
     [(double (+ e_1 e_2) e_3)
      (where e_3 (+ (+ e_1 e_1) (+ e_2 e_2)))])
   
-  (for ([_ 100])
+  (for ([_ 50])
     (define t (generate-term simple #:satisfying (double e_1 e_2) +inf.0))
     (match t
       [`(double ,e1 ,e2)
@@ -183,6 +217,15 @@
       [#f
        (void)]))
   
+  (no-counterexample
+   (redex-check simple
+                #:satisfying
+                (double e_1 e_2)
+                (judgment-holds
+                 (double e_1 e_2))
+                #:attempts 50
+                #:print? #f))
+  
   (define-metafunction simple
     [(duplicate e_1 e_1)
      (+ e_1 e_1 e_1)]
@@ -220,14 +263,25 @@
   (test (judgment-holds (double2 (+ 2 2) (+ 2 2 2)))
               #t)
   
-  (for ([_ 100])
+  (for ([_ 50])
     (define t (generate-term simple #:satisfying (double2 e_1 e_2) +inf.0))
     (match t
       [`(double2 ,e1 ,e2)
        (test (judgment-holds (double2 ,e1 ,e2))
                    #t)]
       [#f
-       (void)])))
+       (void)]))
+  
+  (no-counterexample
+   (redex-check simple
+                #:satisfying
+                (double2 e_1 e_2)
+                (judgment-holds 
+                 (double2 e_1 e_2))
+                #:attempts 50
+                #:print? #f))
+  
+  )
 
 (let ()
   (define-language STLC
@@ -283,7 +337,7 @@
   (test (judgment-holds (typeof ([x_2 int] ([x_1 (int → int)] •)) (x_1 5) int))
               #t)
   
-  (for ([_ 100])
+  (for ([_ 50])
     (define term (generate-term STLC #:satisfying (typeof Γ e τ) 6))
     (match term
       [`(typeof ,g ,e ,t)
@@ -292,7 +346,17 @@
       [#f
        (void)]))
   
-  (for ([_ 100])
+  (no-counterexample
+   (redex-check STLC
+                #:satisfying
+                (typeof Γ e τ)
+                (equal? (car (judgment-holds
+                              (typeof Γ e τ_2) τ_2))
+                        (term τ))
+                #:attempts 50
+                #:print? #f))
+  
+  (for ([_ 50])
     (define term (generate-term if-l #:satisfying (typ-if Γ e τ) 5))
     (match term
       [`(typ-if ,g ,e ,t)
@@ -301,8 +365,18 @@
       [#f
        (void)]))
   
+  (no-counterexample
+   (redex-check STLC
+                #:satisfying
+                (typ-if Γ e τ)
+                (equal? (car (judgment-holds
+                              (typ-if Γ e τ_2) τ_2))
+                        (term τ))
+                #:attempts 50
+                #:print? #f))
+  
   (define g (redex-generator STLC (typeof • e τ) 5))
-  (define terms (filter values (for/list ([_ 400]) (g))))
+  (define terms (filter values (for/list ([_ 100]) (g))))
   (test (length terms)
               (length (remove-duplicates terms)))
   (map (match-lambda
@@ -337,7 +411,7 @@
   (test (generate-term l #:satisfying (filtered (1 (2 (3 (4 •)))) 5 (1 (2 (4 •)))) +inf.0)
               #f)
   
-  (for ([_ 50])
+  (for ([_ 25])
     (define term (generate-term l #:satisfying (filtered e_1 n e_2) 5))
     (match term
       [`(filtered ,e1 ,n ,e2)
@@ -346,7 +420,17 @@
       [#f
        (void)]))
   
-  (for ([_ 50])
+  (no-counterexample
+   (redex-check l
+                #:satisfying
+                (filtered e_1 n e_2)
+                (equal? (car (judgment-holds
+                              (filtered e_1 n e_3) e_3))
+                        (term e_2))
+                #:attempts 25
+                #:print? #f))
+  
+  (for ([_ 25])
     (define t (generate-term l #:satisfying (fltr n e) = e_1 5))
     (match t
       [`((fltr ,n ,e) = ,e1)
@@ -354,6 +438,14 @@
       [#f
        (void)]))
   
+  (no-counterexample
+   (redex-check l 
+                #:satisfying 
+                (fltr n e) = e_1
+                (equal? (term (fltr n e)) (term e_1))
+                #:attempts 25
+                #:print? #f))
+  
   (define g (redex-generator l (fltr n e_1) = e_2 5))
   (define terms (filter values (for/list ([_ 50]) (g))))
   (test (length terms)
@@ -550,7 +642,17 @@
   (test (generate-term l #:satisfying (t 6 7) = 2 +inf.0)
               #f)
   (test (generate-term l #:satisfying (t 6 7) = 1 +inf.0)
-              #f))
+              #f)
+  
+  (no-counterexample
+   (redex-check l 
+                #:satisfying 
+                (t n_1 n_2) = n_3
+                (equal? (term (t n_1 n_2)) (term n_3))
+                #:attempts 50
+                #:print? #f))
+  
+  )
 
 (let ()
   (define-judgment-form L0