Implement more free lambdas

Closes #13

src/LogicIR/Frontend/Java.hs

@@ -46,14 +46,23 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
     fMethodInv inv env decls = case inv of -- TODO: very hardcoded EDSL + lambdas cannot be { return expr; } + ranged 
                                     -- Java: forall(name, bound -> expr);
                                     MethodCall (Name [Ident "forall"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-                                        -> let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
-                                            LQuant QAll i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LImpl (foldExp javaExpToLExprAlgebra expr env decls))
+                                        -> forall name bound expr
                                     -- Java: exists(name, bound -> expr);
                                     MethodCall (Name [Ident "exists"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-                                        -> let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
-                                            LQuant QAny i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LAnd (foldExp javaExpToLExprAlgebra expr env decls))
+                                        -> exists name bound expr
+                                    -- Java: forall(name, bound -> { return expr; });
+                                    MethodCall (Name [Ident "forall"]) [ExpName name ,Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
+                                        -> forall name bound expr
+                                    -- Java: exists(name, bound -> { return expr; });
+                                    MethodCall (Name [Ident "exists"]) [ExpName name ,Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
+                                        -> exists name bound expr
                                     _
                                         -> error $ "Unimplemented fMethodInv: " ++ show inv
+
+                                    where forall name bound expr = let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
+                                                                                  LQuant QAll i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LImpl (foldExp javaExpToLExprAlgebra expr env decls))
+                                          exists name bound expr = let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
+                                                                                  LQuant QAny i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LAnd (foldExp javaExpToLExprAlgebra expr env decls))
     fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
                                              ArrayIndex (ExpName name) [expr]
                                                 -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)

src/SimpleFormulaChecker.hs

@@ -131,4 +131,5 @@ edslSrc = "javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
 testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
 testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
 blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec2")
-blub2 = compareSpec (edslSrc, "test1") (edslSrc, "test2")
\ No newline at end of file
+blub2 = compareSpec (edslSrc, "test1") (edslSrc, "test2")
+blob = compareSpec (edslSrc, "blob1") (edslSrc, "blob1")
\ No newline at end of file

src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java

@@ -107,6 +107,12 @@ public class Main {
         post(a[i] == oldaj);
     }
 
+    public static void blob1(int[] a)
+    {
+        pre(forall(a, i -> { return a[i] == 0; }));
+        post(true);
+    }
+
     public static void test1(int[] a)
     {
         pre(exists(a, i -> a[i+1] > a[i]));