From a9191c4c86995f5860c4eddb7d71fd01a620786a Mon Sep 17 00:00:00 2001 From: eyihluyc Date: Wed, 4 Dec 2024 23:53:57 +0300 Subject: [PATCH] Add examples to rewrite docs --- site/docs/src/eo-phi-normalizer/rewrite.md | 63 ++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/site/docs/src/eo-phi-normalizer/rewrite.md b/site/docs/src/eo-phi-normalizer/rewrite.md index 6825a1ce1..9cfd87175 100644 --- a/site/docs/src/eo-phi-normalizer/rewrite.md +++ b/site/docs/src/eo-phi-normalizer/rewrite.md @@ -166,6 +166,49 @@ Result 1 out of 1: ---------------------------------------------------- ``` +### `--chain` `--tex` + +```$ as tex +eo-phi-normalizer rewrite --chain --tex bar.phi +``` + +```tex +% Rule set following Nov 2024 revision + +\documentclass{article} +\usepackage{eolang} +\begin{document} + + +This is the 1st possible chain of normalizing rewritings: + +\begin{phiquation*} +[[ m -> [[ x -> [[ t -> [[ D> 42- ]] ]].t ]].x ]] \trans_{\rulename{DOT}} + \trans [[ m -> [[ x -> [[ D> 42- ]]( ^ -> [[ t -> [[ D> 42- ]] ]] ) ]].x ]] \trans_{\rulename{DOT}} + \trans [[ m -> [[ D> 42- ]]( ^ -> [[ t -> [[ D> 42- ]] ]] )( ^ -> [[ x -> [[ D> 42- ]]( ^ -> [[ t -> [[ D> 42- ]] ]] ) ]] ) ]] \trans_{\rulename{RHO}} + \trans [[ m -> [[ D> 42-, ^ -> [[ t -> [[ D> 42- ]] ]] ]]( )( ^ -> [[ x -> [[ D> 42- ]]( ^ -> [[ t -> [[ D> 42- ]] ]] ) ]] ) ]] \trans_{\rulename{DUP}} + \trans [[ m -> [[ D> 42-, ^ -> [[ t -> [[ D> 42- ]] ]] ]]( ^ -> [[ x -> [[ D> 42- ]]( ^ -> [[ t -> [[ D> 42- ]] ]] ) ]] ) ]] \trans_{\rulename{STAY}} + \trans [[ m -> [[ ^ -> [[ t -> [[ D> 42- ]] ]], D> 42- ]]( ) ]] \trans_{\rulename{DUP}} + \trans [[ m -> [[ ^ -> [[ t -> [[ D> 42- ]] ]], D> 42- ]] ]] \trans_{\rulename{Normal form}} + \trans [[ m -> [[ ^ -> [[ t -> [[ D> 42- ]] ]], D> 42- ]] ]]. +\end{phiquation*} + +This is the 2nd possible chain of normalizing rewritings: + +\begin{phiquation*} +[[ m -> [[ x -> [[ t -> [[ D> 42- ]] ]].t ]].x ]] \trans_{\rulename{DOT}} + \trans [[ m -> [[ x -> [[ D> 42- ]]( ^ -> [[ t -> [[ D> 42- ]] ]] ) ]].x ]] \trans_{\rulename{RHO}} + \trans [[ m -> [[ x -> [[ D> 42-, ^ -> [[ t -> [[ D> 42- ]] ]] ]]( ) ]].x ]] \trans_{\rulename{DUP}} + \trans [[ m -> [[ x -> [[ D> 42-, ^ -> [[ t -> [[ D> 42- ]] ]] ]] ]].x ]] \trans_{\rulename{DOT}} + \trans [[ m -> [[ D> 42-, ^ -> [[ t -> [[ D> 42- ]] ]] ]]( ^ -> [[ x -> [[ D> 42-, ^ -> [[ t -> [[ D> 42- ]] ]] ]] ]] ) ]] \trans_{\rulename{STAY}} + \trans [[ m -> [[ ^ -> [[ t -> [[ D> 42- ]] ]], D> 42- ]]( ) ]] \trans_{\rulename{DUP}} + \trans [[ m -> [[ ^ -> [[ t -> [[ D> 42- ]] ]], D> 42- ]] ]] \trans_{\rulename{Normal form}} + \trans [[ m -> [[ ^ -> [[ t -> [[ D> 42- ]] ]], D> 42- ]] ]]. +\end{phiquation*} + +\end{document} +``` + ### `--json` ```$ as json @@ -235,6 +278,26 @@ eo-phi-normalizer rewrite --single --json --rules ./eo-phi-normalizer/test/eo/ph "{\n ⟦\n c ↦ Φ.org.eolang.float (\n as-bytes ↦ Φ.org.eolang.bytes (\n Δ ⤍ 40-39-00-00-00-00-00-00\n )\n ),\n result ↦ ξ.c.times (\n x ↦ ⟦\n Δ ⤍ 3F-FC-CC-CC-CC-CC-CC-CD\n ⟧\n )\n .plus (\n x ↦ ⟦\n Δ ⤍ 40-40-00-00-00-00-00-00\n ⟧\n ),\n λ ⤍ Package\n ⟧\n}" ``` +### `--tex` + +```$ as tex +eo-phi-normalizer rewrite --tex bar.phi +``` + +```tex +% Rule set following Nov 2024 revision + +\documentclass{article} +\usepackage{eolang} +\begin{document} + +\begin{phiquation*} +[[ m -> [[ ^ -> [[ t -> [[ D> 42- ]] ]], D> 42- ]] ]] +\end{phiquation*} + +\end{document} +``` + ### `--output-file FILE` Redirects the output to file of the given path instead of `stdout`.