diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,7 +1,7 @@ cabal-version: 3.0 name: phino -version: 0.0.0.4 +version: 0.0.0.5 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at @@ -13,6 +13,7 @@ copyright: 2025 Objectionary.com category: Language, Code Analysis build-type: Simple +extra-source-files: resources/*.yaml source-repository head type: git diff --git a/resources/alpha.yaml b/resources/alpha.yaml new file mode 100644 --- /dev/null +++ b/resources/alpha.yaml @@ -0,0 +1,10 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: ALPHA +pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒) +result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒) +when: + eq: + - ordinal: 𝜏2 + - length: 𝐵1 diff --git a/resources/copy.yaml b/resources/copy.yaml new file mode 100644 --- /dev/null +++ b/resources/copy.yaml @@ -0,0 +1,25 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# @todo #85:60min Simplify Rcopy rule. Right now this rule is quite verbose. +# It captures a lot objects around its targets. It's done in order to have +# scope for contextualization of 𝑒2 right here right away. So it's a hack. +# The origin Rcopy rule looks like this +# pattern: ⟦ 𝐵1, 𝜏1 ↦ ∅, 𝐵3 ⟧(𝜏1 ↦ 𝑒1) +# result: ⟦ 𝐵1, 𝜏1 ↦ 𝑒2, 𝐵3 ⟧ +# where 𝑒2 is an expression contextualized with 𝑒1 and some scope S. +# But with such pattern we don't have this scope, we don't see it. +# It should be calculated somehow. In general this scope is nearest +# outer formation. So we need to create a way to calculate it and +# rewrite this rule. +name: COPY +pattern: ⟦ 𝐵1, 𝜏1 ↦ ⟦ 𝐵2, 𝜏2 ↦ ∅, 𝐵3 ⟧(𝜏2 ↦ 𝑒1) * !t, 𝐵4 ⟧ +result: ⟦ 𝐵1, 𝜏1 ↦ ⟦ 𝐵2, 𝜏2 ↦ 𝑒2, 𝐵3 ⟧ * !t, 𝐵4 ⟧ +when: + fn: 𝑒1 +where: + - meta: 𝑒2 + function: contextualize + args: + - 𝑒1 + - ⟦ 𝐵1, 𝜏1 ↦ ⟦ 𝐵2, 𝜏2 ↦ ∅, 𝐵3 ⟧(𝜏2 ↦ 𝑒1) * !t, 𝐵4 ⟧ diff --git a/resources/dc.yaml b/resources/dc.yaml new file mode 100644 --- /dev/null +++ b/resources/dc.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: DC +pattern: ⊥(𝜏 ↦ 𝑒) +result: ⊥ diff --git a/resources/dd.yaml b/resources/dd.yaml new file mode 100644 --- /dev/null +++ b/resources/dd.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: DD +pattern: ⊥.𝜏 +result: ⊥ diff --git a/resources/dot.yaml b/resources/dot.yaml new file mode 100644 --- /dev/null +++ b/resources/dot.yaml @@ -0,0 +1,14 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: DOT +pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧.𝜏 +result: 𝑒2(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧) +when: + nf: 𝑒1 +where: + - meta: 𝑒2 + function: contextualize + args: + - 𝑒1 + - ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧ diff --git a/resources/miss.yaml b/resources/miss.yaml new file mode 100644 --- /dev/null +++ b/resources/miss.yaml @@ -0,0 +1,14 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: 'MISS' +pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒) +result: ⊥ +when: + and: + - not: + in: + - 𝜏 + - 𝐵 + - not: + alpha: 𝜏 diff --git a/resources/null.yaml b/resources/null.yaml new file mode 100644 --- /dev/null +++ b/resources/null.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: 'NULL' +pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏 +result: ⊥ diff --git a/resources/over.yaml b/resources/over.yaml new file mode 100644 --- /dev/null +++ b/resources/over.yaml @@ -0,0 +1,11 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: OVER +pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2) +result: ⊥ +when: + not: + eq: + - 𝜏 + - ρ diff --git a/resources/phi.yaml b/resources/phi.yaml new file mode 100644 --- /dev/null +++ b/resources/phi.yaml @@ -0,0 +1,15 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: PHI +pattern: ⟦𝐵⟧.𝜏 +result: ⟦𝐵⟧.φ.𝜏 +when: + and: + - in: + - φ + - 𝐵 + - not: + in: + - 𝜏 + - 𝐵 diff --git a/resources/stay.yaml b/resources/stay.yaml new file mode 100644 --- /dev/null +++ b/resources/stay.yaml @@ -0,0 +1,6 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: STAY +pattern: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧(ρ ↦ 𝑒2) +result: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧ diff --git a/resources/stop.yaml b/resources/stop.yaml new file mode 100644 --- /dev/null +++ b/resources/stop.yaml @@ -0,0 +1,20 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: STOP +pattern: ⟦𝐵⟧.𝜏 +result: ⊥ +when: + and: + - not: + in: + - 𝜏 + - 𝐵 + - not: + in: + - φ + - 𝐵 + - not: + in: + - λ + - 𝐵 diff --git a/src/Misc.hs b/src/Misc.hs --- a/src/Misc.hs +++ b/src/Misc.hs @@ -38,8 +38,7 @@ withVoidRho bds = withVoidRho' bds False where withVoidRho' :: [Binding] -> Bool -> [Binding] - withVoidRho' [] True = [] - withVoidRho' [] False = [BiVoid AtRho] + withVoidRho' [] hasRho = [BiVoid AtRho | not hasRho] withVoidRho' (bd : bds) hasRho = case bd of BiMeta _ -> bd : bds diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs --- a/test/ConditionSpec.hs +++ b/test/ConditionSpec.hs @@ -17,12 +17,12 @@ import Printer (printSubstitutions) import System.FilePath import Test.Hspec (Spec, describe, expectationFailure, it, runIO) -import Yaml qualified as Y +import Yaml qualified data ConditionPack = ConditionPack { expression :: Expression, pattern :: Expression, - condition :: Y.Condition + condition :: Yaml.Condition } deriving (Generic, FromJSON, Show)