From 6f71e538ffbdd68a0728008cce90fbd7cf27ae57 Mon Sep 17 00:00:00 2001
From: Marek Kaluba <kalmar@amu.edu.pl>
Date: Mon, 2 Oct 2023 15:20:52 +0200
Subject: [PATCH] rewrite `rewrite` docs :D

---
 docs/src/rewriting.md | 32 ++++++++++++++++++++------------
 src/rewriting.jl      |  2 +-
 2 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/docs/src/rewriting.md b/docs/src/rewriting.md
index 77ca6715..43d3916f 100644
--- a/docs/src/rewriting.md
+++ b/docs/src/rewriting.md
@@ -10,7 +10,9 @@ rewrite
 
 ## Internals
 
-The general rewriting follows the _destructive_ semantics in which
+Implementing rewriting procedure naively could easily lead to quadratic
+complexity due to unnecessary moves of parts of the rewritten word.
+We follow the the linear-complexity algorithm in which we use two stacks and
 `rewrite` function calls internally
 
 ```julia
@@ -20,17 +22,23 @@ function rewrite!(v::AbstractWord, w::AbstractWord, rewriting; kwargs...)
 end
 ```
 
-The semantics are that `v` can be thought of as initially trivial (i.e. empty)
-word, and we want to rewrite `w` **onto** `v`.
-In all our implementations the process follows as follows
-
- 1. we pop the first letter `l = popfirst!(w)` from `w`,
- 2. we push `l` to the end of `v`,
- 3. we try to determine a rewritng rule `lhs → rhs` with `v = v'·lhs` (i.e.
-    `lhs` is equal to a suffix of `v`) and we set
-    * `v ← v'` i.e. we remove the suffix fom `v`, and
-    * `w ← rhs·w` i.e. `rhs` is _prepended_ to `w`
- 4. if no such rule exists we go back to 1.
+The semantics are that `v` and `w` are two stacks and
+
+* `v` is initially empty (represents the trivial word), while
+* `w` contains the content of `u` (the word to be rewritten with its first
+  letter on its top).
+
+In practice we use [`BufferWord`s](@ref Words.BufferWord) (a special
+implementation of `AbstractWord` API) and all our implementations the process
+is as follows.
+
+1. we pop the first letter `l = popfirst!(w)` from `w`,
+2. we push `l` to the end of `v`,
+3. we try to determine a rewritng rule `lhs → rhs` with `v = v'·lhs` (i.e.
+   `lhs` is equal to a suffix of `v`) and we set
+   * `v ← v'` i.e. we remove the suffix fom `v`, and
+   * `w ← rhs·w` i.e. `rhs` is _prepended_ to `w`
+4. if no such rule exists we go back to 1.
 
 These four steps are repeated until `w` becomes empty.
 
diff --git a/src/rewriting.jl b/src/rewriting.jl
index c3c76c68..f4be257e 100644
--- a/src/rewriting.jl
+++ b/src/rewriting.jl
@@ -1,6 +1,6 @@
 """
     rewrite(u::AbstractWord, rewriting)
-Rewrites word `u` (from left) using `rewriting` object. The object must implement
+Rewrites word `u` using the `rewriting` object. The object must implement
 `rewrite!(v::AbstractWord, w::AbstractWord, rewriting)`.
 
 # Example