Fix patch-feedback calculation mistake, to match fixes in redex and coq
This commit is contained in:
parent
0d38e11ee8
commit
dfb0eae02c
|
@ -61,8 +61,10 @@
|
|||
(for/list [(pid affected-pids)]
|
||||
(cond [(equal? pid label)
|
||||
(define feedback
|
||||
(patch (biased-intersection new-routing-table (patch-added delta))
|
||||
(biased-intersection old-routing-table (patch-removed delta))))
|
||||
(patch-union
|
||||
(patch (biased-intersection new-routing-table (patch-added delta))
|
||||
(biased-intersection old-routing-table (patch-removed delta)))
|
||||
(view-patch delta-aggregate (mux-interests-of m pid))))
|
||||
(cons label feedback)]
|
||||
[else
|
||||
(cons pid (view-patch delta-aggregate (mux-interests-of m pid)))]))
|
||||
|
|
|
@ -28,6 +28,7 @@
|
|||
compute-patch
|
||||
biased-intersection
|
||||
view-patch
|
||||
patch-union
|
||||
patch-project
|
||||
patch-project/set
|
||||
patch-project/set/single
|
||||
|
@ -205,6 +206,10 @@
|
|||
(patch (biased-intersection (patch-added p) interests)
|
||||
(biased-intersection (patch-removed p) interests)))
|
||||
|
||||
(define (patch-union p1 p2)
|
||||
(patch (matcher-union (patch-added p1) (patch-added p2))
|
||||
(matcher-union (patch-removed p1) (patch-removed p2))))
|
||||
|
||||
(define (patch-project p spec)
|
||||
(match-define (patch in out) p)
|
||||
(patch (matcher-project in spec) (matcher-project out spec)))
|
||||
|
|
Loading…
Reference in New Issue