diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -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 diff --git a/resources/dataization.yaml b/resources/dataization.yaml --- a/resources/dataization.yaml +++ b/resources/dataization.yaml @@ -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 diff --git a/resources/morphing.yaml b/resources/morphing.yaml --- a/resources/morphing.yaml +++ b/resources/morphing.yaml @@ -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: '๐‘›.๐œ' diff --git a/resources/normalize/phi.yaml b/resources/normalize/phi.yaml deleted file mode 100644 --- a/resources/normalize/phi.yaml +++ /dev/null @@ -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: - - ๐œ - - ๐ต diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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}" diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -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" + ) ] diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs --- a/test/YamlSpec.hs +++ b/test/YamlSpec.hs @@ -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` []