Partial repair for a deep problem with visibility-restriction.
This change makes `during` work "atomically" across a communications delay, by ensuring that a retracted assertion matching the `during`'s pattern triggers the "stop on" clause in the expansion of the `during`. Some discussion of the change exists in the Journal and in my notebook.
This commit is contained in:
parent
ff25f8b377
commit
5923bdd3ce
|
@ -138,7 +138,7 @@
|
||||||
(hash-for-each (skeleton-matched-constant-cache sc)
|
(hash-for-each (skeleton-matched-constant-cache sc)
|
||||||
(lambda (a _)
|
(lambda (a _)
|
||||||
(unpack-scoped-assertion [restriction-path term] a)
|
(unpack-scoped-assertion [restriction-path term] a)
|
||||||
(when (or (not restriction-path) (equal? restriction-path vs))
|
(when (unrestricted? vs restriction-path)
|
||||||
(bag-change! cache (apply-projection term vs) 1))))
|
(bag-change! cache (apply-projection term vs) 1))))
|
||||||
(skeleton-accumulator cache (make-hasheq)))
|
(skeleton-accumulator cache (make-hasheq)))
|
||||||
(define acc (hash-ref! (skeleton-matched-constant-table sc) vs make-accumulator))
|
(define acc (hash-ref! (skeleton-matched-constant-table sc) vs make-accumulator))
|
||||||
|
@ -184,6 +184,34 @@
|
||||||
[(visibility-restriction p t) (values p t)]
|
[(visibility-restriction p t) (values p t)]
|
||||||
[other (values #f other)])))
|
[other (values #f other)])))
|
||||||
|
|
||||||
|
(define (path-cmp a b)
|
||||||
|
(match* (a b)
|
||||||
|
[('() '()) '=]
|
||||||
|
[('() _) '<]
|
||||||
|
[(_ '()) '>]
|
||||||
|
[((cons av a) (cons bv b))
|
||||||
|
(cond [(< av bv) '<]
|
||||||
|
[(> av bv) '>]
|
||||||
|
[else (path-cmp a b)])]))
|
||||||
|
|
||||||
|
(define (unrestricted? capture-paths restriction-paths)
|
||||||
|
;; We are "unrestricted" if Set(capture-paths) ⊆ Set(restriction-paths). Since both variables
|
||||||
|
;; really hold lists, we operate with awareness of the order the lists are built here. We
|
||||||
|
;; know that the lists are built in fringe order; that is, they are sorted wrt `path-cmp`.
|
||||||
|
(or (not restriction-paths)
|
||||||
|
(let outer ((cs capture-paths) (rs restriction-paths))
|
||||||
|
(match cs
|
||||||
|
['() #t]
|
||||||
|
[(cons c cs)
|
||||||
|
(let inner ((rs rs))
|
||||||
|
(match rs
|
||||||
|
['() #f] ;; `c` does not exist in `restriction-paths` ∴ restricted.
|
||||||
|
[(cons r rs)
|
||||||
|
(match (path-cmp c r)
|
||||||
|
['< #f] ;; `c` < `r` ==> `c` not in `restriction-paths` ∴ restricted.
|
||||||
|
['= (outer cs rs)]
|
||||||
|
['> (inner rs)])]))]))))
|
||||||
|
|
||||||
(define (extend-skeleton! sk desc)
|
(define (extend-skeleton! sk desc)
|
||||||
(define (walk-node! rev-path sk pop-count index desc)
|
(define (walk-node! rev-path sk pop-count index desc)
|
||||||
(match desc
|
(match desc
|
||||||
|
@ -251,10 +279,9 @@
|
||||||
;; restriction-path
|
;; restriction-path
|
||||||
;; variable-proj
|
;; variable-proj
|
||||||
;; term0))
|
;; term0))
|
||||||
(when (or (not restriction-path)
|
(when (unrestricted? variable-proj restriction-path)
|
||||||
(equal? restriction-path variable-proj))
|
(define vars (apply-projection term0-term variable-proj))
|
||||||
(define variables (apply-projection term0-term variable-proj))
|
(modify-skacc! acc vars term0)))))))
|
||||||
(modify-skacc! acc variables term0)))))))
|
|
||||||
|
|
||||||
(for [(edge (in-list edges))]
|
(for [(edge (in-list edges))]
|
||||||
(match-define (cons (skeleton-selector pop-count index) table) edge)
|
(match-define (cons (skeleton-selector pop-count index) table) edge)
|
||||||
|
@ -428,4 +455,23 @@
|
||||||
;; sk
|
;; sk
|
||||||
|
|
||||||
(remove-interest! sk i1)
|
(remove-interest! sk i1)
|
||||||
|
|
||||||
|
(check-eq? (path-cmp '() '()) '=)
|
||||||
|
(check-eq? (path-cmp '(1 1) '(1 1)) '=)
|
||||||
|
(check-eq? (path-cmp '(2 2) '(2 2)) '=)
|
||||||
|
(check-eq? (path-cmp '(2 1) '(1 1)) '>)
|
||||||
|
(check-eq? (path-cmp '(1 1) '(2 1)) '<)
|
||||||
|
(check-eq? (path-cmp '(2 1) '(1 2)) '>)
|
||||||
|
(check-eq? (path-cmp '(1 2) '(2 1)) '<)
|
||||||
|
(check-eq? (path-cmp '(2) '(1 1)) '>)
|
||||||
|
(check-eq? (path-cmp '(1) '(2 1)) '<)
|
||||||
|
(check-eq? (path-cmp '(2) '(1 2)) '>)
|
||||||
|
(check-eq? (path-cmp '(1) '(2 1)) '<)
|
||||||
|
(check-eq? (path-cmp '(2 1) '(1)) '>)
|
||||||
|
(check-eq? (path-cmp '(1 1) '(2)) '<)
|
||||||
|
(check-eq? (path-cmp '(2 1) '(1)) '>)
|
||||||
|
(check-eq? (path-cmp '(1 2) '(2)) '<)
|
||||||
|
(check-eq? (path-cmp '(1 2) '(1 2)) '=)
|
||||||
|
(check-eq? (path-cmp '(1) '(1 2)) '<)
|
||||||
|
(check-eq? (path-cmp '(1 2) '(1)) '>)
|
||||||
)
|
)
|
||||||
|
|
Loading…
Reference in New Issue