diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt index db255b1ca2..92064e7e1e 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt +++ b/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?) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt index f0cdc5a08d..32e53c1cac 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt +++ b/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 candidates (apply append - (for/list ([c (in-list cs)]) - (make-list (add1 (length (clause-prems c))) c)))) - (let loop ([candidates candidates]) +(define (shuffle-clauses cs depth bound) + (if (depth-dependent-order?) + (shuffle/binomial cs depth bound) + (shuffle cs))) + +(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)))) - (cons selected (loop (remove* (list selected) candidates)))]))) + (define-values (q r) + (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)) diff --git a/pkgs/redex-pkgs/redex-lib/redex/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/reduction-semantics.rkt index b29fa0b7c0..4c2227bda1 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/reduction-semantics.rkt +++ b/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)