eo-phi-normalizer 2.2.1 → 2.2.2
raw patch · 8 files changed
+85/−30 lines, 8 files
Files
- CHANGELOG.md +21/−0
- app/Main.hs +25/−7
- eo-phi-normalizer.cabal +1/−1
- src/Language/EO/Phi/Rules/Yaml.hs +3/−3
- src/Language/EO/Phi/Syntax.hs +10/−9
- src/Language/EO/Phi/ToLaTeX.hs +3/−3
- src/Language/EO/Test/YamlSpec.hs +3/−1
- test/eo/phi/rules/new.yaml +19/−6
CHANGELOG.md view
@@ -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
app/Main.hs view
@@ -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
eo-phi-normalizer.cabal view
@@ -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 <https://github.com/objectionary/eo-phi-normalizer#readme> homepage: https://github.com/objectionary/eo-phi-normalizer#readme
src/Language/EO/Phi/Rules/Yaml.hs view
@@ -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?
src/Language/EO/Phi/Syntax.hs view
@@ -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
src/Language/EO/Phi/ToLaTeX.hs view
@@ -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 =
src/Language/EO/Test/YamlSpec.hs view
@@ -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
test/eo/phi/rules/new.yaml view
@@ -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)'