phino-0.0.81: resources/morphing.yaml

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

- name: prim
  description: '𝕄(p) ⟿ p'
  match: 𝑝
  then: 𝑝

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

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

- name: stuck
  description: '𝕄(n) ⟿ ⊥ otherwise'
  match: 𝑛
  then: ⊥