1+ // ===--- LeftCanonicalForm.cpp - Left canonical form of a rewrite path ----===//
2+ //
3+ // This source file is part of the Swift.org open source project
4+ //
5+ // Copyright (c) 2021 Apple Inc. and the Swift project authors
6+ // Licensed under Apache License v2.0 with Runtime Library Exception
7+ //
8+ // See https://swift.org/LICENSE.txt for license information
9+ // See https://swift.org/CONTRIBUTORS.txt for the list of Swift project authors
10+ //
11+ // ===----------------------------------------------------------------------===//
12+ //
13+ // Algorithm for reducing a rewrite path to left-canonical form:
14+ //
15+ // - Adjacent steps that are inverses of each other cancel out. for example
16+ // these two steps will be eliminated:
17+ //
18+ // (A => B) ⊗ (B => A)
19+ //
20+ // - Interchange law moves rewrites "to the left", for example
21+ //
22+ // X.(U => V) ⊗ (X => Y).V
23+ //
24+ // becomes
25+ //
26+ // (X => Y).U ⊗ Y.(U => V)
27+ //
28+ // These two transformations are iterated until fixed point to produce a
29+ // equivalent rewrite path that is simpler.
30+ //
31+ // From "Homotopy reduction systems for monoid presentations",
32+ // https://www.sciencedirect.com/science/article/pii/S0022404997000959
33+ //
34+ // ===----------------------------------------------------------------------===//
35+
36+ #include " RewriteLoop.h"
37+ #include " RewriteSystem.h"
38+ #include " llvm/ADT/SmallVector.h"
39+ #include < utility>
40+
41+ using namespace swift ;
42+ using namespace rewriting ;
43+
44+ // / Returns true if this rewrite step is an inverse of \p other
45+ // / (and vice versa).
46+ bool RewriteStep::isInverseOf (const RewriteStep &other) const {
47+ if (Kind != other.Kind )
48+ return false ;
49+
50+ if (StartOffset != other.StartOffset )
51+ return false ;
52+
53+ if (Inverse != !other.Inverse )
54+ return false ;
55+
56+ switch (Kind) {
57+ case RewriteStep::Rule:
58+ return Arg == other.Arg ;
59+
60+ default :
61+ return false ;
62+ }
63+
64+ assert (EndOffset == other.EndOffset && " Bad whiskering?"
65+ return true ;
66+ }
67+
68+ bool RewriteStep::maybeSwapRewriteSteps (RewriteStep &other,
69+ const RewriteSystem &system) {
70+ if (Kind != RewriteStep::Rule ||
71+ other.Kind != RewriteStep::Rule)
72+ return false ;
73+
74+ // Two rewrite steps are _orthogonal_ if they rewrite disjoint subterms
75+ // in context. Orthogonal rewrite steps commute, so we can canonicalize
76+ // a path by placing the left-most step first.
77+ //
78+ // Eg, A.U.B.(X => Y).C ⊗ A.(U => V).B.Y == A.(U => V).B.X ⊗ A.V.B.(X => Y).
79+ //
80+ // Or, in diagram form. We want to turn this:
81+ //
82+ // ----- time ----->
83+ // +---------+---------+
84+ // | A | A |
85+ // +---------+---------+
86+ // | U | U ==> V |
87+ // +---------+---------+
88+ // | B | B |
89+ // +---------+---------+
90+ // | X ==> Y | Y |
91+ // +---------+---------+
92+ // | C | C |
93+ // +---------+---------+
94+ //
95+ // Into this:
96+ //
97+ // +---------+---------+
98+ // | A | A |
99+ // +---------+---------+
100+ // | U ==> V | V |
101+ // +---------+---------+
102+ // | B | B |
103+ // +---------+---------+
104+ // | X | X ==> Y |
105+ // +---------+---------+
106+ // | C | C |
107+ // +---------+---------+
108+ //
109+ // Note that
110+ //
111+ // StartOffset == |A|+|U|+|B|
112+ // EndOffset = |C|
113+ //
114+ // other.StartOffset = |A|
115+ // other.EndOffset = |B|+|Y|+|C|
116+ //
117+ // After interchange, we adjust:
118+ //
119+ // StartOffset = |A|
120+ // EndOffset = |B|+|X|+|C|
121+ //
122+ // other.StartOffset = |A|+|V|+|B|
123+ // other.EndOffset = |C|
124+
125+ const auto &rule = system.getRule (Arg);
126+ auto lhs = (Inverse ? rule.getRHS () : rule.getLHS ());
127+ auto rhs = (Inverse ? rule.getLHS () : rule.getRHS ());
128+
129+ const auto &otherRule = system.getRule (other.Arg );
130+ auto otherLHS = (other.Inverse ? otherRule.getRHS () : otherRule.getLHS ());
131+ auto otherRHS = (other.Inverse ? otherRule.getLHS () : otherRule.getRHS ());
132+
133+ if (StartOffset < other.StartOffset + otherLHS.size ())
134+ return false ;
135+
136+ std::swap (*this , other);
137+ EndOffset += (lhs.size () - rhs.size ());
138+ other.StartOffset += (otherRHS.size () - otherLHS.size ());
139+
140+ return true ;
141+ }
142+
143+ // / Cancels out adjacent rewrite steps that are inverses of each other.
144+ // / This does not change either endpoint of the path, and the path does
145+ // / not necessarily need to be a loop.
146+ bool RewritePath::computeFreelyReducedForm () {
147+ SmallVector<RewriteStep, 4 > newSteps;
148+ bool changed = false ;
149+
150+ for (const auto &step : Steps) {
151+ if (!newSteps.empty () &&
152+ newSteps.back ().isInverseOf (step)) {
153+ changed = true ;
154+ newSteps.pop_back ();
155+ continue ;
156+ }
157+
158+ newSteps.push_back (step);
159+ }
160+
161+ if (!changed)
162+ return false ;
163+ std::swap (newSteps, Steps);
164+ return changed;
165+ }
166+
167+ // / Apply the interchange rule until fixed point (see maybeSwapRewriteSteps()).
168+ bool RewritePath::computeLeftCanonicalForm (const RewriteSystem &system) {
169+ bool changed = false ;
170+
171+ for (unsigned i = 1 , e = Steps.size (); i < e; ++i) {
172+ auto &prevStep = Steps[i - 1 ];
173+ auto &step = Steps[i];
174+
175+ if (prevStep.maybeSwapRewriteSteps (step, system))
176+ changed = true ;
177+ }
178+
179+ return changed;
180+ }
181+
182+ // / Compute freely-reduced left-canonical normal form of a path.
183+ void RewritePath::computeNormalForm (const RewriteSystem &system) {
184+ // FIXME: This can be more efficient.
185+ bool changed;
186+ do {
187+ changed = false ;
188+ changed |= computeFreelyReducedForm ();
189+ changed |= computeLeftCanonicalForm (system);
190+ } while (changed);
191+ }
192+
193+ // / Given a path that is a loop around the given basepoint, cancels out
194+ // / pairs of terms from the ends that are inverses of each other, applying
195+ // / the corresponding translation to the basepoint.
196+ // /
197+ // / For example, consider this loop with basepoint 'X':
198+ // /
199+ // / (X => Y.A) * (Y.A => Y.B) * Y.(B => A) * (Y.A => X)
200+ // /
201+ // / The first step is the inverse of the last step, so the cyclic
202+ // / reduction is the loop (Y.A => Y.B) * Y.(B => A), with a new
203+ // / basepoint 'Y.A'.
204+ bool RewritePath::computeCyclicallyReducedForm (MutableTerm &basepoint,
205+ const RewriteSystem &system) {
206+ RewritePathEvaluator evaluator (basepoint);
207+ unsigned count = 0 ;
208+
209+ while (2 * count + 1 < size ()) {
210+ auto left = Steps[count];
211+ auto right = Steps[Steps.size () - count - 1 ];
212+ if (!left.isInverseOf (right))
213+ break ;
214+
215+ // Update the basepoint by applying the first step in the path.
216+ evaluator.apply (left, system);
217+
218+ ++count;
219+ }
220+
221+ std::rotate (Steps.begin (), Steps.begin () + count, Steps.end () - count);
222+ Steps.erase (Steps.end () - 2 * count, Steps.end ());
223+
224+ basepoint = evaluator.getCurrentTerm ();
225+ return count > 0 ;
226+ }
227+
228+ // / Compute cyclically-reduced left-canonical normal form of a loop.
229+ void RewriteLoop::computeNormalForm (const RewriteSystem &system) {
230+ // FIXME: This can be more efficient.
231+ bool changed;
232+ do {
233+ changed = false ;
234+ changed |= Path.computeFreelyReducedForm ();
235+ changed |= Path.computeCyclicallyReducedForm (Basepoint, system);
236+ changed |= Path.computeLeftCanonicalForm (system);
237+
238+ if (changed)
239+ markDirty ();
240+ } while (changed);
241+ }
0 commit comments