eo-phi-normalizer 2.2.0 → 2.2.1
raw patch · 5 files changed
+631/−3 lines, 5 files
Files
- CHANGELOG.md +8/−2
- eo-phi-normalizer.cabal +4/−1
- test/eo/phi/rules/new.yaml +244/−0
- test/eo/phi/rules/streams.yaml +87/−0
- test/eo/phi/rules/yegor.yaml +288/−0
CHANGELOG.md view
@@ -6,6 +6,12 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v2.2.1 - 2024-11-27++### Changes and fixes++- Fix rules file not included into the released Haskell package ([#568](https://github.com/objectionary/eo-phi-normalizer/pull/568))+ ## v2.2.0 - 2024-11-26 ### Breaking changes@@ -14,11 +20,11 @@ ### Changes and fixes -- Pretty printing doesn't put enough eols ([#550](https://github.com/objectionary/eo-phi-normalizer/pull/550))+- Fix pretty-printing ([#550](https://github.com/objectionary/eo-phi-normalizer/pull/550)) ### Documentation and maintenance -- Menu is broken on the site ([#551](https://github.com/objectionary/eo-phi-normalizer/pull/551))+- Fix menu on the site ([#551](https://github.com/objectionary/eo-phi-normalizer/pull/551)) ## v2.1.0 - 2024-11-22
eo-phi-normalizer.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: eo-phi-normalizer-version: 2.2.0+version: 2.2.1 synopsis: Command line normalizer of 𝜑-calculus expressions. description: Please see the README on GitHub at <https://github.com/objectionary/eo-phi-normalizer#readme> homepage: https://github.com/objectionary/eo-phi-normalizer#readme@@ -189,6 +189,9 @@ data/0.41.2/org/eolang/txt/sscanf.phi data/0.41.2/org/eolang/txt/text.phi data/0.41.2/org/eolang/while.phi+ test/eo/phi/rules/new.yaml+ test/eo/phi/rules/streams.yaml+ test/eo/phi/rules/yegor.yaml source-repository head type: git
+ test/eo/phi/rules/new.yaml view
@@ -0,0 +1,244 @@+# The MIT License (MIT)++# Copyright (c) 2016-2024 Objectionary.com++# Permission is hereby granted, free of charge, to any person obtaining a copy+# of this software and associated documentation files (the "Software"), to deal+# in the Software without restriction, including without limitation the rights+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+# copies of the Software, and to permit persons to whom the Software is+# furnished to do so, subject to the following conditions:++# The above copyright notice and this permission notice shall be included+# in all copies or substantial portions of the Software.++# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+# FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+# SOFTWARE.++title: "Rule set following Nov 2024 revision"+rules:++ - name: DOT+ description: 'Accessing an α-binding'+ pattern: |+ ⟦ !τ ↦ !b, !B ⟧.!τ+ result: |+ ⌈ !b , ⟦ !τ ↦ !b, !B ⟧ ⌉(ρ ↦ ⟦ !τ ↦ !b, !B ⟧)+ when:+ - nf: '!b'+ - nf: '⟦ !B ⟧' #TODO: change the condition, every object in !B should be in the nf+ tests:+ - name: 'Contextualization changes ξ'+ input: ⟦ a ↦ ξ ⟧.a+ output: ['⟦ a ↦ ξ ⟧ (ρ ↦ ⟦ a ↦ ξ ⟧)']+ - name: 'Contextualization applies recursively'+ input: ⟦ a ↦ ξ.b ⟧.a+ output: ['⟦ a ↦ ξ.b ⟧.b (ρ ↦ ⟦ a ↦ ξ.b ⟧)']+ - name: Phi Paper - Example E2+ input: '⟦ x ↦ ξ.t, t ↦ ∅ ⟧.x'+ output: ['⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)']+ - name: Phi Paper - Example E3 - first R_dot+ input: '⟦ x ↦ ⟦t ↦ ⟦ρ ↦ ⟦⟧⟧⟧.t ⟧.x'+ output: ['⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦t ↦ ⟦ρ ↦ ⟦⟧⟧⟧) ⟧.x']+ - name: Phi Paper - Example E3 - second R_dot+ input: '⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧.x'+ output: ['⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦x ↦ ⟦ρ ↦ ⟦⟧⟧⟧)']+ - name: Phi Paper - Example E4 - first R_dot+ input: '⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.y'+ # output: ['⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.x(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)']+ output: ['⟦ y ↦ ξ.x, x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧.x(ρ ↦ ⟦ y ↦ ξ.x, x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧)']+ - name: Phi Paper - Example E4 - second R_dot+ input: ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.x(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)+ output: ['⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)']++ - name: COPY+ description: 'Application of α-binding'+ pattern: |+ ⟦ !τ1 ↦ ⟦ !τ2 ↦ ∅, !B1 ⟧(!τ2 ↦ !b, !B2) * !t, !B3 ⟧+ result: |+ ⟦ !τ1 ↦ ⟦ !τ2 ↦ ⌈ !b , ⟦ !τ1 ↦ ⟦ !τ2 ↦ ∅, !B1 ⟧(!τ2 ↦ !b, !B2), !B3 ⟧ ⌉, !B1 ⟧(!B2) * !t, !B3 ⟧+ when:+ - nf: '!b'+ - nf: '⟦ !B1 ⟧'+ - nf: '⟦ !B3 ⟧'+ tests:+ - name: Should match+ input: ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧+ output: ['⟦ a ↦ ⟦ b ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧ ⟧ () ⟧']+ - name: 'Should match'+ input: ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ).a ⟧+ output: ['⟦ a ↦ ⟦ b ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧ ⟧ ().a ⟧']+ - name: Phi Paper - Example E1+ input: ⟦ k ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧(t ↦ ⟦ρ ↦ ⟦⟧⟧) ⟧+ # output: ['⟦ k ↦ ⟦ x ↦ ξ.t, t ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧() ⟧']+ output: ['⟦ k ↦ ⟦ t ↦ ⟦ρ ↦ ⟦⟧⟧, x ↦ ξ.t ⟧() ⟧']+ - name: Phi Paper - Example E4 - dispatch on y+ input: ⟦ k ↦ ⟦ x ↦ ∅, y ↦ ξ.x ⟧(x ↦ ⟦ρ ↦ ⟦⟧⟧).y ⟧+ output: ['⟦ k ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧().y ⟧']+ - name: Phi Paper - Example E4 - remove dispatch on y+ input: ⟦ k ↦ ⟦ x ↦ ∅, y ↦ ξ.x ⟧(x ↦ ⟦ρ ↦ ⟦⟧⟧) ⟧+ output: ['⟦ k ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧() ⟧']++ - name: RHO+ description: 'Application of a ρ-binding'+ pattern: |+ ⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧+ result: |+ ⟦ !τ ↦ ⟦ !B1, ρ ↦ ⌈ !b , ⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧ ⌉ ⟧(!B2), !B3 ⟧+ when:+ - nf: '!b'+ - absent_attrs:+ attrs: ['ρ']+ bindings: ['!B1']+ tests: []++ - name: phi+ description: 'Accessing a decorated object'+ pattern: |+ ⟦!B ⟧.!τ+ result: |+ ⟦!B ⟧.φ.!τ+ when:+ - nf: '⟦ !B ⟧'+ - present_attrs:+ attrs: ['φ']+ bindings: ['!B']+ - absent_attrs:+ attrs: ['!τ']+ bindings: ['!B']+ tests: []++ # there's no B2 in the result+ - name: STAY+ description: 'Application of a ρ-binding when ρ already exists'+ pattern: |+ ⟦ ρ ↦ !b1, !B1 ⟧ (ρ ↦ !b, !B2)+ result: |+ ⟦ ρ ↦ !b1, !B1 ⟧ (!B2)+ when: []+ tests:+ - name: Phi Paper - Example E3 - first R_stay+ input: ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧)(ρ ↦ ⟦ x ↦ ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧) ⟧)+ output: [⟦ ρ ↦ ⟦⟧ ⟧()(ρ ↦ ⟦ x ↦ ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧) ⟧)]+ - name: 'Should match'+ input: '⟦ ρ ↦ ⟦ c ↦ ∅ ⟧ ⟧ (ρ ↦ ⟦ ⟧, b ↦ ξ)'+ output: ['⟦ ρ ↦ ⟦ c ↦ ∅ ⟧ ⟧ (b ↦ ξ)']++ - name: OVER+ description: 'Invalid application (attribute already attached)'+ pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2)+ result: ⊥+ when:+ - not_equal: ['!τ', 'ρ']+ tests:+ - name: ''+ input: '⟦ t ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'+ output: ['⊥']++ - name: STOP+ description: 'Absent attribute access'+ pattern: |+ ⟦ !B ⟧.!τ+ result: |+ ⊥+ when:+ - absent_attrs:+ attrs: ['!τ', 'φ', 'λ']+ bindings: ['!B']+ - nf: '⟦ !B ⟧'+ tests:+ - name: 'Accessing nonexistent attribute'+ input: '⟦ ρ ↦ ⟦ ⟧ ⟧.x'+ output: ['⊥']++ # Named VOID instead of NULL because NULL is a keyword in yaml+ - name: VOID+ description: 'Void attribute access'+ pattern: |+ ⟦ !τ ↦ ∅, !B ⟧.!τ+ result: |+ ⊥+ when: []+ tests:+ - name: Phi Paper Example E2 second dispatch+ input: '⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)'+ output: ['⊥(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)']++ - name: DUP+ description: 'Empty application'+ pattern: |+ ⟦ !B ⟧()+ result: |+ ⟦ !B ⟧+ when: []+ tests:+ - name: Should match+ input: ⟦ a ↦ ⟦⟧ ⟧()+ output: ['⟦ a ↦ ⟦⟧ ⟧']+ - name: Should not match+ input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧)+ output: []+ - name: Should match in subformation+ input: ⟦ a ↦ ⟦ b ↦ ⟦⟧() ⟧ ⟧+ output: ['⟦ a ↦ ⟦ b ↦ ⟦⟧ ⟧ ⟧']+ - name: Should work with empty formation+ input: ⟦⟧()+ output: ['⟦⟧']++ - name: MISS+ description: 'Invalid application (absent attribute)'+ pattern: ⟦ !B1 ⟧(!τ ↦ !b, !B2)+ result: ⊥+ when:+ - absent_attrs:+ attrs: ['!τ']+ bindings: ['!B1']+ - not_equal: ['!τ', 'ρ']+ tests:+ - name: ''+ input: '⟦ t1 ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'+ output: ['⊥']+ - name: Should not match if attr is present+ input: ⟦ t ↦ ⟦⟧ ⟧(t ↦ ⟦ a ↦ ∅ ⟧)+ output: []+ - name: Should not match for rho+ input: ⟦ ⟧(ρ ↦ ⟦ ⟧)+ output: []+ - name: Should apply in subformations+ input: ⟦ a ↦ ⟦ b ↦ ⟦⟧(t ↦ ⟦⟧) ⟧ ⟧+ output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']++ - name: DD+ description: 'Accessing an attribute on bottom'+ pattern: |+ ⊥.!τ+ result: |+ ⊥+ when: []+ tests:+ - name: 'Dispatch on bottom is bottom'+ input: '⊥.a'+ output: ['⊥']+ - name: 'Dispatch on anything else is not touched'+ input: '⟦ ⟧.a'+ output: []++ - name: DC+ description: 'Application on bottom is bottom'+ pattern: |+ ⊥(!B)+ result: |+ ⊥+ when: []+ tests:+ - name: Should apply in subformations+ input: ⟦ a ↦ ⟦ b ↦ ⊥(t ↦ ⟦⟧, u ↦ ⟦⟧) ⟧ ⟧+ output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']+ - name: Phi Paper Example E2 last application+ input: '⊥(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)'+ output: ['⊥']
+ test/eo/phi/rules/streams.yaml view
@@ -0,0 +1,87 @@+# The MIT License (MIT)++# Copyright (c) 2016-2024 Objectionary.com++# Permission is hereby granted, free of charge, to any person obtaining a copy+# of this software and associated documentation files (the "Software"), to deal+# in the Software without restriction, including without limitation the rights+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+# copies of the Software, and to permit persons to whom the Software is+# furnished to do so, subject to the following conditions:++# The above copyright notice and this permission notice shall be included+# in all copies or substantial portions of the Software.++# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+# FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+# SOFTWARE.++title: "Rules for Java Streams"+rules:+ - name: "[java.util.Stream] map ↦ for-each"+ description: |+ Replacing Java Stream's map with a for-each loop.+ context:+ forall:+ - '!τ1'+ - '!b1'+ - '!b2'+ - '!t1'+ - '!B1'+ pattern: |+ ⟦+ !τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2) * !t1,+ !B1+ ⟧+ result: |+ ⟦+ !τ2 ↦ !b1,+ !τ3 ↦ Φ.opeo.map-for-each(+ α0 ↦ ξ.!τ2,+ α1 ↦ !b2+ ),+ !τ1 ↦ ξ.!τ3 * !t1,+ !B1+ ⟧+ fresh:+ - name: '!τ2'+ prefix: 'foreach_body'+ - name: '!τ3'+ prefix: 'java_util_Stream$map_result'+ when: []+ tests:+ - name: Simple map to for-each example works+ input: |+ ⟦+ list ↦ ∅,+ result ↦ ξ.list.java_util_Stream$filter(+ α0 ↦ ⟦+ el ↦ ∅,+ φ ↦ ξ.el.equals(+ α0 ↦ Φ.org.eolang.string(as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))+ ).not+ ⟧+ ).java_util_Stream$map(+ α0 ↦ ⟦+ el ↦ ∅,+ φ ↦ Φ.java_util_Integer.parseInt(+ α0 ↦ ξ.el+ )+ ⟧+ ).java_util_Stream$toList+ ⟧+ output:+ - |+ ⟦+ foreach_body$1 ↦ ξ.list.java_util_Stream$filter (α0 ↦ ⟦+ el ↦ ∅, φ ↦ ξ.el.equals (α0 ↦ Φ.org.eolang.string (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))).not+ ⟧),+ java_util_Stream$map_result$1 ↦ Φ.opeo.map-for-each (α0 ↦ ξ.foreach_body$1, α1 ↦ ⟦+ el ↦ ∅, φ ↦ Φ.java_util_Integer.parseInt (α0 ↦ ξ.el)+ ⟧),+ result ↦ ξ.java_util_Stream$map_result$1.java_util_Stream$toList, list ↦ ∅+ ⟧
+ test/eo/phi/rules/yegor.yaml view
@@ -0,0 +1,288 @@+# The MIT License (MIT)++# Copyright (c) 2016-2024 Objectionary.com++# Permission is hereby granted, free of charge, to any person obtaining a copy+# of this software and associated documentation files (the "Software"), to deal+# in the Software without restriction, including without limitation the rights+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+# copies of the Software, and to permit persons to whom the Software is+# furnished to do so, subject to the following conditions:++# The above copyright notice and this permission notice shall be included+# in all copies or substantial portions of the Software.++# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+# FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+# SOFTWARE.++title: "Rule set based on Yegor's draft"+rules:++ - name: Phi+ description: 'Φ-dispatch'+ context:+ global_object: '!b'+ pattern: |+ Φ+ result: |+ !b+ when:+ - apply_in_subformations: false+ tests: []++ - name: xi+ description: 'ξ-dispatch'+ context:+ current_object: '!b'+ pattern: |+ ξ+ result: |+ !b+ when:+ - apply_in_subformations: false+ tests:+ - name: Does not replace ξ inside a subformation+ input: '⟦ a ↦ ⟦ ⟧, x ↦ ξ.a, ρ ↦ ⟦ ⟧ ⟧'+ output: []+ # How to test replacing without already having context?++ - name: DOT+ description: 'Accessing an α-binding'+ pattern: |+ ⟦ !τ ↦ !b, !B ⟧.!τ+ result: |+ !b[ ξ ↦ ⟦ !τ ↦ !b, !B ⟧ ]+ when:+ - 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 ↦ ⟦⟧ ⟧ ⟧ ⟧ ⟧']+ - name: Should respect surrounding context+ input: ⟦ hello ↦ ⟦⟧, goodbye ↦ ⟦ a ↦ ⟦⟧ ⟧ ⟧.hello+ output: ['⟦ ρ ↦ ⟦ hello ↦ ⟦⟧, goodbye ↦ ⟦ a ↦ ⟦⟧ ⟧ ⟧ ⟧']++ - name: DOTrho+ description: 'Accessing ρ-binding'+ pattern: |+ ⟦ ρ ↦ !b, !B ⟧.ρ+ result: |+ !b+ when:+ - nf: '⟦ !B ⟧'+ tests:+ - name: Should match+ input: ⟦ ρ ↦ ⟦ ⟧ ⟧.ρ+ output: ['⟦ ⟧']++ - name: phi+ description: 'Accessing a decorated object'+ pattern: |+ ⟦!B ⟧.!τ+ result: |+ ⟦!B ⟧.φ.!τ+ when:+ - present_attrs:+ attrs: ['φ']+ bindings: ['!B']+ - absent_attrs:+ attrs: ['!τ']+ bindings: ['!B']+ tests:+ - name: 'Attribute does not exist'+ input: '⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.b'+ output: ['⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.φ.b']+ - name: 'Attribute exists'+ input: '⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.a'+ output: []+ - name: 'Both attributes do not exist'+ input: '⟦ b ↦ ⟦⟧ ⟧.a'+ output: []++ - name: COPY+ description: 'Application of α-binding'+ context:+ current_object: "!b2"+ pattern: |+ ⟦ !τ ↦ ∅, !B1 ⟧(!τ ↦ !b1, !B2)+ result: |+ ⟦ !τ ↦ !b1[ ξ ↦ !b2 ], !B1 ⟧(!B2)+ when:+ - apply_in_subformations: false+ - nf: '!b1'+ tests:+ - name: Should match+ input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧)+ output: ['⟦ a ↦ ⟦ ρ ↦ ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧) ⟧ ⟧()']+ - name: Should not match in subformations+ input: ⟦ a ↦ ⟦b ↦ ∅⟧(b ↦ ⟦⟧) ⟧+ output: []++ - name: COPY1+ description: 'Application of α-binding'+ # Warning: this is not correct for the chain variant because it only matches the first binding+ # i.e., doesn't match an empty binding after an attached one.+ # We should instead match the first empty binding.+ context:+ current_object: "!b2"+ pattern: |+ ⟦ !τ ↦ ∅, !B ⟧(α0 ↦ !b1)+ result: |+ ⟦ !τ ↦ !b1[ ξ ↦ !b2 ], !B ⟧+ when:+ - apply_in_subformations: false+ - nf: '!b1'+ tests:+ - name: Should match first void attribute+ input: ⟦ hello ↦ ⟦⟧, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧)+ output: ['⟦ bye ↦ ⟦ ρ ↦ ⟦ hello ↦ ⟦⟧, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧) ⟧, hello ↦ ⟦⟧, hey ↦ ∅ ⟧']+ options:+ - take_one: true++ - name: COPY2+ description: 'Application of α-binding'+ # Warning: this is not correct for the chain variant because it only matches the first two bindings+ # i.e., doesn't match an empty binding after an attached one.+ # We should instead match the first two empty bindings.+ context:+ current_object: "!b3"+ pattern: |+ ⟦ !τ1 ↦ ∅, !τ2 ↦ ∅, !B ⟧(α0 ↦ !b1, α1 ↦ !b2)+ result: |+ ⟦ !τ1 ↦ !b1[ ξ ↦ !b3 ], !τ2 ↦ !b2[ ξ ↦ !b3 ], !B ⟧+ when:+ - apply_in_subformations: false+ - nf: '!b1'+ - nf: '!b2'+ tests:+ - name: Should match positional arguments+ input: ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧)+ output: ['⟦ hello ↦ ⟦ ρ ↦ ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) ⟧, bye ↦ ⟦ a ↦ ⟦⟧, ρ ↦ ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) ⟧, hey ↦ ∅ ⟧']+ options:+ - take_one: true++ - name: COPYdelta+ description: 'Application of Δ-binding'+ pattern: |+ ⟦ Δ ⤍ ∅, !B ⟧(Δ ⤍ !y)+ result: |+ ⟦ Δ ⤍ !y, !B ⟧+ when:+ - apply_in_abstract_subformations: false+ tests: []++ - name: EMPTY+ description: 'Empty application'+ pattern: |+ ⟦ !B1 ⟧()+ result: |+ ⟦ !B1 ⟧+ when: []+ tests:+ - name: Should match+ input: ⟦ a ↦ ⟦⟧ ⟧()+ output: ['⟦ a ↦ ⟦⟧ ⟧']+ - name: Should not match+ input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧)+ output: []+ - name: Should match in subformation+ input: ⟦ a ↦ ⟦ b ↦ ⟦⟧() ⟧ ⟧+ output: ['⟦ a ↦ ⟦ b ↦ ⟦⟧ ⟧ ⟧']+ - name: Should work with empty formation+ input: ⟦⟧()+ output: ['⟦⟧']++ - name: OVER+ description: 'Invalid application (attribute already attached)'+ pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2)+ result: ⊥+ when: []+ tests:+ - name: ''+ input: '⟦ t ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'+ output: ['⊥']++ - name: STOP+ description: 'Invalid attribute access'+ pattern: |+ ⟦ !B ⟧.!τ+ result: |+ ⊥+ when:+ - absent_attrs:+ attrs: ['!τ', 'φ', 'λ']+ bindings: ['!B']+ - present_attrs:+ attrs: ['ρ']+ bindings: ['!B']+ - nf: '⟦ !B ⟧'+ tests:+ - name: 'Accessing nonexistent attribute'+ input: '⟦ ρ ↦ ⟦ ⟧ ⟧.x'+ output: ['⊥']++ - name: MISS+ description: 'Invalid application (absent attribute)'+ pattern: ⟦ !B1 ⟧(!τ ↦ !b, !B2)+ result: ⊥+ when:+ - absent_attrs:+ attrs: ['!τ', 'φ', 'λ']+ bindings: ['!B1']+ tests:+ - name: ''+ input: '⟦ t1 ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'+ output: ['⊥']+ - name: Should not match if attr is present+ input: ⟦ t ↦ ⟦⟧ ⟧(t ↦ ⟦ a ↦ ∅ ⟧)+ output: []+ - name: Should not match if phi is present+ input: ⟦ φ ↦ ⟦⟧, a ↦ ⟦⟧ ⟧(t ↦ ⟦ a ↦ ∅ ⟧)+ output: []+ - name: Should apply in subformations+ input: ⟦ a ↦ ⟦ b ↦ ⟦⟧(t ↦ ⟦⟧) ⟧ ⟧+ output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']++ - name: DD+ description: 'Accessing an attribute on bottom'+ pattern: |+ ⊥.!τ+ result: |+ ⊥+ when: []+ tests:+ - name: 'Dispatch on bottom is bottom'+ input: '⊥.a'+ output: ['⊥']+ - name: 'Dispatch on anything else is not touched'+ input: '⟦ ⟧.a'+ output: []++ - name: DC+ description: 'Application on bottom is bottom'+ pattern: |+ ⊥(!B)+ result: |+ ⊥+ when: []+ tests:+ - name: Should apply in subformations+ input: ⟦ a ↦ ⟦ b ↦ ⊥(t ↦ ⟦⟧, u ↦ ⟦⟧) ⟧ ⟧+ output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']