phino-0.0.162: test-resources/evaluate-packs/answers-a-firing-whose-operand-loops.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# A loop met while an operand is being brought down to data, one whole run of 𝔻
# below the spine. The operand dispatches 'foo' off a formation of 'L_loop',
# whose firing answers that very formation, so 𝕄 is about to dispatch off it
# again. The cut answers the whole dispatch with a fresh symbol, named by the
# symbol alone, since no fact leads that formation back to the world (#2307).
# The operand comes down to the datum of the symbol and 'L_outer' answers, and
# the dispatch of 'bar' off its answer is what the run parks on.
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_loop
    𝑛: ⟦ λ ⤍ L_loop ⟧
location: 'Q.x'
acyclic: proven
steps: 250
partial: true
input: >
  ⟦ x ↦ ⟦ arg ↦ ⟦ λ ⤍ L_loop ⟧.foo, λ ⤍ L_outer ⟧.bar ⟧
result: '𝜎2:λ.bar'
protocol: |
  𝕄(Φ.x):
    𝔼(L_outer):
      𝔻(ξ.arg):
        𝕄(ξ.arg):
          𝔼(L_loop):
            𝑛·2·1 := L_loop:λ  # 𝑛
            𝕄(𝑛·2·1):
              morphed 𝑛·2·2 := L_loop:λ
            𝑛·2·3 := L_loop:λ  # 𝕄(𝑛·2·1)
          looped 𝜎1  # proven, repeats L_loop:λ
          morphed 𝑛·1·1 := 𝜎1:λ
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.arg)
      𝑛·1·2 := 𝜎2:λ  # 𝑛
      𝕄(𝑛·1·2):
        morphed 𝑛·1·3 := 𝜎2:λ
      𝑛·1·4 := 𝑛·1·3  # 𝕄(𝑛·1·2)
    unanswered 𝜎2  # 𝕄(𝜎2:λ)