From 96714934b6c7aee7fc756218243b2fdd2e152d8a Mon Sep 17 00:00:00 2001
From: Burke Fetscher <bfetscher@racket-lang.org>
Date: Tue, 30 Sep 2014 17:28:56 -0500
Subject: [PATCH] redex: try harder when checking non-terminals

Unfold non-terminals other than the one we're currently
checking, and follow variable references, when normalizing
patterns for nt checking.
---
 .../redex-doc/redex/scribblings/ref.scrbl     |  15 ++
 .../redex-lib/redex/private/pat-unify.rkt     | 141 ++++++++++--------
 .../redex-test/redex/tests/unify-tests.rkt    |  27 ++++
 3 files changed, 120 insertions(+), 63 deletions(-)

diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
index fa00ca077e..fdb4029f5a 100644
--- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
+++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
@@ -2199,6 +2199,21 @@ with @racket[#:satisfying].}
                     (sum nat_1 nat_2 nat_3)
                     (equal? (term nat_1) (term nat_2)))]
 
+@defparam[depth-dependent-order? depth-dependent boolean?
+                                 #:value #t]{
+
+Toggles whether or not redex will dynamically adjust the
+chance that more recursive clauses of judgment forms or metafunctions 
+are chosen earlierwhen attempting to generate terms 
+with forms that use @racket[#:satisfying]. It is @racket[#t] by
+default, which causes redex to favor more recursive clauses at
+lower depths and less recursive clauses at depths closer to the
+limit, in an attempt to generate larger terms. When it is
+@racket[#f], all clause orderings have equal probability
+above the bound.
+
+}
+
 @defform/subs[(redex-generator language-id satisfying size-expr)
               ([satisfying (judgment-form-id @#,ttpattern ...)
                            (code:line (metafunction-id @#,ttpattern ...) = @#,ttpattern)])
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
index 996e154293..694523c92d 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
@@ -85,7 +85,11 @@
 
 (define predef-pats (set 'any 'number 'string 'integer 'boolean 'real 'variable 'natural 'variable-not-otherwise-mentioned))
 (define (predef-pat? a)
-  (set-member? predef-pats a))
+  (or (set-member? predef-pats a)
+      (match a
+        [`(variable-except ,_ ...) #t]
+        [`(variable-prefix ,_) #t]
+        [_ #f])))
 (define (var? s)
   (symbol? s))
 (define (n-t? s)
@@ -573,7 +577,7 @@
                 (and/fail new-nts
                           (p*e `(cstr ,new-nts ,new-p) res-e))]
                [_
-                (and/fail (for/and ([n nts]) (check-nt n L res-p))
+                (and/fail (for/and ([n nts]) (check-nt n L res-p e))
                           (p*e `(cstr ,nts ,res-p) res-e))])))
   
 (define (u*-2nts n-t n-u e L)
@@ -583,7 +587,7 @@
 
 (define (u*-1nt p u e L)
   (and/fail
-   (check-nt p L u)
+   (check-nt p L u e)
    (if (hash-has-key? (compiled-lang-collapsible-nts L) p)
        (maybe-let ([bn-res (bind-names (fresh-pat-vars (hash-ref (compiled-lang-collapsible-nts L) p) (make-hash)) e L)])
          (unify* (p*e-p bn-res) u (p*e-e bn-res) L))
@@ -773,7 +777,7 @@
 
 (define (merge-ids/sorted l1 l2 lang)
   (and (for*/and ([nt1 l1] [nt2 l2])
-         (check-nt nt1 lang `(nt ,l2)))
+         (check-nt nt1 lang `(nt ,nt2) empty-env))
        (de-dupe/sorted (merge/sorted l1 l2))))
 
 (define (symbol<? s1 s2)
@@ -837,20 +841,6 @@
       [_
        (values (lvar id) res eqs)])))
 
-(provide check-nt
-         normalize-pat)
-
-(define check-nt
-  (let ([memo (make-hash)])
-    (λ (nt clang pat)
-      (define npat (normalize-pat clang pat))
-      (hash-ref memo (list nt clang npat)
-                (λ ()
-                  (define pat-ok? 
-                    (for/or ([ntp (in-list (map ((curry normalize-pat) clang) (nt-pats nt clang)))])
-                      (not-failed? (unify* npat ntp empty-env empty-lang))))
-                  (hash-set! memo (list nt clang npat) pat-ok?)
-                  pat-ok?)))))
 
 (define unsupported-pat-err-name (make-parameter #f))
 
@@ -863,58 +853,83 @@
                               "  pattern: ~a")
                pat))
 
-(define (normalize-pat lang pat)
-  (define err unsupported-pat-err)
-  (let loop ([pat pat])
-    (match-a-pattern #:allow-else pat
-                     [`any pat]
-                     [`number pat]
-                     [`string pat]
-                     [`natural pat]
-                     [`integer pat]
-                     [`real pat]
-                     [`boolean pat]
-                     [`variable pat]
-                     [`(variable-except ,s ...) `variable]
-                     [`(variable-prefix ,s) `variable]
-                     [`variable-not-otherwise-mentioned pat]
-                     [`hole (err pat)]
-                     [`(nt ,id)
-                      (loop (hash-ref (compiled-lang-collapsible-nts lang) id 'any))]
-                     [`(name ,name ,npat)
-                      (if (bound? npat)
-                          `any
-                          `(name ,name ,(loop npat)))]
-                     [`(mismatch-name ,name ,pat) (loop pat)]
-                     [`(in-hole ,p1 ,p2) (err pat)]
-                     [`(hide-hole ,p) (loop p)]
-                     [`(side-condition ,p ,g ,e)
-                      (err pat)]
-                     [`(cross ,s) (err pat)]
-                     [`(list ,sub-pats ...)
-                      `(list ,@(for/list ([sub-pat (in-list sub-pats)])
-                                 (match sub-pat
-                                   [`(repeat ,pat ,name ,mismatch)
-                                    (err sub-pat)]
-                                   [_
-                                    (loop sub-pat)])))]
-                     [(? (compose not pair?)) 
-                      pat]
-                     [_
-                      (match pat
-                        [`(variable-not-in ,p ,s)
-                         `variable])])))
+(define normalizing-nt (make-parameter #f))
 
-(provide nt-pats)
+(define check-nt
+  (let ([memo (make-hash)])
+    (λ (nt clang pat e)
+      (parameterize ([normalizing-nt nt])
+        (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))))
+                    (hash-set! memo (list nt clang npat) pat-ok?)
+                    pat-ok?))))))
+
+(define (normalize-pat lang e pat)
+  (define err unsupported-pat-err)
+  (let loop ([pat pat]
+             [depth 5])
+    (cond
+      [(depth . <= . 0) 'any]
+      [else
+       (match-a-pattern #:allow-else pat
+                        [`any pat]
+                        [`number pat]
+                        [`string pat]
+                        [`natural pat]
+                        [`integer pat]
+                        [`real pat]
+                        [`boolean pat]
+                        [`variable pat]
+                        [`(variable-except ,s ...) pat]
+                        [`(variable-prefix ,s) pat]
+                        [`variable-not-otherwise-mentioned pat]
+                        [`hole (err pat)]
+                        [`(nt ,id)
+                         (cond 
+                           [(and (normalizing-nt)
+                                 (eq? (normalizing-nt) id)) 'any]
+                           [(hash-has-key? (compiled-lang-collapsible-nts lang) id)
+                            (loop (hash-ref (compiled-lang-collapsible-nts lang) id) (sub1 depth))]
+                           [else pat])]
+                        [`(name ,name ,npat)
+                         (if (bound? npat)
+                             (match-let ([(p*e `(name ,n ,(bound)) e-new) (resolve pat e)])
+                               (loop (hash-ref (env-eqs e) (lvar n)) depth))
+                             `(name ,name ,(loop npat (sub1 depth))))]
+                        [`(mismatch-name ,name ,pat) (loop pat (sub1 depth))]
+                        [`(in-hole ,p1 ,p2) (err pat)]
+                        [`(hide-hole ,p) (loop p (sub1 depth))]
+                        [`(side-condition ,p ,g ,e)
+                         (err pat)]
+                        [`(cross ,s) (err pat)]
+                        [`(list ,sub-pats ...)
+                         `(list ,@(for/list ([sub-pat (in-list sub-pats)])
+                                    (match sub-pat
+                                      [`(repeat ,pat ,name ,mismatch)
+                                       (err sub-pat)]
+                                      [_
+                                       (loop sub-pat (sub1 depth))])))]
+                        [(? (compose not pair?)) 
+                         pat]
+                        [_
+                         (match pat
+                           [`(cstr ,cs ,p)
+                            (loop p (sub1 depth))]
+                           [`(variable-not-in ,p ,s)
+                            `variable])])])))
 
 (define (nt-pats nt lang)
   (define this-rhs
     (nt-rhs
      (let ([the-nt (findf (λ (lang-nt)
-                        (equal? nt (nt-name lang-nt)))
-                      (compiled-lang-lang lang))])
+                            (equal? nt (nt-name lang-nt)))
+                          (compiled-lang-lang lang))])
        (unless the-nt
-         (error 'unify "nonterminal ~s not found for provided language... nts found: ~s" 
+         (error 'unify "nonterminal ~a not found for provided language... nts found: ~a" 
                 nt (hash-keys (compiled-lang-nt-map lang))))
        the-nt)))
   (match this-rhs
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt
index 6b9df0f466..f0db3ba2a1 100644
--- a/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt
+++ b/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt
@@ -1193,6 +1193,33 @@
   (env (hash (lvar 'a) 'any (lvar 'b) 'any)
        (list (dq '() `((list (name b ,(bound))) (list 2)))))))
 
+;; unfold non-terminals correctly
+(let ()
+  (define-language lnt
+    (a (a a) 
+       b)
+    (b (n n))
+    (c (n n n))
+    (d (b b b))
+    (n number))
+  
+  (check-equal?
+   (unify '(list 1 2 3) '(nt a) empty-env lnt)
+   (unif-fail))
+  (check-equal?
+   (unify '(nt c) '(nt a) empty-env lnt)
+   (unif-fail))
+  (check-equal?
+   (unify '(nt d) '(nt a) empty-env lnt)
+   (unif-fail))
+  (check-not-equal?
+   (unify '(list 1 2 3) '(nt c) empty-env lnt)
+   (unif-fail))
+  (check-not-equal?
+   (unify '(list 1 2) '(nt a) empty-env lnt)
+   (unif-fail))
+  )
+
 
 
 (let ([untested