From a9191c4c86995f5860c4eddb7d71fd01a620786a Mon Sep 17 00:00:00 2001 From: eyihluyc Date: Wed, 4 Dec 2024 23:53:57 +0300 Subject: [PATCH 1/3] 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 6825a1ce..9cfd8717 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`. From 820a39e456a9f47498e1bcbd7f8d56c6b0369381 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Thu, 5 Dec 2024 02:00:04 +0300 Subject: [PATCH 2/3] fix(site): create a file with a sample program before rewriting the program in that file --- site/docs/src/eo-phi-normalizer/rewrite.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/site/docs/src/eo-phi-normalizer/rewrite.md b/site/docs/src/eo-phi-normalizer/rewrite.md index 9cfd8717..1a75255c 100644 --- a/site/docs/src/eo-phi-normalizer/rewrite.md +++ b/site/docs/src/eo-phi-normalizer/rewrite.md @@ -169,6 +169,8 @@ Result 1 out of 1: ### `--chain` `--tex` ```$ as tex +printf "{⟦ m ↦ ⟦ x ↦ ⟦ t ↦ ⟦ Δ ⤍ 42- ⟧ ⟧.t ⟧.x ⟧}" > bar.phi + eo-phi-normalizer rewrite --chain --tex bar.phi ``` From e81c0684fa9721f8ea57b43392c743a2a24409f7 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Thu, 5 Dec 2024 02:02:22 +0300 Subject: [PATCH 3/3] fix(scripts): remove the file with a sample program --- scripts/update-markdown.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update-markdown.sh b/scripts/update-markdown.sh index 1c98cd17..6233a42c 100755 --- a/scripts/update-markdown.sh +++ b/scripts/update-markdown.sh @@ -41,7 +41,7 @@ mdsh -i site/docs/src/contributing.md --work_dir . cp site/docs/docs/markdown/contributing.md CONTRIBUTING.md -rm celsius.phi +rm celsius.phi bar.phi npm i npx prettier -w "**/*.md"