phino-0.0.160: test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-down-two-decorators.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The bare symbol stands on the left this time, and the right side reaches its
# data two decorators down, the way 'bool.and' of EO carries its argument 'x'
# beside the φ of the 'false' it decorates. A 'cast' block finds the bare one
# of its two terms by itself, casts it into a copy of the other with 𝜎2 in
# place of 𝜎3 at the end of the φ chain, two steps down, and binds each meta
# in the order its lines are written, so '𝑛3' takes the cast and '𝑛4' keeps
# the right side as it is. The cast mints no symbol, and 𝜎2 stays what it
# was (#2187).
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.c
    morph:
      𝑛1: $.a
      𝑛2: $.b
    cast:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      on: 𝛿1
      left: 𝑛3
      right: 𝑛4
location: 'Q.y'
input: '⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, if ↦ Φ.zu ⟧, x ↦ Φ.ty ⟧, λ ⤍ L_fork ⟧.φ ⟧'
result: '⟦ φ ↦ 𝜎4:λ, if ↦ Φ.zu ⟧'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝔻(ξ.c):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)
      𝕄(ξ.a):
        morphed 𝑛·1·1 := 𝜎2:λ
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.a)
      𝕄(ξ.b):
        morphed 𝑛·1·2 := ⟦ φ ↦ ⟦ φ ↦ 𝜎3:λ, if ↦ Φ.zu ⟧, x ↦ Φ.ty ⟧
      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
      cast 𝑛3·1 := ⟦ φ ↦ ⟦ φ ↦ 𝜎2:λ, if ↦ Φ.zu ⟧, x ↦ Φ.ty ⟧  # 𝑛1·1 up to 𝑛2·1
      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
      𝑛·1·3 := ⟦ φ ↦ ⟦ φ ↦ 𝜎4:λ, if ↦ Φ.zu ⟧, x ↦ Φ.ty ⟧
    morphed 𝑛·0·1 := ⟦ φ ↦ 𝜎4:λ, if ↦ Φ.zu ⟧