phino 0.0.91 → 0.0.92
raw patch · 5 files changed
+43/−31 lines, 5 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ CST: BT_PIPED :: BYTES -> BYTES
Files
- phino.cabal +1/−1
- src/CST.hs +1/−0
- src/LaTeX.hs +14/−4
- src/Render.hs +2/−1
- test/CLISpec.hs +25/−25
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.91+version: 0.0.92 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
src/CST.hs view
@@ -74,6 +74,7 @@ | BT_ONE String | BT_MANY [String] | BT_META META+ | BT_PIPED BYTES -- bytes wrapped in vertical pipes, as the eolang LaTeX package expects deriving (Eq, Show) data META_HEAD
src/LaTeX.hs view
@@ -297,8 +297,8 @@ toLaTeX mh = mh instance ToLaTeX BYTES where- toLaTeX (BT_META meta) = BT_META (toLaTeX meta)- toLaTeX bts = bts+ toLaTeX (BT_META meta) = BT_PIPED (BT_META (toLaTeX meta))+ toLaTeX bts = BT_PIPED bts instance ToLaTeX APP_ARG where toLaTeX APP_ARG{..} = APP_ARG (toLaTeX expr) (toLaTeX args)@@ -382,7 +382,7 @@ rule.label rule.when premises- (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (stateName 1) (stateName final) (renderExpr rule.nresult))+ (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (conclusionStateName final 1) (conclusionStateName final final) (renderExpr rule.nresult)) where (premises, final) = premisesToLatex rule.premises @@ -397,7 +397,7 @@ rule.label rule.when premises- (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (stateName 1) (stateName final) (renderBytes rule.dresult))+ (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (conclusionStateName final 1) (conclusionStateName final final) (renderBytes rule.dresult)) where (premises, final) = premisesToLatex rule.premises @@ -418,6 +418,16 @@ -- n/n_1 convention used for terms. stateName :: Int -> String stateName n = "s_" ++ show n++-- The state name for a rule's conclusion. The subscript exists only to+-- distinguish the several states threaded through a rule's premises; when a+-- rule threads a single state ('final' == 1) it carries no information, so the+-- conclusion drops it and renders a bare 's'. Otherwise it keeps the+-- subscripted form (s_1 … s_final) shared with the premises.+conclusionStateName :: Int -> Int -> String+conclusionStateName final index+ | final == 1 = "s"+ | otherwise = stateName index -- Render a rule's premises in order, threading the state through them. The rule -- starts in state s_1; each state-changing premise (𝕄, 𝔻, 𝔼) consumes the
src/Render.hs view
@@ -107,6 +107,7 @@ render (BT_ONE bte) = render bte <> "-" render (BT_MANY bts) = T.intercalate "-" (map render bts) render (BT_META mt) = render mt+ render (BT_PIPED bts) = "|" <> render bts <> "|" instance Render EXCLAMATION where render EXCL = "!"@@ -284,7 +285,7 @@ render ARG_BYTES{..} = render bytes instance Render EXTRA where- render EXTRA{func = "contextualize", args = arg : rest, ..} = render meta <> " \\coloneqq \\ctx{ " <> render arg <> " }{ " <> T.intercalate ", " (map render rest) <> " }"+ render EXTRA{func = "contextualize", args = arg : rest, ..} = "\\phinoContextualize{ " <> render arg <> " }{ " <> T.intercalate ", " (map render rest) <> " }{ " <> render meta <> " }" -- 𝕄 carries the universe and threads a state, 𝕄(n, e, s_1), so a 'morph' extra -- renders with the universe metavariable 'e' and the incoming state 's_1' as its -- trailing arguments. This is a one-off application binding only 'meta', so the
test/CLISpec.hs view
@@ -556,12 +556,12 @@ ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress", "--meet-prefix=foo"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{foo:1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{foo:1}{ [[ D> |42-| ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}" , " \\leadsto \\Big\\{ \\phinoMeet{foo:2}{ [[ |x| -> \\phinoAgain{foo:1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}" , " \\leadsto \\Big\\{ \\phinoAgain{foo:2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}" , " \\leadsto \\Big\\{ \\phinoAgain{foo:1} ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2}, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"- , " \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] \\Big\\}{.}"+ , " \\leadsto \\Big\\{ [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"+ , " \\leadsto \\Big\\{ [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -572,12 +572,12 @@ ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phinoMeet{1}{ [[ D> |42-| ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}" , " \\leadsto \\Big\\{ \\phinoMeet{2}{ [[ |x| -> \\phinoAgain{1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}" , " \\leadsto \\Big\\{ \\phinoAgain{2} . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}" , " \\leadsto \\Big\\{ \\phinoAgain{1} ( \\phiTerminal{\\rho} -> \\phinoAgain{2}, \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"- , " \\leadsto \\Big\\{ [[ D> 42-, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] \\Big\\}{.}"+ , " \\leadsto \\Big\\{ [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"+ , " \\leadsto \\Big\\{ [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{2} ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -878,11 +878,11 @@ [ intercalate "\n" [ "\\begin{phiquation}"- , "\\Big\\{ [[ @ -> [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\Big\\} \\leadsto_{\\nameref{r:contextualize}}"- , " \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"- , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}"+ , "\\Big\\{ [[ @ -> [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\Big\\} \\leadsto_{\\nameref{r:contextualize}}"+ , " \\leadsto \\Big\\{ [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"+ , " \\leadsto \\Big\\{ [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ D> |01-|, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ]] \\Big\\}{.}" , "\\end{phiquation}" , "01-" ]@@ -1007,7 +1007,7 @@ , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" , " { e ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }" , " { }"- , " { e \\coloneqq \\ctx{ n }{ [[ B_1, \\tau -> n, B_2 ]] } }"+ , " { \\phinoContextualize{ n }{ [[ B_1, \\tau -> n, B_2 ]] }{ e } }" , "\\phinoNormalizationRule{miss}" , " { [[ B ]] ( \\tau -> e ) }" , " { T }"@@ -1047,7 +1047,7 @@ [ unlines [ "\\begin{phinoMorphingInference}" , " \\phinoName{mf}"- , " \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s_1 }{ [[ B ]] }{ s_1 } }"+ , " \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s }{ [[ B ]] }{ s } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{ml}"@@ -1088,15 +1088,15 @@ , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{dead}"- , " \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s_1 }{ T }{ s_1 } }"+ , " \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s }{ T }{ s } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{xi}"- , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ T }{ s_1 } }"+ , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s }{ T }{ s } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{mg}"- , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ T }{ s_1 } }"+ , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s }{ T }{ s } }" , "\\end{phinoMorphingInference}" ] ]@@ -1108,38 +1108,38 @@ [ "\\begin{phinoDataizationInference}" , " \\phinoName{delta}" , " \\phinoLabel{\\Delta}"- , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_1 } }"+ , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> |\\delta|, B_2 ]] }{ e }{ s }{ |\\delta| }{ s } }" , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" , " \\phinoName{box}" , " \\phinoCondition{ [ D, 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{ \\phinoDataize{ n_1 }{ e }{ s_1 }{ \\delta }{ s_2 } }"- , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"+ , " \\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{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }"- , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_3 } }"+ , " \\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}" , "\\begin{phinoDataizationInference}" , " \\phinoName{none}" , " \\phinoCondition{ [ D, L, @ ] \\cap \\lparen B \\rparen = \\emptyset }"- , " \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ -- }{ s_1 } }"+ , " \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s }{ |--| }{ s } }" , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" , " \\phinoName{end}"- , " \\phinoConclusion{ \\phinoDataize{ T }{ e }{ s_1 }{ -- }{ s_1 } }"+ , " \\phinoConclusion{ \\phinoDataize{ T }{ e }{ s }{ |--| }{ s } }" , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" , " \\phinoName{norm}" , " \\phinoCondition{ \\phinoNotFormation{ n } \\;\\text{and}\\; n \\not= T }" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"- , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }"- , " \\phinoConclusion{ \\phinoDataize{ n }{ e }{ s_1 }{ \\delta }{ s_3 } }"+ , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ |\\delta| }{ s_3 } }"+ , " \\phinoConclusion{ \\phinoDataize{ n }{ e }{ s_1 }{ |\\delta| }{ s_3 } }" , "\\end{phinoDataizationInference}" ] ]