redex: make the depth-based clause ordering smarter

pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt

@@ -914,4 +914,5 @@
          redex-generator
          (struct-out counterexample)
          (struct-out exn:fail:redex:test)
-         pick-an-index)
+         pick-an-index
+         depth-dependent-order?)

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

@@ -6,6 +6,8 @@
          racket/list
          racket/contract
          racket/set
+         math/distributions
+         (except-in math/number-theory permutations)
          (for-syntax racket/base))
 
 (provide (struct-out clause)
@@ -22,7 +24,8 @@
          get-most-recent-trace
          update-gen-trace!
          generation-logger
-         gen-state)
+         gen-state
+         depth-dependent-order?)
 
 ;; clause : head-pat eq/dqs (listof prem)
 (define-struct clause (head-pat eq/dqs prems lang name) #:transparent)
@@ -44,6 +47,8 @@
 (define-struct fail-cont (env fringe bound)
   #:transparent)
 
+(define depth-dependent-order? (make-parameter #t))
+
 (define-struct gen-trace (tr-loc clause input state bound env) #:prefab)
 
 (define gen-state (make-parameter (set 'shuffle-clauses 'success-jump)))
@@ -75,7 +80,7 @@
                               (list (make-partial-rule 
                                      fresh-pat 
                                      (if (shuffle-clauses?)
-                                         (shuffle/favor-recursive-clauses clauses)
+                                         (shuffle-clauses clauses 0 bound)
                                          (order-clauses clauses))
                                      '() bound))
                               bound)))
@@ -136,6 +141,7 @@
   (inc-pushdown-count)
   (match-define (partial-rule pat clauses tr-loc bound) a-partial-rule)
   (check-depth-limits bound tr-loc fail)
+  (define depth (length tr-loc))
   (cond
     [(null? clauses)
      (fail-back fail)]
@@ -161,7 +167,7 @@
             (make-partial-rule (prem-pat prem) 
                                (if (positive? bound)
                                    (if (shuffle-clauses?)
-                                       (shuffle/favor-recursive-clauses prem-cls)
+                                       (shuffle-clauses prem-cls depth bound)
                                        (order-clauses prem-cls))
                                    (order-clauses prem-cls))
                                (cons n tr-loc)
@@ -172,16 +178,48 @@
                      new-fringe
                      (cons (fail-cont env failure-fringe bound) fail))])]))
 
-(define (shuffle/favor-recursive-clauses cs)
+(define (shuffle-clauses cs depth bound)
-  (define candidates (apply append
+  (if (depth-dependent-order?)
-                            (for/list ([c (in-list cs)])
+      (shuffle/binomial cs depth bound)
-                              (make-list (add1 (length (clause-prems c))) c))))
+      (shuffle cs)))
-  (let loop ([candidates candidates])
+
+(define (shuffle/binomial clauses depth bound)
+  (random-order clauses depth (+ depth bound) 
+                #:key (λ (cls) (length (clause-prems cls)))))
+
+(define (random-order l depth max-depth #:key [key values])
+  (define bd (get-dist l depth max-depth))
+  (define n (round ((distribution-sample bd))))
+  (define perm (nth-lexico-perm (length l) 
+                                (inexact->exact n)))
+  (define l-sorted (reverse (sort (shuffle l) < #:key key)))
+  (for/list ([i (in-list perm)])
+    (list-ref l-sorted i)))
+
+(define get-dist
+  (let ([cache (make-hash)])
+    (λ (l depth max-depth)
+      (hash-ref cache (list l depth max-depth)
+                (λ ()
+                  (define nperms (factorial (length l)))
+                  (define d (binomial-dist (sub1 nperms) 
+                                           (+ (/ depth max-depth) 
+                                              (* 0.05 (- 0.5 (/ depth max-depth))))))
+                  (hash-set! cache d (list l depth max-depth))
+                  d)))))
+
+(define (nth-lexico-perm len n)
+  (let recur ([indices (build-list len values)]
+              [n n])
     (cond
-      [(null? candidates) null]
+      [(= (length indices) 1)
+       indices]
       [else
-       (define selected (list-ref candidates (random (length candidates))))
+       (define-values (q r)
-       (cons selected (loop (remove* (list selected) candidates)))])))
+         (quotient/remainder n (factorial (- (length indices) 1))))
+       (define index (list-ref indices q))
+       (cons index
+             (recur (remove index indices) r))])))
 
 (define (order-clauses cs)
   (define num-prems->cs (make-hash))

pkgs/redex-pkgs/redex-lib/redex/reduction-semantics.rkt

@@ -67,7 +67,8 @@
          redex-generator
          exn:fail:redex:generation-failure?
          (struct-out exn:fail:redex:test)
-         (struct-out counterexample))
+         (struct-out counterexample)
+         depth-dependent-order?)
 
 (provide variable-not-in
          variables-not-in)