Merge pull request #468 from objectionary/488-add-dot-rho

Add `R_DOT_ρ`

eo-phi-normalizer/test/eo/phi/dataization.yaml

@@ -79,7 +79,7 @@ tests:
       {⟦ x ↦ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧.c ⟧.b ⟧.a , λ ⤍ Package ⟧}
     output:
       object: |
-        ⟦ x ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ, ρ ↦ ⟦ ρ ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ ⟧, c ↦ ξ.ρ ⟧ ⟧, λ ⤍ Package ⟧
+        ⟦ x ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ, ρ ↦ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ξ.ρ ⟧.ρ ⟧ ⟧ ⟧, λ ⤍ Package ⟧
 
   - name: "usage of Φ with a loop"
     dependencies: []

eo-phi-normalizer/test/eo/phi/rules/yegor.yaml

@@ -65,13 +65,17 @@ rules:
       - apply_in_abstract_subformations: false
       - nf_inside_formation: '!b'
       - nf: '⟦ !B ⟧'
+      - not_equal: ['!τ', 'ρ']
     tests:
       - name: Should match
         input: ⟦ hello ↦ ⟦⟧ ⟧.hello
         output: ['⟦ ρ ↦ ⟦ hello ↦ ⟦⟧ ⟧ ⟧']
       - name: Shouldn't match
         input: ⟦ ⟧.hello
         output: []
+      - name: Shouldn't match
+        input: ⟦ ρ ↦ ⟦⟧ ⟧.ρ
+        output: []
       - name: Should apply in subformations
         input: ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ⟦⟧ ⟧ ⟧.b ⟧
         output: ['⟦ a ↦ ⟦ c ↦ ⟦⟧, ρ ↦ ⟦ b ↦ ⟦ c ↦ ⟦⟧ ⟧ ⟧ ⟧ ⟧']
@@ -93,6 +97,19 @@ rules:
   #       input: ⟦ ⟧.hello
   #       output: []
 
+  - name: R_DOT_ρ
+    description: 'Accessing ρ-binding'
+    pattern: |
+      ⟦ ρ ↦ !b, !B ⟧.ρ
+    result: |
+      !b
+    when:
+      - nf: '⟦ !B ⟧'
+    tests:
+      - name: Should match
+        input: ⟦ ρ ↦ ⟦ ⟧ ⟧.ρ
+        output: ['⟦ ⟧']
+
   - name: R_COPY2
     description: 'Application of α-binding'
     # Warning: this is not correct for the chain variant because it only matches the first two bindings