phino-0.0.81: resources/dataization.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. The input
# is always a normal form: a non-NF expression matches no clause.

- name: delta
  description: '𝔻(⟦𝐵1, Δ ⤍ δ, 𝐵2⟧) ⟿ δ'
  match: ⟦𝐵1, Δ ⤍ δ, 𝐵2⟧
  then: δ

- name: box
  description: '𝔻(⟦𝐵1, φ ↦ e, 𝐵2⟧) ⟿ 𝔻(𝒩(𝒞(e))) if [Δ, λ] ∩ (𝐵1 ∪ 𝐵2) = ∅'
  match: ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧
  where:
    - meta: 𝑒1
      function: contextualize
      args:
        - 𝑒
        - ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧
  when:
    disjoint:
      - [Δ, λ]
      - [𝐵1, 𝐵2]
  then:
    dataize:
      normalize: 𝑒1

- name: norm
  description: '𝔻(n) ⟿ 𝔻(𝕄(n)) if n ∉ 𝒫'
  match: 𝑛
  when:
    not:
      primitive: 𝑛
  then:
    dataize:
      morph: 𝑛

- name: none
  description: '𝔻(n) ⟿ nothing otherwise'
  match: 𝑛
  then: nothing