syndicate-lang
/
syndicate-rkt
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

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:
Tony Garnock-Jones 2019-06-18 17:56:09 +01:00
parent ff25f8b377
commit 5923bdd3ce
1 changed files with 51 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
syndicate/skeleton.rkt
View File

@ -138,7 +138,7 @@
(hash-for-each (skeleton-matched-constant-cache sc)
(lambda (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))))
(skeleton-accumulator cache (make-hasheq)))
(define acc (hash-ref! (skeleton-matched-constant-table sc) vs make-accumulator))
@ -184,6 +184,34 @@
[(visibility-restriction p t) (values p t)]
[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 (walk-node! rev-path sk pop-count index desc)
(match desc
@ -251,10 +279,9 @@
;; restriction-path
;; variable-proj
;; term0))
(when (or (not restriction-path)
(equal? restriction-path variable-proj))
(define variables (apply-projection term0-term variable-proj))
(modify-skacc! acc variables term0)))))))
(when (unrestricted? variable-proj restriction-path)
(define vars (apply-projection term0-term variable-proj))
(modify-skacc! acc vars term0)))))))
(for [(edge (in-list edges))]
(match-define (cons (skeleton-selector pop-count index) table) edge)
@ -428,4 +455,23 @@
;; sk
(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)) '>)
)