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.98 +version: 0.0.99 license: MIT synopsis: Command-Line Manipulator of πœ‘-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/morphing.yaml b/resources/morphing.yaml --- a/resources/morphing.yaml +++ b/resources/morphing.yaml @@ -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 diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -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 diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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}" diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -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