redex-generator: determine bound order automatically

also, fix a bug where continuations in thunks returned
by redex-generator weren't being shuffled

collects/redex/examples/define-judgment-form/typing-rules-no-ellipses.rkt

@@ -24,22 +24,18 @@
   (i integer)
   (x variable-not-otherwise-mentioned))
 
-;; Order is important!
-;; When generating random terms, the clauses
-;; are tried in order when the depth bound is reached.
-;; (In general, the most recursive clauses should go last.)
 (define-judgment-form STLC
   #:mode (typeof I I O)
   #:contract (typeof Γ e τ)
-  [(typeof Γ i int)]
-  [(typeof Γ add1 (int → int))]
-  [(typeof Γ x τ)
-   (where τ (lookup Γ x))]
   [(typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))
    (typeof ([x τ_1] Γ) e τ_2)]
   [(typeof Γ (e_1 e_2) τ)
    (typeof Γ e_1 (τ_2 → τ))
-   (typeof Γ e_2 τ_2)])
+   (typeof Γ e_2 τ_2)]
+  [(typeof Γ x τ)
+   (where τ (lookup Γ x))]
+  [(typeof Γ i int)]
+  [(typeof Γ add1 (int → int))])
 
 
 (define-metafunction STLC

collects/redex/private/search.rkt

@@ -66,7 +66,7 @@
           (values (and env/f (unify fresh-pat 'any env/f lang))
                   fails)))
       (set-last-gen-trace! (generation-trace))
-      (set! fs (trim-fails fails))
+      (set! fs (shuffle-fails fails))  ;; how to test if we're randomizing here?
       (set! name-nums (unique-name-nums))
       (set! v-locs (visited-locs))
       ans)))
@@ -135,7 +135,7 @@
                                   (if (positive? bound)
                                       #;(shuffle-clauses-stlc prem-cls (sub1 bound))
                                       (shuffle prem-cls)
-                                      prem-cls)
+                                      (order-clauses prem-cls))
                                   (cons n tr-loc)
                                   (- bound 1))))
            (define new-fringe (append new-fringe-elements
@@ -144,6 +144,22 @@
                         new-fringe
                         (cons (fail-cont env failure-fringe bound) fail))])])]))
 
+(define (order-clauses cs)
+  (define num-prems->cs (hash))
+  (for ([c cs])
+    (set! num-prems->cs
+          (hash-set num-prems->cs
+                    (length (clause-prems c))
+                    (set-add
+                     (hash-ref num-prems->cs
+                               (length (clause-prems c))
+                               (λ () (set)))
+                     c))))
+  (apply append
+         (for/list ([k (sort (hash-keys num-prems->cs) <)])
+           (shuffle (set->list (hash-ref num-prems->cs k))))))
+  
+
 
 (define (do-unification clse input env)
   (match clse

collects/redex/tests/gen-test.rkt

@@ -129,6 +129,28 @@
       [#f
        (void)])))
 
+(let ()
+  
+  (define-language TL
+    (T (N T T)
+       (L number)))
+  
+  (define-relation TL
+    [(tree (N T_1 T_2))
+     (tree T_1)
+     (tree T_2)]
+    [(tree (L number))])
+  
+  (test-equal
+   (not
+    (empty?
+     (filter
+      values
+      (for/list ([_ 100])
+        (generate-term TL #:satisfying (tree T) 2)))))
+   #t)
+  )
+
 (let ()
   (define-language STLC
     (τ int