phino-0.0.158: test-resources/evaluate-packs/reduces-a-carried-symbol-through-morphing.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# A 'morph' operand of the firing is a symbol the program already carried:
# 𝕄 hands it back the way it found it, since a symbol is already a normal form
# and there is nothing under it to reduce. The answer then mints after it.
symbolic: |
  - λ: L_keep
    morph:
      𝑛1: $.x
    𝑛: ⟦ z ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧
location: 'Q.y'
input: '⟦ y ↦ ⟦ x ↦ ⟦ λ ⤍ 𝜎4 ⟧, λ ⤍ L_keep ⟧.z ⟧'
result: '𝜎5:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_keep):
      𝕄(ξ.x):
        morphed 𝑛·1·1 := 𝜎4:λ
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.x)
      𝑛·1·2 := 𝜎5:λ:z  # 𝑛
      𝕄(𝑛·1·2):
        morphed 𝑛·1·3 := 𝜎5:λ:z
      𝑛·1·4 := 𝑛·1·3  # 𝕄(𝑛·1·2)
    morphed 𝑛·0·1 := 𝜎5:λ