diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,27 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v2.2.2 - 2024-11-29 + +### New + +- Add `--single-line` option to the `rewrite` command ([#588](https://github.com/objectionary/eo-phi-normalizer/pull/588)) + +### Changes and fixes + +- Fix pretty printing ([#577](https://github.com/objectionary/eo-phi-normalizer/pull/577), [#586](https://github.com/objectionary/eo-phi-normalizer/pull/586), [#589](https://github.com/objectionary/eo-phi-normalizer/pull/589)) +- Allow optional `when` and `tests` keys in rule files ([#578](https://github.com/objectionary/eo-phi-normalizer/pull/578)) +- Improve TeX output ([#579](https://github.com/objectionary/eo-phi-normalizer/pull/579)) +- Fix typo in rule `R_rho` and add more tests ([#587](https://github.com/objectionary/eo-phi-normalizer/pull/587)) + +### Documentation and maintenance + +- Update haskell-actions/run-fourmolu action to v11 ([#516](https://github.com/objectionary/eo-phi-normalizer/pull/516)) +- Update dependency prettier to v3.4.1 ([#552](https://github.com/objectionary/eo-phi-normalizer/pull/552)) +- Update dependency pre-commit to v4 - autoclosed ([#503](https://github.com/objectionary/eo-phi-normalizer/pull/503)) +- Update dependency eolang to ^0.24.0 ([#520](https://github.com/objectionary/eo-phi-normalizer/pull/520)) +- Add `CONTRIBUTE.md` ([#576](https://github.com/objectionary/eo-phi-normalizer/pull/576)) + ## v2.2.1 - 2024-11-27 ### Changes and fixes diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -58,7 +58,7 @@ import Data.Aeson (ToJSON) import Data.Aeson.Encode.Pretty (Config (..), Indent (..), defConfig, encodePrettyToTextBuilder') import Data.FileEmbed (embedFileRelative) -import Data.Foldable (forM_) +import Data.Foldable (Foldable (..), forM_) import Data.List (intercalate, isPrefixOf) import Data.Maybe (fromMaybe) import Data.Text.Internal.Builder (toLazyText) @@ -98,6 +98,7 @@ , rulesPath :: Maybe String , outputFile :: Maybe String , single :: Bool + , singleLine :: Bool , json :: Bool , latex :: Bool , inputFile :: Maybe FilePath @@ -292,7 +293,10 @@ json <- jsonSwitch latex <- latexSwitch outputFile <- outputFileOption - single <- switch (long "single" <> short 's' <> help "Output a single expression.") + let singleFlag :: String + singleFlag = "single" + single <- switch (long singleFlag <> short 's' <> help "Output a single expression.") + singleLine <- switch (long "single-line" <> short 'l' <> help [fmt|Output a single expression on a single line. Has effect only if the --{singleFlag} is enabled.|]) maxDepth <- let maxValue = 10 in option auto (long "max-depth" <> metavar.int <> value maxValue <> help [fmt|Maximum depth of rules application. Defaults to {maxValue}.|]) @@ -593,7 +597,7 @@ Nothing -> do ruleSet :: RuleSet <- decodeThrow $(embedFileRelative "test/eo/phi/rules/new.yaml") return (False, ruleSet.title, convertRuleNamed <$> ruleSet.rules) - unless (single || json) $ logStrLn ruleSetTitle + unless (single || json || (chain && latex)) $ logStrLn ruleSetTitle bindingsWithDeps <- case deepMergePrograms (program' : deps) of Left err -> throw (CouldNotMergeDependencies err) Right (Program bindingsWithDeps) -> return bindingsWithDeps @@ -614,8 +618,10 @@ . encodeToJSONString . printAsProgramOrAsObject $ logEntryLog (head (head uniqueResults)) - | single -> + | single -> do + let removeExtraSpaces = unwords . words logStrLn + . (if singleLine then removeExtraSpaces else id) . printAsProgramOrAsObject $ logEntryLog (head (head uniqueResults)) | json -> @@ -625,10 +631,22 @@ , output = (logEntryToPair . fmap printAsProgramOrAsObject <$>) <$> uniqueResults } | chain && latex -> do - logStrLn . toLatexString $ Formation bindings + logStrLn + [fmtTrim| + % {ruleSetTitle} + + \\documentclass{{article}} + \\usepackage{{eolang}} + \\begin{{document}} + |] forM_ uniqueResults $ \steps -> do - forM_ (init steps) $ \LogEntry{..} -> do - logStrLn . toLatexString $ logEntryLog + let latexLines = toLatexString (Formation bindings) : (toLatexString . (.logEntryLog) <$> steps) + transitions :: [String] = ((\x -> [fmt| \\trans_{{\\rulename{{{logEntryMessage x}}}}} \n|]) <$> steps) <> ["."] + linesCombined :: String = fold $ zipWith (\latexLine transition -> [fmt|{latexLine}{transition}|]) latexLines transitions + logStrLn "\\begin{phiquation*}" + logStrLn [fmtTrim|{linesCombined}|] + logStrLn "\\end{phiquation*}" + logStrLn "\n\\end{document}" | latex -> logStrLn . toLatexString $ logEntryLog (head (head uniqueResults)) | otherwise -> do diff --git a/eo-phi-normalizer.cabal b/eo-phi-normalizer.cabal --- a/eo-phi-normalizer.cabal +++ b/eo-phi-normalizer.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: eo-phi-normalizer -version: 2.2.1 +version: 2.2.2 synopsis: Command line normalizer of 𝜑-calculus expressions. description: Please see the README on GitHub at homepage: https://github.com/objectionary/eo-phi-normalizer#readme diff --git a/src/Language/EO/Phi/Rules/Yaml.hs b/src/Language/EO/Phi/Rules/Yaml.hs --- a/src/Language/EO/Phi/Rules/Yaml.hs +++ b/src/Language/EO/Phi/Rules/Yaml.hs @@ -101,8 +101,8 @@ , pattern :: Object , result :: Object , fresh :: Maybe [FreshMetaId] - , when :: [Condition] - , tests :: [RuleTest] + , when :: Maybe [Condition] + , tests :: Maybe [RuleTest] } deriving (Generic, FromJSON, Show) @@ -183,7 +183,7 @@ let pattern' = applySubst contextSubsts pattern result' = applySubst contextSubsts result subst <- matchObject pattern' obj - guard $ all (\cond -> checkCond ctx cond (contextSubsts <> subst)) when + guard $ all (\cond -> checkCond ctx cond (contextSubsts <> subst)) (fromMaybe [] when) let substFresh = mkFreshSubst ctx result' fresh result'' = applySubst (contextSubsts <> subst <> substFresh) result' -- TODO #152:30m what context should we pass to evaluate meta funcs? diff --git a/src/Language/EO/Phi/Syntax.hs b/src/Language/EO/Phi/Syntax.hs --- a/src/Language/EO/Phi/Syntax.hs +++ b/src/Language/EO/Phi/Syntax.hs @@ -63,8 +63,8 @@ ShowS rend i p = \case "[" : "]" : ts -> showString "[]" . rend i False ts - "(" : ")" : ts -> showString "()" . rend i False ts - "⟦" : "⟧" : ts -> showString "⟦ ⟧" . rend i False ts + "(" : ")" : (t : ts) -> handleTrailingComma "()" t ts + "⟦" : "⟧" : (t : ts) -> handleTrailingComma "⟦⟧" t ts "[" : ts -> char '[' . rend i False ts "(" : ts -> char '(' . new (i + 1) ts "{" : "⟦" : ts -> showChar '{' . onNewLine (i + 1) p . showChar '⟦' . new (i + 2) ts @@ -77,19 +77,20 @@ [";"] -> char ';' ";" : ts -> char ';' . new i ts "." : ts -> rend i p (" ." : ts) - t : ts@(s : ss) - | closingOrPunctuation s -> - (pending . showString t) - . ( case s of - "," -> showChar ',' . new i ss - _ -> rend i False ts - ) + t : (s : ss) | closingOrPunctuation s -> handleTrailingComma t s ss t : ts -> pending . space t . rend i False ts [] -> id where -- Output character after pending indentation. char :: Char -> ShowS char c = pending . showChar c + + handleTrailingComma str t ts = + (pending . showString str) + . ( case t of + "," -> showChar ',' . new i ts + _ -> rend i False (t : ts) + ) -- Output pending indentation. pending :: ShowS diff --git a/src/Language/EO/Phi/ToLaTeX.hs b/src/Language/EO/Phi/ToLaTeX.hs --- a/src/Language/EO/Phi/ToLaTeX.hs +++ b/src/Language/EO/Phi/ToLaTeX.hs @@ -119,7 +119,7 @@ instance ToLatex Condition where toLatex (IsNF nf) = inMathMode $ toLatex nf <> "\\in\\mathcal{N}" toLatex (IsNFInsideFormation nf_inside_formation) = - (inMathMode $ toLatex nf_inside_formation) <> " is nf inside formation" + inMathMode (toLatex nf_inside_formation) <> " is nf inside formation" toLatex (PresentAttrs (AttrsInBindings attrs bindings)) = inMathMode $ fold (intersperse ", " (map toLatex attrs)) <> " \\in " <> foldMap toLatex bindings toLatex (AbsentAttrs (AttrsInBindings attrs bindings)) = @@ -147,7 +147,7 @@ <> inMathMode (toLatex result) <> (if not (null when) || isNonEmptyContext context then "\\\\\\text {if }" else mempty) <> maybe mempty (\c -> "&" <> toLatex c <> "\\\\") context - <> fold (intersperse ",\\\\" (map (("&" <>) . toLatex) when)) + <> fold (intersperse ",\\\\" (maybe [] (map (("&" <>) . toLatex)) when)) instance ToLatex [Rule] where toLatex rules = @@ -166,7 +166,7 @@ <> inMathMode (toLatex result) <> (if not (null when) || isNonEmptyContext context then "\\quad\\text {if }" else "") <> maybe mempty (\c -> toLatex c <> ", ") context - <> fold (intersperse ", " (map toLatex when)) + <> fold (intersperse ", " (maybe [] (map toLatex) when)) rulesToLatexCompact :: [Rule] -> LaTeX rulesToLatexCompact rules = diff --git a/src/Language/EO/Test/YamlSpec.hs b/src/Language/EO/Test/YamlSpec.hs --- a/src/Language/EO/Test/YamlSpec.hs +++ b/src/Language/EO/Test/YamlSpec.hs @@ -27,6 +27,7 @@ module Language.EO.Test.YamlSpec where import Control.Monad (forM_) +import Data.Maybe (fromMaybe) import Language.EO.Phi.Dataize.Context (defaultContext) import Language.EO.Phi.Rules.Common (applyOneRule) import Language.EO.Phi.Rules.Yaml (Rule (..), RuleSet (..), RuleTest (..), RuleTestOption (..), convertRuleNamed) @@ -40,7 +41,8 @@ describe ruleset.title do forM_ ruleset.rules $ \rule -> do describe rule.name do - forM_ rule.tests $ \ruleTest -> do + let tests' = fromMaybe [] rule.tests + forM_ tests' $ \ruleTest -> do it ruleTest.name $ let rule' = convertRuleNamed rule resultOneStep = applyOneRule (defaultContext [rule'] ruleTest.input) ruleTest.input diff --git a/test/eo/phi/rules/new.yaml b/test/eo/phi/rules/new.yaml --- a/test/eo/phi/rules/new.yaml +++ b/test/eo/phi/rules/new.yaml @@ -50,11 +50,16 @@ output: ['⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦x ↦ ⟦ρ ↦ ⟦⟧⟧⟧)'] - name: Phi Paper - Example E4 - first R_dot input: '⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.y' - # output: ['⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.x(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)'] output: ['⟦ y ↦ ξ.x, x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧.x(ρ ↦ ⟦ y ↦ ξ.x, x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧)'] - name: Phi Paper - Example E4 - second R_dot input: ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.x(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧) output: ['⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)'] + - name: Phi Paper - Example E5 - first R_dot + input: ⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.x ⟧ + output: ['⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧'] + - name: Phi Paper - Example E5 - second R_dot + input: ⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.φ.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧ + output: ['⟦ m ↦ ⟦ t ↦ ⟦⟧ ⟧(ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧).t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧'] - name: COPY description: 'Application of α-binding' @@ -89,13 +94,16 @@ pattern: | ⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧ result: | - ⟦ !τ ↦ ⟦ !B1, ρ ↦ ⌈ !b , ⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧ ⌉ ⟧(!B2), !B3 ⟧ + ⟦ !τ ↦ ⟦ !B1, ρ ↦ ⌈ !b , ⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧ ⌉ ⟧(!B2) * !t, !B3 ⟧ when: - nf: '!b' - absent_attrs: attrs: ['ρ'] bindings: ['!B1'] - tests: [] + tests: + - name: Phi Paper - Example E5 - first R_rho + input: ⟦ m ↦ ⟦ t ↦ ⟦⟧ ⟧(ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧).t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧ + output: ['⟦ m ↦ ⟦ t ↦ ⟦⟧, ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧ ⟧().t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧'] - name: phi description: 'Accessing a decorated object' @@ -111,7 +119,10 @@ - absent_attrs: attrs: ['!τ'] bindings: ['!B'] - tests: [] + tests: + - name: Phi Paper - Example E5 - R_phi + input: ⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧ + output: ['⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.φ.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧'] # there's no B2 in the result - name: STAY @@ -156,8 +167,7 @@ input: '⟦ ρ ↦ ⟦ ⟧ ⟧.x' output: ['⊥'] - # Named VOID instead of NULL because NULL is a keyword in yaml - - name: VOID + - name: 'NULL' description: 'Void attribute access' pattern: | ⟦ !τ ↦ ∅, !B ⟧.!τ @@ -189,6 +199,9 @@ - name: Should work with empty formation input: ⟦⟧() output: ['⟦⟧'] + - name: Phi Paper - Example E5 - first R_rho + input: ⟦ m ↦ ⟦ t ↦ ⟦⟧, ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧ ⟧().t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧ + output: ['⟦ m ↦ ⟦ t ↦ ⟦⟧, ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦⟧ ⟧,x ↦ ξ.t ⟧ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧) ⟧'] - name: MISS description: 'Invalid application (absent attribute)'