diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl index 62a89b670e..d7dd3880cd 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl @@ -2199,19 +2199,20 @@ 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]{ +@defparam[depth-dependent-order? depth-dependent (or/c boolean? 'random) + #:value 'random]{ -Toggles whether or not redex will dynamically adjust the +Toggles whether or not Redex will dynamically adjust the chance that more recursive clauses of judgment forms or metafunctions are chosen earlier when 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 +with forms that use @racket[#:satisfying]. If it is @racket[#t], +Redex favors 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 +limit, in an attempt to generate larger terms. +When it is @racket[#f], all clause orderings have equal probability above the bound. - +By default, it is @racket['random], which causes Redex to +choose between the two above alternatives with equal probability. } @defform/subs[(redex-generator language-id satisfying size-expr) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt index cdafb37db4..a478112c0f 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt @@ -47,7 +47,7 @@ (define-struct fail-cont (env fringe bound) #:transparent) -(define depth-dependent-order? (make-parameter #t)) +(define depth-dependent-order? (make-parameter 'random)) (define-struct gen-trace (tr-loc clause input state bound env) #:prefab) @@ -71,40 +71,43 @@ (pushdown-count (add1 (pushdown-count)))) (define (search/next clauses input bound lang) - (define name-nums 0) - (define fresh-pat (parameterize ([unique-name-nums 0]) - (begin0 - (fresh-pat-vars input (make-hash)) - (set! name-nums (unique-name-nums))))) - (define fs (list (fail-cont empty-env - (list (make-partial-rule - fresh-pat - (if (shuffle-clauses?) - (shuffle-clauses clauses 0 bound) - (order-clauses clauses)) - '() bound)) - bound))) - (define v-locs (make-hash)) - (λ () - (parameterize ([unique-name-nums name-nums] - [bt-count 0] - [bt-limit (* bound 10)] - [pushdown-count 0] - [pushdown-limit (* bound 200)]) - (define-values (ans fails) - (with-handlers ([exn:fail:redex:search-failure? (λ (e) - (define f-conts (exn:fail:redex:search-failure-fails e)) - (values (unif-fail) (trim-fails f-conts)))]) - (define-values (env/f fails) - (fail-back fs)) - (values (and/fail env/f (unify fresh-pat 'any env/f lang)) - fails))) - (set-last-gen-trace! (generation-trace)) - (set! fs (if (success-jump?) - fails - (shuffle-fails fails))) ;; how to test if we're randomizing here? - (set! name-nums (unique-name-nums)) - ans))) + (parameterize ([depth-dependent-order? (if (equal? (depth-dependent-order?) 'random) + (> 0.5 (random)) + (depth-dependent-order?))]) + (define name-nums 0) + (define fresh-pat (parameterize ([unique-name-nums 0]) + (begin0 + (fresh-pat-vars input (make-hash)) + (set! name-nums (unique-name-nums))))) + (define fs (list (fail-cont empty-env + (list (make-partial-rule + fresh-pat + (if (shuffle-clauses?) + (shuffle-clauses clauses 0 bound) + (order-clauses clauses)) + '() bound)) + bound))) + (define v-locs (make-hash)) + (λ () + (parameterize ([unique-name-nums name-nums] + [bt-count 0] + [bt-limit (* bound 10)] + [pushdown-count 0] + [pushdown-limit (* bound 200)]) + (define-values (ans fails) + (with-handlers ([exn:fail:redex:search-failure? (λ (e) + (define f-conts (exn:fail:redex:search-failure-fails e)) + (values (unif-fail) (trim-fails f-conts)))]) + (define-values (env/f fails) + (fail-back fs)) + (values (and/fail env/f (unify fresh-pat 'any env/f lang)) + fails))) + (set-last-gen-trace! (generation-trace)) + (set! fs (if (success-jump?) + fails + (shuffle-fails fails))) ;; how to test if we're randomizing here? + (set! name-nums (unique-name-nums)) + ans)))) (define (trim-fails fs) (define rev-fs (reverse fs))