phino-0.0.154: test-resources/evaluate-packs/keeps-a-stuck-firing-for-the-next-firing.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps a stuck firing the way it keeps a
# cut. 'L_pair' reduces 'x' and then 'y', and both spell the very same
# formation of 'L_outer'. The firing under 'x' brings its operand down
# through 𝔻, which gets stuck on 'L_none', so the firing never answers and
# '--partial' parks it. Before #1493 the firing under 'y' reduced its operand
# and got stuck on 'L_none' again, since a stuck firing kept nothing. Now the
# second firing takes the failure the first one met: it is written at its own
# site and nothing under it is reduced.
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_pair
    morph:
      𝑛1: $.x
      𝑛2: $.y
    𝑛: ⟦ φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧
location: 'Q.p'
partial: true
acyclic: plausible
input: >
  ⟦ p ↦ ⟦
      x ↦ ⟦ arg ↦ ⟦ λ ⤍ L_none ⟧, λ ⤍ L_outer ⟧.φ,
      y ↦ ⟦ arg ↦ ⟦ λ ⤍ L_none ⟧, λ ⤍ L_outer ⟧.φ,
      λ ⤍ L_pair ⟧.φ ⟧
protocol: |
  𝕄(Φ.p):
    𝔼(L_pair):
      𝕄(Φ.a🌵0):
        𝔼(L_outer):
          𝔻(Φ.a🌵1):
            unanswered(L_none)  # 𝔻(L_none:λ)
          stuck(L_none)
      𝑛1·1 := ⟦ arg ↦ L_none:λ, λ ⤍ L_outer ⟧.φ  # 𝕄(ξ.x)
      𝕄(Φ.a🌵2):
        𝔼(L_outer):
          stall(L_none)
      𝑛2·1 := ⟦ arg ↦ L_none:λ, λ ⤍ L_outer ⟧.φ  # 𝕄(ξ.y)
      𝑛·1·1 := 𝜎1:λ:φ  # 𝑛
      𝑛·1·2 := 𝜎1:λ:φ  # 𝕄(𝑛·1·1)