phino-0.0.152: test-resources/evaluate-packs/joins-a-negated-bool-whose-literal-a-rewrite-brought-to-one-shape.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The program '!(x > 0)' of eo-runtime: 'not' is 'if. false true', so one
# branch of the fork is the literal 'false' and the other the literal 'true',
# while what the fork answers is a bool carrying a symbol. The two spellings
# are one value, and the 'rewrite' block of the fork says so, turning either
# literal into the shape an answer has with the datum it stands for, which
# 'symbolize' then stands into a known symbol, so the join pairs them and the
# root dataizes the fork of 'not' over the fork of '>' (#1409).
symbolic: |
  - λ: L_number_gt
    dataize:
      𝛿1: $.ρ
      𝛿2: $.b
    𝑛: ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧ ) ⟧
  - λ: L_entry
    dataize:
      𝛿1: $.n
    morph:
      𝑛1: $.v.φ
    𝑛: Φ.l🌵.root( 𝑛1 )
  - λ: L_root
    dataize:
      𝛿1: $.v
    𝑛: ⟦ ⟧
  - λ: L_fork
    dataize:
      𝛿1: $.φ
    morph:
      𝑛1: $.left
      𝑛2: $.right
    rewrite:
      𝑛3:
        of: 𝑛1
        rules: &bool
          - name: false-literal
            pattern: ⟦ !B1, φ ↦ Φ.bool( if ↦ ⟦ ρ ↦ ∅, left ↦ ∅, right ↦ ∅, φ ↦ ξ.right ⟧ ), !B2 ⟧
            result: ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ) ⟧
          - name: true-literal
            pattern: ⟦ !B1, φ ↦ Φ.bool( if ↦ ⟦ ρ ↦ ∅, left ↦ ∅, right ↦ ∅, φ ↦ ξ.left ⟧ ), !B2 ⟧
            result: ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ Δ ⤍ FF- ⟧ ⟧ ) ⟧
          - name: bool-without-rho
            pattern: ⟦ !B1, φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝑒1 ⟧ ), !B2 ⟧
            result: ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝑒1 ⟧ ) ⟧
      𝑛4:
        of: 𝑛2
        rules: *bool
    symbolize:
      𝑛5: 𝑛3
      𝑛6: 𝑛4
    join:
      𝑛7: [𝑛5, 𝑛6]
    𝑛: 𝑛7
location: 'Q.l🌵'
deep: true
partial: true
acyclic: proven
steps: 32
input: |
  ⟦
    number ↦ ⟦ φ ↦ ∅, gt ↦ ⟦ b ↦ ∅, λ ⤍ L_number_gt, ρ ↦ ∅ ⟧ ⟧,
    bytes ↦ ⟦ φ ↦ ∅ ⟧,
    bool ↦ ⟦ if ↦ ∅, φ ↦ ξ.if( left ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ FF- ⟧ ), right ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 00- ⟧ ) ), not ↦ ξ.if( left ↦ Φ.false, right ↦ Φ.true ) ⟧,
    true ↦ ⟦ φ ↦ Φ.bool( if ↦ ⟦ ρ ↦ ∅, left ↦ ∅, right ↦ ∅, φ ↦ ξ.left ⟧ ) ⟧,
    false ↦ ⟦ φ ↦ Φ.bool( if ↦ ⟦ ρ ↦ ∅, left ↦ ∅, right ↦ ∅, φ ↦ ξ.right ⟧ ) ⟧,
    guard ↦ ⟦ x ↦ ∅, φ ↦ ξ.x.gt( b ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 00-00-00-00-00-00-00-00 ⟧ ) ) ).not ⟧,
    l🌵 ↦ ⟦ mark ↦ ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧, root ↦ ⟦ v ↦ ∅, λ ⤍ L_root ⟧,
      e1 ↦ Φ.l🌵.mark( n ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 3F-F0-00-00-00-00-00-00 ⟧ ) ) )( v ↦ Φ.guard( x ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) ) ) ) ⟧
  ⟧
protocol: |
  𝕄(Φ.l🌵):
    𝕄(Φ.l🌵.e1):
      𝑛·0·1 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )
      𝑛·0·2 := Φ.number( φ ↦ 𝑛·0·1 )
      𝑛·0·3 := ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧( n ↦ 𝑛·0·2 )
      𝑛·0·4 := Φ.bytes( φ ↦ 𝜎1:λ )
      𝑛·0·5 := Φ.number( φ ↦ 𝑛·0·4 )
      𝑛·0·6 := Φ.guard( x ↦ 𝑛·0·5 )
      𝑛·0·7 := ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧( n ↦ 𝑛·0·2 )
      𝑛·0·8 := 𝑛·0·7( v ↦ 𝑛·0·6 )
      𝔼(L_entry):
        𝔻(Φ.a🌵0):
          𝕄(Φ.a🌵0):
            𝑛·1·1 := Φ.number( φ ↦ 𝑛·0·1 )
            𝑛·1·2 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )
          𝛿·1·1 := 3F-F0-00-00-00-00-00-00  # 1.0
        𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.n)
        𝕄(Φ.a🌵1):
          𝑛·1·3 := Φ.guard( x ↦ 𝑛·0·5 )
          𝑛·1·4 := Φ.number( φ ↦ 𝑛·0·4 )
          𝑛·1·5 := Φ.number( φ ↦ 𝑛·0·4 )
          𝑛·1·6 := 𝑛·1·5.gt( b ↦ 0 )
          𝔼(L_number_gt):
            𝔻(Φ.a🌵2):
              𝕄(Φ.a🌵2):
                𝑛·2·1 := Φ.number( φ ↦ 𝑛·0·4 )
                𝑛·2·2 := Φ.bytes( φ ↦ 𝜎1:λ )
            𝛿1·2 := 𝔻(𝜎1:λ)  # 𝔻(ξ.ρ)
            𝔻(Φ.a🌵3):
              𝕄(Φ.a🌵3):
                𝑛·2·3 := 0
                𝑛·2·4 := Φ.bytes( φ ↦ 00-00-00-00-00-00-00-00:Δ )
              𝛿·2·1 := 00-00-00-00-00-00-00-00  # 0.0
            𝛿2·2 := 𝛿·2·1  # 𝔻(ξ.b)
            𝑛·2·5 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ ):φ  # 𝑛
            𝑛·2·6 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ ):φ  # 𝕄(𝑛·2·5)
          𝑛·1·7 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ )
          𝑛·1·8 := ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝜎2:λ ⟧( left ↦ Φ.false )
          𝑛·1·9 := 𝑛·1·8( right ↦ Φ.true )
          𝔼(L_fork):
            𝛿1·3 := 𝔻(𝜎2:λ)  # 𝔻(ξ.φ)
            𝕄(Φ.a🌵5):
              𝕄(Φ.a🌵5.φ):
                𝑛·3·1 := Φ.bool( if(left, right) ↦ right:φ )
            𝑛1·3 := 𝑛·3·1:φ  # 𝕄(ξ.left)
            𝕄(Φ.a🌵6):
              𝕄(Φ.a🌵6.φ):
                𝑛·3·2 := Φ.bool( if(left, right) ↦ left:φ )
            𝑛2·3 := 𝑛·3·2:φ  # 𝕄(ξ.right)
            𝑛3·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 00-:Δ ⟧ ):φ  # 𝑛1
            𝑛4·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ FF-:Δ ⟧ ):φ  # 𝑛2
            𝔻(𝜎3:λ) == 00-
            𝑛5·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ ⟧ ):φ  # 𝑛3
            𝔻(𝜎4:λ) == FF-
            𝑛6·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎4:λ ⟧ ):φ  # 𝑛4
            𝔻(𝜎5:λ) ∈ { 𝔻(𝜎3:λ), 𝔻(𝜎4:λ) }
            𝑛7·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ  # [𝑛5, 𝑛6]
            𝑛·3·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ  # 𝑛
            𝑛·3·4 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ  # 𝕄(𝑛·3·3)
        𝑛1·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ  # 𝕄(ξ.v.φ)
        𝑛·1·10 := Φ.l🌵.root( Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ )  # 𝑛
        𝕄(𝑛·1·10):
          𝑛·1·11 := ⟦ v ↦ ∅, λ ⤍ L_root ⟧( v ↦ Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ )
        𝑛·1·12 := 𝑛·1·11  # 𝕄(𝑛·1·10)
      𝔼(L_root):
        𝔻(Φ.a🌵7):
          𝕄(Φ.a🌵7):
            𝑛·4·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ )
          𝑛·4·2 := ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝜎5:λ ⟧( left ↦ Φ.bytes( φ ↦ FF-:Δ ) )
          𝑛·4·3 := 𝑛·4·2( right ↦ Φ.bytes( φ ↦ 00-:Δ ) )
          𝔼(L_fork):
            𝛿1·5 := 𝔻(𝜎5:λ)  # 𝔻(ξ.φ)
            𝕄(Φ.a🌵9):
              𝑛·5·1 := Φ.bytes( φ ↦ FF-:Δ )
            𝑛1·5 := 𝑛·5·1  # 𝕄(ξ.left)
            𝕄(Φ.a🌵10):
              𝑛·5·2 := Φ.bytes( φ ↦ 00-:Δ )
            𝑛2·5 := 𝑛·5·2  # 𝕄(ξ.right)
            𝑛3·5 := 𝑛·5·1  # 𝑛1
            𝑛4·5 := 𝑛·5·2  # 𝑛2
            𝔻(𝜎6:λ) == FF-
            𝑛5·5 := 𝜎6:λ:φ  # 𝑛3
            𝔻(𝜎7:λ) == 00-
            𝑛6·5 := 𝜎7:λ:φ  # 𝑛4
            𝔻(𝜎8:λ) ∈ { 𝔻(𝜎6:λ), 𝔻(𝜎7:λ) }
            𝑛7·5 := 𝜎8:λ:φ  # [𝑛5, 𝑛6]
            𝑛·5·3 := 𝑛7·5  # 𝑛
            𝑛·5·4 := 𝑛7·5  # 𝕄(𝑛·5·3)
        𝛿1·4 := 𝔻(𝜎8:λ)  # 𝔻(ξ.v)
        𝑛·4·4 := ⟦⟧  # 𝑛
        𝑛·4·5 := ⟦⟧  # 𝕄(𝑛·4·4)