phino-0.0.154: test-resources/evaluate-packs/takes-the-answer-of-a-firing-with-the-same-operands.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps what a firing answered by the λ
# function and the operands it brought down, beside the formation it fired.
# The 'evaluate' lines of 'L_pair' fire 'a' and then 'b', two formations,
# since one reads 'x' and the other reads 'y', so the memo of formations
# misses the second. Yet both bring the same datum down, and an entry
# answers from its operands alone. Before #1661 the firing of 'b' minted
# '𝜎2' for the very value '𝜎1' already named. Now it brings its operand
# down, finds the firing already answered and takes '𝜎1', minting nothing
# (#1874).
symbolic: |
  - λ: L_dataized
    dataize:
      𝛿1: $.target
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_pair
    morph:
      𝑛1: $.a
      𝑛2: $.b
    evaluate:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    𝑛: ⟦ φ ↦ ⟦ a ↦ 𝑛3, b ↦ 𝑛4 ⟧ ⟧
location: 'Q.p'
acyclic: plausible
input: >
  ⟦ dataized(target) ↦ L_dataized:λ,
    p ↦ ⟦
      a ↦ Φ.dataized( target ↦ Φ.x ),
      b ↦ Φ.dataized( target ↦ Φ.y ),
      λ ⤍ L_pair ⟧.φ,
    x ↦ ⟦ Δ ⤍ 01- ⟧,
    y ↦ ⟦ Δ ⤍ 01- ⟧ ⟧
result: '⟦ a ↦ 𝜎1:λ, b ↦ 𝜎1:λ ⟧'
protocol: |
  𝕄(Φ.p):
    𝔼(L_pair):
      𝕄(Φ.a🌵0):
        𝑛·1·1 := Φ.dataized( target ↦ Φ.x )
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.a)
      𝕄(Φ.a🌵1):
        𝑛·1·2 := Φ.dataized( target ↦ Φ.y )
      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
      𝔼(L_dataized):  # 𝔼(𝑛1)
        𝔻(Φ.a🌵2):
          𝛿·2·1 := 01-
        𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.target)
        𝑛·2·1 := 𝜎1:λ  # 𝑛
        𝑛·2·2 := 𝜎1:λ  # 𝕄(𝑛·2·1)
      𝑛3·1 := 𝑛·2·2  # 𝔼(𝑛1)
      𝔼(L_dataized):  # 𝔼(𝑛2)
        𝔻(Φ.a🌵3):
          𝛿·3·1 := 01-
        𝛿1·3 := 𝛿·3·1  # 𝔻(ξ.target)
        𝑛·3·1 := 𝑛3·1  # 𝑛
        𝑛·3·2 := 𝑛3·1  # 𝕄(𝑛·3·1)
      𝑛4·1 := 𝑛·3·2  # 𝔼(𝑛2)
      𝑛·1·3 := ⟦ a ↦ 𝜎1:λ, b ↦ 𝜎1:λ ⟧:φ  # 𝑛
      𝑛·1·4 := ⟦ a ↦ 𝜎1:λ, b ↦ 𝜎1:λ ⟧:φ  # 𝕄(𝑛·1·3)