Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update judgment-forms caches to use alpha-equivalence. #103

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Update judgment-forms caches to use alpha-equivalence. #103

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1e7ff97
Update apply-reduction-relation* to be sensitive to alpha-equivalence
howell May 9, 2017
30bfde1
Change judgment-form cache to an α-hash
wilbowma May 27, 2017
bfd6495
Changed some missing hashes to α-hashes
wilbowma May 27, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 2 additions & 4 deletions redex-gui-lib/redex/private/stepper.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,10 +66,8 @@ todo:
;; all-nodes-ht : hash[sexp -o> (is-a/c node%)]

(define all-nodes-ht
(let* ([lang (reduction-relation-lang red)]
[term-equal? (lambda (x y) (α-equal? (compiled-lang-binding-table lang) match-pattern x y))]
[term-hash (lambda (x) (α-equal-hash-code (compiled-lang-binding-table lang) match-pattern x))])
(make-custom-hash term-equal? term-hash)))
(make-α-hash (compiled-lang-binding-table (reduction-relation-lang red))
match-pattern))

(define root (new node%
[pp pp]
Expand Down
4 changes: 1 addition & 3 deletions redex-gui-lib/redex/private/traces.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,9 +353,7 @@
[(IO-judgment-form? reductions) (runtime-judgment-form-lang reductions)]))

(define snip-cache
(let* ([term-equal? (lambda (x y) (α-equal? (compiled-lang-binding-table reductions-lang) match-pattern x y))]
[term-hash (lambda (x) (α-equal-hash-code (compiled-lang-binding-table reductions-lang) match-pattern x))])
(make-custom-hash term-equal? term-hash)))
(make-α-hash (compiled-lang-binding-table reductions-lang) match-pattern))

;; call-on-eventspace-main-thread : (-> any) -> any
;; =reduction thread=
Expand Down
7 changes: 6 additions & 1 deletion redex-lib/redex/private/binding-forms.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ to traverse the whole value at once, rather than one binding form at a time.
;; == public interface ==

(provide freshen α-equal? α-equal-hash-code safe-subst binding-forms-opened?
make-α-hash)
make-α-hash make-immutable-α-hash)

;; == parameters ==

Expand Down Expand Up @@ -137,6 +137,11 @@ to traverse the whole value at once, rather than one binding form at a time.
(λ (x) (α-equal-hash-code language-bf-table match-pattern x))
(λ (x) (α-equal-secondary-hash-code language-bf-table match-pattern x))))

(define (make-immutable-α-hash language-bf-table match-pattern)
(make-immutable-custom-hash (λ (x y) (α-equal? language-bf-table match-pattern x y))
(λ (x) (α-equal-hash-code language-bf-table match-pattern x))
(λ (x) (α-equal-secondary-hash-code language-bf-table match-pattern x))))

;; α-equal? : (listof (list compiled-pattern bspec))
;; (compiled-pattern redex-val -> (union #f mtch)) redex-val -> boolean
(define (α-equal? language-bf-table match-pattern redex-val-lhs redex-val-rhs)
Expand Down
22 changes: 13 additions & 9 deletions redex-lib/redex/private/judgment-form.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
racket/list
racket/stxparam
racket/dict
racket/function
(only-in "pat-unify.rkt"
unsupported-pat-err-name
unsupported-pat-err)
Expand Down Expand Up @@ -410,12 +411,12 @@
(car pair-of-boxed-caches)
(cdr pair-of-boxed-caches)))
(when (caching-enabled?)
(when (>= (hash-count (unbox boxed-cache)) cache-size)
(set-box! boxed-cache (make-hash))))
(when (>= (dict-count (unbox boxed-cache)) cache-size)
(set-box! boxed-cache (make-α-hash (compiled-lang-binding-table ct-lang) match-pattern))))
(define traced (current-traced-metafunctions))
(define cache (unbox boxed-cache))
(define in-cache? (and (caching-enabled?)
(let ([cache-value (hash-ref cache input not-in-cache)])
(let ([cache-value (dict-ref cache input not-in-cache)])
(not (eq? cache-value not-in-cache)))))
(define p-a-e (print-as-expression))
(define (form-proc/cache recur input derivation-init pair-of-boxed-caches)
Expand All @@ -424,12 +425,12 @@
[binding-forms-opened? (if (caching-enabled?) (box #f) #f)])
(cond
[(caching-enabled?)
(define candidate (hash-ref cache input not-in-cache))
(define candidate (dict-ref cache input not-in-cache))
(cond
[(equal? candidate not-in-cache)
[(eq? candidate not-in-cache)
(define computed-ans (form-proc recur input derivation-init pair-of-boxed-caches))
(unless (unbox (binding-forms-opened?))
(hash-set! cache input computed-ans))
(dict-set! cache input computed-ans))
computed-ans]
[else
candidate])]
Expand Down Expand Up @@ -467,8 +468,10 @@
outputs)
(form-proc/cache form-proc/cache input derivation-init pair-of-boxed-caches)))

(define without-exact-duplicates-vec (apply vector (remove-duplicates dwoos)))
(define ht (make-α-hash (compiled-lang-binding-table ct-lang) match-pattern))
(define btable (compiled-lang-binding-table ct-lang))
(define without-exact-duplicates-vec
(apply vector (remove-duplicates dwoos (curry α-equal? btable match-pattern))))
(define ht (make-α-hash btable match-pattern))
(for ([d (in-vector without-exact-duplicates-vec)]
[i (in-naturals)])
(define t (derivation-with-output-only-output d))
Expand Down Expand Up @@ -783,7 +786,8 @@
(define jf-lws (compiled-judgment-form-lws #,clauses #,judgment-form-name #,stx))
(define judgment-runtime-gen-clauses (mk-judgment-gen-clauses #,lang (λ () (judgment-runtime-gen-clauses))))
(define jf-term-proc (make-jf-term-proc #,judgment-form-name #,syn-err-name #,lang #,nts #,mode-stx))
(define jf-cache (cons (box (make-hash)) (box (make-hash))))
(define jf-cache (cons (box (make-α-hash (compiled-lang-binding-table #,lang) match-pattern))
(box (make-α-hash (compiled-lang-binding-table #,lang) match-pattern))))
(define the-runtime-judgment-form
(runtime-judgment-form '#,judgment-form-name
judgment-form-runtime-proc
Expand Down
29 changes: 17 additions & 12 deletions redex-lib/redex/private/reduction-semantics.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,13 +12,15 @@
"lang-struct.rkt"
"enum.rkt"
(only-in "binding-forms.rkt"
α-equal? safe-subst binding-forms-opened?)
α-equal? α-equal-hash-code safe-subst binding-forms-opened?
make-α-hash make-immutable-α-hash)
(only-in "binding-forms-definitions.rkt"
shadow nothing bf-table-entry-pat bf-table-entry-bspec)
racket/trace
racket/contract
racket/list
racket/set
racket/dict
racket/pretty
rackunit/log
(rename-in racket/match (match match:)))
Expand Down Expand Up @@ -2558,9 +2560,12 @@
#:all? [return-all? #f]
#:cache-all? [cache-all? (or return-all? (current-cache-all?))]
#:stop-when [stop-when (λ (x) #f)])
(define visited (and (or cache-all? return-all?) (make-hash)))
(define lang (reduction-relation-lang reductions))
(define binding-table (compiled-lang-binding-table lang))
(define (term-equal? x y) (α-equal? binding-table match-pattern x y))
(define visited (and (or cache-all? return-all?) (make-α-hash binding-table match-pattern)))
(let/ec return
(define answers (if return-all? #f (make-hash)))
(define answers (if return-all? #f (make-α-hash binding-table match-pattern)))
(define cycle? #f)
(define cutoff? #f)
(let loop ([term start]
Expand All @@ -2570,39 +2575,39 @@
;; in commit
;; 152084d5ce6ef49df3ec25c18e40069950146041
;; suggest that a hash works better than a trie.
[path (make-immutable-hash '())]
[path (make-immutable-α-hash binding-table match-pattern)]
[more-steps steps])
(if (and goal? (goal? term))
(return (search-success))
(cond
[(hash-ref path term #f)
[(dict-ref path term #f)
(set! cycle? #t)]
[else
(visit term)
(cond
[(stop-when term)
(unless goal?
(when answers
(hash-set! answers term #t)))]
(dict-set! answers term #t)))]
[else
(define nexts (apply-reduction-relation reductions term))
(cond
[(null? nexts)
(unless goal?
(when answers
(hash-set! answers term #t)))]
(dict-set! answers term #t)))]
[else (if (zero? more-steps)
(set! cutoff? #t)
(for ([next (in-list (remove-duplicates nexts))])
(for ([next (in-list (remove-duplicates nexts term-equal?))])
(when (or (not visited)
(not (hash-ref visited next #f)))
(when visited (hash-set! visited next #t))
(not (dict-ref visited next #f)))
(when visited (dict-set! visited next #t))
(loop next
(hash-set path term #t)
(dict-set path term #t)
(sub1 more-steps)))))])])])))
(if goal?
(search-failure cutoff?)
(values (sort (hash-map (or answers visited) (λ (x y) x))
(values (sort (dict-map (or answers visited) (λ (x y) x))
string<?
#:key (λ (x) (format "~s" x)))
cycle?))))
Expand Down