phino-0.0.154: test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-two-symbols-when-lenient.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A lenient join answers a copy of the branch a bare symbol stands against only
# when that branch holds exactly one symbol (#1817), since only then is it
# clear which symbol the bare one pairs with. Here the call of 'Φ.bool' holds
# two, '𝜎2' and '𝜎3', so the join is refused and the firing gets stuck.
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    join:
      𝑛3: [𝑛1, 𝑛2]
    lenient: true
    𝑛: 𝑛3
location: 'Q.y'
input: |
  ⟦
    bool(if) ↦ ⟦ φ ↦ ξ.if( α0 ↦ ⟦ Δ ⤍ FF- ⟧, α1 ↦ ⟦ Δ ⤍ 00- ⟧ ) ⟧,
    y ↦ ⟦
      a ↦ ⟦ λ ⤍ 𝜎1 ⟧,
      b ↦ ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, was ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧ ) ⟧,
      λ ⤍ L_fork
    ⟧.φ
  ⟧
fails: "No entry of --symbolic answers the λ function 'L_fork'"
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := 𝜎1:λ  # 𝕄(ξ.a)
      𝑛2·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ, was ↦ 𝜎3:λ ⟧ ):φ  # 𝕄(ξ.b)
      stuck(L_fork)