dot.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Dispatch 𝜏1 on a formation: contextualize the dispatched body 𝑛1 and decorate
# it with the whole formation as ρ. The context of the contextualization is
# the formation WITHOUT the dispatched binding, ⟦𝐵1, 𝐵2⟧, on purpose: a body
# must not reach itself, so normalization admits no recursion through ξ and
# stays total (#967). A ξ in 𝑛1 therefore stands for a formation one attribute
# short of the one it is written in, and that holds for every path through ξ,
# not only for a path back to 𝜏1:
#   - a body reading 𝜏1 finds no 𝜏1 and answers ⊥ by 'stop', directly as in
#     ⟦ a ↦ ξ.a ⟧.a, or through a sibling as in ⟦ a ↦ ξ.b, b ↦ ξ.a ⟧.a;
#   - a body that is ξ answers the short formation, an ordinary object rather
#     than ⊥: ⟦ a ↦ ξ ⟧.a steps to ⟦⟧(ρ ↦ ⟦ a ↦ ξ ⟧), and
#     ⟦ a ↦ ⟦⟧, b ↦ ξ ⟧.b normalizes to ⟦ a ↦ ⟦⟧ ⟧;
#   - a sibling reached through ξ is the sibling of the short formation, so a
#     sibling that itself holds ξ sees the short formation too:
#     ⟦ a ↦ ξ, b ↦ ξ.a ⟧.b normalizes to ⟦⟧, not to the whole formation
#     (#1438).
# A sibling holding no ξ reads as written: ⟦ a ↦ ⟦ z ↦ Φ ⟧, b ↦ ξ.a ⟧.b
# normalizes to ⟦ z ↦ Φ ⟧. Only the ρ of the answer holds the whole
# formation; the context the body is read in never does.
# The rule does not dispatch on a formation holding both λ and Δ: 'dl' says
# such a formation is ⊥, and carrying it out into ρ would leave a ρ ↦ ⊥ in a
# normal form that 'dl' firing first reduces to ⊥ outright, so the answer would
# hang on rule order (#1395).
# The ρ carries the name of the formation where it has one: the whole program
# is 'Φ', and a formation reached as 'Φ.number', or as 'Φ.number( φ ↦ 𝑘 )', is
# an object of the immutable world, so the 'named' function writes that name
# back instead of the object, and a dispatch off it does not copy the program
# or every method the object declares into the term (#1318, #1446). The world
# 'named' looks the name up in is phino's to know, not the rule's: the rule is
# about a term alone and never binds the world itself (#1460). Where the
# formation has no name, or no world is known — the 'rewrite' command, and
# 'isNF' asking about a term on its own — 'named' answers with the formation
# itself and the ρ holds it.
name: dot
pattern: ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1
when:
  not:
    in:
      - [Δ, λ]
      - [𝐵1, 𝐵2]
result: 𝑒1(ρ ↦ 𝑒2)
where:
  - meta: 𝑒1
    function: contextualize
    args:
      - 𝑛1
      - ⟦𝐵1, 𝐵2⟧
  - meta: 𝑒2
    function: named
    args:
      - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧