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

@@ -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];

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_()

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]'