diff --git a/imperative/skeleton.rkt b/imperative/skeleton.rkt index 9a1a57d..c50213b 100644 --- a/imperative/skeleton.rkt +++ b/imperative/skeleton.rkt @@ -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)) '>) )