phino-0.0.0.75: resources/morphing.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Morphing 𝕄 — applied top-to-bottom, first matching clause wins.

- name: Mprim
  description: '𝕄(e) ⟿ e if e ∈ 𝒫'
  match: 𝑒
  when:
    primitive: 𝑒
  then: 𝑒

- name: Mnmz
  description: '𝕄(e) ⟿ 𝕄(𝒩(e)) if e ∉ NF'
  match: 𝑒
  when:
    not:
      nf: 𝑒
  then:
    morph:
      normalize: 𝑒

- name: Mlambda
  description: '𝕄(⟦𝐵1, λ ⤍ F, 𝐵2⟧ * t) ⟿ 𝕄(F(⟦𝐵1, 𝐵2⟧) * t)'
  match: '⟦𝐵1, λ ⤍ !F, 𝐵2⟧ * !t'
  where:
    - meta: 𝑒
      function: lambda
      args:
        - '⟦𝐵1, λ ⤍ !F, 𝐵2⟧'
  then:
    morph: '𝑒 * !t'

- name: Mphi
  description: '𝕄(Φ.τ * t) ⟿ 𝕄(e * t) if Φ ↦ ⟦𝐵1, τ ↦ e, 𝐵2⟧'
  match: 'Φ.𝜏 * !t'
  where:
    - meta: 𝑒
      function: global
      args:
        - 𝜏
  then:
    morph: '𝑒 * !t'

- name: Mstuck
  description: '𝕄(e) ⟿ ⊥ otherwise'
  match: 𝑒
  then: ⊥