diff --git a/collects/redex/private/jdg-gen.rkt b/collects/redex/private/jdg-gen.rkt index 1dc9b93d25..1a5c638d40 100644 --- a/collects/redex/private/jdg-gen.rkt +++ b/collects/redex/private/jdg-gen.rkt @@ -202,4 +202,3 @@ (lookup new-id env)] [_ (values (lvar id) res)])) - diff --git a/collects/redex/private/pat-unify.rkt b/collects/redex/private/pat-unify.rkt index 039d082d38..df954d64d1 100644 --- a/collects/redex/private/pat-unify.rkt +++ b/collects/redex/private/pat-unify.rkt @@ -700,7 +700,8 @@ (for/or ([ntp (in-list (map normalize-pat (nt-pats nt clang)))]) (not-failed? (unify* npat ntp #f empty-lang)))) (set! memo - (hash-set memo (list nt clang npat) pat-ok?))))))) + (hash-set memo (list nt clang npat) pat-ok?)) + pat-ok?))))) (define (normalize-pat pat) (let loop ([pat pat]) @@ -757,4 +758,4 @@ (define empty-lang (compiled-lang #f #f #f #f #f #f #f #f #f #f '() #f (hash) - (lang-enumerators '()))) + (lang-enumerators '()))) \ No newline at end of file diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index d78c448692..cb40cb516d 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -1469,28 +1469,6 @@ (apply set-union (set) (map pat-vars ps))] [_ (set)])) - -(define-for-syntax (fix-and-extract-dq-vars pat) - (define new-ids (hash)) - (let recur ([pat pat]) - (syntax-case pat (list name) - [(name vname p) - (with-syntax ([((vs ...) new-p) (recur #'p)] - [new-vn (datum->syntax #'vname - (let ([vn (syntax-e #'vname)]) - (hash-ref new-ids vn - (λ () - (define new (string->symbol (format "~s_p" vn))) - (set! new-ids (hash-set new-ids vn new)) - new))) - #'vname)]) - #'((new-vn vs ...) (name new-vn new-p)))] - [(list ps ...) - (with-syntax* ([(((vs ...) new-ps) ...) (map recur (syntax->list #'(ps ...)))] - [(u-vs ...) (remove-duplicates (syntax->list #'(vs ... ...)) #:key syntax-e)]) - #'((u-vs ...) (list new-ps ...)))] - [pat - #'(() pat)]))) (define-for-syntax (check-arity-consistency mode contracts full-def) (when (and contracts (not (= (length mode) (length contracts)))) diff --git a/collects/redex/private/search.rkt b/collects/redex/private/search.rkt index 6288a211d8..002c8e34e5 100644 --- a/collects/redex/private/search.rkt +++ b/collects/redex/private/search.rkt @@ -21,7 +21,8 @@ last-gen-trace get-most-recent-trace update-gen-trace! - generation-logger) + generation-logger + gen-state) ;; clause : head-pat eq/dqs (listof prem) (define-struct clause (head-pat eq/dqs prems lang name) #:transparent) @@ -45,12 +46,25 @@ (define-struct gen-trace (tr-loc clause input state bound env) #:prefab) +(define gen-state (make-parameter (set 'shuffle-clauses 'success-jump))) + +(define (shuffle-clauses?) + (set-member? (gen-state) 'shuffle-clauses)) + +(define (success-jump?) + (set-member? (gen-state) 'success-jump)) + (define bt-count (make-parameter 0)) -(define BT-LIMIT 40) +(define bt-limit (make-parameter 0)) (define (inc-bt-count) (bt-count (add1 (bt-count)))) +(define pushdown-count (make-parameter 0)) +(define pushdown-limit (make-parameter 0)) +(define (inc-pushdown-count) + (pushdown-count (add1 (pushdown-count)))) + (define (search/next clauses input bound lang) (define name-nums 0) (define fresh-pat (parameterize ([unique-name-nums 0]) @@ -58,12 +72,18 @@ (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 (shuffle clauses) '() bound)) + (list (make-partial-rule fresh-pat (if (shuffle-clauses?) + (shuffle clauses) + (order-clauses clauses)) + '() bound)) bound))) (define v-locs (make-hash)) (λ () (parameterize ([unique-name-nums name-nums] - [bt-count 0]) + [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)) @@ -73,7 +93,8 @@ (values (and/fail env/f (unify fresh-pat 'any env/f lang)) fails))) (set-last-gen-trace! (generation-trace)) - (set! fs (shuffle-fails fails)) ;; how to test if we're randomizing here? + (when (success-jump?) + (set! fs (shuffle-fails fails))) ;; how to test if we're randomizing here? (set! name-nums (unique-name-nums)) ans))) @@ -109,6 +130,7 @@ (push-down (car fringe) env (cdr fringe) fail)])) (define (push-down a-partial-rule env fringe fail) + (inc-pushdown-count) (match a-partial-rule [(partial-rule pat clauses tr-loc bound) (check-depth-limits bound tr-loc fail) @@ -136,7 +158,9 @@ (define prem-cls (prem-clauses prem)) (make-partial-rule (prem-pat prem) (if (positive? bound) - (shuffle prem-cls) + (if (shuffle-clauses?) + (shuffle prem-cls) + (order-clauses prem-cls)) (order-clauses prem-cls)) (cons n tr-loc) (- bound 1)))) @@ -241,8 +265,12 @@ (define-struct (exn:fail:redex:search-failure exn:fail:redex) (fails)) (define (check-depth-limits bound tr-loc fails) - (when (> (bt-count) BT-LIMIT) - (define str (format "backtrack count of ~s exceeded at ~s" BT-LIMIT tr-loc)) + (when ((pushdown-count) . > . (pushdown-limit)) + (define str (format "pushdown count of ~s exceeded at ~s" (pushdown-count) tr-loc)) + ;(printf "!*\n\t~s\t*!\n" str) + (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))) + (when (> (bt-count) (bt-limit)) + (define str (format "backtrack count of ~s exceeded at ~s" (bt-limit) tr-loc)) (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))) (when (> (length tr-loc) (* 3 (+ (length tr-loc) bound))) (define str (format "depth bound exceeded at depth: ~s" (length tr-loc))) @@ -282,5 +310,4 @@ most-recent-trace) (define (set-last-gen-trace! trace) - (set! most-recent-trace trace)) - + (set! most-recent-trace trace)) \ No newline at end of file