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 apply-reduction-relation* to be sensitive to alpha-equivalence #102

Closed
wants to merge 1 commit into from
Closed

Update apply-reduction-relation* to be sensitive to alpha-equivalence #102

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As the make-*-custom-hash interface is deprecated, perhaps this is a good time to redefine these using define-custom-hash-types.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I missed that these were deprecated.

The define-custom-hash-types interface is a bit awkward for this use case. The functions for computing equality and hashing need to close over the language binding table and match pattern, which aren't provided until we actually make a hash. So the result would look like

(define (make-α-hash language-bf-table match-pattern)
  (define-custom-hash-types this-lang-α-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)))
  (make-mutable-this-lang-α-hash))

It's a bit awkward, but maybe still better than using a deprecated version?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Except it will be worse, since define-custom-hash-types defines 7 names. You need to abstract all 7 definitions over the bf-table and match-pattern.. it's a bit gross.
Makes me want a macro that is like splicing-let, but instead of splicing in definitions, it .. splices in additional arguments? Essentially, allows eta expanding a bunch of definitions with respect to a set of arguments ..?

(splicing-lambda (x y)
  (define-values (f g h) (values (lambda (z) x) (lambda (z) y) (lambda (z) z))))
(check-equal? (f 1 2 3) 1)
(check-equal? (g 1 2 3) 2)
(check-equal? (h 1 2 3) 3)

(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
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