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

improve judgment form performance in some situations when

Browse Source 
ambiguous judgment forms lead to exponential blowup
This commit is contained in:
Robby Findler 2014-07-25 18:37:14 -05:00
parent 41175d74be
commit 0416b8403d
2 changed files with 59 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
View File

@ -6,6 +6,7 @@
"error.rkt" "error.rkt"
"search.rkt" "search.rkt"
racket/trace racket/trace
racket/list
racket/stxparam racket/stxparam
"term-fn.rkt" "term-fn.rkt"
"rewrite-side-conditions.rkt" "rewrite-side-conditions.rkt"
@ -332,15 +333,30 @@
(apply trace-call form-name wrapped (assemble mode input spacers)) (apply trace-call form-name wrapped (assemble mode input spacers))
outputs) outputs)
(form-proc form-proc input derivation-init))) (form-proc form-proc input derivation-init)))
(for/list ([v (in-list vecs)]) (remove-duplicates
(define subs (derivation-with-output-only-subs v)) (for/list ([v (in-list vecs)])
(define rulename (derivation-with-output-only-name v)) (define subs (derivation-with-output-only-subs v))
(define this-output (derivation-with-output-only-output v)) (define rulename (derivation-with-output-only-name v))
(derivation-subs-acc (define this-output (derivation-with-output-only-output v))
(and subs (derivation (cons form-name (assemble mode input this-output)) (derivation-subs-acc
rulename (and subs (derivation (cons form-name (assemble mode input this-output))
(reverse subs)))
this-output))) ;; just drop the subderivations
;; and the name when we know we
;; won't be using them.
;; this lets the remove-duplicates
;; call just above do something
;; and possibly avoid exponential blowup
(if (include-entire-derivation)
rulename
"")
(if (include-entire-derivation)
(reverse subs)
'())))
this-output))))
(define include-entire-derivation (make-parameter #f))
(define (verify-name-ok orig-name the-name) (define (verify-name-ok orig-name the-name)
(unless (symbol? the-name) (unless (symbol? the-name)
@ -797,12 +813,13 @@
id-or-not)]) id-or-not)])
(check-judgment-arity stx judgment) (check-judgment-arity stx judgment)
(syntax-property (syntax-property
(if id-or-not #`(parameterize ([include-entire-derivation #,derivation?])
#`(let ([#,id-or-not '()]) #,(if id-or-not
#,main-stx) #`(let ([#,id-or-not '()])
#`(sort #,main-stx #,main-stx)
string<=? #`(sort #,main-stx
#:key (λ (x) (format "~s" x)))) string<=?
#:key (λ (x) (format "~s" x)))))
'disappeared-use 'disappeared-use
(syntax-local-introduce #'form-name)))] (syntax-local-introduce #'form-name)))]
[(_ stx-name derivation? (not-form-name . _) . _) [(_ stx-name derivation? (not-form-name . _) . _)

27
pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
View File

@ -2767,6 +2767,33 @@
(test (judgment-holds (Q (3 4) number_1) number_1) (test (judgment-holds (Q (3 4) number_1) number_1)
'(14))) '(14)))
(let ()
(define-judgment-form empty-language
#:mode (J I)
[(D any_x) ...
--------------
(J (any_x ...))])
(define-judgment-form empty-language
#:mode (D I)
[----------- nat
(D natural)]
[----------- num
(D number)])
;; this test is designed to check to see if we are
;; avoiding an exponential blow up. On my laptop,
;; a list of length 14 was taking 2 seconds before
;; the fix and 1 msec afterwards. After the fix,
;; a list of length 100 (as below) was also taking
;; no time.
(define-values (_ cpu real gc)
(time-apply
(λ ()
(judgment-holds (J ,(build-list 100 add1))))))
(test (< cpu 1000) #t))
(parameterize ([current-namespace (make-base-namespace)]) (parameterize ([current-namespace (make-base-namespace)])
(eval '(require errortrace)) (eval '(require errortrace))