phino-0.0.156: test-resources/evaluate-packs/fires-the-arguments-of-a-copy-it-defers.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The deferral of #1892 over a copy with two arguments: 'x' reads to the bare
# symbol '𝜎1', so the copy is deferred, and 'w' is a call of 'L_inc'. Before it
# writes the 'deferred' line, the 'unfold' line morphs 'w' at '𝑛2.w' and fires
# what it comes to, so the line names the object 'Φ.num' the argument stands
# for, instead of the call as the code spells it (#1916, #1921).
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    unfold:
      𝑛3: {of: 𝑛2, defer: true}
    join:
      𝑛4: [𝑛1, 𝑛3]
    𝑛: ⟦ φ ↦ 𝑛4 ⟧
  - λ: L_inc
    dataize:
      𝛿1: $.x
    𝑛: Φ.num( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
location: 'Q.y'
input: '⟦ box(x, w) ↦ ⟦ φ ↦ x.next ⟧, num(φ) ↦ ⟦⟧, inc(x) ↦ ⟦ λ ⤍ L_inc ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.box( x ↦ Φ.items.tail, w ↦ Φ.inc( ⟦ Δ ⤍ 2A- ⟧ ) ), λ ⤍ L_fork ⟧.φ ⟧'
result: '𝜎5:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := 𝜎2:λ  # 𝕄(ξ.a)
      𝕄(Φ.a🌵1):
        𝑛·1·1 := Φ.box( x ↦ Φ.items.tail )
        𝑛·1·2 := 𝑛·1·1( w ↦ Φ.inc( 2A-:Δ ) )
      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
      𝕄(𝑛2.w):
        𝑛·1·3 := Φ.inc( x ↦ 2A-:Δ )
      𝔼(L_inc):  # 𝔼(𝑛2.w)
        𝔻(Φ.a🌵2):
          𝛿·2·1 := 2A-
        𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.x)
        𝑛·2·1 := Φ.num( φ ↦ 𝜎3:λ )  # 𝑛
        𝕄(𝑛·2·1):
          𝑛·2·2 := Φ.num( φ ↦ 𝜎3:λ )
        𝑛·2·3 := 𝑛·2·2  # 𝕄(𝑛·2·1)
      deferred(𝜎4) := Φ.box( x ↦ 𝜎1:λ, w ↦ 𝑛·2·2 )  # 𝕄(𝑛2.φ)
      𝔻(𝜎5:λ) ∈ { 𝔻(𝜎2:λ), 𝔻(𝜎4:λ) }
      𝑛4·1 := 𝜎5:λ  # [𝑛1, 𝑛3]
      𝑛·1·4 := 𝜎5:λ:φ  # 𝑛
      𝑛·1·5 := 𝜎5:λ:φ  # 𝕄(𝑛·1·4)