Skip to content

Commit 1e7ff97

Browse files
committed
Update apply-reduction-relation* to be sensitive to alpha-equivalence
Also add an immutable alpha hash constructor and update hashes in the gui to use the form provided by binding-forms.rkt Fixes racket#96
1 parent e5676a1 commit 1e7ff97

File tree

4 files changed

+26
-20
lines changed

4 files changed

+26
-20
lines changed

redex-gui-lib/redex/private/stepper.rkt

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -66,10 +66,8 @@ todo:
6666
;; all-nodes-ht : hash[sexp -o> (is-a/c node%)]
6767

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

7472
(define root (new node%
7573
[pp pp]

redex-gui-lib/redex/private/traces.rkt

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -353,9 +353,7 @@
353353
[(IO-judgment-form? reductions) (runtime-judgment-form-lang reductions)]))
354354

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

360358
;; call-on-eventspace-main-thread : (-> any) -> any
361359
;; =reduction thread=

redex-lib/redex/private/binding-forms.rkt

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ to traverse the whole value at once, rather than one binding form at a time.
8989
;; == public interface ==
9090

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

9494
;; == parameters ==
9595

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

140+
(define (make-immutable-α-hash language-bf-table match-pattern)
141+
(make-immutable-custom-hash (λ (x y) (α-equal? language-bf-table match-pattern x y))
142+
(λ (x) (α-equal-hash-code language-bf-table match-pattern x))
143+
(λ (x) (α-equal-secondary-hash-code language-bf-table match-pattern x))))
144+
140145
;; α-equal? : (listof (list compiled-pattern bspec))
141146
;; (compiled-pattern redex-val -> (union #f mtch)) redex-val -> boolean
142147
(define (α-equal? language-bf-table match-pattern redex-val-lhs redex-val-rhs)

redex-lib/redex/private/reduction-semantics.rkt

Lines changed: 17 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,13 +12,15 @@
1212
"lang-struct.rkt"
1313
"enum.rkt"
1414
(only-in "binding-forms.rkt"
15-
α-equal? safe-subst binding-forms-opened?)
15+
α-equal? α-equal-hash-code safe-subst binding-forms-opened?
16+
make-α-hash make-immutable-α-hash)
1617
(only-in "binding-forms-definitions.rkt"
1718
shadow nothing bf-table-entry-pat bf-table-entry-bspec)
1819
racket/trace
1920
racket/contract
2021
racket/list
2122
racket/set
23+
racket/dict
2224
racket/pretty
2325
rackunit/log
2426
(rename-in racket/match (match match:)))
@@ -2558,9 +2560,12 @@
25582560
#:all? [return-all? #f]
25592561
#:cache-all? [cache-all? (or return-all? (current-cache-all?))]
25602562
#:stop-when [stop-when (λ (x) #f)])
2561-
(define visited (and (or cache-all? return-all?) (make-hash)))
2563+
(define lang (reduction-relation-lang reductions))
2564+
(define binding-table (compiled-lang-binding-table lang))
2565+
(define (term-equal? x y) (α-equal? binding-table match-pattern x y))
2566+
(define visited (and (or cache-all? return-all?) (make-α-hash binding-table match-pattern)))
25622567
(let/ec return
2563-
(define answers (if return-all? #f (make-hash)))
2568+
(define answers (if return-all? #f (make-α-hash binding-table match-pattern)))
25642569
(define cycle? #f)
25652570
(define cutoff? #f)
25662571
(let loop ([term start]
@@ -2570,39 +2575,39 @@
25702575
;; in commit
25712576
;; 152084d5ce6ef49df3ec25c18e40069950146041
25722577
;; suggest that a hash works better than a trie.
2573-
[path (make-immutable-hash '())]
2578+
[path (make-immutable-α-hash binding-table match-pattern)]
25742579
[more-steps steps])
25752580
(if (and goal? (goal? term))
25762581
(return (search-success))
25772582
(cond
2578-
[(hash-ref path term #f)
2583+
[(dict-ref path term #f)
25792584
(set! cycle? #t)]
25802585
[else
25812586
(visit term)
25822587
(cond
25832588
[(stop-when term)
25842589
(unless goal?
25852590
(when answers
2586-
(hash-set! answers term #t)))]
2591+
(dict-set! answers term #t)))]
25872592
[else
25882593
(define nexts (apply-reduction-relation reductions term))
25892594
(cond
25902595
[(null? nexts)
25912596
(unless goal?
25922597
(when answers
2593-
(hash-set! answers term #t)))]
2598+
(dict-set! answers term #t)))]
25942599
[else (if (zero? more-steps)
25952600
(set! cutoff? #t)
2596-
(for ([next (in-list (remove-duplicates nexts))])
2601+
(for ([next (in-list (remove-duplicates nexts term-equal?))])
25972602
(when (or (not visited)
2598-
(not (hash-ref visited next #f)))
2599-
(when visited (hash-set! visited next #t))
2603+
(not (dict-ref visited next #f)))
2604+
(when visited (dict-set! visited next #t))
26002605
(loop next
2601-
(hash-set path term #t)
2606+
(dict-set path term #t)
26022607
(sub1 more-steps)))))])])])))
26032608
(if goal?
26042609
(search-failure cutoff?)
2605-
(values (sort (hash-map (or answers visited) (λ (x y) x))
2610+
(values (sort (dict-map (or answers visited) (λ (x y) x))
26062611
string<?
26072612
#:key (λ (x) (format "~s" x)))
26082613
cycle?))))

0 commit comments

Comments
 (0)