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.91 +version: 0.0.92 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -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 diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -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 diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -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 diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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}" ] ]