phino 0.0.101 → 0.0.102
raw patch · 7 files changed
+104/−41 lines, 7 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- phino.cabal +1/−1
- resources/dataization.yaml +11/−7
- resources/morphing.yaml +32/−5
- resources/normalize/phi.yaml +0/−16
- test/CLISpec.hs +14/−11
- test/DataizeSpec.hs +12/−0
- test/YamlSpec.hs +34/−1
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.101+version: 0.0.102 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
resources/dataization.yaml view
@@ -14,9 +14,13 @@ # ordered 'premises' reduce as stated. A premise binds its 'n-result'/'d-result' # to one judgment — 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('evaluate') # or 𝒞 ('contextualize'). 'e-match' is the universe-argument matcher of-# 𝔻(n, e); it is always the e meta. The single bytes result is named δ; derived-# terms are 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match'-# already binds it.+# 𝔻(n, e); it is always the e meta. The single bytes result is named δ. A+# normal-form-valued result (𝕄 'morph', 𝒩 'normalize') is named 𝑛, 𝑛1, … in+# premise order, skipping the bare 𝑛 only when 'match' already binds it; an+# expression-valued result (𝒞 'contextualize', 𝔼 'evaluate') is not a normal+# form — that is why a 'normalize' premise follows it — so it takes an 𝑒-family+# name (𝑒1, 𝑒2, …, the next index free of 'match', 𝑒 itself being the universe)+# rather than an 𝑛 name reserved for normal forms. # # The clauses are disjoint, so their relative order does not change behavior. # 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is@@ -43,12 +47,12 @@ - [Δ, λ] - [𝐵1, 𝐵2] premises:- - n-result: 𝑛+ - n-result: 𝑒2 contextualize: - 𝑒1 - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧ - n-result: 𝑛1- normalize: 𝑛+ normalize: 𝑒2 - d-result: δ dataize: 𝑛1 @@ -57,12 +61,12 @@ e-match: 𝑒 d-result: δ premises:- - n-result: 𝑛+ - n-result: 𝑒1 evaluate: - ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧ - 𝑒 - n-result: 𝑛1- normalize: 𝑛+ normalize: 𝑒1 - d-result: δ dataize: 𝑛1
resources/morphing.yaml view
@@ -19,9 +19,12 @@ # ordered 'premises' reduce as stated. A premise binds 'n-result' to the result # of one judgment — 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('evaluate'). 'e-match' is # the universe-argument matcher of 𝕄(n, e); usually the e meta, but a rule may-# pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). Derived terms are-# named 𝑛, 𝑛1, … in premise order; the bare 𝑛 is skipped only when 'match'-# already binds it.+# pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). A normal-form-valued+# result (𝕄 'morph', 𝒩 'normalize') is named 𝑛, 𝑛1, … in premise order, the bare+# 𝑛 skipped only when 'match' already binds it; an expression-valued result (𝔼+# 'evaluate') is not a normal form — that is why a 'normalize' premise follows+# it — so it takes an 𝑒-family name (𝑒1, 𝑒2, …, the next index free of 'match',+# 𝑒 itself being the universe) rather than an 𝑛 name reserved for normal forms. # # 'ml' and 'md' are kept mutually exclusive: 'md' fires only # when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation@@ -54,14 +57,38 @@ e-match: 𝑒 n-result: 𝑛2 premises:- - n-result: 𝑛+ - n-result: 𝑒1 evaluate: - '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧' - 𝑒 - n-result: 𝑛1- normalize: '𝑛.𝜏'+ normalize: '𝑒1.𝜏' - n-result: 𝑛2 morph: 𝑛1++- name: mphi+ label: \phi+ match: ⟦𝐵⟧.𝜏+ e-match: 𝑒+ n-result: 𝑛1+ when:+ and:+ - in:+ - φ+ - 𝐵+ - not:+ in:+ - 𝜏+ - 𝐵+ - not:+ in:+ - λ+ - 𝐵+ premises:+ - n-result: 𝑛+ normalize: ⟦𝐵⟧.φ.𝜏+ - n-result: 𝑛1+ morph: 𝑛 - name: md match: '𝑛.𝜏'
− resources/normalize/phi.yaml
@@ -1,16 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----name: phi-label: \phi-pattern: ⟦𝐵⟧.𝜏-result: ⟦𝐵⟧.φ.𝜏-when:- and:- - in:- - φ- - 𝐵- - not:- in:- - 𝜏- - 𝐵
test/CLISpec.hs view
@@ -1039,11 +1039,6 @@ , " { T }" , " { i = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }" , " { }"- , "\\phinoNormalizationRule[\\phi]{phi}"- , " { [[ B ]] . \\tau }"- , " { [[ B ]] . @ . \\tau }"- , " { @ \\in B \\;\\text{and}\\; \\tau \\notin B }"- , " { }" , "\\phinoNormalizationRule{stay}" , " { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] ( \\phiTerminal{\\rho} -> e_2 ) }" , " { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] }"@@ -1068,12 +1063,20 @@ , "\\begin{phinoMorphingInference}" , " \\phinoName{ml}" , " \\phinoLabel{\\lambda}"- , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n }{ s_2 } }"- , " \\phinoPremise{ \\phinoNormalize{ n . \\tau }{ n_1 } }"+ , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ e_1 }{ s_2 } }"+ , " \\phinoPremise{ \\phinoNormalize{ e_1 . \\tau }{ n_1 } }" , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_2 }{ n_2 }{ s_3 } }" , " \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_2 }{ s_3 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}"+ , " \\phinoName{mphi}"+ , " \\phinoLabel{\\phi}"+ , " \\phinoCondition{ @ \\in B \\;\\text{and}\\; \\tau \\notin B \\;\\text{and}\\; L \\notin B }"+ , " \\phinoPremise{ \\phinoNormalize{ [[ B ]] . @ . \\tau }{ n } }"+ , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"+ , " \\phinoConclusion{ \\phinoMorph{ [[ B ]] . \\tau }{ e }{ s_1 }{ n_1 }{ s_2 } }"+ , "\\end{phinoMorphingInference}"+ , "\\begin{phinoMorphingInference}" , " \\phinoName{md}" , " \\phinoCondition{ \\phinoNotFormation{ n } }" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"@@ -1144,15 +1147,15 @@ , "\\begin{phinoDataizationInference}" , " \\phinoName{box}" , " \\phinoCondition{ [ D \\char44{} L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }"- , " \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ n } }"- , " \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }"+ , " \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ e_2 } }"+ , " \\phinoPremise{ \\phinoNormalize{ e_2 }{ n_1 } }" , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_1 }{ \\delta }{ s_2 } }" , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }" , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" , " \\phinoName{fire}"- , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n }{ s_2 } }"- , " \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }"+ , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ e_1 }{ s_2 } }"+ , " \\phinoPremise{ \\phinoNormalize{ e_1 }{ n_1 } }" , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }" , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_3 } }" , "\\end{phinoDataizationInference}"
test/DataizeSpec.hs view
@@ -388,4 +388,16 @@ ] , BtMany ["40", "14", "00", "00", "00", "00", "00", "00"] )+ , -- Dispatching an absent attribute on a φ-decorated formation now resolves+ -- the inherited attribute through morphing 'mphi' (#973): PHI used to be a+ -- normalization rule, but following the decoration is a semantic 𝕄 step,+ -- so it moved into 'morphing.yaml'. Here '.t' is missing from the outer+ -- formation, so 𝕄 walks the '@' decoration to the parent that defines 't'+ -- and dataizes its datum.++ ( "InheritedThroughPhi"+ , "Q"+ , "[[ @ -> [[ t -> [[ D> 2A- ]] ]] ]].t"+ , BtOne "2A"+ ) ]
test/YamlSpec.hs view
@@ -16,7 +16,7 @@ import Files (allPathsIn) import System.FilePath import Test.Hspec (Spec, describe, it, runIO, shouldBe, shouldReturn, shouldSatisfy, shouldThrow)-import Yaml (ContextualizeRule (..), DataizeRule (..), MorphRule (..), contextualizationRules, dataizationRules, morphingRules, yamlRule)+import Yaml (ContextualizeRule (..), DataizeRule (..), MorphRule (..), Operation (..), Premise (..), contextualizationRules, dataizationRules, morphingRules, yamlRule) spec :: Spec spec = do@@ -73,3 +73,36 @@ ++ map (\DataizeRule{name, label} -> fromMaybe name label) dataizationRules ++ map (\ContextualizeRule{name, label} -> fromMaybe name label) contextualizationRules (labels \\ nub labels) `shouldBe` []++ describe "reserves 𝑛-family metas for normal forms" $+ -- 𝒞 ('contextualize') and 𝔼 ('evaluate') return an expression that is not+ -- necessarily a normal form — that is why a 'normalize' premise follows+ -- them — so binding their result to an 𝑛-reserved meta (internal prefix+ -- "n") in a morphing or dataization rule conflates the calculus's 'e'+ -- (expression) with 'n' (normal form). Such a slip is notational, not+ -- functional (the meta name is only a substitution-map key), so it is easy+ -- to miss by eye; flag it automatically instead. Contextualization is+ -- excluded on purpose: its 𝒞-valued results are the point and its header+ -- reserves nothing (see #971).+ it "no contextualize/evaluate premise in a morphing or dataization rule binds an 𝑛-reserved meta" $ do+ let expressionValued :: Operation -> Bool+ expressionValued OpContextualize{} = True+ expressionValued OpEvaluate{} = True+ expressionValued _ = False+ verbOf :: Operation -> String+ verbOf OpContextualize{} = "contextualize"+ verbOf OpEvaluate{} = "evaluate"+ verbOf _ = "?"+ premisesOf :: [(String, [Premise])]+ premisesOf =+ map (\MorphRule{name, premises} -> (name, premises)) morphingRules+ ++ map (\DataizeRule{name, premises} -> (name, premises)) dataizationRules+ offenders :: [String]+ offenders =+ [ ruleName ++ ": " ++ verbOf operation ++ " result '" ++ T.unpack result ++ "'"+ | (ruleName, premises) <- premisesOf+ , Premise{result, operation} <- premises+ , expressionValued operation+ , T.isPrefixOf (T.pack "n") result+ ]+ offenders `shouldBe` []