joins-a-bare-symbol-a-cast-brought-into-the-shape-of-a-decorator.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The right side is a bare symbol, a branch that already reached its data,
# while the left side wraps its data in φ and holds 'k' beside it, a branch
# one step short of its data. As they are, the two differ at .k, the right
# side has λ, and the join diverges, even under 'otherwise' (#2187). A 'cast'
# block reads its two metas as one pair and casts the bare symbol into a copy
# of the left side with 𝜎3 in place of 𝜎2 at the end of its φ chain, so the
# two sides differ in their symbols alone and the join makes one term of them.
# The cast mints no symbol. The protocol writes the line of '𝑛20', which took
# the cast, as 'cast 𝑛20·1 := …' with the meta it read and the meta whose
# shape it took. The line of '𝑛19' binds its term as it is and writes
# nothing (#2192).
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.on🌵
    morph:
      𝑛13: $.left🌵
      𝑛14: $.right🌵
    cast:
      𝑛19: 𝑛13
      𝑛20: 𝑛14
    join:
      on: 𝛿1
      left: 𝑛19
      right: 𝑛20
      otherwise: L_fork
location: 'Q.e1'
input: '⟦ e1 ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, right🌵 ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧.φ ⟧'
result: '𝜎4:λ'
protocol: |
  𝕄(Φ.e1):
    𝔼(L_fork):
      𝔻(ξ.on🌵):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
      𝕄(ξ.left🌵):
        morphed 𝑛·1·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎2:λ ⟧
      𝑛13·1 := 𝑛·1·1  # 𝕄(ξ.left🌵)
      𝕄(ξ.right🌵):
        morphed 𝑛·1·2 := 𝜎3:λ
      𝑛14·1 := 𝑛·1·2  # 𝕄(ξ.right🌵)
      cast 𝑛20·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎3:λ ⟧  # 𝑛14·1 up to 𝑛13·1
      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
      𝑛·1·3 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎4:λ ⟧
    morphed 𝑛·0·1 := 𝜎4:λ