From 1127ea8d8037278415fa5cb2d8917d972b122983 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Fri, 19 Feb 2010 21:52:12 +0000
Subject: Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda
 expressions; they might not yet fully work for polymorphic maps.

---
 Source/Core/BoogiePL.atg | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'Source/Core/BoogiePL.atg')

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index ab7e6c81..ee9675a5 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -1289,6 +1289,12 @@ AtomExpression<out Expr! e>
           QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e> 
                                             (. if (typeParams.Length + ds.Length > 0)
                                                  e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .)
+        | Lambda                            (. x = token; .)
+          QuantifierBody<x, out typeParams, out ds, out kv, out trig, out e> 
+                                            (. if (trig != null)
+                                                 SemErr("triggers not allowed in lambda expressions");
+                                               if (typeParams.Length + ds.Length > 0)
+                                                 e = new LambdaExpr(x, typeParams, ds, kv, e); .)
         )
     ")"
   | IfThenElseExpression<out e>
@@ -1382,6 +1388,7 @@ QuantifierBody<IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,
 
 Forall = "forall" | '\u2200'.
 Exists = "exists" | '\u2203'.
+Lambda = "lambda" | '\u03bb'.
 QSep = "::" | '\u2022'.
 
 /*------------------------------------------------------------------------*/
-- 
cgit v1.2.3