added lambda_exprt

Author: Daniel Kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -289,13 +289,12 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
     // already fine, just set some type
     expr.type()=void_type();
   }
-  else if(expr.id()==ID_forall ||
-          expr.id()==ID_exists)
+  else if(
+    expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda)
   {
     // op0 is a declaration,
     // op1 the bound expression
     assert(expr.operands().size()==2);
-    expr.type()=bool_typet();
 
     if(expr.op0().get(ID_statement)!=ID_decl)
     {
@@ -315,7 +314,16 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
     symbol_exprt bound=to_symbol_expr(expr.op0().op0());
     expr.op0().swap(bound);
 
-    implicit_typecast_bool(expr.op1());
+    if(expr.id() == ID_lambda)
+    {
+      expr.type() =
+        mathematical_function_typet({expr.op0().type()}, expr.op1().type());
+    }
+    else
+    {
+      expr.type() = bool_typet();
+      implicit_typecast_bool(expr.op1());
+    }
   }
   else if(expr.id()==ID_label)
   {
@@ -736,7 +744,8 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
   {
     typecheck_code(to_code(expr.op0()));
   }
-  else if(expr.id()==ID_forall || expr.id()==ID_exists)
+  else if(
+    expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda)
   {
     assert(expr.operands().size()==2);
 

src/ansi-c/parser.y

@@ -187,6 +187,7 @@ extern char *yyansi_ctext;
 %token TOK_EXISTS      "exists"
 %token TOK_ACSL_FORALL "\\forall"
 %token TOK_ACSL_EXISTS "\\exists"
+%token TOK_ACSL_LAMBDA "\\lambda"
 %token TOK_ACSL_LET    "\\let"
 %token TOK_ARRAY_OF    "array_of"
 %token TOK_CPROVER_BITVECTOR "__CPROVER_bitvector"
@@ -500,6 +501,16 @@ quantifier_expression:
           mto($$, $4);
           PARSER.pop_scope();
         }
+        | TOK_ACSL_LAMBDA compound_scope declaration primary_expression
+        {
+          // The precedence of this operator is too high; it is meant
+          // to bind only very weakly.
+          $$=$1;
+          set($$, ID_lambda);
+          mto($$, $3);
+          mto($$, $4);
+          PARSER.pop_scope();
+        }
         ;
 
 loop_invariant_opt:

src/ansi-c/scanner.l

@@ -1287,6 +1287,10 @@ __decltype          { if(PARSER.cpp98 &&
                   loc(); return TOK_ACSL_EXISTS;
                 }
 
+"\\lambda"      { /* Non-standard, obviously. Found in ACSL syntax. */
+                  loc(); return TOK_ACSL_LAMBDA;
+                }
+
 "\\let"         { /* Non-standard, obviously. Found in ACSL syntax. */
                   loc(); return TOK_ACSL_LET;
                 }

src/util/format_expr.cpp

@@ -287,17 +287,43 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
   else if(id == ID_type)
     return format_rec(os, expr.type());
   else if(id == ID_forall)
+  {
     return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
               << " : " << format(to_quantifier_expr(expr).symbol().type())
               << " . " << format(to_quantifier_expr(expr).where());
+  }
   else if(id == ID_exists)
+  {
     return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
               << " : " << format(to_quantifier_expr(expr).symbol().type())
               << " . " << format(to_quantifier_expr(expr).where());
+  }
   else if(id == ID_let)
+  {
     return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
               << format(to_let_expr(expr).value()) << " IN "
               << format(to_let_expr(expr).where());
+  }
+  else if(id == ID_lambda)
+  {
+    const auto &lambda_expr = to_lambda_expr(expr);
+
+    os << u8"\u1d706 ";
+
+    bool first = true;
+
+    for(auto &v : lambda_expr.variables())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+
+      os << format(v);
+    }
+
+    return os << " . " << format(lambda_expr.where());
+  }
   else if(id == ID_array || id == ID_struct)
   {
     os << "{ ";

src/util/mathematical_expr.cpp

@@ -21,3 +21,25 @@ function_application_exprt::function_application_exprt(
   const auto &domain = to_mathematical_function_type(_function.type()).domain();
   PRECONDITION(domain.size() == arguments().size());
 }
+
+static mathematical_function_typet
+lambda_type(const lambda_exprt::variablest &variables, exprt where)
+{
+  mathematical_function_typet::domaint domain;
+
+  domain.reserve(variables.size());
+
+  for(const auto &v : variables)
+    domain.push_back(v.type());
+
+  return mathematical_function_typet(std::move(domain), where.type());
+}
+
+lambda_exprt::lambda_exprt(const variablest &_variables, exprt _where)
+  : binary_exprt(
+      tuple_exprt((const operandst &)_variables),
+      ID_lambda,
+      _where,
+      lambda_type(_variables, _where))
+{
+}

src/util/mathematical_expr.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 /// \file util/mathematical_expr.h
 /// API to expression classes for 'mathematical' expressions
 
+#include "mathematical_types.h"
 #include "std_expr.h"
 
 /// Transition system, consisting of state invariant, initial state predicate,
@@ -392,4 +393,85 @@ inline exists_exprt &to_exists_expr(exprt &expr)
   return ret;
 }
 
+/// \brief A (mathematical) lambda expression (an "abstraction" in lambda
+/// calculus terminology)
+class lambda_exprt : public binary_exprt
+{
+public:
+  using variablest = std::vector<symbol_exprt>;
+
+  /// construct the lambda expression -- the type is derived from
+  /// the types of the variables and the expression
+  lambda_exprt(const variablest &_variables, exprt _where);
+
+  mathematical_function_typet &type()
+  {
+    return static_cast<mathematical_function_typet &>(binary_exprt::type());
+  }
+
+  const mathematical_function_typet &type() const
+  {
+    return static_cast<const mathematical_function_typet &>(
+      binary_exprt::type());
+  }
+
+  variablest &variables()
+  {
+    return (variablest &)static_cast<tuple_exprt &>(op0()).operands();
+  }
+
+  const variablest &variables() const
+  {
+    return (variablest &)static_cast<const tuple_exprt &>(op0()).operands();
+  }
+
+  exprt &where()
+  {
+    return op1();
+  }
+
+  const exprt &where() const
+  {
+    return op1();
+  }
+};
+
+/// \brief Cast an exprt to a \ref lambda_exprt
+///
+/// \a expr must be known to be \ref lambda_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref lambda_exprt
+inline const lambda_exprt &to_lambda_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_lambda);
+  DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
+  DATA_INVARIANT(
+    expr.type().id() == ID_mathematical_function,
+    "lambda must have right type");
+  return static_cast<const lambda_exprt &>(expr);
+}
+
+/// \copydoc to_lambda_expr(const exprt &)
+inline lambda_exprt &to_lambda_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_lambda);
+  DATA_INVARIANT(expr.operands().size() == 2, "lambda must have two operands");
+  DATA_INVARIANT(
+    expr.type().id() == ID_mathematical_function,
+    "lambda must have right type");
+  return static_cast<lambda_exprt &>(expr);
+}
+
+template <>
+inline bool can_cast_expr<lambda_exprt>(const exprt &base)
+{
+  return base.id() == ID_lambda;
+}
+
+inline void validate_expr(const lambda_exprt &value)
+{
+  validate_operands(value, 2, "lambda must have two operands");
+}
+
 #endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H