phino-0.0.152: 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):
      𝑛1·1 := 𝜎4:λ  # 𝕄(ξ.x)
      𝑛·1·1 := 𝜎5:λ:z  # 𝑛
      𝑛·1·2 := 𝜎5:λ:z  # 𝕄(𝑛·1·1)