python: support operator rewriting in __format__

Fixes #168.

* python/spot/__init__.py: Implement it.
* tests/python/formulas.ipynb: Test it.
* NEWS: Mention it.

NEWS

@@ -55,6 +55,11 @@ New in spot 2.0a (not yet released)
 
   * The tgba_determinize() function is now accessible in Python.
 
+  * The __format__() method for formula support the same
+    operator-rewritting feature introduced in ltldo and ltlcross.
+    So "{:[i]s}".format(f) is the same as
+    "{:s}".format(f.unabbreviate("i")).
+
   Bug fixes:
 
   * Typo in documentation of the -H option in --help output.

python/spot/__init__.py

@@ -230,6 +230,8 @@ class formula:
                quotes are *not* added)
         - 'q': quote and escape for shell output, using single
                quotes or double quotes depending on the contents.
+        - '[...]': rewrite away all the operators specified in brackets,
+               using spot.unabbreviate().
 
         - ':spec': pass the remaining specification to the
                    formating function for strings.
@@ -240,6 +242,8 @@ class formula:
         parent = False
         escape = None
 
+        form = self
+
         while spec:
             c, spec = spec[0], spec[1:]
             if c in ('f', 's', '8', 'l', 'w', 'x', 'X'):
@@ -250,10 +254,16 @@ class formula:
                 escape = c
             elif c == ':':
                 break
+            elif c == '[':
+                pos = spec.find(']')
+                if pos < 0:
+                    raise ValueError("unclosed bracket: [" + spec)
+                form = form.unabbreviate(spec[0:pos])
+                spec = spec[pos+1:]
             else:
                 raise ValueError("unknown format specification: " + c + spec)
 
-        s = self.to_str(syntax, parent)
+        s = form.to_str(syntax, parent)
 
         if escape == 'c':
             o = ostringstream()

tests/python/formulas.ipynb

@@ -204,7 +204,8 @@
       "Spin+parentheses:   {0:sp}\n",
       "Spot (default):     {0}\n",
       "Spot+shell quotes:  {0:q}\n",
-      "LBT, right aligned: {0:l:~>40}\"\"\".format(f))"
+      "LBT, right aligned: {0:l:~>40}\n",
+      "LBT, no M/W/R:      {0:[MWR]l}\"\"\".format(f))"
      ],
      "language": "python",
      "metadata": {},
@@ -217,7 +218,8 @@
         "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"
+        "LBT, right aligned: ~~~~~~~~~~~~~~~~~~~~~U p1 V p2 & p3 ! p4\n",
+        "LBT, no M/W/R:      U p1 U & p3 ! p4 | & & p2 p3 ! p4 G & p3 ! p4\n"
        ]
       }
      ],
@@ -277,6 +279,8 @@
         "           quotes are *not* added)\n",
         "    - 'q': quote and escape for shell output, using single\n",
         "           quotes or double quotes depending on the contents.\n",
+        "    - '[...]': rewrite away all the operators specified in brackets,\n",
+        "           using spot.unabbreviate().\n",
         "    \n",
         "    - ':spec': pass the remaining specification to the\n",
         "               formating function for strings.\n",
@@ -724,4 +728,4 @@
    "metadata": {}
   }
  ]
-}
+}