phino-0.0.157: test-resources/evaluate-packs/fires-the-arguments-of-a-copy-a-defer-line-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 'defer' line reading the right side defers the copy,
# and 'w' is a call of 'L_inc'. Before it writes the 'deferred' line, the
# line morphs 'w' in the copy the meta '𝑛2' is bound to, 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, #1933,
# and #1982). The left side is the bare symbol '𝜎3', so the two sides differ
# in their symbols alone, and the join makes one term of them.
symbolic: |
  - λ: L_inc
    dataize:
      𝛿1: $.x
    𝑛: Φ.num( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
  - λ: L_fork
    dataize:
      𝛿1: $.c
    morph:
      𝑛1: $.a
      𝑛2: $.b
    defer:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      on: 𝛿1
      left: 𝑛3
      right: 𝑛4
location: 'Q.y'
input: '⟦ box(x, w) ↦ ⟦ φ ↦ x.next ⟧, num(φ) ↦ ⟦⟧, inc(x) ↦ ⟦ λ ⤍ L_inc ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ x ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎2 ⟧, a ↦ ⟦ λ ⤍ 𝜎3 ⟧, b ↦ Φ.box( x ↦ Φ.items.tail, w ↦ Φ.inc( ⟦ Δ ⤍ 2A- ⟧ ) ), λ ⤍ L_fork ⟧, λ ⤍ L_inc ⟧.φ ⟧'
result: '𝜎7:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_inc):
      𝔻(Φ.a🌵0):
        𝔼(L_fork):
          𝛿1·2 := 𝔻(𝜎2:λ)  # 𝔻(ξ.c)
          𝑛1·2 := 𝜎3:λ  # 𝕄(ξ.a)
          𝕄(Φ.a🌵3):
            𝑛·2·1 := Φ.box( x ↦ Φ.items.tail )
            𝑛·2·2 := 𝑛·2·1( w ↦ Φ.inc( 2A-:Δ ) )
          𝑛2·2 := 𝑛·2·2  # 𝕄(ξ.b)
          𝑛3·2 := 𝑛1·2  # 𝑛1
          𝕄(𝑛2.w):
            𝑛·2·3 := Φ.inc( x ↦ 2A-:Δ )
          𝔼(L_inc):  # 𝔼(𝑛2.w)
            𝔻(Φ.a🌵4):
              𝛿·3·1 := 2A-
            𝛿1·3 := 𝛿·3·1  # 𝔻(ξ.x)
            𝑛·3·1 := Φ.num( φ ↦ 𝜎4:λ )  # 𝑛
            𝕄(𝑛·3·1):
              𝑛·3·2 := Φ.num( φ ↦ 𝜎4:λ )
            𝑛·3·3 := 𝑛·3·2  # 𝕄(𝑛·3·1)
          deferred 𝜎5 := Φ.box( x ↦ 𝜎1:λ, w ↦ 𝑛·3·2 )  # 𝕄(𝑛2.φ)
          joined 𝜎6 := 𝛿1·2 ? 𝜎3 : 𝜎5
          𝑛·2·4 := 𝜎6:λ  # 𝑛3, 𝑛4
      𝛿1·1 := 𝔻(𝜎6:λ)  # 𝔻(ξ.x)
      𝑛·1·1 := Φ.num( φ ↦ 𝜎7:λ )  # 𝑛
      𝕄(𝑛·1·1):
        𝑛·1·2 := Φ.num( φ ↦ 𝜎7:λ )
      𝑛·1·3 := 𝑛·1·2  # 𝕄(𝑛·1·1)