diff --git a/.markdownlint.jsonc b/.markdownlint.jsonc new file mode 100644 index 000000000..1344b312f --- /dev/null +++ b/.markdownlint.jsonc @@ -0,0 +1,3 @@ +{ + "MD013": false +} diff --git a/README.md b/README.md index ec3f483fe..f4224c1a2 100644 --- a/README.md +++ b/README.md @@ -5,380 +5,4 @@ Command line normalizer of 𝜑-calculus expressions (as produced by the [EO compiler](https://github.com/objectionary/eo)). -## About - -This project aims to apply term rewriting techniques to "simplify" an input 𝜑-expression -and prepare it for further optimization passes. The simplification procedure is expected -to be a form of partial evaluation and normalization. -Contrary to traditional normalization in λ-calculus, we aim at rewriting rules that would -help reduce certain metrics of expressions. In particular, we are interested in reducing -attribute access (`t.a`) that amounts to _dynamic dispatch_. - -## Install - -You can install the `normalizer-phi` executable globally via [stack](https://docs.haskellstack.org/en/stable). -Then, the `normalize-phi` executable will be available on `PATH`. - -### Install from the repository - -```sh -git clone https://github.com/objectionary/normalizer -cd normalizer -export LANG=C.UTF-8 -stack install normalize-phi -normalize-phi --help -``` - -### Install from Hackage - -```sh -stack update -export LANG=C.UTF-8 -stack install --resolver lts-22.11 eo-phi-normalizer -``` - -### Uninstall - -Learn where `stack` installs programs. - -```sh -stack path --programs -``` - -Learn how to uninstall a program. - -```sh -stack uninstall -``` - -## Use - -Learn about `normalize-phi` options. - -```sh -normalize-phi --help -``` - -```console -Normalizer - -Usage: normalize-phi [-c|--chain] [--rules-yaml STRING] [-o|--output STRING] - [-s|--single] [STRING] - -Available options: - -h,--help Show this help text - -c,--chain Print out steps of reduction - --rules-yaml STRING Path to the Yaml file with custom rules - -o,--output STRING Output file path (defaults to stdout) - -s,--single Print a single normalized expression -``` - -### Sample program - -Save a $\varphi$-calculus program to a file. -This program will be used in subsequent commands. - -```sh -cat > program.phi <`. - -## Rulesets - -A ruleset describes a set of user-defined rewriting rules. - -Here is a sample ruleset (see the full ruleset in [yegor.yaml](./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml)). - -```yaml -title: "Rule set based on Yegor's draft" -rules: - - name: Rule 6 - description: "Accessing an α-binding" - pattern: | - ⟦ !a ↦ !n, !B ⟧.!a - result: | - !n(ρ ↦ ⟦ !B ⟧) - when: - - nf: ["!n"] - tests: - - name: Should match - input: ⟦ hello ↦ ⟦⟧ ⟧.hello - output: ⟦⟧(ρ ↦ ⟦⟧) - matches: true - - name: Shouldn't match - input: ⟦ ⟧.hello - output: "" - matches: false -``` - -A ruleset has a number of rules. Each rule describes a `pattern`, `when` to apply that pattern, and a `result`. - -The `pattern` has metavariables denoted as `!`. -The `pattern` is matched against an `input` expression. The rules in the `when` list help avoid unwanted matches. For example, `nf: ["!n"]` means that only an expression in a normal form can be matched with `!n`. - -When there is a match, the matched parts of the expression are bound to metavariables. Next, these metavariables are used to construct the `result`. - -Additionally, there are unit tests for rules. Each unit test provides `input` and `output` expressions. An `output` expression is not reused in other tests, so it is safe to let it be an empty string when no match can happen. - -## Develop - -We recommend using [stack](https://docs.haskellstack.org/en/stable/README/) for quick local development and testing. - -Clone this project and run `stack build`. - -```sh -git clone https://github.com/objectionary/normalizer -cd normalizer -stack build -``` - -### Run - -Run the executable via `stack run`. - -```sh -stack run normalize-phi -- --help -``` - -Or, omit the executable name. - -```sh -stack run -- --help -``` - -### Test - -Run all tests - -```sh -stack test -``` - -## Contribute - -### pre-commit - -We use [pre-commit](https://pre-commit.com/) to ensure code quality. - -Collaborators **MUST** set them up before commiting any code to our repository. - -Otherwise, the triggered CI jobs will fail. - -#### Set up pre-commit - -##### Single command - -```console -pip3 install -pre-commit install -stack install fourmolu -chmod +x scripts/run-fourmolu.sh -``` - -##### Step by step - -1. Install [Python 3](https://www.python.org/downloads/) (e.g., Python 3.10). -1. [Install pre-commit](https://pre-commit.com/#1-install-pre-commit). - - Alternatively, run `pip3 install`. -1. [Install the git hook scripts](https://pre-commit.com/#3-install-the-git-hook-scripts). -1. Install [fourmolu](https://github.com/fourmolu/fourmolu). - - ```console - stack install fourmolu - ``` - - - You can remove `fourmolu` later (see [SO post](https://stackoverflow.com/a/38639959)) - -1. Make a script executable. - - ```console - chmod +x scripts/run-fourmolu.sh - ``` - -#### pre-commit configs - -See [docs](https://pre-commit.com/#adding-pre-commit-plugins-to-your-project). - -See [.pre-commit-config.yaml](.pre-commit-config.yaml). - -You can run a specific hook (see [docs](https://pre-commit.com/#pre-commit-run)): - -```console -pre-commit run -c .pre-commit-config.yaml fourmolu-format --all -``` - -#### pre-commit workflow - -- `pre-commit` runs before a commit (at the [pre-commit phase](https://git-scm.com/book/en/v2/Customizing-Git-Git-Hooks#_committing_workflow_hooks)) - - > The pre-commit hook is run first, before you even type in a commit message. It's used to inspect the snapshot that's about to be committed, to see if you've forgotten something, to make sure tests run, or to examine whatever you need to inspect in the code. Exiting non-zero from this hook aborts the commit ... - -- `pre-commit` stashes ([link](https://git-scm.com/docs/git-stash)) unstaged ([link](https://git-scm.com/book/en/v2/Getting-Started-What-is-Git%3F#_the_three_states)) files. - - ```console - [WARNING] Unstaged files detected. - [INFO] Stashing unstaged files to /home/eyjafjallajokull/.cache/pre-commit/patch1705090051-437857. - ``` - -- `pre-commit` runs hooks. -- A hook may exit with an error, e.g.: - - ```md - Format Haskell (.hs) files...............................................Failed - - - hook id: fourmolu - - exit code: 102 - - files were modified by this hook - ``` - - - In case of the [fourmolu](https://github.com/fourmolu/fourmolu) formatter, - it's assumed that formatting a formatted `Haskell` file doesn't modify it. - However, `pre-commit` runs the `fourmolu` hook and reports that it has modified some files. - This error won't allow you to commit. - -- `pre-commit` unstashes files. - -- You should stage all changes so that `pre-commit` does not complain. - - - In case of `fourmolu`, stage the formatted code regions. - -- Now, you can commit. +Consult the [project documentation](https://www.objectionary.com/normalizer/) for more details. diff --git a/eo-phi-normalizer/app/Main.hs b/eo-phi-normalizer/app/Main.hs index 79fac28a4..c14ea3145 100644 --- a/eo-phi-normalizer/app/Main.hs +++ b/eo-phi-normalizer/app/Main.hs @@ -1,109 +1,199 @@ +{-# LANGUAGE ApplicativeDo #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-partial-fields #-} {-# OPTIONS_GHC -Wno-type-defaults #-} -module Main where +module Main (main) where import Control.Monad (unless, when) import Data.Foldable (forM_) import Control.Lens ((^.)) import Data.Aeson (ToJSON) -import Data.Aeson.Text (encodeToLazyText) +import Data.Aeson.Encode.Pretty (Config (..), Indent (..), defConfig, encodePrettyToTextBuilder') +import Data.String.Interpolate (i) +import Data.Text.Internal.Builder (toLazyText) import Data.Text.Lazy.Lens -import Language.EO.Phi (Attribute (Sigma), Object (Formation), Program (Program), defaultMain, parseProgram, printTree) +import GHC.Generics (Generic) +import Language.EO.Phi (Attribute (Sigma), Object (Formation), Program (Program), parseProgram, printTree) +import Language.EO.Phi.Metrics.Collect (collectMetrics) import Language.EO.Phi.Rules.Common (Context (..), applyRules, applyRulesChain) import Language.EO.Phi.Rules.Yaml (RuleSet (rules, title), convertRule, parseRuleSetFromFile) -import Options.Generic -import System.IO (IOMode (WriteMode), hClose, hPutStr, hPutStrLn, openFile, stdout) +import Options.Applicative +import Options.Applicative.Types qualified as Optparse (Context (..)) +import System.IO (IOMode (WriteMode), getContents', hFlush, hPutStr, hPutStrLn, openFile, stdout) -data CLINamedParams = CLINamedParams +data CLI'TransformPhi = CLI'TransformPhi { chain :: Bool - , rulesYaml :: Maybe String - , outPath :: Maybe String + , rulesPath :: String + , outputFile :: Maybe String , single :: Bool , json :: Bool + , inputFile :: Maybe FilePath } - deriving (Generic, Show, ParseRecord, Read, ParseField) + deriving (Show) -instance ParseFields CLINamedParams where - parseFields _ _ _ _ = - CLINamedParams - <$> parseFields (Just "Print out steps of reduction") (Just "chain") (Just 'c') Nothing - <*> parseFields (Just "Path to the Yaml file with custom rules") (Just "rules-yaml") Nothing Nothing - <*> parseFields (Just "Output file path (defaults to stdout)") (Just "output") (Just 'o') Nothing - <*> parseFields (Just "Print a single normalized expression") (Just "single") (Just 's') Nothing - <*> parseFields (Just "Print JSON") (Just "json") (Just 'j') Nothing +data CLI'MetricsPhi = CLI'MetricsPhi + { inputFile :: Maybe FilePath + , outputFile :: Maybe FilePath + } + deriving (Show) + +data CLI + = CLI'TransformPhi' CLI'TransformPhi + | CLI'MetricsPhi' CLI'MetricsPhi + deriving (Show) + +fileMetavarName :: String +fileMetavarName = "FILE" + +fileMetavar :: Mod OptionFields a +fileMetavar = metavar fileMetavarName + +outputFileOption :: Parser (Maybe String) +outputFileOption = optional $ strOption (long "output-file" <> short 'o' <> help [i|Output to #{fileMetavarName}. When this option is not specified, output to stdout.|] <> fileMetavar) + +inputFileArg :: Parser (Maybe String) +inputFileArg = optional $ strArgument (metavar fileMetavarName <> help [i|#{fileMetavarName} to read input from. When no #{fileMetavarName} is specified, read from stdin.|]) + +jsonSwitch :: Parser Bool +jsonSwitch = switch (long "json" <> short 'j' <> help "Output JSON.") + +cliTransformPhiParser :: Parser CLI'TransformPhi +cliTransformPhiParser = do + rulesPath <- strOption (long "rules" <> short 'r' <> help [i|#{fileMetavarName} with user-defined rules. Must be specified.|] <> fileMetavar) + chain <- switch (long "chain" <> short 'c' <> help "Output transformation steps.") + json <- jsonSwitch + outputFile <- outputFileOption + single <- switch (long "single" <> short 's' <> help "Output a single expression.") + inputFile <- inputFileArg + pure CLI'TransformPhi{..} + +cliMetricsPhiParser :: Parser CLI'MetricsPhi +cliMetricsPhiParser = do + inputFile <- inputFileArg + outputFile <- outputFileOption + pure CLI'MetricsPhi{..} -data CLIOptions = CLIOptions CLINamedParams (Maybe FilePath) - deriving (Generic, Show, ParseRecord) +metricsParserInfo :: ParserInfo CLI +metricsParserInfo = info (CLI'MetricsPhi' <$> cliMetricsPhiParser) (progDesc "Collect metrics for a PHI program.") + +transformParserInfo :: ParserInfo CLI +transformParserInfo = info (CLI'TransformPhi' <$> cliTransformPhiParser) (progDesc "Transform a PHI program.") + +transformCommandName :: String +transformCommandName = "transform" + +metricsCommandName :: String +metricsCommandName = "metrics" + +cli :: Parser CLI +cli = + hsubparser + ( command transformCommandName transformParserInfo + <> command metricsCommandName metricsParserInfo + ) + +cliOpts :: ParserInfo CLI +cliOpts = + info + (cli <**> helper) + (fullDesc <> progDesc "Work with PHI expressions.") data StructuredJSON = StructuredJSON { input :: String - , results :: [[String]] + , output :: [[String]] } deriving (Generic, ToJSON) -encodeString :: (ToJSON a) => a -> String -encodeString = (^. unpacked) . encodeToLazyText +encodeToJSONString :: (ToJSON a) => a -> String +encodeToJSONString = (^. unpacked) . toLazyText . encodePrettyToTextBuilder' defConfig{confIndent = Spaces 2} + +pprefs :: ParserPrefs +pprefs = prefs (showHelpOnEmpty <> showHelpOnError) + +die :: Optparse.Context -> String -> IO a +die parserContext message = do + handleParseResult . Failure $ + parserFailure pprefs cliOpts (ErrorMsg message) [parserContext] + +getProgram :: Optparse.Context -> Maybe FilePath -> IO Program +getProgram parserContext inputFile = do + src <- maybe getContents' readFile inputFile + case parseProgram src of + Left err -> die parserContext [i|"An error occurred when parsing the input program: #{err}|] + Right program -> pure program + +getLoggers :: Maybe FilePath -> IO (String -> IO (), String -> IO ()) +getLoggers outputFile = do + handle <- maybe (pure stdout) (`openFile` WriteMode) outputFile + pure + ( \x -> hPutStrLn handle x >> hFlush handle + , \x -> hPutStr handle x >> hFlush handle + ) main :: IO () main = do - opts <- getRecord "Normalizer" - let (CLIOptions params inPath) = opts - let (CLINamedParams{..}) = params - case rulesYaml of - Just path -> do - handle <- maybe (pure stdout) (`openFile` WriteMode) outPath - let logStr = hPutStr handle - let logStrLn = hPutStrLn handle - ruleSet <- parseRuleSetFromFile path + opts <- customExecParser pprefs cliOpts + case opts of + CLI'MetricsPhi' CLI'MetricsPhi{..} -> do + let parserContext = Optparse.Context metricsCommandName metricsParserInfo + program' <- getProgram parserContext inputFile + (logStrLn, _) <- getLoggers outputFile + let metrics = collectMetrics program' + logStrLn $ encodeToJSONString metrics + CLI'TransformPhi' CLI'TransformPhi{..} -> do + let parserContext = Optparse.Context transformCommandName transformParserInfo + program' <- getProgram parserContext inputFile + (logStrLn, logStr) <- getLoggers outputFile + ruleSet <- parseRuleSetFromFile rulesPath unless (single || json) $ logStrLn ruleSet.title - src <- maybe getContents readFile inPath - let progOrError = parseProgram src - case progOrError of - Left err -> error ("An error occurred parsing the input program: " <> err) - Right input@(Program bindings) -> do - let uniqueResults - | chain = applyRulesChain (Context (convertRule <$> ruleSet.rules) [Formation bindings] Sigma) (Formation bindings) - | otherwise = pure <$> applyRules (Context (convertRule <$> ruleSet.rules) [Formation bindings] Sigma) (Formation bindings) - totalResults = length uniqueResults - when (null uniqueResults || null (head uniqueResults)) $ error "Could not normalize the program" - let printFormationAsProgramOrObject = \case - Formation bindings' -> printTree $ Program bindings' - x -> printTree x - if single - then - logStrLn - . (if json then encodeString else id) - . printFormationAsProgramOrObject - $ head (head uniqueResults) - else do - if json - then - logStrLn . encodeString $ - StructuredJSON - { input = printTree input - , results = (printFormationAsProgramOrObject <$>) <$> uniqueResults - } - else do - logStrLn "Input:" - logStrLn (printTree input) - logStrLn "====================================================" - forM_ (zip [1 ..] uniqueResults) $ \(i, steps) -> do - logStrLn $ - "Result " <> show i <> " out of " <> show totalResults <> ":" - let n = length steps - forM_ (zip [1 ..] steps) $ \(k, step) -> do - when chain $ - logStr ("[ " <> show k <> " / " <> show n <> " ]") - logStrLn . printFormationAsProgramOrObject $ step - logStrLn "----------------------------------------------------" - hClose handle - -- TODO #48:15m still need to consider `chain` (should rewrite/change defaultMain to mainWithOptions) - Nothing -> defaultMain + let Program bindings = program' + uniqueResults + | chain = applyRulesChain (Context (convertRule <$> ruleSet.rules) [Formation bindings] Sigma) (Formation bindings) + | otherwise = pure <$> applyRules (Context (convertRule <$> ruleSet.rules) [Formation bindings] Sigma) (Formation bindings) + totalResults = length uniqueResults + when (null uniqueResults || null (head uniqueResults)) $ die parserContext [i|Could not normalize the program.|] + let printAsProgramOrAsObject = \case + Formation bindings' -> printTree $ Program bindings' + x -> printTree x + if + | single && json -> + logStrLn + . encodeToJSONString + . printAsProgramOrAsObject + $ head (head uniqueResults) + | single -> + logStrLn + . printAsProgramOrAsObject + $ head (head uniqueResults) + | json -> + logStrLn . encodeToJSONString $ + StructuredJSON + { input = printTree program' + , output = (printAsProgramOrAsObject <$>) <$> uniqueResults + } + | otherwise -> do + logStrLn "Input:" + logStrLn (printTree program') + logStrLn "====================================================" + forM_ (zip [1 ..] uniqueResults) $ \(index, steps) -> do + logStrLn $ + "Result " <> show index <> " out of " <> show totalResults <> ":" + let n = length steps + forM_ (zip [1 ..] steps) $ \(k, step) -> do + when chain $ + logStr ("[ " <> show k <> " / " <> show n <> " ]") + logStrLn . printAsProgramOrAsObject $ step + logStrLn "----------------------------------------------------" diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal index ba3d08287..0f7405137 100644 --- a/eo-phi-normalizer/eo-phi-normalizer.cabal +++ b/eo-phi-normalizer/eo-phi-normalizer.cabal @@ -66,10 +66,11 @@ library , lens , mtl , string-interpolate + , text , yaml default-language: Haskell2010 -executable normalize-phi +executable normalizer main-is: Main.hs other-modules: Paths_eo_phi_normalizer @@ -85,6 +86,7 @@ executable normalize-phi BNFC:bnfc >=2.9.4.1 build-depends: aeson + , aeson-pretty , array >=0.5.5.0 , base >=4.7 && <5 , directory @@ -93,8 +95,9 @@ executable normalize-phi , generic-lens , lens , mtl - , optparse-generic + , optparse-applicative , string-interpolate + , text , yaml default-language: Haskell2010 @@ -133,5 +136,6 @@ test-suite eo-phi-normalizer-test , lens , mtl , string-interpolate + , text , yaml default-language: Haskell2010 diff --git a/eo-phi-normalizer/package.yaml b/eo-phi-normalizer/package.yaml index 298af367b..e20350276 100644 --- a/eo-phi-normalizer/package.yaml +++ b/eo-phi-normalizer/package.yaml @@ -46,6 +46,7 @@ dependencies: - string-interpolate - lens - generic-lens + - text default-extensions: - ImportQualifiedPost @@ -75,7 +76,7 @@ library: - Language.EO.Phi.Rules.Syntax.Skel executables: - normalize-phi: + normalizer: main: Main.hs source-dirs: app ghc-options: @@ -84,7 +85,8 @@ executables: - -with-rtsopts=-N dependencies: - eo-phi-normalizer - - optparse-generic + - optparse-applicative + - aeson-pretty tests: eo-phi-normalizer-test: diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Metrics/Collect.hs b/eo-phi-normalizer/src/Language/EO/Phi/Metrics/Collect.hs index 3df16ca63..2e0d3630f 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Metrics/Collect.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Metrics/Collect.hs @@ -17,6 +17,7 @@ import Control.Lens ((+=)) import Control.Monad (forM_) import Control.Monad.State (State, execState) import Data.Aeson (FromJSON) +import Data.Aeson.Types (ToJSON) import Data.Generics.Labels () import GHC.Generics (Generic) import Language.EO.Phi.Rules.Common () @@ -28,7 +29,7 @@ data Metrics = Metrics , formations :: Int , dispatches :: Int } - deriving (Generic, Show, FromJSON, Eq) + deriving (Generic, Show, FromJSON, ToJSON, Eq) defaultMetrics :: Metrics defaultMetrics = diff --git a/flake.lock b/flake.lock index bb01383d7..d3cf6bbfa 100644 --- a/flake.lock +++ b/flake.lock @@ -16,6 +16,24 @@ "type": "github" } }, + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1705309234, + "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, "flakes": { "locked": { "lastModified": 1704589266, @@ -43,11 +61,63 @@ "url": "https://repo.maven.apache.org/maven2/org/apache/maven/wrapper/maven-wrapper/3.2.0/maven-wrapper-3.2.0.jar" } }, + "mdsh": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1708988125, + "narHash": "sha256-nx9+tTLliKBPT/TSKTBSYOYxglewOKiw+gYLBvV+9Bg=", + "owner": "deemp", + "repo": "mdsh", + "rev": "ab378bfd391e5147e29fb0812e1dea7e079a1559", + "type": "github" + }, + "original": { + "owner": "deemp", + "ref": "update-flake", + "repo": "mdsh", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1708847675, + "narHash": "sha256-RUZ7KEs/a4EzRELYDGnRB6i7M1Izii3JD/LyzH0c6Tg=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "2a34566b67bef34c551f204063faeecc444ae9da", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, "root": { "inputs": { "eoc": "eoc", "flakes": "flakes", - "maven-wrapper-jar": "maven-wrapper-jar" + "maven-wrapper-jar": "maven-wrapper-jar", + "mdsh": "mdsh" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" } } }, diff --git a/flake.nix b/flake.nix index 03b4f8d99..4de7dc746 100644 --- a/flake.nix +++ b/flake.nix @@ -11,6 +11,7 @@ flake = false; url = "https://repo.maven.apache.org/maven2/org/apache/maven/wrapper/maven-wrapper/3.2.0/maven-wrapper-3.2.0.jar"; }; + mdsh.url = "github:deemp/mdsh/update-flake"; }; outputs = inputs: inputs.flakes.makeFlake { inputs = { @@ -18,7 +19,7 @@ haskell-tools drv-tools devshell flakes-tools nixpkgs formatter slimlock; - inherit (inputs) eoc maven-wrapper-jar; + inherit (inputs) eoc maven-wrapper-jar mdsh; }; perSystem = { inputs, system }: let @@ -33,6 +34,7 @@ inherit (inputs.drv-tools.lib.${system}) mkShellApps; inherit (inputs.flakes-tools.lib.${system}) mkFlakesTools; inherit (inputs.haskell-tools.lib.${system}) toolsGHC; + mdsh = inputs.mdsh.packages.${system}.default; # --- Parameters --- @@ -96,6 +98,8 @@ cabal stack pkgs.gh + mdsh + pkgs.mdbook # `cabal` already has a `ghc` on its `PATH`, # so you may remove `ghc` from this list. # Then, you can access `ghc` like `cabal exec -- ghc --version`. @@ -131,7 +135,7 @@ }; }; - # + # # --- Haskell package --- @@ -165,6 +169,32 @@ description = "Run pipeline"; excludeShellChecks = [ "SC2139" ]; }; + + mdsh = { + runtimeInputs = [ + mdsh + pkgs.nodePackages.prettier + stack + ]; + text = '' + export LANG=C.utf8 + mdsh + # create sample program + mdsh -i site/docs/src/common/sample-program.md --work_dir . + # run commands on it + + ${lib.concatMapStringsSep "\n" + (x: "mdsh -i site/docs/src/${x} --work_dir .") + [ + "commands/normalizer.md" + "commands/normalizer-transform.md" + "commands/normalizer-metrics.md" + "contributing.md" + ] + } + prettier -w "**/*.md" + ''; + }; }; # --- Devshells --- diff --git a/hie.yaml b/hie.yaml index b55ca8337..923a5fe52 100644 --- a/hie.yaml +++ b/hie.yaml @@ -4,7 +4,7 @@ cradle: component: "eo-phi-normalizer:lib" - path: "eo-phi-normalizer/app/Main.hs" - component: "eo-phi-normalizer:exe:normalize-phi" + component: "eo-phi-normalizer:exe:normalizer" - path: "eo-phi-normalizer/app/Paths_eo_phi_normalizer.hs" component: "eo-phi-normalizer:exe:normalize-phi" diff --git a/site/docs/src/README.md b/site/docs/src/README.md deleted file mode 120000 index 8a33348c7..000000000 --- a/site/docs/src/README.md +++ /dev/null @@ -1 +0,0 @@ -../../../README.md \ No newline at end of file diff --git a/site/docs/src/SUMMARY.md b/site/docs/src/SUMMARY.md index 1a904800c..d27b77ad6 100644 --- a/site/docs/src/SUMMARY.md +++ b/site/docs/src/SUMMARY.md @@ -1,4 +1,9 @@ # Summary -- [README](./README.md) -- [User-defined rules](./user-defined-rules.md) +- [Introduction](./introduction.md) +- [Installation](./installation.md) +- [Commands](./commands.md) + - [normalizer](./commands/normalizer.md) + - [normalizer transform](./commands/normalizer-transform.md) + - [normalizer metrics](./commands/normalizer-metrics.md) +- [Contributing](./contributing.md) diff --git a/site/docs/src/commands.md b/site/docs/src/commands.md new file mode 100644 index 000000000..3d4a5c032 --- /dev/null +++ b/site/docs/src/commands.md @@ -0,0 +1,3 @@ +# Commands + +This section lists commands and options that you can use when you work with `normalizer`. diff --git a/site/docs/src/commands/normalizer-metrics.md b/site/docs/src/commands/normalizer-metrics.md new file mode 100644 index 000000000..08b57de5d --- /dev/null +++ b/site/docs/src/commands/normalizer-metrics.md @@ -0,0 +1,90 @@ +# normalizer metrics + +## Metrics + +We count: + +- [Object applications](#object-applications) +- [Object formations](#object-formations) +- [Dynamic dispatches](#dynamic-dispatches) +- [Dataless formations](#dataless-formations) + +### PHI grammar + +![phi-grammar](../media/phi-grammar.png) + +### Object formations + +- `⟦ d ↦ ∅, c ↦ ∅ ⟧` + +### Object applications + +- `ξ.b(c ↦ ⟦ ⟧)` + +### Dynamic dispatches + +- `ξ.ρ.c` + +### Dataless formations + +- `Primitive formation` - a formation that has a `Δ` attribute. + - `⟦ Δ ⤍ 00- ⟧` +- `Dataless formation` - not primitive and does not have attributes that map to primitive formations. + - `⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧` + - the outermost formation with attributes `d` and `c` is dataless because it is not primitive and its attributes do not map to primitive formations. + - `d` is not dataless because it has an attribute `ν` that maps to a primitive formation. + +## Environment + +{{#include ../common/sample-program.md}} + +## CLI + +### `--help` + +```$ as console +normalizer metrics --help +``` + +```console +Usage: normalizer metrics [FILE] [-o|--output-file FILE] + + Collect metrics for a PHI program. + +Available options: + FILE FILE to read input from. When no FILE is specified, + read from stdin. + -o,--output-file FILE Output to FILE. When this option is not specified, + output to stdout. + -h,--help Show this help text +``` + +### `FILE` + +```$ as json +normalizer metrics program.phi +``` + +```json +{ + "applications": 1, + "dataless": 5, + "dispatches": 5, + "formations": 5 +} +``` + +### `FILE` not specified (read from stdin) + +```$ as json +cat program.phi | normalizer metrics +``` + +```json +{ + "applications": 1, + "dataless": 5, + "dispatches": 5, + "formations": 5 +} +``` diff --git a/site/docs/src/commands/normalizer-transform.md b/site/docs/src/commands/normalizer-transform.md new file mode 100644 index 000000000..22b39f4c5 --- /dev/null +++ b/site/docs/src/commands/normalizer-transform.md @@ -0,0 +1,239 @@ +# normalizer transform + +## `MetaPHI` + +You can define [rewrite rules](https://en.wikipedia.org/wiki/Rewriting#Term_rewriting_systems) for the `PHI` language (the $\varphi$-calculus language) using `YAML` and the `MetaPHI` language that is a superset of `PHI`. + +See the `MetaPHI` [Labelled BNF](https://bnfc.readthedocs.io/en/latest/lbnf.html) in [Syntax.cf](https://github.com/objectionary/normalizer/blob/master/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf). + +## phi-paper rules + +Currently, the `PHI` normalizer supports rules defined in an unpublished paper by Yegor Bugayenko. + +![Rules](media/rules.jpg) + +### yegor.yaml + +These rules translated to `MetaPHI` are in [yegor.yaml](https://github.com/objectionary/normalizer/blob/master/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml). + +Each rule has the following structure: + +- `name` - Rule name. +- `description` - Rule description. +- `context` - (optional) Rule context. A context may contain: + - `global-object` - (optional) Global object `MetaId`. + - `current-object` - (optional) Current object `MetaId`. +- `pattern` - Term pattern. + - When this term pattern matches a subterm of a `PHI` term, `MetaId`s from the term pattern become associated with matching subexpressions of that subterm. +- `result` - Substitution result. + - `MetaId`s in the subterm pattern get replaced by their associated subexpressions. +- `when` - A list of conditions for pattern matching. + - `nf` - A list of `MetaId`s associated with subexpressions that shoud be in [normal form](#normal-form). + - `present_attrs` - A list of attributes that must be present in subexpression bindings. + - `attrs` - A list of attributes. Can include `MetaId`s. + - `bindings` - A list of bindings that must contain these attributes. + - `absent_attrs` - A list of attributes that must not be present in subexpression bindings. + - `attrs` - A list of attributes. Can include `MetaId`s. + - `bindings` - A list of bindings that must not contain these attributes. +- `tests` - A list of unit tests for this rule. + - `name` - Test name. + - `input` - An initial `PHI` term. + - `output` - The initial `PHI` term after this rule was applied. + - `matches` - Whether the term pattern should match any subterm. + +### Normal form + +An expression is in normal form when no rule can be applied to that expression. + +## Environment + +### Repository + +The commands in the following sections access files that are available in the project repository. +Clone and enter the repository directory. + +```sh +git clone https://github.com/objectionary/normalizer +cd normalizer +``` + +### Sample program + +{{#include ../common/sample-program.md}} + +## CLI + +### `--help` + +```$ as console +normalizer transform --help +``` + +```console +Usage: normalizer transform (-r|--rules FILE) [-c|--chain] [-j|--json] + [-o|--output-file FILE] [-s|--single] [FILE] + + Transform a PHI program. + +Available options: + -r,--rules FILE FILE with user-defined rules. Must be specified. + -c,--chain Output transformation steps. + -j,--json Output JSON. + -o,--output-file FILE Output to FILE. When this option is not specified, + output to stdout. + -s,--single Output a single expression. + FILE FILE to read input from. When no FILE is specified, + read from stdin. + -h,--help Show this help text +``` + +### `--rules` + +Normalize a 𝜑-expression from `program.phi` using the [yegor.yaml](#yegoryaml) rules. + +There can be multiple numbered results that correspond to multiple rule application sequences. + +```$ as console +normalizer transform --rules ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi +``` + +```console +Rule set based on Yegor's draft +Input: +{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +==================================================== +Result 1 out of 1: +{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +---------------------------------------------------- +``` + +### `--chain` + +Use `--chain` to see numbered normalization steps for each normalization result. + +```$ as console +normalizer transform --chain --rules ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi +``` + +```console +Rule set based on Yegor's draft +Input: +{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +==================================================== +Result 1 out of 6: +[ 1 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 2 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ } +[ 3 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +[ 4 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +---------------------------------------------------- +Result 2 out of 6: +[ 1 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 2 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ } +[ 3 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧ ⟧) ⟧ } +[ 4 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +---------------------------------------------------- +Result 3 out of 6: +[ 1 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 2 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 3 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +[ 4 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +---------------------------------------------------- +Result 4 out of 6: +[ 1 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 2 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 3 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 4 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +---------------------------------------------------- +Result 5 out of 6: +[ 1 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 2 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 3 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧ ⟧) ⟧ } +[ 4 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +---------------------------------------------------- +Result 6 out of 6: +[ 1 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 2 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 3 / 4 ]{ ⟦ a ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ } +[ 4 / 4 ]{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +---------------------------------------------------- +``` + +### `--json` + +```$ as json +normalizer transform --json --chain --rules ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi +``` + +```json +{ + "input": "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "output": [ + [ + "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }" + ], + [ + "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧ ⟧) ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }" + ], + [ + "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }" + ], + [ + "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }" + ], + [ + "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧ ⟧) ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }" + ], + [ + "{ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ }", + "{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }" + ] + ] +} +``` + +### `--single` + +```$ as console +normalizer transform --single --rules ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi +``` + +```console +{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ } +``` + +### `--single` `--json` + +```$ as console +normalizer transform --single --json --rules ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi +``` + +```console +"{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }" +``` + +### `FILE` not specified (read from stdin) + +```$ as console +cat program.phi | normalizer transform --single --json --rules ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml +``` + +```console +"{ ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }" +``` diff --git a/site/docs/src/commands/normalizer.md b/site/docs/src/commands/normalizer.md new file mode 100644 index 000000000..045acedbb --- /dev/null +++ b/site/docs/src/commands/normalizer.md @@ -0,0 +1,20 @@ +# normalizer + +See commands supported by the `normalizer` executable. + +```$ as console +normalizer --help +``` + +```console +Usage: normalizer COMMAND + + Work with PHI expressions. + +Available options: + -h,--help Show this help text + +Available commands: + transform Transform a PHI program. + metrics Collect metrics for a PHI program. +``` diff --git a/site/docs/src/common/normalize-phi-options.md b/site/docs/src/common/normalize-phi-options.md deleted file mode 100644 index 2d1ece1ea..000000000 --- a/site/docs/src/common/normalize-phi-options.md +++ /dev/null @@ -1,19 +0,0 @@ -Learn about `normalize-phi` options. - -```sh -normalize-phi --help -``` - -```console -Normalizer - -Usage: normalize-phi [-c|--chain] [--rules-yaml STRING] [-o|--output STRING] - [-s|--single] [STRING] - -Available options: - -h,--help Show this help text - -c,--chain Print out steps of reduction - --rules-yaml STRING Path to the Yaml file with custom rules - -o,--output STRING Output file path (defaults to stdout) - -s,--single Print a single normalized expression -``` diff --git a/site/docs/src/common/sample-program.md b/site/docs/src/common/sample-program.md index 05e56084b..1b35d6a58 100644 --- a/site/docs/src/common/sample-program.md +++ b/site/docs/src/common/sample-program.md @@ -1,7 +1,7 @@ Save a `PHI` program to a file. This program will be used in subsequent commands. -```sh +```$ cat > program.phi < The pre-commit hook is run first, before you even type in a commit message. It's used to inspect the snapshot that's about to be committed, to see if you've forgotten something, to make sure tests run, or to examine whatever you need to inspect in the code. Exiting non-zero from this hook aborts the commit ... + +- `pre-commit` stashes ([link](https://git-scm.com/docs/git-stash)) unstaged ([link](https://git-scm.com/book/en/v2/Getting-Started-What-is-Git%3F#_the_three_states)) files. + + ```console + [WARNING] Unstaged files detected. + [INFO] Stashing unstaged files to /home/eyjafjallajokull/.cache/pre-commit/patch1705090051-437857. + ``` + +- `pre-commit` runs hooks. +- A hook may exit with an error, e.g.: + + ```md + Format Haskell (.hs) files...............................................Failed + + - hook id: fourmolu + - exit code: 102 + - files were modified by this hook + ``` + + - In case of the [fourmolu](https://github.com/fourmolu/fourmolu) formatter, + it's assumed that formatting a formatted `Haskell` file doesn't modify it. + However, `pre-commit` runs the `fourmolu` hook and reports that it has modified some files. + This error won't allow you to commit. + +- `pre-commit` unstashes files. + +- You should stage all changes so that `pre-commit` does not complain. + + - In case of `fourmolu`, stage the formatted code regions. + +- Now, you can commit. diff --git a/site/docs/src/installation.md b/site/docs/src/installation.md new file mode 100644 index 000000000..8241bce77 --- /dev/null +++ b/site/docs/src/installation.md @@ -0,0 +1,35 @@ +# Installation + +Install the `normalizer` executable globally via [stack](https://docs.haskellstack.org/en/stable). +Then, the `normalizer` executable will be available on `PATH`. + +## Install from the repository + +```sh +git clone https://github.com/objectionary/normalizer +cd normalizer +export LANG=C.UTF-8 +stack install normalizer +``` + +## Install from Hackage + +```sh +stack update +export LANG=C.UTF-8 +stack install --resolver lts-22.11 eo-phi-normalizer +``` + +## Uninstall + +Learn where `stack` installs programs. + +```sh +stack path --programs +``` + +Learn how to uninstall a program. + +```sh +stack uninstall +``` diff --git a/site/docs/src/introduction.md b/site/docs/src/introduction.md new file mode 100644 index 000000000..4fa4e8dd6 --- /dev/null +++ b/site/docs/src/introduction.md @@ -0,0 +1,7 @@ +# Normalizer for 𝜑-calculus + +Command line normalizer of 𝜑-calculus (`PHI`) expressions (as produced by the [EO compiler](https://github.com/objectionary/eo)). + +This project aims to apply term rewriting techniques to "simplify" an input `PHI` expression and prepare it for further optimization passes. The simplification procedure will be a form of partial evaluation and normalization (see [normalizer transform](./commands/normalizer-transform.md)). + +Contrary to traditional normalization in λ-calculus, we aim at rewriting rules that would help reduce certain metrics of expressions (see [normalizer metrics](./commands/normalizer-metrics.md)). diff --git a/site/docs/src/media/phi-grammar.png b/site/docs/src/media/phi-grammar.png new file mode 100644 index 000000000..02aafb6ae Binary files /dev/null and b/site/docs/src/media/phi-grammar.png differ diff --git a/site/docs/src/user-defined-rules.md b/site/docs/src/user-defined-rules.md deleted file mode 100644 index a40256dfc..000000000 --- a/site/docs/src/user-defined-rules.md +++ /dev/null @@ -1,115 +0,0 @@ -# User-defined rules - -## `MetaPHI` - -You can define [rewrite rules](https://en.wikipedia.org/wiki/Rewriting#Term_rewriting_systems) for the `PHI` language (the $\varphi$-calculus language) using `YAML` and the `MetaPHI` language that is a superset of `PHI`. - -See the `MetaPHI` [Labelled BNF](https://bnfc.readthedocs.io/en/latest/lbnf.html) in [Syntax.cf](https://github.com/objectionary/normalizer/blob/master/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf). - -## phi-paper rules - -Currently, the `PHI` normalizer supports rules defined in an unpublished paper by Yegor Bugayenko. - -![Rules](media/rules.jpg) - -### yegor.yaml - -These rules translated to `MetaPHI` are in [yegor.yaml](https://github.com/objectionary/normalizer/blob/master/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml). - -Each rule has the following structure: - -- `name` - Rule name. -- `description` - Rule description. -- `context` - (optional) Rule context. A context may contain: - - `global-object` - (optional) Global object `MetaId`. - - `current-object` - (optional) Current object `MetaId`. -- `pattern` - Term pattern. - - When this term pattern matches a subterm of a `PHI` term, `MetaId`s from the term pattern become associated with matching subexpressions of that subterm. -- `result` - Substitution result. - - `MetaId`s in the subterm pattern get replaced by their associated subexpressions. -- `when` - A list of conditions for pattern matching. - - `nf` - A list of `MetaId`s associated with subexpressions that shoud be in [normal form](#normal-form). - - `present_attrs` - A list of attributes that must be present in subexpression bindings. - - `attrs` - A list of attributes. Can include `MetaId`s. - - `bindings` - A list of bindings that must contain these attributes. - - `absent_attrs` - A list of attributes that must not be present in subexpression bindings. - - `attrs` - A list of attributes. Can include `MetaId`s. - - `bindings` - A list of bindings that must not contain these attributes. -- `tests` - A list of unit tests for this rule. - - `name` - Test name. - - `input` - An initial `PHI` term. - - `output` - The initial `PHI` term after this rule was applied. - - `matches` - Whether the term pattern should match any subterm. - -### Normal form - - - -## Use rules - -{{#include ./common/normalize-phi-options.md}} - -### Sample program - -{{#include ./common/sample-program.md}} - -### Prepare environment - -The commands in the following sections access files that are available in the project repository. -Clone and enter the repository directory. - -```sh -git clone https://github.com/objectionary/normalizer -cd normalizer -``` - -#### `--ruleset-yaml` - -Normalize a 𝜑-expression from `program.phi` using the [yegor.yaml](#yegoryaml) rules. - -There can be multiple numbered results that correspond to multiple rule application sequences. - -```sh -normalize-phi --rules-yaml ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi -``` - -```console -Rule set based on Yegor's draft -Input: -{ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e } -==================================================== -Result 1 out of 1: -⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ ----------------------------------------------------- -``` - -#### `--chain` - -Use `--chain` to see numbered normalization steps for each normalization result. - -```sh -normalize-phi --chain --rules-yaml ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi -``` - -```console -Rule set based on Yegor's draft -Input: -{ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e } -==================================================== -Result 1 out of 1: -[ 1 / 2 ]⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧, e ↦ ξ.b (c ↦ ⟦ ⟧).d ⟧.e ⟧ -[ 2 / 2 ]⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ ----------------------------------------------------- -``` - -#### `--single` - -Use `--single` to print a single normalized program. - -```sh -normalize-phi --single --rules-yaml ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi -``` - -```console -⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ -```