phino 0.0.95 → 0.0.96
raw patch · 9 files changed
+52/−21 lines, 9 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- README.md +1/−1
- phino.cabal +1/−1
- resources/dataization.yaml +4/−1
- resources/morphing.yaml +8/−2
- resources/normalize/dl.yaml +5/−5
- src/Dataize.hs +11/−2
- src/Render.hs +7/−3
- test/CLISpec.hs +9/−6
- test/DataizeSpec.hs +6/−0
README.md view
@@ -34,7 +34,7 @@ ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.81+cabal install --overwrite-policy=always phino-0.0.95 phino --version ```
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.95+version: 0.0.96 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
@@ -67,11 +67,14 @@ - name: none match: ⟦𝐵⟧ e-match: 𝑒- d-result: '--'+ d-result: δ when: disjoint: - [Δ, λ, φ] - [𝐵]+ premises:+ - d-result: δ+ dataize: ⊥ - name: end match: ⊥
resources/morphing.yaml view
@@ -110,9 +110,15 @@ - name: xi match: ξ e-match: 𝑒- n-result: ⊥+ n-result: 𝑛+ premises:+ - n-result: 𝑛+ morph: ⊥ - name: mg match: Φ e-match: Φ- n-result: ⊥+ n-result: 𝑛+ premises:+ - n-result: 𝑛+ morph: ⊥
resources/normalize/dl.yaml view
@@ -2,13 +2,13 @@ # SPDX-License-Identifier: MIT --- name: dl-pattern: ⟦𝐵⟧+pattern: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧ result: ⊥ when:- and:+ or: - in: - Δ- - 𝐵+ - 𝐵1 - in:- - λ- - 𝐵+ - Δ+ - 𝐵2
src/Dataize.hs view
@@ -161,7 +161,8 @@ -- ternary, 𝔻(n, e, s): besides the term 'n' it takes the universe 'e' ('univ'), -- which it forwards to 𝕄, and the mutable state 's', returning the bytes together -- with the new state. Its rules come from 'dataization.yaml': 'delta' yields the--- asset bytes, 'none' (a formation) and 'end' (⊥) yield empty bytes (--),+-- asset bytes, 'end' (⊥) yields empty bytes (--) and 'none' (a formation with no+-- Δ/λ/φ) delegates to 'end' by dataizing ⊥, -- 'box' contextualizes the φ-body and keeps dataizing (its step is labelled by -- its 'contextualize' side-computation), and 'norm' reduces through morphing, -- splicing the morphing steps into the chain. The clauses are disjoint (see@@ -215,11 +216,14 @@ built <- buildExpressionThrows inner final ((morphed', seq'), state'') <- morph (built, seq) univ state' ctx dataize' (morphed', seq') univ state'' ctx+ -- 𝔻(⊥) (the 'none' rule) hands a literal term straight to 𝔻 with no+ -- producing side-computation, so the transition to that term is labelled+ -- by the conclusion's own verb ('dataize') rather than a side premise. _ -> do let side = rule.premises `excluding` [concl] (final, state') <- sides side subst built <- buildExpressionThrows arg final- seq' <- leadsTo seq (labelOf side) built ctx+ seq' <- leadsTo seq (labelOr (verb concl.operation) side) built ctx dataize' (built, seq') univ state' ctx Just _ -> throwIO (userError (printf "dataization rule '%s' must conclude with a 'dataize' premise" rule.name)) sides :: [Y.Premise] -> Subst -> IO (Subst, State)@@ -229,6 +233,11 @@ labelOf :: [Y.Premise] -> String labelOf (premise : _) = verb premise.operation labelOf [] = ""+ -- As 'labelOf', but falls back to the given label when there is no+ -- side-computation to name the step (the 'none' rule's 𝔻(⊥) premise).+ labelOr :: String -> [Y.Premise] -> String+ labelOr _ premises@(_ : _) = labelOf premises+ labelOr fallback [] = fallback -- The premise binding the given expression meta, if any. The conclusion of a -- morphing rule and the argument of a continuation premise are looked up here to
src/Render.hs view
@@ -273,9 +273,13 @@ render CO_DISJOINT{..} = "[ " <> T.intercalate " \\char44{} " (map render attrs)- <> " ] \\cap \\lparen "- <> T.intercalate " \\cup " (map render groups)- <> " \\rparen = \\emptyset"+ <> " ] \\cap "+ <> renderGroups groups+ <> " = \\emptyset"+ where+ renderGroups :: [BINDING] -> Text+ renderGroups [group] = render group+ renderGroups gs = "\\lparen " <> T.intercalate " \\cup " (map render gs) <> " \\rparen" render CO_EMPTY = "" renderFunc :: Render a => Text -> a -> Text
test/CLISpec.hs view
@@ -1004,9 +1004,9 @@ , " { }" , " { }" , "\\phinoNormalizationRule{dl}"- , " { [[ B ]] }"+ , " { [[ B_1, L> F, B_2 ]] }" , " { T }"- , " { D \\in B \\;\\text{and}\\; L \\in B }"+ , " { D \\in B_1 \\;\\text{or}\\; D \\in B_2 }" , " { }" , "\\phinoNormalizationRule{dot}" , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"@@ -1097,11 +1097,13 @@ , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{xi}"- , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s }{ T }{ s } }"+ , " \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"+ , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ n }{ s_2 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{mg}"- , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s }{ T }{ s } }"+ , " \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"+ , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n }{ s_2 } }" , "\\end{phinoMorphingInference}" ] ]@@ -1132,8 +1134,9 @@ , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" , " \\phinoName{none}"- , " \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap \\lparen B \\rparen = \\emptyset }"- , " \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s }{ |--| }{ s } }"+ , " \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B = \\emptyset }"+ , " \\phinoPremise{ \\phinoDataize{ T }{ e }{ s_1 }{ \\delta }{ s_2 } }"+ , " \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }" , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" , " \\phinoName{end}"
test/DataizeSpec.hs view
@@ -261,6 +261,12 @@ it "dataizes a located reference through the expected rules" $ do labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]" labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf"]+ -- The 'none' rule no longer emits '--' itself: it delegates to 'end' by+ -- dataizing ⊥, so the empty formation reduces through one labelled 'dataize'+ -- step (𝔻(⟦⟧) → 𝔻(⊥)) before 'end' yields the empty bytes (#942).+ it "dataizes an empty formation by delegating to end" $ do+ labels <- labelsOf "Q" "Q -> [[ ]]"+ labels `shouldBe` ["dataize"] testDataize [