tl: add some simplifications for first_match

Following a discussion with Victor Khomenko.

* doc/tl/tl.tex: Document those rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.

doc/tl/tl.tex

@@ -801,7 +801,8 @@ $b_1$, $b_2$ are assumed to be Boolean formulas.
   &&
   f\FSTAR{\mvar{i}..\mvar{j}}\FSTAR{\mvar{k}..\mvar{l}} &\equiv f\FSTAR{\mvar{ik}..\mvar{jl}}\text{~if~}i(k+1)\le jk+1 \\
   f\FSTAR{0}&\equiv \1 & f\FSTAR{1}&\equiv f\text{~if~}\varepsilon\nVDash f\\
-  \FIRSTMATCH\code(b\code) &\equiv b & \FIRSTMATCH\code(f\code) &\equiv \eword\text{~if~}\varepsilon\VDash f
+  \FIRSTMATCH\code(b\code) &\equiv b & \FIRSTMATCH\code(f\code) &\equiv \eword\text{~if~}\varepsilon\VDash f \\
+                                    && \FIRSTMATCH\code(\FIRSTMATCH\code(f\code)\code) &\equiv \FIRSTMATCH\code(f\code)
 \end{align*}
 
 \noindent
@@ -995,22 +996,6 @@ operator, even if the operator has multiple synonyms (like \samp{|},
 \end{align*}
 
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
 \section{Operator precedence}
 
 The following operator precedence describes the current parser of
@@ -1600,7 +1585,14 @@ SERE.
   \sere{b_1\FUSION r_1}\ANDALT\sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\ANDALT r_2} &
   \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} \\
   \sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\
-  \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \mathrlap{\quad\text{if~}\varepsilon\nVDash r_1\land\varepsilon\nVDash r_2}\\
+  \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \mathrlap{\quad\text{if~}\varepsilon\nVDash r_1\land\varepsilon\nVDash r_2}
+\end{align*}
+\begin{align*}
+  \FIRSTMATCH\code(b\STAR{\mvar{i}..\mvar{j}}\code) &\equiv b\STAR{\mvar{i}} \\
+  \FIRSTMATCH\code(r\STAR{\mvar{i}..\mvar{j}}\code) &\equiv \FIRSTMATCH\code(r\STAR{\mvar{i}}\code) \\
+  \FIRSTMATCH\code(r_1\CONCAT{}r_2\STAR{\mvar{i}..\mvar{j}}\code) &\equiv \FIRSTMATCH(r_1\CONCAT\mathrlap{r_2\STAR{\mvar{i}})} \\
+  \FIRSTMATCH\code(b\CONCAT{}r\code) &\equiv b\CONCAT\FIRSTMATCH\code(r\code) \\
+  \FIRSTMATCH\code(r_1\CONCAT{}r_2\code) &\equiv\FIRSTMATCH(r_1)\mathrlap{\quad\text{if~} \varepsilon\VDash r_2}
 \end{align*}
 
 Starred subformulas are rewritten in Star Normal

spot/tl/simplify.cc

@@ -856,7 +856,6 @@ namespace spot
           case op::ap:
           case op::Not:
           case op::FStar:
-          case op::first_match:
             return f;
           case op::X:
             {
@@ -1429,6 +1428,58 @@ namespace spot
                 }
               return formula::Star(h, min, f.max());
             }
+          case op::first_match:
+            {
+              formula h = f[0];
+              if (h.is(op::Star))
+                {
+                  // first_match(b[*i..j]) = b[*i]
+                  // first_match(f[*i..j]) = first_match(f[*i])
+                  unsigned m = h.min();
+                  formula s = formula::Star(h[0], m, m);
+                  return h[0].is_boolean() ? s : formula::first_match(s);
+                }
+              else if (h.is(op::Concat))
+                {
+                  // If b is Boolean and e accepts [*0], we have
+                  // first_match(b;f) = b;first_match(f)
+                  // first_match(f;e) = first_match(f)
+                  // first_match(f;g[*i..j]) = first_match(f;g[*i])
+                  // the first two rules can be repeated, so we will loop
+                  // to save the recursion and intermediate caching.
+
+                  // Extract Boolean formulas at the beginning.
+                  int i = 0;
+                  int n = h.size();
+                  while (i < n && h[i].is_boolean())
+                    ++i;
+                  vec prefix;
+                  prefix.reserve(i + 1); // +1 to append first_match()
+                  for (int ii = 0; ii < i; ++ii)
+                    prefix.push_back(h[ii]);
+                  // Extract suffix, minus trailing formulas that accept [*0].
+                  // "i" is the start of the suffix.
+                  do
+                    --n;
+                  while (i <= n && h[n].accepts_eword());
+                  vec suffix;
+                  suffix.reserve(n + 1 - i);
+                  for (int ii = i; ii <= n; ++ii)
+                    suffix.push_back(h[ii]);
+                  if (!suffix.empty() && suffix.back().is(op::Star))
+                    {
+                      formula s = suffix.back();
+                      unsigned smin = s.min();
+                      suffix.back() = formula::Star(s[0], smin, smin);
+                    }
+                  prefix.push_back(formula::first_match
+                                   (formula::Concat(suffix)));
+                  formula res = formula::Concat(prefix);
+                  if (res != f)
+                    return recurse(res);
+                }
+              return f;
+            }
           }
         SPOT_UNREACHABLE();
       }

tests/core/reduccmp.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009-2014, 2016-2018 Laboratoire de Recherche et
+# Copyright (C) 2009-2014, 2016-2019 Laboratoire de Recherche et
 # Developpement de l'Epita (LRDE).
 # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -436,6 +436,16 @@ GF(a && GF(b) && c), G(F(a & c) & Fb)
 # not reduced
 {a;(b[*2..4];c*;([*0]+{d;e}))*}!, {a;(b[*2..4];c*;([*0]+{d;e}))*}!
 {c[*];e[*]}[]-> a, {c[*];e[*]}[]-> a
+# first_match
+{first_match(a*);b}, b
+{first_match(a)}, a
+{first_match(a;b*)}, a
+{first_match(a;c;b*)}, a & Xc
+{first_match(a;c;b*;e)}, a & X(c & X{first_match(b[*];e)})
+{first_match(a;c;b*;(e | [*0]))}, a & Xc
+{first_match(a;c;b[+];(e | [*0]))}, a & X(c & Xb)
+{first_match(b[+];(e | [*0]))}, b
+{first_match(b[*2..3])}, b & Xb
 EOF
 
 run 0 ../reduccmp nottau.txt