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 (#1409).
# Morphing leaves the fork of 'not' as a call, so the entry fires it with an
# 'evaluate' line (#1874). The dispatch of φ that ends 'e1' fires the entry
# and then the root it answers, and the root dataizes the fork of 'not' over
# the fork of '>'.
symbolic: |
  - λ: L_number_gt
    dataize:
      𝛿1: $.ρ
      𝛿2: $.b
    𝑛: ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧ ) ⟧
  - λ: L_entry
    dataize:
      𝛿1: $.n
    morph:
      𝑛1: $.v.φ
    evaluate:
      𝑛2: 𝑛1
    𝑛: Φ.l🌵.root( 𝑛2 )
  - λ: 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🌵.e1'
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🌵.e1):
    𝑛·0·1 := ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧( n ↦ 1 )
    𝑛·0·2 := 𝑛·0·1( v ↦ Φ.guard( x ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ) ) )
    𝔼(L_entry):
      𝔻(Φ.a🌵0):
        𝕄(Φ.a🌵0):
          𝑛·1·1 := 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 ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ) )
        𝑛·1·4 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) )
        𝑛·1·5 := 𝑛·1·4.gt( b ↦ 0 )
        𝔼(L_number_gt):
          𝔻(Φ.a🌵2):
            𝕄(Φ.a🌵2):
              𝑛·2·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) )
              𝑛·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·6 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ )
        𝑛·1·7 := ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝜎2:λ ⟧( left ↦ Φ.false )
        𝑛·1·8 := 𝑛·1·7( right ↦ Φ.true )
      𝑛1·1 := 𝑛·1·8  # 𝕄(ξ.v.φ)
      𝔼(L_fork):  # 𝔼(𝑛1)
        𝛿1·3 := 𝔻(𝜎2:λ)  # 𝔻(ξ.φ)
        𝑛1·3 := Φ.bool( if(left, right) ↦ right:φ ):φ  # 𝕄(ξ.left)
        𝑛2·3 := Φ.bool( if(left, right) ↦ left:φ ):φ  # 𝕄(ξ.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·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ  # 𝑛
        𝑛·3·2 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ  # 𝕄(𝑛·3·1)
      𝑛2·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ  # 𝔼(𝑛1)
      𝑛·1·9 := Φ.l🌵.root( Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ )  # 𝑛
      𝕄(𝑛·1·9):
        𝑛·1·10 := ⟦ v ↦ ∅, λ ⤍ L_root ⟧( v ↦ Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎5:λ ⟧ ):φ )
      𝑛·1·11 := 𝑛·1·10  # 𝕄(𝑛·1·9)
    𝔼(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)