suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

redex: randomly choose between search heuristics

Browse Source
This commit is contained in:
Burke Fetscher 2014-10-09 12:51:24 -05:00
parent cefa13c4d7
commit d17fca3838
2 changed files with 47 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
View File

@ -2199,19 +2199,20 @@ with @racket[#:satisfying].}
(sum nat_1 nat_2 nat_3) (sum nat_1 nat_2 nat_3)
(equal? (term nat_1) (term nat_2)))] (equal? (term nat_1) (term nat_2)))]
@defparam[depth-dependent-order? depth-dependent boolean? @defparam[depth-dependent-order? depth-dependent (or/c boolean? 'random)
#:value #t]{ #: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 chance that more recursive clauses of judgment forms or metafunctions
are chosen earlier when attempting to generate terms are chosen earlier when attempting to generate terms
with forms that use @racket[#:satisfying]. It is @racket[#t] by with forms that use @racket[#:satisfying]. If it is @racket[#t],
default, which causes redex to favor more recursive clauses at Redex favors more recursive clauses at
lower depths and less recursive clauses at depths closer to the lower depths and less recursive clauses at depths closer to the
limit, in an attempt to generate larger terms. When it is limit, in an attempt to generate larger terms.
@racket[#f], all clause orderings have equal probability When it is @racket[#f], all clause orderings have equal probability
above the bound. 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) @defform/subs[(redex-generator language-id satisfying size-expr)

73
pkgs/redex-pkgs/redex-lib/redex/private/search.rkt
View File

@ -47,7 +47,7 @@
(define-struct fail-cont (env fringe bound) (define-struct fail-cont (env fringe bound)
#:transparent) #: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) (define-struct gen-trace (tr-loc clause input state bound env) #:prefab)
@ -71,40 +71,43 @@
(pushdown-count (add1 (pushdown-count)))) (pushdown-count (add1 (pushdown-count))))
(define (search/next clauses input bound lang) (define (search/next clauses input bound lang)
(define name-nums 0) (parameterize ([depth-dependent-order? (if (equal? (depth-dependent-order?) 'random)
(define fresh-pat (parameterize ([unique-name-nums 0]) (> 0.5 (random))
(begin0 (depth-dependent-order?))])
(fresh-pat-vars input (make-hash)) (define name-nums 0)
(set! name-nums (unique-name-nums))))) (define fresh-pat (parameterize ([unique-name-nums 0])
(define fs (list (fail-cont empty-env (begin0
(list (make-partial-rule (fresh-pat-vars input (make-hash))
fresh-pat (set! name-nums (unique-name-nums)))))
(if (shuffle-clauses?) (define fs (list (fail-cont empty-env
(shuffle-clauses clauses 0 bound) (list (make-partial-rule
(order-clauses clauses)) fresh-pat
'() bound)) (if (shuffle-clauses?)
bound))) (shuffle-clauses clauses 0 bound)
(define v-locs (make-hash)) (order-clauses clauses))
(λ () '() bound))
(parameterize ([unique-name-nums name-nums] bound)))
[bt-count 0] (define v-locs (make-hash))
[bt-limit (* bound 10)] (λ ()
[pushdown-count 0] (parameterize ([unique-name-nums name-nums]
[pushdown-limit (* bound 200)]) [bt-count 0]
(define-values (ans fails) [bt-limit (* bound 10)]
(with-handlers ([exn:fail:redex:search-failure? (λ (e) [pushdown-count 0]
(define f-conts (exn:fail:redex:search-failure-fails e)) [pushdown-limit (* bound 200)])
(values (unif-fail) (trim-fails f-conts)))]) (define-values (ans fails)
(define-values (env/f fails) (with-handlers ([exn:fail:redex:search-failure? (λ (e)
(fail-back fs)) (define f-conts (exn:fail:redex:search-failure-fails e))
(values (and/fail env/f (unify fresh-pat 'any env/f lang)) (values (unif-fail) (trim-fails f-conts)))])
fails))) (define-values (env/f fails)
(set-last-gen-trace! (generation-trace)) (fail-back fs))
(set! fs (if (success-jump?) (values (and/fail env/f (unify fresh-pat 'any env/f lang))
fails fails)))
(shuffle-fails fails))) ;; how to test if we're randomizing here? (set-last-gen-trace! (generation-trace))
(set! name-nums (unique-name-nums)) (set! fs (if (success-jump?)
ans))) fails
(shuffle-fails fails))) ;; how to test if we're randomizing here?
(set! name-nums (unique-name-nums))
ans))))
(define (trim-fails fs) (define (trim-fails fs)
(define rev-fs (reverse fs)) (define rev-fs (reverse fs))