Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor CLI and docs #153

Merged
Merged
Show file tree
Hide file tree
Changes from 34 commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
2e9077a
feat: use transform-phi and metrics-phi subcommands
deemp Feb 25, 2024
98e00a6
fix: executable name
deemp Feb 25, 2024
8dbf6ad
fix: switch to optparse-applicative
deemp Feb 26, 2024
dcfe91b
refactor: cli
deemp Feb 26, 2024
becae09
fix: remove unused option
deemp Feb 26, 2024
dd50987
feat: script to run mdsh
deemp Feb 26, 2024
3b6086e
chore: update mds
deemp Feb 26, 2024
129f2bc
feat: add markdownlint config
deemp Feb 26, 2024
49f0076
refactor: make command for sample program mdsh-runnable
deemp Feb 27, 2024
35e01e9
refactor: move `user-defined rules` to `normalizer transform`
deemp Feb 27, 2024
b125e0b
refactor: remove symlink to readme
deemp Feb 27, 2024
cd264b9
refactor: remove normalize-phi options page
deemp Feb 27, 2024
75c7f33
refactor: move `normalizer transform` docs
deemp Feb 27, 2024
fa266d9
fix: write to file strictly
deemp Feb 27, 2024
fe803d2
feat: support read from stdin
deemp Feb 27, 2024
ddf3c7b
refactor: move from readme to site
deemp Feb 27, 2024
f63185f
feat: installation page
deemp Feb 27, 2024
f0cab74
feat: contributing page
deemp Feb 27, 2024
d0bd6d6
feat: normalizer-metrics page
deemp Feb 27, 2024
e82869b
refactor: normalizer-transform page
deemp Feb 27, 2024
0f3df58
feat: normalizer page
deemp Feb 27, 2024
f7fede4
feat: introduction page
deemp Feb 27, 2024
42ef088
fix: include new sections into summary
deemp Feb 27, 2024
f26482a
feat: include phi-grammar
deemp Feb 27, 2024
407bdca
fix: update dependencies
deemp Feb 27, 2024
566f0aa
fix: pretty-print json output
deemp Feb 27, 2024
5a61fe0
refactor: format
deemp Feb 27, 2024
5610078
fix: run mdsh script on more files
deemp Feb 27, 2024
03c4223
feat: add mdbook to devshell
deemp Feb 27, 2024
bd3b55d
fix: include `normalizer` into summary
deemp Feb 27, 2024
4c3dd3f
refactor: remove toc
deemp Feb 27, 2024
97ea0a0
feat: commands page
deemp Feb 27, 2024
d035d6e
feat: links to commands pages
deemp Feb 27, 2024
b2ceb5d
feat: top-level `commands` section
deemp Feb 27, 2024
bc4cc56
refactor: remove ImplicitParams
deemp Feb 28, 2024
1d06413
refactor: use MultiWayIf
deemp Feb 28, 2024
5ecd803
fix: names
deemp Feb 28, 2024
c159261
refactor: dataless formation definition
deemp Feb 28, 2024
b69a7a1
refactor: simplify reading the program in the `transform` command
deemp Feb 28, 2024
3b87fd7
chore: update CLI docs
deemp Feb 28, 2024
f3c2c36
fix: CLI option descriptions
deemp Feb 28, 2024
fbb182b
chore: update docs
deemp Feb 28, 2024
4e4f676
Merge remote-tracking branch 'origin' into 147-add-a-command-to-print…
deemp Feb 28, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .markdownlint.jsonc
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
{
"MD013": false
}
378 changes: 1 addition & 377 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 <<EOM
{
a ↦
b ↦
c ↦ ∅,
d ↦ ⟦ φ ↦ ξ.ρ.c ⟧
⟧,
e ↦ ξ.b(c ↦ ⟦⟧).d
⟧.e
}
EOM
```

### 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 a ruleset (See [Rulesets](#rulesets)).

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 ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }
----------------------------------------------------
```

#### Input

Normalize an expression using a ruleset (See [Rulesets](#rulesets)).
Read the expression from stdin.

```sh
cat program.phi | normalize-phi --rules-yaml ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
```

```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- ⟧ ⟧ ⟧) ⟧ }
----------------------------------------------------
```

Alternatively, the path to the file containing a Phi expression can be passed as a positional argument:

```sh
normalize-phi --rules-yaml ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi
```

#### `--chain`

Use `--chain` to see numbered normalization steps for each normalization result.

```sh
cat program.phi | normalize-phi --chain --rules-yaml ./eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
```

```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- ⟧ ⟧ ⟧) ⟧ }
----------------------------------------------------
```

#### `--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 ↦ ⟦ d ↦ ⟦ φ ↦ ξ.ρ.c, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, c ↦ ∅, ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧) ⟧ }
```

#### Output

By default, the normalization output will be printed to `stdout`.
The `--output` CLI option (or its shorthand `-o`) can be used to specify the path to the file to which the output will be written instead.
The file will be created if it didn't originally exist.

This is equivalent to redirecting the output from `stdout` to a file using `>`.

## 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 `!<Identifier>`.
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.
Loading
Loading