Use []=> and <>=> as sugar in the output when possible.

* src/ltlast/multop.hh (is_multop): Take a constant formula as input.
* src/ltlvisit/tostring.cc (to_string_visitor::visit(multop*)):
Output []=> or <>=> when the left argument of a []-> or <>-> is
a concatenation that ends in 1.
* doc/tl/tl.tex: Document this desugaring.

doc/tl/tl.tex

@@ -99,6 +99,9 @@
 % rewriting rules that enlarge the formula
 \newcommand{\equiV}{\stackrel{\star}{\equiv}}
 
+% marked rewriting rules
+\newcommand{\equivM}{\stackrel{\dag}{\equiv}}
+
 \def\limplies{\rightarrow}
 \def\simp{\rightrightharpoons}
 \def\Simp{\stackrel{+}{\simp}}
@@ -717,7 +720,7 @@ $b_1$, $b_2$ are assumed to be Boolean formul\ae.
 \end{align*}
 
 \noindent
-The following rules are all valid with the two arguments swapped, except the one marked with $\stackrel{\dag}{\equiv}$.
+The following rules are all valid with the two arguments swapped, except the one marked with $\equivM$.
 %(Even for the non-commutative operators \samp{$\CONCAT$} and
 %\samp{$\FUSION$}.)
 
@@ -746,7 +749,7 @@ The following rules are all valid with the two arguments swapped, except the one
   b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
   &&
   &&
-  b:f &\stackrel{\dag}{\equiv} b\AND f\\
+  b:f &\equivM b\AND f\\
 \end{align*}
 
 \section{SERE-LTL Binding Operators}
@@ -804,14 +807,14 @@ is therefore a model of the formula \samp{$\sere{a\PLUS{};\NOT
 
 The syntax on the left is equivalent to the syntax on the right.
 These rewritings are performed from left to right when parsing a
-formula.\spottodo{It would be nice to have the opposite rewritings on
-  output.}
+formula.  Except the one marked with $\equivM$, the opposite
+rewritings are also preformed on output to ease reading.
 
 \begin{align*}
   \sere{r}\EsuffixEQ f &\equiv \sere{r\CONCAT\1}\Esuffix f &
   \sere{r}\AsuffixEQ f &\equiv \sere{r\CONCAT\1}\Asuffix f\\
   \seren{r} &\equiv \sere{r}\Esuffix \1 &
-  \sere{r}\AsuffixALTEQ f &\equiv \sere{r\CONCAT\1}\Asuffix f\\
+  \sere{r}\AsuffixALTEQ f &\equivM \sere{r\CONCAT\1}\Asuffix f\\
 \end{align*}
 
 $\AsuffixEQ$ and $\AsuffixALTEQ$ are synonyms in the same way as

src/ltlast/multop.hh

@@ -185,11 +185,11 @@ namespace spot
     /// Returns 0 otherwise.
     inline
     multop*
-    is_multop(formula* f, multop::type op)
+    is_multop(const formula* f, multop::type op)
     {
       if (f->kind() != formula::MultOp)
 	return 0;
-      multop* mo = static_cast<multop*>(f);
+      multop* mo = static_cast<multop*>(const_cast<formula*>(f));
       if (mo->op() != op)
 	return 0;
       return mo;
@@ -197,8 +197,8 @@ namespace spot
 
     /// \brief Cast \a f into a multop if it has type \a op1 or \a op2.
     ///
-    /// Cast \a f into a multop iff it is a multop instance with operator \a op1
-    /// or \a op2.   Returns 0 otherwise.
+    /// Cast \a f into a multop iff it is a multop instance with
+    /// operator \a op1 or \a op2.  Returns 0 otherwise.
     inline
     multop*
     is_multop(const formula* f, multop::type op1, multop::type op2)

src/ltlvisit/tostring.cc

@@ -122,6 +122,8 @@ namespace spot
 	  if (!top_level)
 	    openp();
 
+	  bool onelast = false;
+
 	  switch (bo->op())
 	    {
 	    case binop::UConcat:
@@ -130,6 +132,21 @@ namespace spot
 	      os_ << "{";
 	      in_ratexp_ = true;
 	      top_level_ = true;
+	      {
+		multop* m = is_multop(bo->first(), multop::Concat);
+		if (m)
+		  {
+		    unsigned s = m->size();
+		    if (m->nth(s - 1) == constant::true_instance())
+		      {
+			formula* tmp = m->all_but(s - 1);
+			tmp->accept(*this);
+			tmp->destroy();
+			onelast = true;
+			break;
+		      }
+		  }
+	      }
 	      // fall through
 	    default:
 	      bo->first()->accept(*this);
@@ -160,7 +177,7 @@ namespace spot
 	      os_ << " M ";
 	      break;
 	    case binop::UConcat:
-	      os_ << "} []-> ";
+	      os_ << (onelast ? "} []=> " : "} []-> ");
 	      in_ratexp_ = false;
 	      top_level_ = top_level;
 	      break;
@@ -171,12 +188,12 @@ namespace spot
 		  in_ratexp_ = false;
 		  goto second_done;
 		}
-	      os_ << "} <>-> ";
+	      os_ << (onelast ? "} <>=> " : "} <>-> ");
 	      in_ratexp_ = false;
 	      top_level_ = false;
 	      break;
 	    case binop::EConcatMarked:
-	      os_ << "} <>+> ";
+	      os_ << (onelast ? "} <>=+> " : "} <>+> ");
 	      in_ratexp_ = false;
 	      top_level_ = false;
 	      break;