phino-0.0.157: test-resources/evaluate-packs/tells-why-a-join-fabricated-nothing-of-a-side-that-is-no-formation.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The 'rewrite' line takes 'Φ.k' out of the formation the left side morphs to,
# and the join compares that formation with the dispatch. They differ as a
# whole, so no attribute tells where. The block names 'L_join' under
# 'otherwise', but the right side is no formation, so nothing is fabricated of
# the two, and the comment of 'diverged' says so (#2043).
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.c
    morph:
      𝑛1: $.a
    rewrite:
      𝑛2:
        of: 𝑛1
        rules:
          - name: unwrap
            pattern: ⟦ φ ↦ 𝑒1 ⟧
            result: 𝑒1
    join:
      on: 𝛿1
      left: 𝑛1
      right: 𝑛2
      otherwise: L_join
location: 'Q.y'
partial: true
input: '⟦ k ↦ ⟦⟧, y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ φ ↦ Φ.k ⟧, λ ⤍ L_fork ⟧.φ ⟧'
result: '⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ φ ↦ Φ.k ⟧, λ ⤍ L_fork ⟧.φ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝛿1·1 := 𝔻(𝜎1:λ)  # 𝔻(ξ.c)
      𝑛1·1 := Φ.k:φ  # 𝕄(ξ.a)
      𝑛2·1 := Φ.k  # rewrite(𝑛1)
      diverged 𝑛1·1 vs 𝑛2·1  # the right side is no formation