phino-0.0.157: test-resources/evaluate-packs/joins-a-side-an-evaluate-line-fired-with-a-bool-it-left-as-it-is.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The sides of a join may go through 'evaluate' lines (#1999). The left side
# morphs down to a call of 'L_eq' 𝕄 left unfired, which could never join with
# a bool, so its 'evaluate' line fires it and binds the bool the entry
# answers. The right side is a bool already, a formation with no λ, so its
# 'evaluate' line leaves it as it is. The two bools differ in their symbols
# alone, and the join makes one term of them.
symbolic: |
  - λ: L_eq
    𝑛: Φ.bool( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
  - λ: L_fork
    dataize:
      𝛿1: $.c
    morph:
      𝑛1: $.a
      𝑛2: $.b
    evaluate:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      on: 𝛿1
      left: 𝑛3
      right: 𝑛4
location: 'Q.y'
input: '⟦ bool(φ) ↦ ⟦⟧, y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ L_eq ⟧, b ↦ Φ.bool( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ), λ ⤍ L_fork ⟧.φ ⟧'
result: '𝜎4:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝛿1·1 := 𝔻(𝜎1:λ)  # 𝔻(ξ.c)
      𝑛1·1 := L_eq:λ  # 𝕄(ξ.a)
      𝕄(Φ.a🌵2):
        𝑛·1·1 := Φ.bool( φ ↦ 𝜎2:λ )
      𝑛2·1 := 𝑛·1·1  # 𝕄(ξ.b)
      𝔼(L_eq):  # 𝔼(𝑛1)
        𝑛·2·1 := Φ.bool( φ ↦ 𝜎3:λ )  # 𝑛
        𝕄(𝑛·2·1):
          𝑛·2·2 := Φ.bool( φ ↦ 𝜎3:λ )
        𝑛·2·3 := 𝑛·2·2  # 𝕄(𝑛·2·1)
      𝑛3·1 := 𝑛·2·3  # 𝔼(𝑛1)
      𝑛4·1 := 𝑛2·1  # 𝔼(𝑛2)
      joined 𝜎4 := 𝛿1·1 ? 𝜎3 : 𝜎2
      𝑛·1·2 := 𝜎4:λ:φ  # 𝑛3, 𝑛4