redex: bug fix for gerating terms including #f

please include in the release

collects/redex/private/generate-term.rkt

@@ -501,9 +501,9 @@
   (define gen (search/next (mk-clauses) pat size lang))
   (define (termify search-res)
     (cond
-      [search-res
+      [(not-failed? search-res)
        (define exp (pat->term lang (p*e-p search-res) (p*e-e search-res)))
-       (and exp
+       (and (not-failed? exp)
             (cons jf-id exp))]
       [else #f]))
   (λ ()
@@ -516,11 +516,11 @@
                            size
                            lang))
   (define (termify res)
-    (and res
+    (and (not-failed? res)
          (match res
            [(p*e lhs+rhs env)
             (define lhs+rhs-term (pat->term lang lhs+rhs env))
-            (and lhs+rhs-term
+            (and (not-failed? lhs+rhs-term)
                  (match lhs+rhs-term
                    [(list lhs-term rhs-term)
                     `((,fn ,@lhs-term) = ,rhs-term)]))])))

collects/redex/private/jdg-gen.rkt

@@ -41,20 +41,20 @@
          (match pat
            [`(nt ,p-nt)
             (define all-nts (cons p-nt nts))
-            (for/or ([nt-pat all-nts])
+            (for/not-failed ([nt-pat all-nts])
               (define term (recur `(nt ,nt-pat)))
-              (and (for/and ([nt (remove nt-pat all-nts)])
+              (and/fail (for/and ([nt (remove nt-pat all-nts)])
                           ((get-matcher nt) term))
                         term))]
            [`any
-            (for/or ([nt-pat nts])
+            (for/not-failed ([nt-pat nts])
               (define term (recur `(nt ,nt-pat)))
-              (and (for/and ([nt (remove nt-pat nts)])
+              (and/fail (for/and ([nt (remove nt-pat nts)])
                           ((get-matcher nt) term))
                         term))]
            [else
             (define term (recur pat))
-            (and (for/and ([nt nts])
+            (and/fail (for/and ([nt nts])
                         ((get-matcher nt) term))
                       term)])]
         [`(name ,var ,pat)
@@ -63,14 +63,21 @@
          (call/ec (λ (fail)
                     (for/list ([p ps])
                       (let ([res (recur p)])
-                        (unless res (fail #f))
+                        (unless (not-failed? res) (fail (unif-fail)))
                         res))))]
         [else
          (let-values ([(p bs) (gen-term p lang 2)])
            p)])))
-  (and (check-dqs (remove-empty-dqs (env-dqs full-env)) term-e lang eqs)
+  (and/fail (check-dqs (remove-empty-dqs (env-dqs full-env)) term-e lang eqs)
             res-term))
 
+(define-syntax-rule (for/not-failed ((x xs)) b ...)
+  (for/fold ([res (unif-fail)])
+    ([x xs])
+    #:break (not-failed? res)
+    b ...))
+    
+
 (define (check-dqs dqs term-e lang eqs)
   (for/and ([dq dqs])
     (define te (hash-copy term-e))

collects/redex/private/pat-unify.rkt

@@ -23,7 +23,9 @@
          pat*-clause-p?s
          bind-names
          remove-empty-dqs
+         and/fail
          (struct-out unif-fail)
+         not-failed?
          dq)
 
 
@@ -157,7 +159,7 @@
     (define res (and/fail (not-failed? t*) 
                           (not-failed? u*)
                           (unify* t* u* eqs L)))
-    (and (not-failed? res)
+    (and/fail (not-failed? res)
          (let* ([static-eqs (hash/mut->imm eqs)]
                 [found-pre-dqs 
                  (apply set-union (set) 
@@ -166,10 +168,10 @@
                 [found-dqs
                  (for/list ([pdq found-pre-dqs])
                    (disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))])
-           (and (for/and ([d found-dqs]) d)
+           (and/fail (for/and ([d found-dqs]) d)
                      (let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)]
                             [new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)])
-                  (and new-dqs
+                       (and/fail new-dqs
                                  (p*e res
                                       (env static-eqs new-dqs)))))))))
 

collects/redex/private/search.rkt

@@ -61,10 +61,10 @@
       (define-values (ans fails)
         (with-handlers ([exn:fail:redex:search-failure? (λ (e) 
                                                           (define f-conts (exn:fail:redex:search-failure-fails e))
-                                                          (values #f (trim-fails f-conts)))])
+                                                          (values (unif-fail) (trim-fails f-conts)))])
           (define-values (env/f fails)
             (fail-back fs))
-          (values (and env/f (unify fresh-pat 'any env/f lang))
+          (values (and/fail env/f (unify fresh-pat 'any env/f lang))
                   fails)))
       (set-last-gen-trace! (generation-trace))
       (set! fs (shuffle-fails fails))  ;; how to test if we're randomizing here?
@@ -174,9 +174,9 @@
             (define u-res (disunify ps lhs rhs e lang))
             (and u-res
                  (loop u-res rest))])))
-     (define head-p*e (and env1 (unify input head-pat env1 lang)))
+     (define head-p*e (and/fail env1 (unify input head-pat env1 lang)))
      (cond
-       [head-p*e
+       [(not-failed? head-p*e)
         (define res-p (p*e-p head-p*e))
         (let loop ([e (p*e-e head-p*e)]
                    [eqs eqs])

collects/redex/tests/gen-test.rkt

@@ -711,3 +711,47 @@
                            5)
        [`((f (,a ,b)) = 1) #f]
        [else #t]))))
+
+(let ()
+  (define-language L0)
+  
+  (define-relation L0
+    [(R (#f #f #f) 3)]
+    [(R (#f #f) 2)]
+    [(R #f 1)])
+  
+  (is-not-false
+   (generate-term
+    L0
+    #:satisfying
+    (R any_1 any_2)
+    +inf.0))
+  
+  (is-not-false
+   (generate-term
+    L0
+    #:satisfying
+    (R (any_1 any_2) any_3)
+    +inf.0))
+  
+  (is-not-false
+   (generate-term
+    L0
+    #:satisfying
+    (R (any_1 any_2 any_3) any_4)
+    +inf.0))
+  
+  (is-false
+   (generate-term
+    L0
+    #:satisfying
+    (R (any_1 any_2) 3)
+    +inf.0))
+  
+  (is-not-false
+   (generate-term
+    L0
+    #:satisfying
+    (R #f any)
+    +inf.0))
+  )

collects/redex/tests/unify-tests.rkt

@@ -226,8 +226,8 @@
           (p*e? res-pe-bkwd)
           (p*e-equivalent? res-pe res-pe-bkwd eqs))
      (p*e (p*e-p res-pe) (env-eqs (p*e-e res-pe)))]
-    [(and (not res-pe)
+    [(and (unif-fail? res-pe)
-          (not res-pe-bkwd))
+          (unif-fail? res-pe-bkwd))
      #f]
     [else 
      (list 'different-orders=>different-results
@@ -241,13 +241,13 @@
   (define res-p (unify*/lt p1 p2 e L))
   (define res-p-bkwd (unify*/lt p2 p1 e2 L))
   (cond
-    [(and res-p
+    [(and (not-failed? res-p)
-          res-p-bkwd
+          (not-failed? res-p-bkwd)
           (p*e-equivalent? (p*e res-p (env e '())) 
                            (p*e res-p-bkwd (env e2 '())) eqs))
      res-p]
-    [(and (not res-p)
+    [(and (unif-fail? res-p)
-          (not res-p-bkwd))
+          (unif-fail? res-p-bkwd))
      #f]
     [else 
      (list 'different-orders=>different-results
@@ -852,12 +852,14 @@
                                                           (name e2 ,(bound))))
                                       (env (m-hash (lvar 'e1) `(cstr (e) (nt e))
                                                    (lvar 'e2) `(nt e)) '()))))
-(check-false (pat->term λn `(cstr (x) (list (nt e) (nt e))) (env (hash) '())))
+(check-equal? (pat->term λn `(cstr (x) (list (nt e) (nt e))) (env (hash) '()))
+              (unif-fail))
 (check-not-false (pat->term λn `(cstr (e) (list (nt e) (nt e))) (env (hash) '())))
-(check-false (pat->term λn `(cstr (x) (list (name e1 ,(bound))
+(check-equal? (pat->term λn `(cstr (x) (list (name e1 ,(bound))
                                              (name e2 ,(bound))))
                          (env (m-hash (lvar 'e1) `(cstr (e) (nt e))
-                                     (lvar 'e2) `(nt e)) '())))
+                                      (lvar 'e2) `(nt e)) '()))
+              (unif-fail))
 (check-not-false
  (redex-match λn (e_1 e_1) (pat->term λn `(list (name x1 ,(bound))
                                                 (name x2 ,(bound)))
@@ -955,8 +957,8 @@
               [dqs-in (make-dqs dqs)]
               [res (unify/lt t u (env eqs-in dqs-in) L0)])
          (if true/false
-             (check-not-false res)
+             (check-not-false (not-failed? res))
-             (check-false res))))]))
+             (check-equal? res (unif-fail)))))]))
 
 (test-disunify/no-params 1 2 '() '() '() '())
 (test-disunify/no-params '(list 1 2) '(list 1 3) '() '() '() '())