phino-0.0.82: 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: fire
  description: '𝔻(⟦𝐵1, λ ⤍ F, 𝐵2⟧) ⟿ 𝔻(𝒩(𝔼(⟦𝐵1, λ ⤍ F, 𝐵2⟧)))'
  match: ⟦𝐵1, λ ⤍ !F, 𝐵2⟧
  where:
    - meta: 𝑒
      function: lambda
      args:
        - ⟦𝐵1, λ ⤍ !F, 𝐵2⟧
  then:
    dataize:
      normalize: 𝑒

- name: none
  description: '𝔻(⟦𝐵⟧) ⟿ nothing'
  match: ⟦𝐵⟧
  then: nothing

- name: bott
  description: '𝔻(⊥) ⟿ nothing'
  match: ⊥
  then: nothing

- name: norm
  description: '𝔻(n) ⟿ 𝔻(𝕄(n)) otherwise'
  match: 𝑛
  then:
    dataize:
      morph: 𝑛