mints-past-the-symbols-a-stuck-firing-minted.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The firing of 'L_inner' mints 𝜎1 for its answer and then gets stuck, since
# nothing answers a dispatch off a symbol, and '--partial' parks its site. The
# protocol keeps what that firing wrote, so 𝜎1 is spelled there already. Before
# #1738 the parked frame handed back the state it started from, the count of
# minted symbols went back with it, and 'L_outer' minted 𝜎1 once more, for
# another value. Now the count never goes back, and 'L_outer' mints 𝜎2.
symbolic: |
  - λ: L_inner
    𝑛: ⟦ λ ⤍ 𝜎 ⟧.foo
  - λ: L_outer
    morph:
      𝑛1: $.a
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
location: 'Q.y'
partial: true
input: '⟦ y ↦ ⟦ a ↦ ⟦ λ ⤍ L_inner ⟧.v, λ ⤍ L_outer ⟧.z ⟧'
result: '𝜎2:λ.z'
protocol: |
  𝕄(Φ.y):
    𝔼(L_outer):
      𝕄(Φ.a🌵0):
        𝔼(L_inner):
          𝑛·2·1 := 𝜎1:λ.foo  # 𝑛
          𝕄(𝑛·2·1):
            unanswered(𝜎1)  # 𝕄(𝜎1:λ)
          stuck(𝜎1)
      𝑛1·1 := L_inner:λ.v  # 𝕄(ξ.a)
      𝑛·1·1 := 𝜎2:λ  # 𝑛
      𝑛·1·2 := 𝜎2:λ  # 𝕄(𝑛·1·1)
    unanswered(𝜎2)  # 𝕄(𝜎2:λ)