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.90 +version: 0.0.91 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -484,25 +484,21 @@ -- 𝕄, 𝔻 and 𝔼 carry the universe and thread the state from 'sIn' to a new -- 'sOut', 𝕄(input, e, sIn) ⟿ ⟨output, sOut⟩, so they render with the universe --- and incoming state as the middle arguments and a paired conclusion: --- \phinoMorph{ input }{ e }{ sIn }{ ⟨output, sOut⟩ }. 𝒩 and 𝒞 carry neither +-- and incoming state as the middle arguments and the new term and outgoing +-- state as the last two arguments: +-- \phinoMorph{ input }{ e }{ sIn }{ output }{ sOut }. 𝒩 and 𝒞 carry neither -- universe nor state. phinoMorph :: String -> String -> String -> String -> String -> String -phinoMorph input univ sIn sOut output = printf "\\phinoMorph{ %s }{ %s }{ %s }{ %s }" input univ sIn (paired output sOut) +phinoMorph input univ sIn sOut output = printf "\\phinoMorph{ %s }{ %s }{ %s }{ %s }{ %s }" input univ sIn output sOut phinoDataize :: String -> String -> String -> String -> String -> String -phinoDataize input univ sIn sOut output = printf "\\phinoDataize{ %s }{ %s }{ %s }{ %s }" input univ sIn (paired output sOut) +phinoDataize input univ sIn sOut output = printf "\\phinoDataize{ %s }{ %s }{ %s }{ %s }{ %s }" input univ sIn output sOut phinoNormalize :: String -> String -> String phinoNormalize input = printf "\\phinoNormalize{ %s }{ %s }" input phinoEvaluate :: String -> String -> String -> String -> String -> String -phinoEvaluate input univ sIn sOut output = printf "\\phinoEvaluate{ %s }{ %s }{ %s }{ %s }" input univ sIn (paired output sOut) - --- The state-passing functions 𝕄, 𝔻 and 𝔼 return a pair ⟨output, state⟩, the --- new value alongside the threaded state. -paired :: String -> String -> String -paired output state = printf "\\langle %s, %s \\rangle" output state +phinoEvaluate input univ sIn sOut output = printf "\\phinoEvaluate{ %s }{ %s }{ %s }{ %s }{ %s }" input univ sIn output sOut phinoContextualize :: String -> String -> String -> String phinoContextualize input context = printf "\\phinoContextualize{ %s }{ %s }{ %s }" input context diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -1047,56 +1047,56 @@ [ unlines [ "\\begin{phinoMorphingInference}" , " \\phinoName{mf}" - , " \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s_1 }{ \\langle [[ B ]], s_1 \\rangle } }" + , " \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s_1 }{ [[ B ]] }{ s_1 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{ml}" , " \\phinoLabel{\\lambda}" - , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\langle n, s_2 \\rangle } }" + , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n }{ s_2 } }" , " \\phinoPremise{ \\phinoNormalize{ n . \\tau }{ n_1 } }" - , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_2 }{ \\langle n_2, s_3 \\rangle } }" - , " \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ \\langle n_2, s_3 \\rangle } }" + , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_2 }{ n_2 }{ s_3 } }" + , " \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_2 }{ s_3 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{md}" , " \\phinoCondition{ \\phinoNotFormation{ n } }" - , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }" + , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }" , " \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }" - , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ \\langle n_3, s_3 \\rangle } }" - , " \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ s_1 }{ \\langle n_3, s_3 \\rangle } }" + , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }" + , " \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{ma}" - , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }" + , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }" , " \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau -> e_1 ) }{ n_2 } }" - , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ \\langle n_3, s_3 \\rangle } }" - , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> e_1 ) }{ e }{ s_1 }{ \\langle n_3, s_3 \\rangle } }" + , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }" + , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> e_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{maa}" - , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }" + , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }" , " \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ n_2 } }" - , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ \\langle n_3, s_3 \\rangle } }" - , " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ e }{ s_1 }{ \\langle n_3, s_3 \\rangle } }" + , " \\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 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{root}" , " \\phinoCondition{ e \\not= Q }" , " \\phinoPremise{ \\phinoNormalize{ e }{ n } }" - , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }" - , " \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }" + , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }" + , " \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ s_1 }{ n_1 }{ s_2 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{dead}" - , " \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s_1 }{ \\langle T, s_1 \\rangle } }" + , " \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s_1 }{ T }{ s_1 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{xi}" - , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ \\langle T, s_1 \\rangle } }" + , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ T }{ s_1 } }" , "\\end{phinoMorphingInference}" , "\\begin{phinoMorphingInference}" , " \\phinoName{mg}" - , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ \\langle T, s_1 \\rangle } }" + , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ T }{ s_1 } }" , "\\end{phinoMorphingInference}" ] ] @@ -1108,38 +1108,38 @@ [ "\\begin{phinoDataizationInference}" , " \\phinoName{delta}" , " \\phinoLabel{\\Delta}" - , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ s_1 }{ \\langle \\delta, s_1 \\rangle } }" + , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_1 } }" , "\\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 }{ \\langle \\delta, s_2 \\rangle } }" - , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ s_1 }{ \\langle \\delta, s_2 \\rangle } }" + , " \\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 }{ \\langle n, s_2 \\rangle } }" + , " \\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 }{ \\langle \\delta, s_3 \\rangle } }" - , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\langle \\delta, s_3 \\rangle } }" + , " \\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 }{ \\langle --, s_1 \\rangle } }" + , " \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ -- }{ s_1 } }" , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" , " \\phinoName{end}" - , " \\phinoConclusion{ \\phinoDataize{ T }{ e }{ s_1 }{ \\langle --, s_1 \\rangle } }" + , " \\phinoConclusion{ \\phinoDataize{ T }{ e }{ s_1 }{ -- }{ s_1 } }" , "\\end{phinoDataizationInference}" , "\\begin{phinoDataizationInference}" , " \\phinoName{norm}" , " \\phinoCondition{ \\phinoNotFormation{ n } \\;\\text{and}\\; n \\not= T }" - , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }" - , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\langle \\delta, s_3 \\rangle } }" - , " \\phinoConclusion{ \\phinoDataize{ n }{ e }{ s_1 }{ \\langle \\delta, s_3 \\rangle } }" + , " \\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 } }" , "\\end{phinoDataizationInference}" ] ]