yegor.yaml

title: "Rule set based on Yegor's draft"
rules:
  # - name: Rule 3
  #   description: 'Initialization of parent attribute'
  #   pattern: |
  #     ⟦ !B ⟧
  #   result: |
  #     ⟦ !B, ρ ↦ ξ.σ ⟧
  #   when:
  #     - present_attrs:
  #         attrs: ['σ']
  #         bindings: ['!B']
  #     - absent_attrs:
  #         attrs: ['ρ']
  #         bindings: ['!B']
  #   tests:
  #     - name: 'Has sigma and no rho'
  #       input: '⟦ b ↦ ⟦ ⟧, σ ↦ ⟦ ⟧ ⟧ '
  #       output: ['⟦ b ↦ ⟦ ⟧, σ ↦ ⟦ ⟧, ρ ↦ ξ.σ ⟧']
  #     - name: 'Has both sigma and rho'
  #       input: '⟦ a ↦ ⟦ b ↦ ⟦ ⟧, ρ ↦ ⟦ ⟧, σ ↦ ⟦ ⟧ ⟧ ⟧'
  #       output: []
  #     - name: 'Has neither sigma nor rho'
  #       input: '⟦ a ↦ ⟦ b ↦ ⟦ ⟧ ⟧ ⟧'
  #       output: []

  - name: Φ-dispatch
    description: 'Φ-dispatch'
    context:
      global_object: '!b'
    pattern: |
      Φ
    result: |
      !b
    when:
      - apply_in_subformations: false
    tests: []

  - name: ξ-dispatch
    description: 'ξ-dispatch'
    context:
      current_object: '!b'
    pattern: |
      ξ
    result: |
      !b
    when:
      - apply_in_subformations: false
      # - present_attrs:
      #     attrs: ['ρ']
      #     bindings: ['!B']
    tests:
      - name: Does not replace ξ inside a subformation
        input: '⟦ a ↦ ⟦ ⟧, x ↦ ξ.a, ρ ↦ ⟦ ⟧ ⟧'
        output: []
      # How to test replacing without already having context?

  - name: R_DOT
    description: 'Accessing an α-binding'
    pattern: |
      ⟦ !τ ↦ !b, !B ⟧.!τ
    result: |
      !b[ ξ ↦ ⟦ !τ ↦ !b, !B ⟧ ]
    when:
      - apply_in_abstract_subformations: false
      - nf_inside_formation: '!b'
      - nf: '⟦ !B ⟧'
    tests:
      - name: Should match
        input: ⟦ hello ↦ ⟦⟧ ⟧.hello
        output: ['⟦ ρ ↦ ⟦ hello ↦ ⟦⟧ ⟧ ⟧']
      - name: Shouldn't match
        input: ⟦ ⟧.hello
        output: []

  # - name: Rule 6a
  #   description: 'Accessing an α-binding (for object with ρ ↦ ∅)'
  #   pattern: |
  #     ⟦ !τ ↦ !b, ρ ↦ ∅, !B ⟧.!τ
  #   result: |
  #     !b[ ξ ↦ ⟦ !τ ↦ !b, ρ ↦ ∅, !B ⟧ ]
  #   when: []
  #   tests:
  #     - name: Should match
  #       input: ⟦ hello ↦ ⟦⟧, ρ ↦ ∅ ⟧.hello
  #       output: ['⟦ ρ ↦ ⟦ hello ↦ ⟦⟧, ρ ↦ ∅ ⟧ ⟧']
  #     - name: Shouldn't match
  #       input: ⟦ ⟧.hello
  #       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
    # i.e., doesn't match an empty binding after an attached one.
    # We should instead match the first two empty bindings.
    pattern: |
      ⟦ !τ1 ↦ ∅, !τ2 ↦ ∅, !B ⟧(α0 ↦ !b0, α1 ↦ !b1)
    result: |
      ⟦ !τ1 ↦ !b0, !τ2 ↦ !b1, !B ⟧
    when:
      - apply_in_abstract_subformations: false
      - nf: '!b0'
      - nf: '!b1'
    tests: []

  - name: R_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.
    pattern: |
      ⟦ !τ ↦ ∅, !B ⟧(α0 ↦ !b)
    result: |
      ⟦ !τ ↦ !b, !B ⟧
    when:
      - apply_in_abstract_subformations: false
      - nf: '!b'
    tests: []

  - name: R_COPY
    description: 'Application of α-binding'
    pattern: |
      ⟦ !τ ↦ ∅, !B ⟧(!τ ↦ !b)
    result: |
      ⟦ !τ ↦ !b, !B ⟧
    when:
      - apply_in_abstract_subformations: false
      - nf: '!b'
    tests: []

  - name: R_COPY_Δ
    description: 'Application of Δ-binding'
    pattern: |
      ⟦ Δ ⤍ ∅, !B ⟧(Δ ⤍ !y)
    result: |
      ⟦ Δ ⤍ !y, !B ⟧
    when:
      - apply_in_abstract_subformations: false
    tests: []

  - name: R_φ
    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: R_OVER
    description: 'Invalid application (attribute already attached)'
    pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2)
    result: ⊥
    when: []
    tests:
      - name: ''
        input: '⟦ t ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'
        output: ['⊥']

  - name: R_MISS
    description: 'Invalid application (absent attribute)'
    pattern: ⟦ !B1 ⟧(!τ ↦ !b2, !B2)
    result: ⊥
    when:
      - absent_attrs:
          attrs: ['!τ', 'φ', 'λ']
          bindings: ['!B1']
    tests:
      - name: ''
        input: '⟦ t1 ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'
        output: ['⊥']

  - name: R_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: R_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: R_DC
    description: 'Application on bottom is bottom'
    pattern: |
      ⊥(!B)
    result: |
      ⊥
    when: []
    tests: []