Preprocess nt patterns in pattern unification.

Specifically, correctly handle cases where an nt
production has named patterns.

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

@@ -30,7 +30,10 @@
          (struct-out unif-fail)
          not-failed?
          dq
-         predef-pat?)
+         predef-pat?
+         unique-name-nums
+         fresh-pat-vars
+         make-uid)
 
 
 ;;
@@ -338,7 +341,7 @@
 ;; which match both pat and pat*...
 ;; (those are the ones bind-names does nothing with)
 
-;; bind-names : pat env lang -> pat* or #f
+;; bind-names : pat env lang -> pat* or unif-fail
 (define (bind-names pat e L)
   (match pat
     [`(name ,name ,(bound))
@@ -383,7 +386,7 @@
     [_ pat]))
 
 
-;; unify* : pat* pat* env lang -> pat* or #f
+;; unify* : pat* pat* env lang -> pat* or unif-fail
 (define (unify* t0 u0 e L)
   (define t (resolve t0 e))
   (define u (resolve u0 e))
@@ -463,18 +466,18 @@
                              `(cstr ,nts ,res))]))))
   
 (define (u*-2nts n-t n-u e L)
-    (if (equal? n-t n-u)
-        (let ([n n-t])
-          (if (hash-has-key? (compiled-lang-collapsible-nts L) n)
-              (hash-ref (compiled-lang-collapsible-nts L) n)
-              `(nt ,n)))
-        (u*-1nt n-t `(nt ,n-u) e L)))
+  (if (equal? n-t n-u)
+      `(nt ,n-t)
+      (u*-1nt n-t `(nt ,n-u) e L)))
 
 (define (u*-1nt p u e L)
   (and/fail
    (check-nt p L u)
    (if (hash-has-key? (compiled-lang-collapsible-nts L) p)
-       (unify* (hash-ref (compiled-lang-collapsible-nts L) p) u e L)
+       (let ([p-bn (bind-names (fresh-pat-vars (hash-ref (compiled-lang-collapsible-nts L) p) (make-hash)) e L)])
+         (and/fail
+          (not-failed? p-bn)
+          (unify* p-bn u e L)))
        (let ([res (unify* u u e L)]) ;; look at structure of nt here?
          (and/fail (not-failed? res)
                    (when (lvar? res)
@@ -762,4 +765,27 @@
 (define empty-lang
   (compiled-lang
    #f #f #f #f #f #f #f #f #f #f '() #f (hash)
-   (lang-enumerators '())))
+   (lang-enumerators '())))
+
+(define unique-name-nums (make-parameter 0))
+
+;; TODO: compare with free-identifier=? so renaming is safe
+;; w/r/t macro expansion
+;; (use free-id-table)
+(define (fresh-pat-vars pre-pat instantiations)
+  (match pre-pat
+    [`(name ,id ,pat)
+     (define new-id (hash-ref instantiations id
+                              (λ ()
+                                (define unique-id (make-uid id))
+                                (hash-set! instantiations id unique-id)
+                                unique-id)))
+     `(name ,new-id ,(fresh-pat-vars pat instantiations))]
+    [`(list ,pats ...)
+     `(list ,@(for/list ([p pats]) (fresh-pat-vars p instantiations)))]
+    [_ pre-pat]))
+
+(define (make-uid id)
+  (let ([uid-num (unique-name-nums)])
+    (unique-name-nums (add1 uid-num))
+    (string->symbol (string-append (symbol->string id) "_" (number->string uid-num)))))

pkgs/redex-pkgs/redex-lib/redex/private/search.rkt

@@ -215,29 +215,6 @@
              (and (not-failed? u-res)
                   (loop (p*e-e u-res) rest))]))]
        [else #f])]))
-           
-         
-
-;; TODO: compare with free-identifier=? so renaming is safe
-;; w/r/t macro expansion
-;; (use free-id-table)
-(define (fresh-pat-vars pre-pat instantiations)
-  (match pre-pat
-    [`(name ,id ,pat)
-     (define new-id (hash-ref instantiations id
-                              (λ ()
-                                (define unique-id (make-uid id))
-                                (hash-set! instantiations id unique-id)
-                                unique-id)))
-     `(name ,new-id ,(fresh-pat-vars pat instantiations))]
-    [`(list ,pats ...)
-     `(list ,@(for/list ([p pats]) (fresh-pat-vars p instantiations)))]
-    [_ pre-pat]))
-
-(define (make-uid id)
-  (let ([uid-num (unique-name-nums)])
-    (unique-name-nums (add1 uid-num))
-    (string->symbol (string-append (symbol->string id) "_" (number->string uid-num)))))
 
 (define (fresh-clause-vars clause-raw)
   (define instantiations (make-hash))
@@ -276,7 +253,6 @@
     (define str (format "depth bound exceeded at depth: ~s" (length tr-loc)))
     (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))))
 
-(define unique-name-nums (make-parameter 0))
 
 (define generation-logger (make-logger 'generation-log (current-logger)))
 

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

@@ -795,3 +795,13 @@
     (test (gen-ith 0) 0)
     (test (gen-ith 1) 1)))
 
+(let ()
+  (define-language L
+    (e ::= (name aha! any)))
+
+  (define-judgment-form L
+    #:mode (J I I)
+    [(J e e)])
+  
+  (is-not-false
+   (generate-term L #:satisfying (J e_1 e_2) 10)))

pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt

@@ -587,8 +587,12 @@
                 (p*e 'variable (hash)))
   (check-equal? (unify/format `(nt y) 'any (hash) ntl)
                 (p*e 'variable (hash)))
+  ;; asymmetry ok here - if the nt doesn't get unified against,
+  ;; it doesn't get collapsed
   (check-equal? (unify/format `(nt y) '(nt Q) (hash) ntl)
-                (p*e '(cstr (Q) variable) (hash)))
+                `(different-orders=>different-results 
+                 ,(p*e '(cstr (Q) variable) (env (hash) '()))
+                 ,(p*e '(cstr (Q) (nt y)) (env (hash) '()))))
   )
 
 
@@ -820,7 +824,7 @@
         (p*e `(list λ y (name e_2 ,(bound))) (m-hash (lvar 'e_2) `(cstr (e) 3))))
 (u-test λn (λ x 3) (λ x e_2) (hash) 
         (p*e `(list λ (name x ,(bound)) (name e_2 ,(bound)))
-             (m-hash (lvar 'e_2) `(cstr (e) 3) (lvar 'x) `variable-not-otherwise-mentioned)))
+             (m-hash (lvar 'e_2) `(cstr (e) 3) (lvar 'x) `(nt x))))
 (u-fails λn (λ x 3) (e_1 e_2) (hash))
 (u-test λn (e_1 e_2) ((λ x x) 3) (hash) 
         (p*e `(list (name e_1 ,(bound)) (name e_2 ,(bound)))
@@ -829,7 +833,7 @@
                      (lvar 'e_1)
                      `(cstr (e) (list λ (name x ,(bound)) (name x ,(bound))))
                      (lvar 'x)
-                     `variable-not-otherwise-mentioned)))
+                     `(nt x))))
 
 (define-language p-types
   (t (t -> t)