Add visibility-restriction, making the test pass

This commit is contained in:
Tony Garnock-Jones 2019-03-25 16:32:09 +00:00
parent 9e923e1c63
commit 759bbdf1c3
5 changed files with 43 additions and 35 deletions

View File

@ -35,12 +35,12 @@
(on (message (broker-packet address (Ping)))
(w (Pong)))
(during (observe (from-broker address $spec))
(during (observe ($ pat (from-broker address $spec)))
(define ep (next-ep))
(on-start (w (Assert ep (observe spec))))
(on-stop (w (Clear ep)))
(on (message (broker-packet address (Add ep $vs)))
(react (assert (instantiate-term->value (from-broker address spec) vs))
(react (assert (instantiate-term->value pat vs))
(stop-when (message (broker-packet address (Del ep vs))))))
(on (message (broker-packet address (Msg ep $vs)))
(send! (instantiate-term->value (from-broker address spec) vs)))))
(send! (instantiate-term->value pat vs)))))

View File

@ -81,7 +81,11 @@
x
(lambda (op . captured-values)
(when (eq? op '+)
(define term (instantiate-term->value pattern captured-values))
(define term
(instantiate-term->value pattern captured-values
#:visibility-restriction-proj #f))
;; TODO: flawed?? Needs visibility-restriction, or some other way
;; of ignoring the opaque placeholders!
(schedule-script!
(current-actor)
(lambda ()

View File

@ -77,34 +77,35 @@
(define outer-capture-proj (term->capture-proj x))
(define inner-capture-proj (map (lambda (p) (cons 0 p)) outer-capture-proj))
;; ^ inner-capture-proj accounts for the extra (inbound ...) layer around assertions
(define i (term->skeleton-interest
x
#:capture-projection outer-capture-proj
(lambda (op . captured-values)
(define term (inbound (instantiate-term->value x captured-values)))
(define assertion (visibility-restriction inner-capture-proj term))
;; (log-info "~a => ~a ~a ~v"
;; outer-facet
;; inner-facet
;; op
;; assertion)
(match op
['+ (apply-patch! inner-ds inner-actor (bag assertion +1))]
['- (apply-patch! inner-ds inner-actor (bag assertion -1))]
['! (send-assertion! (dataspace-routing-table inner-ds) assertion)])
(schedule-inner!))
#:cleanup
(lambda (cache)
(apply-patch!
inner-ds
inner-actor
(for/bag/count [(captured-values (in-bag cache))]
;; (log-info "~a (cleanup) ~v" inner-actor term)
(values (visibility-restriction
inner-capture-proj
(inbound (instantiate-term->value x captured-values)))
-1)))
(schedule-inner!))))
(define i
(term->skeleton-interest
x
#:capture-projection outer-capture-proj
(lambda (op . captured-values)
(define assertion
(instantiate-term->value (inbound x) captured-values
#:visibility-restriction-proj inner-capture-proj))
;; (log-info "~a => ~a ~a ~v"
;; outer-facet
;; inner-facet
;; op
;; assertion)
(match op
['+ (apply-patch! inner-ds inner-actor (bag assertion +1))]
['- (apply-patch! inner-ds inner-actor (bag assertion -1))]
['! (send-assertion! (dataspace-routing-table inner-ds) assertion)])
(schedule-inner!))
#:cleanup
(lambda (cache)
(apply-patch!
inner-ds
inner-actor
(for/bag/count [(captured-values (in-bag cache))]
;; (log-info "~a (cleanup) ~v" inner-actor term)
(values (instantiate-term->value (inbound x) captured-values
#:visibility-restriction-proj inner-capture-proj)
-1)))
(schedule-inner!))))
(add-endpoint-if-live! outer-facet
inbound-endpoints
x

View File

@ -24,7 +24,7 @@
;; A VisibilityRestriction describes ... TODO
;; (visibility-restriction SkProj Assertion)
(struct visibility-restriction (path term) #:transparent)
(struct visibility-restriction (proj term) #:transparent)
;; A ScopedAssertion is a VisibilityRestriction or an Assertion.
;; (Corollary: Instances of `visibility-restriction` can never be assertions.)

View File

@ -93,7 +93,8 @@
;; otherwise-potentially-matching constant positions in instantiated
;; terms
(define (instantiate-term->value t actuals)
(define (instantiate-term->value t actuals
#:visibility-restriction-proj [vrproj (term->capture-proj t)])
(define (pop-actual!)
(define v (car actuals))
(set! actuals (cdr actuals))
@ -129,7 +130,9 @@
(for/vector [(tt t)] (walk tt))]
[other other]))
(walk t))
(if vrproj
(visibility-restriction vrproj (walk t))
(walk t)))
;; Omits captures.
(define (term-intersect t1 t2 ks kf)