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.141 +version: 0.0.142 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 @@ -587,7 +587,7 @@ extraArgumentsToLatex Nothing = "{ }" extraArgumentsToLatex (Just extras) = let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras - in braced (intercalate " and " extras') + in braced (intercalate (" " <> T.unpack (render AND) <> " ") extras') -- Every rule is bared before it is rendered: an index that tells a meta from no -- other within the rule is dropped, so a rule naming a single expression meta diff --git a/src/Morph.hs b/src/Morph.hs --- a/src/Morph.hs +++ b/src/Morph.hs @@ -749,12 +749,13 @@ -- can name is named by that locator and the attribute it is bound to, which -- is the very locator '--locator' would aim a run of its own at. A binding -- the walk has entered in another copy of the same object of the world is - -- left as it was written (see 'fresh'). + -- left as it was written (see 'fresh'), unless its body reads the copy it + -- stands in (see 'closed'). bindings :: Maybe Expression -> Maybe (Expression, [Attribute]) -> [Binding] -> [Binding] -> State -> ReduceContext -> IO ([Binding], State) bindings _ _ _ [] state' _ = pure ([], state') bindings standing alias whole (BiTau attr body : rest) state' caller | attr /= AtRho = do - new <- fresh alias attr caller + new <- if closed body then fresh alias attr caller else pure True (entered, state'') <- if new then go (fmap (`ExDispatch` attr) standing) Nothing (scope attr whole) body state' caller @@ -800,6 +801,17 @@ unless seen (visit caller._memo object attr) pure (not seen) fresh _ _ _ = pure True + -- Whether a body cannot see the copy it stands in, that is, holds no ΞΎ + -- outside the formations nested in it, since the ΞΎ of a nested formation + -- is that formation. Two copies filling their voids differently make two + -- different programs of a body reading ΞΎ, so the walk of one tells nothing + -- about the other and such a body is walked in every copy (#1485). + closed :: Expression -> Bool + closed ExXi = False + closed (ExDispatch target _) = closed target + closed (ExApplication target (ArTau _ arg)) = closed target && closed arg + closed (ExApplication target (ArAlpha _ arg)) = closed target && closed arg + closed _ = True -- The context a binding's body is entered in: the formation without that -- binding, the very context 'dot' contextualizes a dispatched body in, so -- a body reaching back at itself through ΞΎ collapses instead of looping. diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -294,6 +294,7 @@ render CO_PART_OF{..} = "part-of\\lparen " <> render expr <> ", " <> render binding <> " \\rparen" render CO_FORMATION{..} = "\\phinoIsFormation{ " <> render expr <> " }" render CO_DISJOINT{..} = render (ST_ATTRIBUTES attrs) <> " \\cap " <> union groups <> " = \\emptyset" + render CO_SUBSET{attrs = [attr], ..} = render attr <> " " <> render belongs <> " " <> union groups render CO_SUBSET{belongs = NOT_IN, ..} = render (ST_ATTRIBUTES attrs) <> " \\not\\subseteq " <> union groups render CO_SUBSET{..} = render (ST_ATTRIBUTES attrs) <> " \\subseteq " <> union groups render CO_EMPTY = "" @@ -316,11 +317,10 @@ -- trailing arguments. This is a one-off application binding only 'meta', so the -- returned state is dropped (the engine discards it too, see 'execBuildTerm'). render EXTRA{func = "morph", ..} = render meta <> " \\coloneqq \\phinoMorph{ " <> T.intercalate ", " (map render args) <> " }{ e }{ s_1 }" - -- The name a formation goes by in the universe 'e'. The rule never writes the - -- universe, since phino knows it where the rule applies (#1460), so it - -- renders as the metavariable 'e', the way a 'morph' extra renders it, and - -- the formation the name stands for gets an argument of its own. - render EXTRA{func = "named", args = [form], ..} = render meta <> " \\coloneqq \\phinoNamed{ e }{ " <> render form <> " }" + -- The name a formation goes by in the universe. The rule never writes the + -- universe, since phino knows it where the rule applies (#1460), so the name + -- and the formation it stands for are the two sides of one relation. + render EXTRA{func = "named", args = [form], ..} = "\\phinoNamed{ " <> render meta <> " }{ " <> render form <> " }" render EXTRA{..} = render meta <> " \\coloneqq " <> macro func <> "{ " <> T.intercalate ", " (map render args) <> " }" where macro :: String -> Text diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -16,7 +16,8 @@ import Data.Time.Clock (addUTCTime, getCurrentTime) import Data.Time.Clock.POSIX (getPOSIXTime) import Data.Version (showVersion) -import Fixtures (lambdasFile, loopingLambdas, readUtf8, withLambdasOf) +import Files (allPathsIn) +import Fixtures (explainPack, lambdasFile, loopingLambdas, readUtf8, withLambdasOf) import GHC.IO.Handle import Paths_phino (version) import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist, getTemporaryDirectory, listDirectory, removeDirectoryRecursive, removeFile, removePathForcibly, setModificationTime) @@ -2503,17 +2504,9 @@ ["explain", "--help"] ["Explain built-in morphing rules", "Explain built-in dataization rules", "Explain built-in contextualization rules"] - it "explains single rule" $ - testCLISucceeded - ["explain", "--rule=resources/normalize/copy.yaml"] - [ unlines - [ "\\phinoNormalizationRule{copy}" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }" - , " { [[ B_1, \\tau -> k, B_2 ]] }" - , " { }" - , " { }" - ] - ] + it "explains single rule" $ do + latex <- explainPack "test-resources/explain-packs/normalize/copy.yaml" + testCLISucceeded ["explain", "--rule=resources/normalize/copy.yaml"] [latex <> "\n"] it "explains single rule with a label" $ testCLISucceeded @@ -2549,249 +2542,17 @@ ["explain", "--seed=7", "--normalize"] ["\\phinoNormalizationRule{alpha}"] - it "explains normalization rules" $ - testCLISucceeded - ["explain", "--normalize"] - [ unlines - [ "\\phinoNormalizationRule{alpha}" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }" - , " { i = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }" - , " { }" - , "\\phinoNormalizationRule{amiss}" - , " { [[ B ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }" - , " { T }" - , " { \\vert \\overline{ B } \\vert \\leq i }" - , " { }" - , "\\phinoNormalizationRule{copy}" - , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }" - , " { [[ B_1, \\tau -> k, B_2 ]] }" - , " { }" - , " { }" - , "\\phinoNormalizationRule{dc}" - , " { T ( \\tau -> e ) }" - , " { T }" - , " { }" - , " { }" - , "\\phinoNormalizationRule{dca}" - , " { T ( \\phiTerminal{\\alpha_{i}} -> e ) }" - , " { T }" - , " { }" - , " { }" - , "\\phinoNormalizationRule{dd}" - , " { T . \\tau }" - , " { T }" - , " { }" - , " { }" - , "\\phinoNormalizationRule{dl}" - , " { [[ B_1, L> f, B_2 ]] }" - , " { T }" - , " { [ D ] \\subseteq \\lparen B_1 \\cup B_2 \\rparen }" - , " { }" - , "\\phinoNormalizationRule{dot}" - , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" - , " { e_1 ( \\phiTerminal{\\rho} -> e_2 ) }" - , " { [ D \\char44{} L ] \\not\\subseteq \\lparen B_1 \\cup B_2 \\rparen }" - , " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e_1 } and e_2 \\coloneqq \\phinoNamed{ e }{ [[ B_1, \\tau -> n, B_2 ]] } }" - , "\\phinoNormalizationRule{miss}" - , " { [[ B ]] ( \\tau -> e ) }" - , " { T }" - , " { \\tau \\notin B \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }" - , " { }" - , "\\phinoNormalizationRule{null}" - , " { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }" - , " { T }" - , " { }" - , " { }" - , "\\phinoNormalizationRule{over}" - , " { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }" - , " { T }" - , " { \\tau \\not= \\phiTerminal{\\rho} }" - , " { }" - , "\\phinoNormalizationRule{overa}" - , " { [[ B_1, \\tau -> e_1, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e_2 ) }" - , " { T }" - , " { i = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }" - , " { }" - , "\\phinoNormalizationRule{skip}" - , " { [[ B ]] ( \\phiTerminal{\\rho} -> e ) }" - , " { [[ B ]] }" - , " { \\phiTerminal{\\rho} \\notin B }" - , " { }" - , "\\phinoNormalizationRule{stay}" - , " { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] ( \\phiTerminal{\\rho} -> e_2 ) }" - , " { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] }" - , " { }" - , " { }" - , "\\phinoNormalizationRule{stop}" - , " { [[ B ]] . \\tau }" - , " { T }" - , " { [ \\tau \\char44{} @ \\char44{} L ] \\cap B = \\emptyset }" - , " { }" - ] - ] - - it "explains morphing rules" $ - testCLISucceeded - ["explain", "--morph"] - [ unlines - [ "\\begin{phinoMorphingInference}" - , " \\phinoName{dead}" - , " \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s }{ T }{ s } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{ma}" - , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoPremise{ \\phinoNormalize{ n_2 ( \\tau -> k ) }{ n_3 } }" - , " \\phinoPremise{ \\phinoMorph{ n_3 }{ e }{ s_2 }{ n_4 }{ s_3 } }" - , " \\phinoConclusion{ \\phinoMorph{ n_1 ( \\tau -> k ) }{ e }{ s_1 }{ n_4 }{ s_3 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{maa}" - , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoPremise{ \\phinoNormalize{ n_2 ( \\phiTerminal{\\alpha_{i}} -> k ) }{ n_3 } }" - , " \\phinoPremise{ \\phinoMorph{ n_3 }{ e }{ s_2 }{ n_4 }{ s_3 } }" - , " \\phinoConclusion{ \\phinoMorph{ n_1 ( \\phiTerminal{\\alpha_{i}} -> k ) }{ e }{ s_1 }{ n_4 }{ s_3 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{maad}" - , " \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }" - , " \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{mad}" - , " \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }" - , " \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{md}" - , " \\phinoCondition{ \\phinoNotFormation{ n_1 } }" - , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoPremise{ \\phinoNormalize{ n_2 . \\tau }{ n_3 } }" - , " \\phinoPremise{ \\phinoMorph{ n_3 }{ e }{ s_2 }{ n_4 }{ s_3 } }" - , " \\phinoConclusion{ \\phinoMorph{ n_1 . \\tau }{ e }{ s_1 }{ n_4 }{ s_3 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{mf}" - , " \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s }{ [[ B ]] }{ s } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{mg}" - , " \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n }{ s_2 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{ml}" - , " \\phinoLabel{\\lambda}" - , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> f, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }" - , " \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }" - , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }" - , " \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> f, B_2 ]] . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{mphi}" - , " \\phinoLabel{\\varphi}" - , " \\phinoCondition{ @ \\in B \\;\\text{and}\\; [ \\tau \\char44{} L ] \\cap B = \\emptyset }" - , " \\phinoPremise{ \\phinoNormalize{ [[ B ]] . @ . \\tau }{ n_1 } }" - , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ [[ B ]] . \\tau }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{universe}" - , " \\phinoLabel{\\Phi}" - , " \\phinoCondition{ e \\not= Q }" - , " \\phinoPremise{ \\phinoNormalize{ e }{ n_1 } }" - , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , "\\end{phinoMorphingInference}" - , "\\begin{phinoMorphingInference}" - , " \\phinoName{xi}" - , " \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }" - , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ n }{ s_2 } }" - , "\\end{phinoMorphingInference}" - ] - ] - - it "explains dataization rules" $ - testCLISucceeded - ["explain", "--dataize"] - [ unlines - [ "\\begin{phinoDataizationInference}" - , " \\phinoName{box}" - , " \\phinoCondition{ [ D \\char44{} L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }" - , " \\phinoPremise{ \\phinoContextualize{ e_2 }{ [[ B_1, @ -> e_2, B_2 ]] }{ e_3 } }" - , " \\phinoPremise{ \\phinoNormalize{ e_3 }{ n } }" - , " \\phinoPremise{ \\phinoDataize{ n }{ e_1 }{ s_1 }{ \\delta }{ s_2 } }" - , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_2, B_2 ]] }{ e_1 }{ s_1 }{ \\delta }{ s_2 } }" - , "\\end{phinoDataizationInference}" - , "\\begin{phinoDataizationInference}" - , " \\phinoName{delta}" - , " \\phinoLabel{\\Delta}" - , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ s }{ \\delta }{ s } }" - , "\\end{phinoDataizationInference}" - , "\\begin{phinoDataizationInference}" - , " \\phinoName{fire}" - , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> f, B_2 ]] }{ e }{ s_1 }{ n }{ s_2 } }" - , " \\phinoPremise{ \\phinoDataize{ n }{ 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 \\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{norm}" - , " \\phinoCondition{ \\phinoNotFormation{ n_1 } \\;\\text{and}\\; n_1 \\not= T }" - , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }" - , " \\phinoPremise{ \\phinoDataize{ n_2 }{ e }{ s_2 }{ \\delta }{ s_3 } }" - , " \\phinoConclusion{ \\phinoDataize{ n_1 }{ e }{ s_1 }{ \\delta }{ s_3 } }" - , "\\end{phinoDataizationInference}" - ] - ] - - it "explains contextualization rules" $ - testCLISucceeded - ["explain", "--contextualize"] - [ unlines - [ "\\begin{phinoContextualizationInference}" - , " \\phinoName{ca}" - , " \\phinoPremise{ \\phinoContextualize{ n_1 }{ k }{ n_2 } }" - , " \\phinoPremise{ \\phinoContextualize{ e }{ k }{ n_3 } }" - , " \\phinoConclusion{ \\phinoContextualize{ n_1 ( \\tau -> e ) }{ k }{ n_2 ( \\tau -> n_3 ) } }" - , "\\end{phinoContextualizationInference}" - , "\\begin{phinoContextualizationInference}" - , " \\phinoName{caa}" - , " \\phinoPremise{ \\phinoContextualize{ n_1 }{ k }{ n_2 } }" - , " \\phinoPremise{ \\phinoContextualize{ e }{ k }{ n_3 } }" - , " \\phinoConclusion{ \\phinoContextualize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> e ) }{ k }{ n_2 ( \\phiTerminal{\\alpha_{i}} -> n_3 ) } }" - , "\\end{phinoContextualizationInference}" - , "\\begin{phinoContextualizationInference}" - , " \\phinoName{cd}" - , " \\phinoPremise{ \\phinoContextualize{ n_1 }{ k }{ n_2 } }" - , " \\phinoConclusion{ \\phinoContextualize{ n_1 . \\tau }{ k }{ n_2 . \\tau } }" - , "\\end{phinoContextualizationInference}" - , "\\begin{phinoContextualizationInference}" - , " \\phinoName{cf}" - , " \\phinoConclusion{ \\phinoContextualize{ [[ B ]] }{ k }{ [[ B ]] } }" - , "\\end{phinoContextualizationInference}" - , "\\begin{phinoContextualizationInference}" - , " \\phinoName{cg}" - , " \\phinoConclusion{ \\phinoContextualize{ Q }{ k }{ Q } }" - , "\\end{phinoContextualizationInference}" - , "\\begin{phinoContextualizationInference}" - , " \\phinoName{ct}" - , " \\phinoConclusion{ \\phinoContextualize{ T }{ k }{ T } }" - , "\\end{phinoContextualizationInference}" - , "\\begin{phinoContextualizationInference}" - , " \\phinoName{cxi}" - , " \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k }{ k } }" - , "\\end{phinoContextualizationInference}" - ] - ] + forM_ + [ ("normalization", "--normalize", "normalize") + , ("morphing", "--morph", "morphing") + , ("dataization", "--dataize", "dataization") + , ("contextualization", "--contextualize", "contextualization") + ] + ( \(judgment, option, dir) -> it ("explains " <> judgment <> " rules") $ do + packs <- allPathsIn ("test-resources/explain-packs" dir) + latex <- mapM explainPack (sort packs) + testCLISucceeded ["explain", option] [unlines latex] + ) it "fails with no rules specified" $ testCLIFailed diff --git a/test/Fixtures.hs b/test/Fixtures.hs --- a/test/Fixtures.hs +++ b/test/Fixtures.hs @@ -9,6 +9,7 @@ -- '--symbolic' reads, or a file of its own written for the occasion. module Fixtures ( defaultReduceContext + , explainPack , fixtureLambdas , lambdasFile , loopingLambdas @@ -26,10 +27,12 @@ import CLI.Helpers (withEvalFunc) import CLI.Types (IOFormat (PHI), PrintContext (PrintCtx)) import Control.Exception (bracket, evaluate) +import Data.Aeson (FromJSON (parseJSON), withObject, (.:)) import Data.ByteString qualified as BS import Data.Map.Strict qualified as Map import Data.Text qualified as T import Data.Text.Encoding (encodeUtf8) +import Data.Yaml qualified as Yaml import Dataize (reduction) import Deps (Judgment (..), SaveEvalFunc, dontSaveEval, dontSaveStep) import Evaluate (evaluation, fired) @@ -157,6 +160,18 @@ Nothing Nothing PHI + +-- The LaTeX that 'explain' prints for one built-in rule, as the 'latex' key of +-- its pack in 'test-resources/explain-packs' spells it. +newtype ExplainPack = ExplainPack String + +instance FromJSON ExplainPack where + parseJSON = withObject "ExplainPack" (\pack -> ExplainPack <$> pack .: "latex") + +explainPack :: FilePath -> IO String +explainPack path = do + ExplainPack latex <- Yaml.decodeFileThrow path + pure latex -- Read a text file phino wrote, in the encoding it wrote it with. The whole -- content is forced before the handle closes, since a lazy read of a closed diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs --- a/test/LaTeXSpec.hs +++ b/test/LaTeXSpec.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com @@ -18,6 +19,7 @@ import Data.Text qualified as T import Data.Yaml qualified as Yaml import Files (allPathsIn) +import Fixtures (explainPack) import GHC.Generics (Generic) import LaTeX ( LatexContext (..) @@ -34,7 +36,7 @@ ) import Lining (LineFormat (MULTILINE)) import Parser (parseExpressionThrows) -import System.FilePath (makeRelative) +import System.FilePath (makeRelative, (<.>), ()) import Test.Hspec (Spec, describe, expectationFailure, it, runIO, shouldBe, shouldContain) import Yaml qualified as Y @@ -60,6 +62,18 @@ expressionToLaTeX parsed defaultLatexContext `shouldBe` result pack ) + describe "explain packs" $ + forM_ + ( map (\rule -> ("normalize", rule.name, explainRules [rule])) Y.normalizationRules + <> map (\rule -> ("morphing", rule.name, explainMorphRules [rule])) Y.morphingRules + <> map (\rule -> ("dataization", rule.name, explainDataizeRules [rule])) Y.dataizationRules + <> map (\rule -> ("contextualization", rule.name, explainContextualizeRules [rule])) Y.contextualizationRules + ) + ( \(judgment, rule, explained) -> it (judgment rule) $ do + latex <- explainPack ("test-resources" "explain-packs" judgment rule <.> "yaml") + explained `shouldBe` latex + ) + describe "meet expression in expression" $ forM_ [ ("Q.x.y", "Q.x.y", "[[ x -> Q.x.y ]]", ["Q.x.y"]) @@ -295,7 +309,7 @@ , "{ n }" , "{ n }" , "{ \\isnormal{ n } \\;\\text{and}\\; \\phinoIsFormation{ n } }" - , "{ \\phiTerminal{\\rho} \\coloneqq \\foo{ n, \\phiTerminal{\\rho} -> ?, 01-02- } and @ \\coloneqq \\bar{ n } }" + , "{ \\phiTerminal{\\rho} \\coloneqq \\foo{ n, \\phiTerminal{\\rho} -> ?, 01-02- } \\;\\text{and}\\; @ \\coloneqq \\bar{ n } }" ] ) , diff --git a/test/RenderSpec.hs b/test/RenderSpec.hs --- a/test/RenderSpec.hs +++ b/test/RenderSpec.hs @@ -334,7 +334,17 @@ , CO_SUBSET [AT_LABEL "a", AT_LABEL "b"] IN [bindingXi "x", bindingXi "y"] , "[ a \\char44{} b ] \\subseteq \\lparen x ↦ ΞΎ \\cup y ↦ ΞΎ \\rparen" ) - , ("CO_SUBSET negated", CO_SUBSET [AT_LABEL "a"] NOT_IN [bindingXi "x"], "[ a ] \\not\\subseteq x ↦ ΞΎ") + , ("CO_SUBSET negated", CO_SUBSET [AT_LABEL "a", AT_LABEL "b"] NOT_IN [bindingXi "x"], "[ a \\char44{} b ] \\not\\subseteq x ↦ ΞΎ") + , + ( "CO_SUBSET of one attribute prints membership" + , CO_SUBSET [AT_LABEL "q"] IN [bindingXi "k", bindingXi "w"] + , "q \\in \\lparen k ↦ ΞΎ \\cup w ↦ ΞΎ \\rparen" + ) + , + ( "CO_SUBSET of one attribute negated prints non-membership" + , CO_SUBSET [AT_LABEL "u"] NOT_IN [bindingXi "m", bindingXi "z"] + , "u \\notin \\lparen m ↦ ΞΎ \\cup z ↦ ΞΎ \\rparen" + ) , ("CO_EMPTY", CO_EMPTY, "") ] (\(desc, node, expected) -> it desc (render node `shouldBe` expected))