phino-0.0.152: test-resources/evaluate-packs/walks-on-past-a-firing-it-could-not-make.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# A firing the deep walk opened and could not make: the entry of 'L_root'
# dataizes what it was applied to, that operand never comes down to data, and
# the firing is parked the way a term 𝕄 could not reduce is. The walk goes on
# to the binding after it instead of ending the whole run, so one argument
# nothing can dataize taints its own binding and nothing else (#1288).
symbolic: |
  - λ: L_root
    dataize:
      𝛿1: $.v
    𝑛: ⟦ ⟧
location: 'Q'
deep: true
partial: true
input: >
  ⟦ root(v) ↦ ⟦ λ ⤍ L_root ⟧,
    e1 ↦ Φ.root( ⟦ λ ⤍ L_none ⟧.foo ),
    e2 ↦ Φ.root( ⟦ λ ⤍ 𝜎1 ⟧ ) ⟧
protocol: |
  𝕄(Φ):
    𝕄(Φ.e1):
      unanswered(L_none)  # 𝕄(L_none:λ)
      𝑛·0·1 := Φ.root( v ↦ L_none:λ.foo )
      𝔼(L_root):
        𝔻(Φ.a🌵0):
          𝕄(Φ.a🌵0):
            unanswered(L_none)  # 𝕄(L_none:λ)
        stuck(L_none)
    𝕄(Φ.e2):
      𝑛·0·2 := Φ.root( v ↦ 𝜎1:λ )
      𝔼(L_root):
        𝛿1·2 := 𝔻(𝜎1:λ)  # 𝔻(ξ.v)
        𝑛·2·1 := ⟦⟧  # 𝑛
        𝑛·2·2 := ⟦⟧  # 𝕄(𝑛·2·1)