phino-0.0.158: test-resources/evaluate-packs/dataizes-what-a-morph-operand-of-the-same-entry-brought-down.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The entry morphs the body of 'v' and dataizes what the morph came to, the
# way the 'L_entry' of the lowering of EO wants both the object a body morphs
# into and the data that object dataizes to (#2139). An operand of 'dataize'
# naming the meta 'morph' bound runs as a line once that meta is bound, so
# one entry does what took the 'L_entry' and the 'L_root' of EO two. The
# protocol writes the line of '𝛿2' right after the line of '𝑛1' it read,
# commented with the dataization of that meta, while '𝛿1', reading '$', still
# comes down before every operand of 'morph'.
symbolic: |
  - λ: L_entry
    morph:
      𝑛1: $.v.φ
    dataize:
      𝛿1: $.n
      𝛿2: 𝑛1
    𝑛: ⟦ φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧
location: 'Q.y'
input: '⟦ y ↦ ⟦ n ↦ ⟦ λ ⤍ 𝜎1 ⟧, v ↦ ⟦ φ ↦ Φ.t ⟧, λ ⤍ L_entry ⟧.φ, t ↦ ⟦ Δ ⤍ 2A- ⟧ ⟧'
result: '𝜎2:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_entry):
      𝔻(ξ.n):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.n)
      𝕄(ξ.v.φ):
        morphed 𝑛·1·1 := 2A-:Δ
      𝑛1·1 := 2A-:Δ  # 𝕄(ξ.v.φ)
      𝔻(𝑛1):
        𝛿·1·2 := 2A-
      𝛿2·1 := 𝛿·1·2  # 𝔻(𝑛1)
      𝑛·1·2 := 𝜎2:λ:φ  # 𝑛
      𝕄(𝑛·1·2):
        morphed 𝑛·1·3 := 𝜎2:λ:φ
      𝑛·1·4 := 𝑛·1·3  # 𝕄(𝑛·1·2)
    morphed 𝑛·0·1 := 𝜎2:λ