phino 0.0.141 → 0.0.142
raw patch · 8 files changed
+79/−267 lines, 8 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- phino.cabal +1/−1
- src/LaTeX.hs +1/−1
- src/Morph.hs +14/−2
- src/Render.hs +5/−5
- test/CLISpec.hs +16/−255
- test/Fixtures.hs +15/−0
- test/LaTeXSpec.hs +16/−2
- test/RenderSpec.hs +11/−1
phino.cabal view
@@ -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 <https://github.com/objectionary/phino#readme>
src/LaTeX.hs view
@@ -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
src/Morph.hs view
@@ -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.
src/Render.hs view
@@ -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
test/CLISpec.hs view
@@ -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
test/Fixtures.hs view
@@ -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
test/LaTeXSpec.hs view
@@ -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 } }" ] ) ,
test/RenderSpec.hs view
@@ -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))