python: implement formula.__format__

Fixes #105.

* src/bin/common_trans.cc (quote_shell_string): Move ...
* src/misc/escape.cc, src/misc/escape.hh (quote_shell_string):
... here.
* wrap/python/spot_impl.i: Wrap escape.hh.
* wrap/python/spot.py: Implement formula.__format__.
* wrap/python/tests/ltlsimple.py: Test it.
* NEWS, doc/org/tut01.org, wrap/python/tests/formulas.ipynb: Document
it.

NEWS

@@ -3,6 +3,8 @@ New in spot 1.99.4a (not yet released)
   Python:
 
   * Add bindings for complete().
+  * Formulas now have a custom __format__ function.  See
+    https://spot.lrde.epita.fr/tut01.html for examples.
 
   Bugs fixed:
 

doc/org/tut01.org

@@ -376,3 +376,81 @@ ltlfilt --lenient -f '(a U ) U c'
 
 In C++ you can enable lenient using one of the Boolean arguments of
 =parse_infix_psl()=.
+** Python formatting
+
+Formulas have a custom format specification language that allows you
+to easily change the way a formula should be output when using the
+=format()= method of strings.
+
+#+BEGIN_SRC python :results output :exports both
+import spot
+formula = spot.formula('a U b U "$strange[0]=name"')
+print("""\
+Default output:    {f}
+Spin syntax:       {f:s}
+(Spin syntax):     {f:sp}
+Default for shell: echo {f:q} | ...
+LBT for shell:     echo {f:lq} | ...
+Default for CSV:   ...,{f:c},...
+Wring, centered:   {f:w:~^50}""".format(f = formula))
+#+END_SRC
+
+#+RESULTS:
+: Default output:    a U (b U "$strange[0]=name")
+: Spin syntax:       a U (b U ($strange[0]=name))
+: (Spin syntax):     (a) U ((b) U ($strange[0]=name))
+: Default for shell: echo 'a U (b U "$strange[0]=name")' | ...
+: LBT for shell:     echo 'U "a" U "b" "$strange[0]=name"' | ...
+: Default for CSV:   ...,"a U (b U ""$strange[0]=name"")",...
+: Wring, centered:   ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~
+
+The specifiers after the first =:= are specific to formulas.  The
+specifiers after the second =:= (if any) are the usual [[https://docs.python.org/3/library/string.html#formatspec][format
+specifiers]] (typically alignment choices) and are applied on the string
+produced from the formula.
+
+The complete list of specified that apply to formulas can always be
+printed with =help(spot.formula.__format__)=:
+
+#+BEGIN_SRC python :results output :exports results
+import spot
+help(spot.formula.__format__)
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+Help on function _formula_format in module spot:
+
+_formula_format(self, spec)
+    Format the formula according to spec.
+
+    'spec' should be a list of letters that select
+    how the formula should be formatted.
+
+    Use one of the following letters to select the syntax:
+
+    - 'f': use Spot's syntax (default)
+    - '8': use Spot's syntax in UTF-8 mode
+    - 's': use Spin's syntax
+    - 'l': use LBT's syntax
+    - 'w': use Wring's syntax
+    - 'x': use LaTeX output
+    - 'X': use self-contained LaTeX output
+
+    Add some of those letters for additional options:
+
+    - 'p': use full parentheses
+    - 'c': escape the formula for CSV output (this will
+           enclose the formula in double quotes, and escape
+           any included double quotes)
+    - 'h': escape the formula for HTML output
+    - 'd': escape double quotes and backslash,
+           for use in C-strings (the outermost double
+           quotes are *not* added)
+    - 'q': quote and escape for shell output, using single
+           quotes or double quotes depending on the contents.
+
+    - ':spec': pass the remaining specification to the
+               formating function for strings.
+
+#+end_example

src/bin/common_trans.cc

@@ -30,6 +30,7 @@
 
 #include "tl/print.hh"
 #include "common_conv.hh"
+#include "misc/escape.hh"
 
 // A set of tools for which we know the correct output
 static struct shorthands_t
@@ -146,39 +147,10 @@ translator_spec::~translator_spec()
 
 std::vector<translator_spec> translators;
 
-static void
-quote_shell_string(std::ostream& os, const char* str)
-{
-  // Single quotes are best, unless the string to quote contains one.
-  if (!strchr(str, '\''))
-    {
-      os << '\'' << str << '\'';
-    }
-  else
-    {
-      // In double quotes we have to escape $ ` " or \.
-      os << '"';
-      while (*str)
-	switch (*str)
-	  {
-	  case '$':
-	  case '`':
-	  case '"':
-	  case '\\':
-	    os << '\\';
-	    // fall through
-	  default:
-	    os << *str++;
-	    break;
-	  }
-      os << '"';
-    }
-}
-
 void
 quoted_string::print(std::ostream& os, const char*) const
 {
-  quote_shell_string(os, val().c_str());
+  spot::quote_shell_string(os, val().c_str());
 }
 
 printable_result_filename::printable_result_filename()
@@ -209,7 +181,7 @@ printable_result_filename::print(std::ostream& os, const char*) const
   snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
   const_cast<printable_result_filename*>(this)->val_ =
     spot::create_tmpfile(prefix);
-  quote_shell_string(os, val()->name());
+  spot::quote_shell_string(os, val()->name());
 }
 
 

src/misc/escape.cc

@@ -27,6 +27,7 @@
 #include <functional>
 #include <cctype>
 #include <locale>
+#include <cstring>
 #include "escape.hh"
 
 namespace spot
@@ -143,4 +144,35 @@ namespace spot
 	      std::find_if(str.begin(), str.end(),
 			   std::not1(std::ptr_fun<int, int>(std::isspace))));
   }
+
+  std::ostream&
+  quote_shell_string(std::ostream& os, const char* str)
+  {
+    // Single quotes are best, unless the string to quote contains one.
+    if (!strchr(str, '\''))
+      {
+	os << '\'' << str << '\'';
+      }
+    else
+      {
+	// In double quotes we have to escape $ ` " or \.
+	os << '"';
+	while (*str)
+	  switch (*str)
+	    {
+	    case '$':
+	    case '`':
+	    case '"':
+	    case '\\':
+	      os << '\\';
+	      // fall through
+	    default:
+	      os << *str++;
+	      break;
+	    }
+	os << '"';
+      }
+    return os;
+  }
+
 }

src/misc/escape.hh

@@ -65,5 +65,13 @@ namespace spot
   /// \brief Remove spaces at the front and back of \a str.
   SPOT_API void
   trim(std::string& str);
+
+  /// \brief Output \a str between simple quote or double quotes
+  ///
+  /// Simple quotes are preferred unless \a str contains some simple
+  /// quotes.  In that case we use double quotes and escape anything
+  /// that needs to be escaped.
+  SPOT_API std::ostream&
+  quote_shell_string(std::ostream& os, const char* str);
   /// @}
 }

wrap/python/spot.py

@@ -114,23 +114,92 @@ def _formula_str_ctor(self, str):
     self.this = parse_formula(str)
 
 def _formula_to_str(self, format = 'spot', parenth = False):
-    if format == 'spot':
+    if format == 'spot' or format == 'f':
         return str_psl(self, parenth)
-    elif format == 'spin':
+    elif format == 'spin' or format == 's':
         return str_spin_ltl(self, parenth)
-    elif format == 'utf8':
+    elif format == 'utf8' or format == '8':
         return str_utf8_psl(self, parenth)
-    elif format == 'lbt':
+    elif format == 'lbt' or format == 'l':
         return str_lbt_ltl(self)
-    elif format == 'wring':
+    elif format == 'wring' or format == 'w':
         return str_wring_ltl(self)
-    elif format == 'latex':
+    elif format == 'latex' or format == 'x':
         return str_latex_psl(self, parenth)
-    elif format == 'sclatex':
+    elif format == 'sclatex' or format == 'X':
         return str_sclatex_psl(self, parenth)
     else:
         raise ValueError("unknown string format: " + format)
 
+def _formula_format(self, spec):
+    """Format the formula according to spec.
+
+    'spec' should be a list of letters that select
+    how the formula should be formatted.
+
+    Use one of the following letters to select the syntax:
+
+    - 'f': use Spot's syntax (default)
+    - '8': use Spot's syntax in UTF-8 mode
+    - 's': use Spin's syntax
+    - 'l': use LBT's syntax
+    - 'w': use Wring's syntax
+    - 'x': use LaTeX output
+    - 'X': use self-contained LaTeX output
+
+    Add some of those letters for additional options:
+
+    - 'p': use full parentheses
+    - 'c': escape the formula for CSV output (this will
+           enclose the formula in double quotes, and escape
+           any included double quotes)
+    - 'h': escape the formula for HTML output
+    - 'd': escape double quotes and backslash,
+           for use in C-strings (the outermost double
+           quotes are *not* added)
+    - 'q': quote and escape for shell output, using single
+           quotes or double quotes depending on the contents.
+
+    - ':spec': pass the remaining specification to the
+               formating function for strings.
+    """
+
+    syntax = 'f'
+    parent = False
+    escape = None
+
+    while spec:
+        c, spec = spec[0], spec[1:]
+        if c in ('f', 's', '8', 'l', 'w', 'x', 'X'):
+            syntax = c
+        elif c == 'p':
+            parent = True
+        elif c in ('c', 'd', 'h', 'q'):
+            escape = c
+        elif c == ':':
+            break
+        else:
+            raise ValueError("unknown format specification: " + c + spec)
+
+    s = self.to_str(syntax, parent)
+
+    if escape == 'c':
+        o = ostringstream()
+        escape_rfc4180(o, s)
+        s = '"' + o.str() + '"'
+    elif escape == 'd':
+        s = escape_str(s)
+    elif escape == 'h':
+        o = ostringstream()
+        escape_html(o, s)
+        s = o.str()
+    elif escape == 'q':
+        o = ostringstream()
+        quote_shell_string(o, s)
+        s = o.str()
+
+    return s.__format__(spec)
+
 def _formula_traverse(self, func):
     if func(self):
         return
@@ -158,6 +227,7 @@ formula.__init__ = _formula_str_ctor
 formula.to_str = _formula_to_str
 formula.show_ast = _render_formula_as_svg
 formula.traverse = _formula_traverse
+formula.__format__ = _formula_format
 formula.map = _formula_map
 
 def _twa_to_str(a, format='hoa', opt=None):

wrap/python/spot_impl.i

@@ -79,6 +79,7 @@
 #include "misc/minato.hh"
 #include "misc/optionmap.hh"
 #include "misc/random.hh"
+#include "misc/escape.hh"
 
 #include "tl/formula.hh"
 
@@ -215,6 +216,7 @@ using namespace spot;
 %include "misc/minato.hh"
 %include "misc/optionmap.hh"
 %include "misc/random.hh"
+%include "misc/escape.hh"
 
 %implicitconv std::vector<spot::formula>;
 

wrap/python/tests/formulas.ipynb

@@ -1,7 +1,23 @@
 {
  "metadata": {
-  "name": "",
+  "kernelspec": {
-  "signature": "sha256:049261ec6b13505007796a9e9d1d8279783233b9b1eb8f9b8e5727070a38db7a"
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.4.3+"
+  },
+  "name": ""
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -172,6 +188,100 @@
      ],
      "prompt_number": 6
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "Formulas output via `format()` can also use some convenient shorthand to select the syntax:"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "print(\"\"\"\\\n",
+      "Spin:               {0:s}\n",
+      "Spin+parentheses:   {0:sp}\n",
+      "Spot (default):     {0}\n",
+      "Spot+shell quotes:  {0:q}\n",
+      "LBT, right aligned: {0:l:~>40}\"\"\".format(f))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "output_type": "stream",
+       "stream": "stdout",
+       "text": [
+        "Spin:               p1 U (p2 V (p3 && !p4))\n",
+        "Spin+parentheses:   (p1) U ((p2) V ((p3) && (!(p4))))\n",
+        "Spot (default):     p1 U (p2 R (p3 & !p4))\n",
+        "Spot+shell quotes:  'p1 U (p2 R (p3 & !p4))'\n",
+        "LBT, right aligned: ~~~~~~~~~~~~~~~~~~~~~U p1 V p2 & p3 ! p4\n"
+       ]
+      }
+     ],
+     "prompt_number": 7
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "The specifiers that can be used with `format` are documented as follows:"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "help(spot.formula.__format__)"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "output_type": "stream",
+       "stream": "stdout",
+       "text": [
+        "Help on function _formula_format in module spot:\n",
+        "\n",
+        "_formula_format(self, spec)\n",
+        "    Format the formula according to spec.\n",
+        "    \n",
+        "    'spec' should be a list of letters that select\n",
+        "    how the formula should be formatted.\n",
+        "    \n",
+        "    Use one of the following letters to select the syntax:\n",
+        "    \n",
+        "    - 'f': use Spot's syntax (default)\n",
+        "    - '8': use Spot's syntax in UTF-8 mode\n",
+        "    - 's': use Spin's syntax\n",
+        "    - 'l': use LBT's syntax\n",
+        "    - 'w': use Wring's syntax\n",
+        "    - 'x': use LaTeX output\n",
+        "    - 'X': use self-contained LaTeX output\n",
+        "    \n",
+        "    Add some of those letters for additional options:\n",
+        "    \n",
+        "    - 'p': use full parentheses\n",
+        "    - 'c': escape the formula for CSV output (this will\n",
+        "           enclose the formula in double quotes, and escape\n",
+        "           any included double quotes)\n",
+        "    - 'h': escape the formula for HTML output\n",
+        "    - 'd': escape double quotes and backslash,\n",
+        "           for use in C-strings (the outermost double\n",
+        "           quotes are *not* added)\n",
+        "    - 'q': quote and escape for shell output, using single\n",
+        "           quotes or double quotes depending on the contents.\n",
+        "    \n",
+        "    - ':spec': pass the remaining specification to the\n",
+        "               formating function for strings.\n",
+        "\n"
+       ]
+      }
+     ],
+     "prompt_number": 8
+    },
     {
      "cell_type": "markdown",
      "metadata": {},
@@ -191,13 +301,13 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 7,
+       "prompt_number": 9,
        "text": [
         "True"
        ]
       }
      ],
-     "prompt_number": 7
+     "prompt_number": 9
     },
     {
      "cell_type": "code",
@@ -211,13 +321,13 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 8,
+       "prompt_number": 10,
        "text": [
         "False"
        ]
       }
      ],
-     "prompt_number": 8
+     "prompt_number": 10
     },
     {
      "cell_type": "markdown",
@@ -238,13 +348,13 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 9,
+       "prompt_number": 11,
        "text": [
         "True"
        ]
       }
      ],
-     "prompt_number": 9
+     "prompt_number": 11
     },
     {
      "cell_type": "code",
@@ -258,13 +368,13 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 10,
+       "prompt_number": 12,
        "text": [
         "False"
        ]
       }
      ],
-     "prompt_number": 10
+     "prompt_number": 12
     },
     {
      "cell_type": "code",
@@ -278,13 +388,13 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 11,
+       "prompt_number": 13,
        "text": [
         "True"
        ]
       }
      ],
-     "prompt_number": 11
+     "prompt_number": 13
     },
     {
      "cell_type": "markdown",
@@ -308,13 +418,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 12,
+       "prompt_number": 14,
        "text": [
         "\"a > b\" & \"proc[2]@init\" & GF_foo_"
        ]
       }
      ],
-     "prompt_number": 12
+     "prompt_number": 14
     },
     {
      "cell_type": "code",
@@ -331,13 +441,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 13,
+       "prompt_number": 15,
        "text": [
         "a & b & GFc"
        ]
       }
      ],
-     "prompt_number": 13
+     "prompt_number": 15
     },
     {
      "cell_type": "code",
@@ -354,13 +464,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 14,
+       "prompt_number": 16,
        "text": [
         "p0 & p1 & GFp2"
        ]
       }
      ],
-     "prompt_number": 14
+     "prompt_number": 16
     },
     {
      "cell_type": "markdown",
@@ -388,7 +498,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 15,
+       "prompt_number": 17,
        "svg": [
         "<svg height=\"260pt\" viewBox=\"0.00 0.00 269.00 260.00\" width=\"269pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 256)\">\n",
@@ -493,11 +603,11 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f4dfea9c710>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
-     "prompt_number": 15
+     "prompt_number": 17
     },
     {
      "cell_type": "code",
@@ -514,13 +624,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 16,
+       "prompt_number": 18,
        "text": [
         "F(a & X(!a & b))"
        ]
       }
      ],
-     "prompt_number": 16
+     "prompt_number": 18
     },
     {
      "cell_type": "markdown",
@@ -544,13 +654,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 17,
+       "prompt_number": 19,
        "text": [
         "F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))"
        ]
       }
      ],
-     "prompt_number": 17
+     "prompt_number": 19
     },
     {
      "cell_type": "markdown",
@@ -575,13 +685,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 18,
+       "prompt_number": 20,
        "text": [
         "(0 R !(a <-> b)) -> (1 U (a <-> b))"
        ]
       }
      ],
-     "prompt_number": 18
+     "prompt_number": 20
     },
     {
      "cell_type": "code",
@@ -598,13 +708,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 19,
+       "prompt_number": 21,
        "text": [
         "(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))"
        ]
       }
      ],
-     "prompt_number": 19
+     "prompt_number": 21
     }
    ],
    "metadata": {}

wrap/python/tests/ltlsimple.py

@@ -93,3 +93,26 @@ def count_g(f):
         x += 1
 f.traverse(count_g)
 assert x == 3
+
+#----------------------------------------------------------------------
+
+# The example from tut01.org
+
+formula = spot.formula('a U b U "$strange[0]=name"')
+res = """\
+Default output:    {f}
+Spin syntax:       {f:s}
+(Spin syntax):     {f:sp}
+Default for shell: echo {f:q} | ...
+LBT for shell:     echo {f:lq} | ...
+Default for CSV:   ...,{f:c},...
+Wring, centered:   {f:w:~^50}""".format(f = formula)
+
+assert res == """\
+Default output:    a U (b U "$strange[0]=name")
+Spin syntax:       a U (b U ($strange[0]=name))
+(Spin syntax):     (a) U ((b) U ($strange[0]=name))
+Default for shell: echo 'a U (b U "$strange[0]=name")' | ...
+LBT for shell:     echo 'U "a" U "b" "$strange[0]=name"' | ...
+Default for CSV:   ...,"a U (b U ""$strange[0]=name"")",...
+Wring, centered:   ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~"""