joins-a-number-with-a-formation-an-undress-took-the-number-out-of.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The left side is a number and the right side a formation binding that number
# in φ alone, so 𝕄 brings the left side to a number and stops at the right side
# one φ short of it, and the join could never make one term of the two (#2174).
# An operand of 'undress' morphs a path from '$' where it stands, as an operand
# of 'morph' does, and then, while the term is a formation binding φ alone
# beside its ρ, dispatches φ off it and morphs that, so both sides come to a
# number. The protocol writes each such pass as an 'undressed' line naming the
# φ it took and the 𝕄 block named after it, and comments the line of the meta
# with 'undress' only where a pass took place.
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.on🌵
    undress:
      𝑛1: $.left🌵
      𝑛2: $.right🌵
    symbolize:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      on: 𝛿1
      left: 𝑛3
      right: 𝑛4
location: 'Q.y'
input: '⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ neg ↦ ⟦ φ ↦ ρ ⟧ ⟧, y ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ 42, right🌵 ↦ ⟦ φ ↦ 7 ⟧ ⟧.φ ⟧'
result: '𝜎4:λ:φ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝔻(ξ.on🌵):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
      𝕄(ξ.left🌵):
        𝑛·1·1 := 42.0
        𝑛·1·2 := ⟦ φ ↦ Φ.bytes( φ ↦ 40-45-00-00-00-00-00-00:Δ ), neg ↦ ρ:φ ⟧
        morphed 𝑛·1·3 := 𝑛·1·2
      𝑛1·1 := 𝑛·1·3  # 𝕄(ξ.left🌵)
      𝕄(ξ.right🌵):
        morphed 𝑛·1·4 := 7.0:φ
      undressed 𝑛·1·5 := 𝑛·1·4.φ
      𝕄(𝑛·1·5):
        𝑛·1·6 := 7.0
        𝑛·1·7 := ⟦ φ ↦ Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ), neg ↦ ρ:φ ⟧
        morphed 𝑛·1·8 := 𝑛·1·7
      𝑛2·1 := 𝑛·1·8  # undress(ξ.right🌵)
      symbolized 𝜎2 := 40-45-00-00-00-00-00-00  # 42.0
      𝑛3·1 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ), neg ↦ ρ:φ ⟧  # symbolize(𝑛1)
      symbolized 𝜎3 := 40-1C-00-00-00-00-00-00  # 7.0
      𝑛4·1 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎3:λ ), neg ↦ ρ:φ ⟧  # symbolize(𝑛2)
      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
      𝑛·1·9 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ), neg ↦ ρ:φ ⟧  # 𝑛3, 𝑛4
    𝑛·0·1 := Φ.bytes( φ ↦ 𝜎4:λ )
    𝑛·0·2 := 𝜎4:λ:φ
    morphed 𝑛·0·3 := 𝑛·0·2