From 533268000daee249f030676446c97cdc18a2e806 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 27 Sep 2015 20:36:07 +0200
Subject: [PATCH] python: implement __getitem__ for formula

* wrap/python/spot_impl.i: Implement it.
* wrap/python/tests/ltlsimple.py: Test a for loop.
* src/ltlast/formula.hh: Remove superfluous assert().
---
 src/ltlast/formula.hh          |  1 -
 wrap/python/spot_impl.i        | 12 ++++++++++++
 wrap/python/tests/ltlsimple.py |  3 +++
 3 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index a602a196b..cd73a513e 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -200,7 +200,6 @@ namespace spot
 
       const fnode* nth(unsigned i) const
       {
-	assert(i < size());
 	if (i >= size())
 	  throw std::runtime_error("access to non-existing child");
 	return children[i];
diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i
index 1ef2cd651..a85fbfe7d 100644
--- a/wrap/python/spot_impl.i
+++ b/wrap/python/spot_impl.i
@@ -295,10 +295,22 @@ namespace std {
 
 #undef ltl
 
+%exception spot::ltl::formula::__getitem__ {
+  try {
+    $action
+  }
+  catch (const std::runtime_error& e)
+  {
+    SWIG_exception(SWIG_IndexError, e.what());
+  }
+}
+
 %extend spot::ltl::formula {
   // __cmp__ is for Python 2.0
   int __cmp__(spot::ltl::formula b) { return self->id() - b.id(); }
   size_t __hash__() { return self->id(); }
+  unsigned __len__() { return self->size(); }
+  formula __getitem__(unsigned pos) { return self->nth(pos); }
 
   std::string __repr__() { return spot::ltl::str_psl(*self); }
   std::string _repr_latex_()
diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py
index 7a5c6c38d..0cf231f50 100755
--- a/wrap/python/tests/ltlsimple.py
+++ b/wrap/python/tests/ltlsimple.py
@@ -71,3 +71,6 @@ f5 = spot.formula.Xor(F, c)
 del a, b, c, T, F, f1, f2, f4, f5
 
 assert spot.fnode_instances_check()
+
+#----------------------------------------------------------------------
+assert str([x for x in spot.formula('a &b & c')]) == '[a, b, c]'
-- 
GitLab