objectionary / normalizer

Command Line Normalizer of 𝜑-calculus Expressions
https://www.objectionary.com/normalizer/
MIT License
7 stars 2 forks source link

Support printing rules in LaTeX #474

Closed eyihluyc closed 1 week ago

eyihluyc commented 4 weeks ago

Issue: #471

This PR adds printing rules in LaTeX format.

Usage:

normalizer print-rules --tex -r filename

PR-Codex overview

This PR introduces a new feature to print rules in LaTeX format, enhances command line options, updates documentation, and adds new imports.

Detailed summary

The following files were skipped due to too many changes: eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs, eo-phi-normalizer/test/eo/phi/rules/yegor.yaml, site/docs/src/normalizer/print-rules.md

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

eyihluyc commented 4 weeks ago

There are two versions now:

  1. When conditions are listed on new lines image
\begin{figure*}
\begin{tabular}{rl}
  \rrule{Phi}: & $ Q $ \(\trans\) $ b $ \\\text {if }& $ Q -> b $ \\&not in subformations\\\\
  \rrule{xi}: & $ \xi $ \(\trans\) $ b $ \\\text {if }& $ b $  is the scope of the redex\\&not in subformations\\\\
  \rrule{DOT}: & $ [[ \tau -> b, B ]].\tau $ \(\trans\) $ \mathbb{S}(b, [[ \tau -> b, B ]]) $ \\\text {if }&not in subformations,\\& $ b $  is nf inside formation,\\& $ [[ B ]]\in\mathcal{N} $ ,\\& $ \tau \neq ^ $ \\\\
  \rrule{DOTrho}: & $ [[ ^ -> b, B ]].^ $ \(\trans\) $ b $ \\\text {if }& $ [[ B ]]\in\mathcal{N} $ \\\\
  \rrule{phi}: & $ [[ B ]].\tau $ \(\trans\) $ [[ B ]].@.\tau $ \\\text {if }& $ @ \in B $ ,\\& $ \tau \notin B $ \\\\
  \rrule{COPY}: & $ [[ \tau -> ?, B1 ]]( \tau -> b1, B2 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B1 ]]( B2 ) $ \\\text {if }& $ b2 $  is the scope of the redex\\&not in subformations,\\& $ b1\in\mathcal{N} $ \\\\
  \rrule{COPY1}: & $ [[ \tau -> ?, B ]]( 0-> b1 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B ]] $ \\\text {if }& $ b2 $  is the scope of the redex\\&not in subformations,\\& $ b1\in\mathcal{N} $ \\\\
  \rrule{COPY2}: & $ [[ \tau1 -> ?, \tau2 -> ?, B ]]( 0-> b1, 1-> b2 ) $ \(\trans\) $ [[ \tau1 -> \mathbb{S}(b1, b3), \tau2 -> \mathbb{S}(b2, b3), B ]] $ \\\text {if }& $ b3 $  is the scope of the redex\\&not in subformations,\\& $ b1\in\mathcal{N} $ ,\\& $ b2\in\mathcal{N} $ \\\\
  \rrule{COPYdelta}: & $ [[ D> ?, B ]]( D> y ) $ \(\trans\) $ [[ D> y, B ]] $ \\\text {if }&not in subformations\\\\
  \rrule{EMPTY}: & $ [[ B1 ]](  ) $ \(\trans\) $ [[ B1 ]] $ \\\\
  \rrule{OVER}: & $ [[ \tau -> b1, B1 ]]( \tau -> b2, B2 ) $ \(\trans\) $ \dead $ \\\\
  \rrule{STOP}: & $ [[ B ]].\tau $ \(\trans\) $ \dead $ \\\text {if }& $ \tau, @, \lambda \notin B $ ,\\& $ [[ B ]]\in\mathcal{N} $ \\\\
  \rrule{MISS}: & $ [[ B1 ]]( \tau -> b, B2 ) $ \(\trans\) $ \dead $ \\\text {if }& $ \tau, @, \lambda \notin B1 $ \\\\
  \rrule{DD}: & $ \dead.\tau $ \(\trans\) $ \dead $ \\\\
  \rrule{DC}: & $ \dead( B ) $ \(\trans\) $ \dead $ \\\\
\end{tabular}
\end{figure*}
  1. When the whole rule is one line (but this one is commented out) image
\begin{figure*}
  \rrule{Phi}:  $ Q $ \(\trans\) $ b $ \quad\text {if } $ Q -> b $ , not in subformations\\\vspace*{0.5em}
  \rrule{xi}:  $ \xi $ \(\trans\) $ b $ \quad\text {if } $ b $  is the scope of the redex, not in subformations\\\vspace*{0.5em}
  \rrule{DOT}:  $ [[ \tau -> b, B ]].\tau $ \(\trans\) $ \mathbb{S}(b, [[ \tau -> b, B ]]) $ \quad\text {if }not in subformations,  $ b $  is nf inside formation,  $ [[ B ]]\in\mathcal{N} $ ,  $ \tau \neq ^ $ \\\vspace*{0.5em}
  \rrule{DOTrho}:  $ [[ ^ -> b, B ]].^ $ \(\trans\) $ b $ \quad\text {if } $ [[ B ]]\in\mathcal{N} $ \\\vspace*{0.5em}
  \rrule{phi}:  $ [[ B ]].\tau $ \(\trans\) $ [[ B ]].@.\tau $ \quad\text {if } $ @ \in B $ ,  $ \tau \notin B $ \\\vspace*{0.5em}
  \rrule{COPY}:  $ [[ \tau -> ?, B1 ]]( \tau -> b1, B2 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B1 ]]( B2 ) $ \quad\text {if } $ b2 $  is the scope of the redex, not in subformations,  $ b1\in\mathcal{N} $ \\\vspace*{0.5em}
  \rrule{COPY1}:  $ [[ \tau -> ?, B ]]( 0-> b1 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B ]] $ \quad\text {if } $ b2 $  is the scope of the redex, not in subformations,  $ b1\in\mathcal{N} $ \\\vspace*{0.5em}
  \rrule{COPY2}:  $ [[ \tau1 -> ?, \tau2 -> ?, B ]]( 0-> b1, 1-> b2 ) $ \(\trans\) $ [[ \tau1 -> \mathbb{S}(b1, b3), \tau2 -> \mathbb{S}(b2, b3), B ]] $ \quad\text {if } $ b3 $  is the scope of the redex, not in subformations,  $ b1\in\mathcal{N} $ ,  $ b2\in\mathcal{N} $ \\\vspace*{0.5em}
  \rrule{COPYdelta}:  $ [[ D> ?, B ]]( D> y ) $ \(\trans\) $ [[ D> y, B ]] $ \quad\text {if }not in subformations\\\vspace*{0.5em}
  \rrule{EMPTY}:  $ [[ B1 ]](  ) $ \(\trans\) $ [[ B1 ]] $ \\\vspace*{0.5em}
  \rrule{OVER}:  $ [[ \tau -> b1, B1 ]]( \tau -> b2, B2 ) $ \(\trans\) $ \dead $ \\\vspace*{0.5em}
  \rrule{STOP}:  $ [[ B ]].\tau $ \(\trans\) $ \dead $ \quad\text {if } $ \tau, @, \lambda \notin B $ ,  $ [[ B ]]\in\mathcal{N} $ \\\vspace*{0.5em}
  \rrule{MISS}:  $ [[ B1 ]]( \tau -> b, B2 ) $ \(\trans\) $ \dead $ \quad\text {if } $ \tau, @, \lambda \notin B1 $ \\\vspace*{0.5em}
  \rrule{DD}:  $ \dead.\tau $ \(\trans\) $ \dead $ \\\vspace*{0.5em}
  \rrule{DC}:  $ \dead( B ) $ \(\trans\) $ \dead $ \\\vspace*{0.5em}
\end{figure*}
deemp commented 4 weeks ago

@yegor256, which version(s) should normalizer support?

yegor256 commented 4 weeks ago

@deemp the second one, please

deemp commented 3 weeks ago

@yegor256, I believe normalizer may support both versions since both versions are implemented.

I suggest to introduce the compact (short version is c) flag that will determine the version.

@eyihluyc, @yegor256, WDYT?

yegor256 commented 3 weeks ago

@deemp sounds good to me

fizruk commented 3 weeks ago

@eyihluyc can you please look into the failing tests?

deemp commented 3 weeks ago

@eyihluyc, please document this new command and its options in a new site file.

  1. Create site/docs/src/normalizer/print-rules.md.
  2. Update the ToC in normalizer/site/docs/src/SUMMARY.md
  3. Write in print-rules.md about the command and its options.
  4. Demonstrate the output of the command with different options. The output will be generated by mdsh in CI if you insert blocks like this.
```$ as latex
normalizer print-rules --tex -r filename
```
deemp commented 2 weeks ago

@eyihluyc, if you use nix, insert here a line for normalizer/print-rules.md. Next, run nix run .#update-markdown. This command will run mdsh on the print-rules.md file, generate scripts/update-markdown.sh and update other Markdown files.

Otherwise, insert a line for normalizer/print-rules.md both here and here, so that the script update-markdown.sh is in sync with the flake script update-markdown. Then, run scripts/update-markdown.sh.

0crat commented 1 week ago

@fizruk Great job on the review! 🎉 You've earned an impressive +11 points: +4 base points and +7 for reviewing 716 hits-of-code. Your dedication is paying off, as your balance now stands at +29. Keep up the excellent work!

0crat commented 1 week ago

@eyihluyc Thank you for your contribution! We appreciate your effort, but there are a few points to consider. Your submission of 495 hits-of-code exceeds our 200 limit, resulting in an 8-point deduction. However, you've earned 4 base points for your contribution. Your final score for this submission is -4 points. Remember to keep your contributions concise and focused. Your updated running balance is -10. We look forward to your future contributions!