phino 0.0.98 → 0.0.99
raw patch · 5 files changed
+67/−10 lines, 5 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- phino.cabal +1/−1
- resources/morphing.yaml +33/−4
- src/Render.hs +2/−1
- test/CLISpec.hs +14/−4
- test/DataizeSpec.hs +17/−0
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.98+version: 0.0.99 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
resources/morphing.yaml view
@@ -27,6 +27,19 @@ # when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation # head — λ-bearing or not — is left to 'ml' (and 'mf'). The two clauses # are disjoint and their relative order does not change behavior.+#+# 'ma'/'maa' and 'mad'/'maad' partition application-headed normal forms on+# the argument's absoluteness (#959). Both pairs pin the argument to a+# normal-form meta, so the split is total over the normal forms 𝕄 actually+# sees: 'ma'/'maa' take a '𝑘' argument — absolute (xi-free) and in normal+# form — and recurse by re-normalizing the application; 'mad'/'maad' take an+# '𝑛' argument (a normal form) that is 'not (absolute 𝑛1)' and yield ⊥ with+# no recursion. A non-absolute argument can never fill a slot, so ⊥ is the+# correct outcome and morphing stays total: exactly one of the four fires,+# and the ⊥ axioms add no regress. Without them, a void slot receiving a+# non-absolute argument — e.g. ⟦ x ↦ ∅ ⟧( x ↦ ξ.foo ) — had no terminating+# derivation: 'copy' cannot fire on a non-absolute argument, so 'ma'+# re-morphed the identical stuck term forever. - name: mf match: ⟦𝐵⟧@@ -64,28 +77,44 @@ morph: 𝑛2 - name: ma- match: '𝑛(𝜏 ↦ 𝑒1)'+ match: '𝑛(𝜏 ↦ 𝑘1)' e-match: 𝑒 n-result: 𝑛3 premises: - n-result: 𝑛1 morph: 𝑛 - n-result: 𝑛2- normalize: '𝑛1(𝜏 ↦ 𝑒1)'+ normalize: '𝑛1(𝜏 ↦ 𝑘1)' - n-result: 𝑛3 morph: 𝑛2 - name: maa- match: '𝑛(α𝑖 ↦ 𝑒1)'+ match: '𝑛(α𝑖 ↦ 𝑘1)' e-match: 𝑒 n-result: 𝑛3 premises: - n-result: 𝑛1 morph: 𝑛 - n-result: 𝑛2- normalize: '𝑛1(α𝑖 ↦ 𝑒1)'+ normalize: '𝑛1(α𝑖 ↦ 𝑘1)' - n-result: 𝑛3 morph: 𝑛2++- name: mad+ match: '𝑛(𝜏 ↦ 𝑛1)'+ e-match: 𝑒+ n-result: ⊥+ when:+ not:+ absolute: 𝑛1++- name: maad+ match: '𝑛(α𝑖 ↦ 𝑛1)'+ e-match: 𝑒+ n-result: ⊥+ when:+ not:+ absolute: 𝑛1 - name: universe label: \Phi
src/Render.hs view
@@ -263,7 +263,8 @@ renderWrapped cond@CO_LOGIC{} = "\\lparen " <> render cond <> " \\rparen" renderWrapped cond = render cond render CO_NF{..} = "\\isnormal{ " <> render expr <> " }"- render CO_ABSOLUTE{..} = render expr <> " " <> render belongs <> " \\mathcal{K}"+ render CO_ABSOLUTE{belongs = NOT_IN, ..} = "\\phinoNotAbsolute{ " <> render expr <> " }"+ render CO_ABSOLUTE{..} = "\\phinoAbsolute{ " <> render expr <> " }" render CO_NOT{condition = CO_FORMATION{..}} = "\\phinoNotFormation{ " <> render expr <> " }" render CO_NOT{..} = renderFunc "not" condition render CO_COMPARE{..} = render left <> " " <> render equal <> " " <> render right
test/CLISpec.hs view
@@ -1078,16 +1078,26 @@ , "\\begin{phinoMorphingInference}" , " \\phinoName{ma}" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"- , " \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau -> e_1 ) }{ n_2 } }"+ , " \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau -> k_1 ) }{ n_2 } }" , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"- , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> e_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"+ , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> k_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{maa}" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"- , " \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ n_2 } }"+ , " \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> k_1 ) }{ n_2 } }" , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"- , " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"+ , " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> k_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"+ , "\\end{phinoMorphingInference}"+ , "\\begin{phinoMorphingInference}"+ , " \\phinoName{mad}"+ , " \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"+ , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e }{ s }{ T }{ s } }"+ , "\\end{phinoMorphingInference}"+ , "\\begin{phinoMorphingInference}"+ , " \\phinoName{maad}"+ , " \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"+ , " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e }{ s }{ T }{ s } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{universe}"
test/DataizeSpec.hs view
@@ -68,6 +68,16 @@ , ExFormation [BiTau (AtLabel "x") (ExFormation [])] , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])] )+ , -- A void slot fed a non-absolute argument can never be filled, so 'copy'+ -- cannot fire and the application is a stuck normal form. Before #959,+ -- 'ma' re-morphed this identical term forever; now the 'mad' axiom+ -- morphs it straight to ⊥, keeping 𝕄 total.++ ( "[[ x -> ? ]](x -> $.foo) => T"+ , ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo")))+ , ExRoot+ , ExTermination+ ) ] -- 'defaultDataizeContext' runs with '_shuffle' on, so 'morph' walks the@@ -197,6 +207,13 @@ `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException)) failsOn "throws on ⊥ instead of mapping it to empty bytes" ExTermination failsOn "throws on a data-less formation, which dataizes ⊥" (ExFormation [])+ -- A void slot fed a non-absolute argument morphs to ⊥ via 'mad' (#959) and+ -- then fails through the same terminator path. The regression is that this+ -- test terminates at all: before the fix 'ma' re-morphed the stuck term+ -- forever and dataization never returned.+ failsOn+ "throws on a void slot fed a non-absolute argument instead of looping forever"+ (ExApplication (ExFormation [BiVoid (AtLabel "x")]) (ArTau (AtLabel "x") (ExDispatch ExXi (AtLabel "foo")))) describe "labels every step with a defined rule or operation" $ do let verb op = case op of