dotg.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# The 'dot' rule where the formation dispatched on is the whole program. Φ is
# the name of that formation, so the body is decorated with the name and not
# with the program: writing the program out copies it into the term, and into
# every term that term then dispatches, so the copies compound until one term
# weighs hundreds of times what the program does (#1318). Whoever reads the ρ
# resolves Φ through the 'universe' morphing rule, which answers with the
# program in normal form — the very formation that would have stood here, since
# a dispatch reaches this rule only once Φ has already been resolved that way.
# Everything else is 'dot': the same pattern, the same contextualization
# context, and a guard that is the exact complement of the one there, so the
# two never both answer a dispatch and never both refuse one, save a formation
# holding both λ and Δ, which both refuse and leave to 'dl' (#1395).
name: dotg
pattern: ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1
e-match: 𝑒1
when:
  and:
    - eq:
        - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧
        - 𝑒1
    - or:
        - disjoint:
            - [λ]
            - [𝐵1, 𝐵2]
        - disjoint:
            - [Δ]
            - [𝐵1, 𝐵2]
result: 𝑒2(ρ ↦ Φ)
where:
  - meta: 𝑒2
    function: contextualize
    args:
      - 𝑛1
      - ⟦𝐵1, 𝐵2⟧