phino 0.0.0.63 → 0.0.0.64
raw patch · 16 files changed
+34/−35 lines, 16 files
Files
- README.md +6/−6
- phino.cabal +1/−1
- resources/alpha.yaml +1/−1
- resources/copy.yaml +1/−1
- resources/dc.yaml +1/−1
- resources/dd.yaml +1/−1
- resources/dot.yaml +1/−1
- resources/miss.yaml +1/−1
- resources/null.yaml +1/−1
- resources/over.yaml +1/−1
- resources/phi.yaml +1/−1
- resources/stay.yaml +1/−1
- resources/stop.yaml +1/−1
- src/Rewriter.hs +1/−2
- src/Rule.hs +1/−1
- test/CLISpec.hs +14/−14
README.md view
@@ -29,7 +29,7 @@ ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.0.62+cabal install --overwrite-policy=always phino-0.0.0.63 phino --version ``` @@ -195,23 +195,23 @@ ```bash $ phino explain --normalize \begin{tabular}{rl}-\trrule{ALPHA}+\trrule{alpha} { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_2 -> e ) } { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_1 -> e ) }- { if $ \indexof{ \tau_2 } = |B_1| $ }+ { if $ \indexof{ \tau_2 } = \vert B_1 \vert $ } { }-\trrule{COPY}+\trrule{copy} { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e_1 ) } { [[ B_1, \tau -> e_3, B_2 ]] } { if $ \isnormal{ e_1 } $ } { where $ e_2 \coloneqq \scopeof{ e_1 } $ and $ e_3 \coloneqq \ctx{ e_1 }{ e_2 } $ }-\trrule{DC}+\trrule{dc} { T ( \tau -> e ) } { T } { } { } ...-\trrule{STOP}+\trrule{stop} { [[ B ]] . \tau } { T } { if $ \tau \notin B \;\text{and}\; @ \notin B \;\text{and}\; L \notin B $ }
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.0.63+version: 0.0.0.64 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
resources/alpha.yaml view
@@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: ALPHA+name: alpha pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒) result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒) when:
resources/copy.yaml view
@@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: COPY+name: copy pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒1) result: ⟦ 𝐵1, 𝜏 ↦ 𝑒3, 𝐵2 ⟧ when:
resources/dc.yaml view
@@ -1,6 +1,6 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: DC+name: dc pattern: ⊥(𝜏 ↦ 𝑒) result: ⊥
resources/dd.yaml view
@@ -1,6 +1,6 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: DD+name: dd pattern: ⊥.𝜏 result: ⊥
resources/dot.yaml view
@@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: DOT+name: dot pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧.𝜏 result: 𝑒2(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧) when:
resources/miss.yaml view
@@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: MISS+name: miss pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒) result: ⊥ when:
resources/null.yaml view
@@ -1,6 +1,6 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: 'NULL'+name: 'null' pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏 result: ⊥
resources/over.yaml view
@@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: OVER+name: over pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2) result: ⊥ when:
resources/phi.yaml view
@@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: PHI+name: phi pattern: ⟦𝐵⟧.𝜏 result: ⟦𝐵⟧.φ.𝜏 when:
resources/stay.yaml view
@@ -1,6 +1,6 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: STAY+name: stay pattern: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧(ρ ↦ 𝑒2) result: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧
resources/stop.yaml view
@@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----name: STOP+name: stop pattern: ⟦𝐵⟧.𝜏 result: ⊥ when:
src/Rewriter.hs view
@@ -13,7 +13,6 @@ import AST import Builder import Control.Exception (Exception, throwIO)-import Data.Char (toLower) import Data.Maybe (fromMaybe) import qualified Data.Set as Set import Deps@@ -180,7 +179,7 @@ where leadsTo :: Program -> [Rewritten] leadsTo _prog = case _rewrittens of- (program, _) : rest -> (_prog, Nothing) : (program, Just (map toLower (fromMaybe "unknown" (Y.name rule)))) : rest+ (program, _) : rest -> (_prog, Nothing) : (program, Just (fromMaybe "unknown" (Y.name rule))) : rest [] -> [(_prog, Nothing)] -- Rewrite program by provided locator from RewriteContext
src/Rule.hs view
@@ -292,7 +292,7 @@ logDebug "The 'when' condition wasn't met" pure [] else do- logDebug (printf "Rule %s" (fromMaybe "unknown" (Y.name rule)))+ logDebug (printf "Rule %s" name) extended <- extraSubstitutions when' (Y.where_ rule) ctx if null extended then do
test/CLISpec.hs view
@@ -723,7 +723,7 @@ ["rewrite", "--log-level=debug", "--log-lines=1", "--normalize"] [ intercalate "\n"- [ "[DEBUG]: Applied 'COPY' (44 nodes -> 39 nodes)"+ [ "[DEBUG]: Applied 'copy' (44 nodes -> 39 nodes)" , "---| log is limited by --log-lines=1 option |---" ] ]@@ -821,7 +821,7 @@ ["explain", "--rule=resources/copy.yaml"] [ unlines [ "\\begin{tabular}{rl}"- , "\\trrule{COPY}"+ , "\\trrule{copy}" , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }" , " { [[ B_1, \\tau -> e_3, B_2 ]] }" , " { if $ \\isnormal{ e_1 } $ }"@@ -833,64 +833,64 @@ it "explains multiple rules" $ testCLISucceeded ["explain", "--rule=resources/copy.yaml", "--rule=resources/alpha.yaml"]- ["\\begin{tabular}{rl}", "\\trrule{COPY}", "\\trrule{ALPHA}"]+ ["\\begin{tabular}{rl}", "\\trrule{copy}", "\\trrule{alpha}"] it "explains normalization rules" $ testCLISucceeded ["explain", "--normalize"] [ unlines [ "\\begin{tabular}{rl}"- , "\\trrule{ALPHA}"+ , "\\trrule{alpha}" , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_2 -> e ) }" , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e ) }" , " { if $ \\indexof{ \\tau_2 } = \\vert B_1 \\vert $ }" , " { }"- , "\\trrule{COPY}"+ , "\\trrule{copy}" , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }" , " { [[ B_1, \\tau -> e_3, B_2 ]] }" , " { if $ \\isnormal{ e_1 } $ }" , " { where $ e_2 \\coloneqq \\scopeof{ e_1 } $ and $ e_3 \\coloneqq \\ctx{ e_1 }{ e_2 } $ }"- , "\\trrule{DC}"+ , "\\trrule{dc}" , " { T ( \\tau -> e ) }" , " { T }" , " { }" , " { }"- , "\\trrule{DD}"+ , "\\trrule{dd}" , " { T . \\tau }" , " { T }" , " { }" , " { }"- , "\\trrule{DOT}"+ , "\\trrule{dot}" , " { [[ B_1, \\tau -> e_1, B_2 ]] . \\tau }" , " { e_2 ( ^ -> [[ B_1, \\tau -> e_1, B_2 ]] ) }" , " { if $ \\isnormal{ e_1 } $ }" , " { where $ e_2 \\coloneqq \\ctx{ e_1 }{ [[ B_1, \\tau -> e_1, B_2 ]] } $ }"- , "\\trrule{MISS}"+ , "\\trrule{miss}" , " { [[ B ]] ( \\tau -> e ) }" , " { T }" , " { if $ \\tau \\notin B \\;\\text{and}\\; \\tau \\notin [ ~0, ~1, \\dots ] $ }" , " { }"- , "\\trrule{NULL}"+ , "\\trrule{null}" , " { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }" , " { T }" , " { }" , " { }"- , "\\trrule{OVER}"+ , "\\trrule{over}" , " { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }" , " { T }" , " { if $ \\tau \\not= ^ $ }" , " { }"- , "\\trrule{PHI}"+ , "\\trrule{phi}" , " { [[ B ]] . \\tau }" , " { [[ B ]] . @ . \\tau }" , " { if $ @ \\in B \\;\\text{and}\\; \\tau \\notin B $ }" , " { }"- , "\\trrule{STAY}"+ , "\\trrule{stay}" , " { [[ B_1, ^ -> e_1, B_2 ]] ( ^ -> e_2 ) }" , " { [[ B_1, ^ -> e_1, B_2 ]] }" , " { }" , " { }"- , "\\trrule{STOP}"+ , "\\trrule{stop}" , " { [[ B ]] . \\tau }" , " { T }" , " { if $ \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B $ }"