# 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 ↦ ⊥ ⟧ ⟧']