0. #lang racket
1. (define (a/equal? d₀ d₁ store-spaces μ)
2.   (define/match (egal-equal? a₀ a₁)
3.     [((Address-Egal space a) (Address-Egal space a))
4.      (match (hash-ref μ a₀ 'ω)
5.        [1 #t]
6.        ['ω 'b.⊤]
7.        [0 (error 'a/match "Live address with count 0: ~a (Counts ~a) (Store ~a)" a₀ μ store-spaces)])]
8.     [(_ _) #f])
9.  
10.   (define (ffun-equal? f₀ f₁)
11.     (if abs?
12.         (b∧ (ffun-⊑? f₀ f₁)
13.             (ffun-⊑? f₁ f₀))
14.         (concrete-ffun-equal? f₀ f₁)))
15.  
16.   ;; Slow path: linearly look for a key "equal" to k with "equal" values.
17.   (define (slow-equal k v f)
18.     (for/b∨ ([(k₁ v₁) (in-dict f)])
19.             (b∧ (a/equal? k k₁)
20.                 (a/equal? v v₁))))
21.  
22.   (define (ffun-⊑? dom f₀ f₁)
23.     (for/b∧ ([(k v) (in-dict f₀)])
24.             (match (dict-ref f₁ k -unmapped)
25.               [(== -unmapped eq?) (slow-equal k v f₁)]
26.               [v₁ ;; fast path: check the structurally equal key
27.                (b∨ (a/equal? v₀ v₁)
28.                    (slow-equal k v f₁))])))
29.  
30.   (define (concrete-ffun-equal? m₀ m₁)
31.     (and (= (dict-count m₀) (dict-count m₁))
32.          (for/b∧ ([(k₀ v₀) (in-dict m₀)])
33.                  (match (dict-ref m₁ k₀ -unmapped)
34.                    ;; Concrete domains w/o structural equality are actually abstract.
35.                    ;; Note this is different from the concrete semantics.
36.                    [(== -unmapped eq?) #f]
37.                    ;; Note we don't use b∨ with the slow path
38.                    [v₁ (a/equal? v₀ v₁)]))))
39.  
40.   (define (discrete-ffun-equal? m₀ m₁)
41.     (and (= (dict-count m₀) (dict-count m₁))
42.          (for/b∧ ([(k₀ v₀) (in-dict m₀)])
43.                  (match (dict-ref m₁ k₀ -unmapped)
44.                    [(== -unmapped eq?) #f]
45.                    [v₁ (b∧
46.                         ;; Discrete maps get structural equality on keys, but can only be
47.                         ;; truly equal if the key has cardinality 1.
48.                         (if (∣γ∣>1 k₀ μ) 'b.⊤ #t)
49.                         (a/equal? v₀ v₁))]))))
50.  
51.   (define (equal-step d₀ d₁)
52.     (match* (d₀ d₁)
53.       [((variant v ds₀) (variant v ds₁))
54.        (for/b∧ ([d₀ (in-vector ds₀)]
55.                 [d₁ (in-vector ds₁)])
56.                (a/equal? d₀ d₁))]
57.  
58.       ;; Addresses are the same if they have cardinality 1. Distinct addresses don't overlap.
59.       [((? Address-Egal?) (? Address-Egal?))
60.        (egal-equal? d₀ d₁)]
61.  
62.       [((? Address-Structural? a₀) (? Address-Structural? a₁))
63.        (if (eq? (egal-equal? a₀ a₁) #t)
64.            #t
65.            ;; INVARIANT: not possible to be -unmapped since there must be
66.            ;; at least one value mapped in a store's address.
67.            (for*/bδ ([d₀ (in-set (store-ref store-spaces a₀))]
68.                      [d₁ (in-set (store-ref store-spaces a₁))])
69.                     (a/equal? d₀ d₁)))]
70.  
71.       [((? dict? m₀) (? dict? m₁)) (concrete-ffun-equal? m₀ m₁)]
72.  
73.       ;; If at least one map has qualification, we can check the other with the expectation of the same.
74.       ;; We log the incident for future debugging, since it seems like we shouldn't get this far.
75.       [((? dict? m₀) (abstract-ffun m₁))
76.        (log-info (format "Qualified/unqualified dictionary equality check ~a ~a" d₀ d₁))
77.        (ffun-equal? m₀ m₁)]
78.       [((abstract-ffun m₀) (? dict? m₁))
79.        (log-info (format "Qualified/unqualified dictionary equality check ~a ~a" d₀ d₁))
80.        (ffun-equal? m₀ m₁)]
81.       [((abstract-ffun m₀) (abstract-ffun m₁)) (ffun-equal? m₀ m₁)]
82.       ;; Discrete cases
83.       [((discrete-ffun m₀) (? dict? m₁))
84.        (log-info (format "Qualified/unqualified (discrete) dictionary equality check ~a ~a" d₀ d₁))
85.        (discrete-ffun-equal? m₀ m₁)]
86.       [((? dict? m₀) (discrete-ffun m₁))
87.        (log-info (format "Qualified/unqualified (discrete) dictionary equality check ~a ~a" d₀ d₁))
88.        (discrete-ffun-equal? m₀ m₁)]
89.       [((discrete-ffun m₀) (discrete-ffun m₁))
90.        (discrete-ffun-equal? m₀ m₁)]
91.  
92.       ;; OPT-OP: This has no information on discrete abstractions, thus n²logn instead of sometimes nlogn
93.       [((? set? s₀) (? set? s₁))
94.        (define (⊆? s₀ s₁)
95.          (for/b∧ ([v (in-set s₀)])
96.                  (for/b∨ ([v* (in-set s₁)])
97.                          (a/equal? v v*))))
98.        (b∧ (⊆? s₀ s₁) (⊆? s₁ s₀))]
99.  
100.       [(atom atom) #t]
101.  
102.       [((external ex v₀) (external ex v₁))
103.        (match-define (External-Space _ card precision special-equality) ex)
104.        (if special-equality
105.            (special-equality v₀ v₁ μ #;a/equal?)
106.            (match precision
107.              ['concrete (equal? v₀ v₁)]
108.              ['discrete-abstraction (b∧ (equal? v₀ v₁) (implies (eq? (card v₀ μ)) 'b.⊤))]
109.              ['abstract (error 'a/match "Cannot have non-discrete abstraction of external values without a custom equality relation ~a" d₀)]))]
110.       [(_ _) #f]))
111.  
112.   ;; Circular addresses are possible
113.   ;; OPT-OP?: Racket impl of equal? uses union-find instead of Map[_,Set[_]].
114.   ;;          Is that applicable here?
115.   (define seen (make-hasheq))
116.   (define (a/equal? d₀ d₁)
117.     (define checked-against (hash-ref! seen d₀ mutable-seteq))
118.     ;; already checked ⇒ assume equal
119.     ;; XXX: should this be #t or 'b.⊤?
120.     (or (set-member? checked-against d₁)
121.         (begin (set-add! checked-against d₁)
122.                (equal-step d₀ d₁))))
123.  
124.   (a/equal? d₀ d₁))

=>

eval:2:0: match: syntax error in pattern

in: (Address-Egal space a)