Rewriting with AC (not modulo AC), using a small scale command.

This replaces opA, opC, opAC, opCA, ... and any combinations of them

- Right now the rewrite relies on an rather efficient computation
  of perm_eq using a "spaghetti sort" in O(n log n)
- Wrongly formed AC statements send error messages showing the
  discrepancy between LHS and RHS patterns.

 Usage :
   rewrite [pattern](AC operator pattern-shape re-ordering)
   rewrite [pattern](ACl operator re-ordering)

 - pattern is optional, as usual,
 - operator must have a canonical Monoid.com_law structure
   (additions, multiplications, conjunction and disjunction do)
 - pattern-shape is expressed using the syntax
      p := n | p * p'
      where "*" is purely formal
        and n > 0 is number of left associated symbols
   examples of pattern shapes:
   + 4 represents (n * m * p * q)
   + (1*2) represents (n * (m * p))
 - re-ordering is expressed using the syntax
     s := n | s * s'
   where "*" is purely formal and n is the position in the LHS

 If the ACl variant is used, the pattern-shape defaults to the
 pattern fully associated to the left i.e. n i.e (x * y * ...)

 Examples of re-orderings:
 - ACl op ((0*1)*2) is the identity (and should fail to rewrite)
 - opAC == ACl op ((0*2)*1) == AC op 3 ((0*2)*1)
 - opCA == AC op (2*1) (0*1*2)
 - rewrite opCA -opA == rewrite (ACl op (0*(2*1))
 - opACA == AC (2*2) ((0*2)*(1*3))

1 files changed, 1 insertions, 0 deletions

diff --git a/mathcomp/Make b/mathcomp/Make
index 0a2c4a4..1d837c1 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -81,6 +81,7 @@ ssreflect/order.v
 ssreflect/path.v
 ssreflect/prime.v
 ssreflect/seq.v
+ssreflect/ssrAC.v
 ssreflect/ssrbool.v
 ssreflect/ssreflect.v
 ssreflect/ssrfun.v