make check-metafunction and check-reduction-relation

pay attention to the contract/#:domain spec

closes PR 13616

collects/redex/private/generate-term.rkt

@@ -159,7 +159,8 @@
 (define (check generator property attempts retries show
                #:source [source #f]
                #:term-fix [term-fix #f]
-               #:term-match [term-match #f])
+               #:term-match [term-match #f]
+               #:skip-term? [skip-term? (λ (x) #f)])
   (let loop ([remaining attempts])
     (if (zero? remaining)
         #t
@@ -180,6 +181,9 @@
                                     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
@@ -200,19 +204,25 @@
                                   (format-attempts attempt)
                                   (if source (format " with ~a" source) "")))
                          (pretty-write term (current-output-port)))
-                    (make-counterexample term)))))))))
+                       (make-counterexample term)))])))))))
 
 (define (check-lhs-pats lang mf/rr prop attempts retries what show term-fix
                         #:term-match [term-match #f])
-  (let ([lang-gen (compile lang what)])
-    (let-values ([(pats srcs)
+  (define lang-gen (compile lang what))
+  (define-values (pats srcs skip-term?)
     (cond [(metafunc-proc? mf/rr)
            (values (map (λ (case) ((metafunc-case-lhs+ case) lang)) 
                         (metafunc-proc-cases mf/rr))
-                                 (metafunction-srcs mf/rr))]
+                   (metafunction-srcs mf/rr)
+                   (compose not (metafunc-proc-in-dom? mf/rr)))]
           [(reduction-relation? mf/rr)
            (values (map (λ (rwp) ((rewrite-proc-lhs rwp) lang)) (reduction-relation-make-procs mf/rr))
-                                 (reduction-relation-srcs mf/rr))])])
+                   (reduction-relation-srcs mf/rr)
+                   (let ([pat (compile-pattern (reduction-relation-lang mf/rr)
+                                               (reduction-relation-domain-pat mf/rr)
+                                               #f)])
+                     (λ (x) (not (match-pattern? pat x)))))]))
+  
   (let loop ([pats pats] [srcs srcs])
     (if (and (null? pats) (null? srcs))
         (if show
@@ -230,12 +240,13 @@
                     attempts
                     retries
                     show
+                    #:skip-term? skip-term?
                     #:source (car srcs)
                     #:term-match term-match
                     #:term-fix term-fix))])
           (if (counterexample? c)
               (unless show c)
-                  (loop (cdr pats) (cdr srcs)))))))))
+              (loop (cdr pats) (cdr srcs)))))))
 
 (define-syntax (check-metafunction stx)
   (syntax-case stx ()

collects/redex/tests/rg-test.rkt

@@ -1048,6 +1048,17 @@
                 #:attempts 1))))
           #rx"no counterexamples"))
   
+  ;; just check that this doesn't raise an errors.
+  (let ()
+    (define-language empty)
+    (define red (reduction-relation
+                 empty
+                 #:domain 1
+                 (--> any any)))
+    (check-reduction-relation 
+     red 
+     (λ (x) (apply-reduction-relation red x))))
+  
   (let ([U (reduction-relation L (--> (side-condition any #f) any))])
     (test (raised-exn-msg
            exn:fail:redex:generation-failure?
@@ -1229,6 +1240,20 @@
          (check-metafunction n (λ (_) #t) #:retries 42))
         #rx"check-metafunction: unable .* in 42")
 
+  
+  (let ()
+    (define-metafunction empty
+      mf : 1 -> 1
+      [(mf any) any])
+    
+    ;; just make sure no errors
+    (test (begin
+            (check-metafunction
+             mf
+             (λ (args) (term (mf ,@args))))
+            42)
+          42))
+  
   (let ()
     (define-metafunction empty bogo : any -> any)
 

doc/release-notes/redex/HISTORY.txt

@@ -4,6 +4,13 @@ v5.3.4
     have overlapping non-terminals; in that case the productions are
     combined
 
+  * Adjust check-metafunction and check-reduction-relation so that
+    they skip over randomly generated terms that don't match the
+    contract spec (or #:domain spec). This means that when there is a
+    case in the metafunction (or reduction-relation) whose nominal
+    pattern is more general than the contract would allow, that those
+    terms are discarded instead of used as inputs to the predicate.
+
 v5.3.3
 
 No changes