From 3e10dba97876ee8f5de44c015280b71cae0a2ffd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 28 Sep 2015 14:00:34 +0200
Subject: [PATCH] python: work around old swig version

Swig 3.0.2 (currently installed by Debian), install strongly typed
enumerator in the main namespace instead of in its own namespace.
This is fixed in latter versions of Swig.

* wrap/python/spot.py: If spot.op does not exists, populated it with all
operators from the spot namespace.
* wrap/python/tests/ltlsimple.py: Use operators from spot.op.
---
 wrap/python/spot.py            | 29 +++++++++++++++++++++++------
 wrap/python/tests/ltlsimple.py |  6 +++---
 2 files changed, 26 insertions(+), 9 deletions(-)

diff --git a/wrap/python/spot.py b/wrap/python/spot.py
index 17177ebe4..bd2d9049c 100644
--- a/wrap/python/spot.py
+++ b/wrap/python/spot.py
@@ -51,6 +51,21 @@ def setup(**kwargs):
     d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets
     os.environ['SPOT_DOTDEFAULT'] = d
 
+# In version 3.0.2, Swig puts strongly typed enum in the main
+# namespace without prefixing them.  Latter versions fix this.  So we
+# can remove for following hack once 3.0.2 is no longer used in our
+# build farm.
+if not 'op_ff' in globals():
+    for i in ('ff', 'tt', 'eword', 'ap', 'Not', 'X', 'F', 'G',
+              'Closure', 'NegClosure', 'NegClosureMarked',
+              'Xor', 'Implies', 'Equiv', 'U', 'R', 'W', 'M',
+              'EConcat', 'EConcatMarked', 'UConcat', 'Or',
+              'OrRat', 'And', 'AndRat', 'AndNLM', 'Concat',
+              'Fusion', 'Star', 'FStar'):
+        globals()['op_' + i] = globals()[i];
+        del globals()[i]
+
+
 # Global BDD dict so that we do not have to create one in user code.
 _bdd_dict = make_bdd_dict()
 
@@ -124,16 +139,18 @@ def _formula_traverse(self, func):
 
 def _formula_map(self, func):
     k = self.kind()
-    if k in (ff, tt, eword, ap):
+    if k in (op_ff, op_tt, op_eword, op_ap):
         return self;
-    if k in (Not, X, F, G, Closure, NegClosure, NegClosureMarked):
+    if k in (op_Not, op_X, op_F, op_G, op_Closure,
+             op_NegClosure, op_NegClosureMarked):
         return formula.unop(k, func(self[0]))
-    if k in (Xor, Implies, Equiv, U, R, W, M, EConcat,
-             EConcatMarked, UConcat):
+    if k in (op_Xor, op_Implies, op_Equiv, op_U, op_R, op_W,
+             op_M, op_EConcat, op_EConcatMarked, op_UConcat):
         return formula.binop(k, func(self[0]), func(self[1]))
-    if k in (Or, OrRat, And, AndRat, AndNLM, Concat, Fusion):
+    if k in (op_Or, op_OrRat, op_And, op_AndRat, op_AndNLM,
+             op_Concat, op_Fusion):
         return formula.multop(k, [func(x) for x in self])
-    if k in (Star, FStar):
+    if k in (op_Star, op_FStar):
         return formula.bunop(k, func(self[0]), self.min(), self.max())
     raise ValueError("unknown type of formula")
 
diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py
index ba65aa1b4..10be6e283 100755
--- a/wrap/python/tests/ltlsimple.py
+++ b/wrap/python/tests/ltlsimple.py
@@ -77,9 +77,9 @@ assert str([x for x in spot.formula('a &b & c')]) == '[a, b, c]'
 
 
 def switch_g_f(x):
-    if x._is(spot.G):
+    if x._is(spot.op_G):
         return spot.formula.F(switch_g_f(x[0]))
-    if x._is(spot.F):
+    if x._is(spot.op_F):
         return spot.formula.G(switch_g_f(x[0]))
     return x.map(switch_g_f)
 
@@ -89,7 +89,7 @@ assert str(switch_g_f(f)) == 'FGa & XGFb & Gc & F(a | b | Gd)'
 x = 0
 def count_g(f):
     global x
-    if f._is(spot.G):
+    if f._is(spot.op_G):
         x += 1
 f.traverse(count_g)
 assert x == 3