fixed #195

When checking to see if a non-terminal is viable wrt to
some unification problem, the old code didn't convert
the pats to pat*s. I think it probably should have been,
however, so this commit makes it do so.

Author: rfindler

redex-lib/redex/private/pat-unify.rkt

@@ -863,9 +863,11 @@
         (define npat (normalize-pat clang e pat))
         (hash-ref memo (list nt clang npat)
                   (λ ()
-                    (define pat-ok? 
-                      (for/or ([ntp (in-list (map (((curry normalize-pat) clang) e) (nt-pats nt clang)))])
-                        (not-failed? (unify* npat ntp empty-env clang))))
+                    (define pat-ok?
+                      (for/or ([pat (in-list (nt-pats nt clang))])
+                        (define ntp (normalize-pat clang e pat))
+                        (define ntp* (bind-names (fresh-pat-vars ntp (make-hash)) e clang))
+                        (not-failed? (unify* npat (p*e-p ntp*) (p*e-e ntp*) clang))))
                     (hash-set! memo (list nt clang npat) pat-ok?)
                     pat-ok?))))))
 

redex-test/redex/tests/gen-test.rkt

@@ -974,3 +974,24 @@
   (test (with-handlers ([exn:fail? exn-message])
           (redex-check let-nl e #t #:source eval))
         #rx"language of the metafunction does not"))
+
+(let ()
+  (define-language Boxy
+    (e ::= x (e_1 e_2))
+    (t ::= nat bool)
+    (x u ::= variable-not-otherwise-mentioned))
+
+  (define-judgment-form
+    Boxy
+    #:mode (type I O)
+    #:contract (type e t)
+
+    [-------------
+     (type x bool)]
+
+    [(type e_1 bool)
+     (type e_2 bool)
+     ---------------------
+     (type (e_1 e_2) nat)])
+
+  (is-not-false (generate-term Boxy #:satisfying (type e nat) 10)))