From 743bcb441e270b3ce66b49e513a2b417caa71ca8 Mon Sep 17 00:00:00 2001
From: "Ogilvie, D.H. (Duncan)" <d.h.ogilvie2@students.uu.nl>
Date: Sun, 22 Oct 2017 14:18:22 +0200
Subject: [PATCH] Implement more free lambdas
Closes #13
---
src/LogicIR/Frontend/Java.hs | 17 +++++++++++++----
src/SimpleFormulaChecker.hs | 3 ++-
.../src/nl/uu/javawlp_edsl/Main.java | 6 ++++++
3 files changed, 21 insertions(+), 5 deletions(-)
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index f5c6072..7d63f3c 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/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)
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 455cd08..dadcc66 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/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
diff --git a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index 9a61276..6cd5993 100644
--- a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/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]));
--
GitLab