fix expr2c on lambda expressions

Lambda expressions are not quantifier expressions, but both quantifier
expressions and lambda expressions are bindings.  This commit fixes the
conversion of lambda expressions to C syntax by generalizing the conversion
of quantifier expressions to binding expressions.

Author: kroening

src/ansi-c/expr2c.cpp

@@ -832,22 +832,22 @@ std::string expr2ct::convert_trinary(
   return dest;
 }
 
-std::string expr2ct::convert_quantifier(
-  const quantifier_exprt &src,
+std::string expr2ct::convert_binding(
+  const binding_exprt &src,
   const std::string &symbol,
   unsigned precedence)
 {
   // our made-up syntax can only do one symbol
-  if(src.op0().operands().size() != 1)
+  if(src.variables().size() != 1)
     return convert_norep(src, precedence);
 
   unsigned p0, p1;
 
-  std::string op0 = convert_with_precedence(src.symbol(), p0);
+  std::string op0 = convert_with_precedence(src.variables().front(), p0);
   std::string op1 = convert_with_precedence(src.where(), p1);
 
   std::string dest=symbol+" { ";
-  dest += convert(src.symbol().type());
+  dest += convert(src.variables().front().type());
   dest+=" "+op0+"; ";
   dest+=op1;
   dest+=" }";
@@ -3816,16 +3816,13 @@ std::string expr2ct::convert_with_precedence(
     return convert_trinary(to_if_expr(src), "?", ":", precedence = 3);
 
   else if(src.id()==ID_forall)
-    return convert_quantifier(
-      to_quantifier_expr(src), "forall", precedence = 2);
+    return convert_binding(to_quantifier_expr(src), "forall", precedence = 2);
 
   else if(src.id()==ID_exists)
-    return convert_quantifier(
-      to_quantifier_expr(src), "exists", precedence = 2);
+    return convert_binding(to_quantifier_expr(src), "exists", precedence = 2);
 
   else if(src.id()==ID_lambda)
-    return convert_quantifier(
-      to_quantifier_expr(src), "LAMBDA", precedence = 2);
+    return convert_binding(to_lambda_expr(src), "LAMBDA", precedence = 2);
 
   else if(src.id()==ID_with)
     return convert_with(src, precedence=16);

src/ansi-c/expr2c_class.h

@@ -141,8 +141,8 @@ class expr2ct
   std::string convert_overflow(
     const exprt &src, unsigned &precedence);
 
-  std::string convert_quantifier(
-    const quantifier_exprt &,
+  std::string convert_binding(
+    const binding_exprt &,
     const std::string &symbol,
     unsigned precedence);