initial skeleton for LogicIR.Frontend and LogicIR.Backend

README.md

@@ -85,6 +85,11 @@ syntactical constraints; so some pre-processing is required before a source file
 to javawlp.
 
 - Reference to an instance member x should be explicitly written as this.x
-- Binary subexpressions should be explicitly parathesized since our parser does not take
-  Java's built in operators priority into account. So, instead of `x==y && x+z>0` write
-  `(x==y) && ((x+z)>0)`
+
+### IMPRESS EDSL
+
+TODO: Write more information.
+
+#### LogicIR
+
+![](https://i.imgur.com/fBUDkGY.png)
\ No newline at end of file

src/LogicIR/Backend/Z3.hs

+module LogicIR.Backend.Z3 (lExprToZ3Ast) where
+
+import Z3.Monad
+
+import LogicIR.Expr
+import LogicIR.Fold
+
+nExprToZ3Ast :: NExpr -> Z3 AST
+nExprToZ3Ast = foldNExpr nExprToZ3AstAlgebra
+
+nExprToZ3AstAlgebra :: NExprAlgebra (Z3 AST)
+nExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fArray) where
+    fConst = undefined
+    fVar = undefined
+    fUnop = undefined
+    fBinop = undefined
+    fArray = undefined
+
+lExprToZ3Ast :: LExpr -> Z3 AST
+lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
+
+lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
+lExprToZ3AstAlgebra = (fConst, fVar, fNot, fBinop, fComp, fQuant, fArray) where
+    fConst = undefined
+    fVar = undefined
+    fNot = undefined
+    fBinop = undefined
+    fComp = undefined
+    fQuant = undefined
+    fArray = undefined
\ No newline at end of file

src/LogicIR/Fold.hs

@@ -12,13 +12,13 @@ type NExprAlgebra r = (Int -> r, -- NConst
 
 -- Fold for numeral expressions
 foldNExpr :: NExprAlgebra r -> NExpr -> r
-foldNExpr (const, var, unop, binop, array) = fold where
+foldNExpr (fConst, fVar, fUnop, fBinop, fArray) = fold where
     fold e = case e of
-                  NConst n -> const n
-                  NVar n -> var n
-                  NUnop o e -> unop o (fold e)
-                  NBinop a o b -> binop (fold a) o (fold b)
-                  NArray n e -> array n (fold e)
+                  NConst n -> fConst n
+                  NVar n -> fVar n
+                  NUnop o e -> fUnop o (fold e)
+                  NBinop a o b -> fBinop (fold a) o (fold b)
+                  NArray n e -> fArray n (fold e)
 
 -- Fold algebra for logical expressions
 type LExprAlgebra r = (Bool -> r, -- LConst
@@ -32,12 +32,12 @@ type LExprAlgebra r = (Bool -> r, -- LConst
 
 -- Fold for logical expressions
 foldLExpr :: LExprAlgebra r -> LExpr -> r
-foldLExpr (const, var, not, binop, comp, quant, array) = fold where
+foldLExpr (fConst, fVar, fNot, fBinop, fComp, fQuant, fArray) = fold where
     fold e = case e of
-                  LConst c -> const c
-                  LVar n -> var n
-                  LNot e -> not (fold e)
-                  LBinop a o b -> binop (fold a) o (fold b)
-                  LComp a o b -> comp a o b
-                  LQuant o vs e -> quant o vs (fold e)
-                  LArray n e -> array n e
\ No newline at end of file
+                  LConst c -> fConst c
+                  LVar n -> fVar n
+                  LNot e -> fNot (fold e)
+                  LBinop a o b -> fBinop (fold a) o (fold b)
+                  LComp a o b -> fComp a o b
+                  LQuant o vs e -> fQuant o vs (fold e)
+                  LArray n e -> fArray n e
\ No newline at end of file

src/LogicIR/Frontend/Java.hs

+module LogicIR.Frontend.Java (javaExpToLExpr) where
+
+import Javawlp.Engine.Folds
+
+import Language.Java.Syntax
+import Language.Java.Parser
+import Language.Java.Pretty
+
+import LogicIR.Expr
+
+javaExpToLExpr :: Exp -> LExpr
+javaExpToLExpr = foldExp javaExpToLExprAlgebra
+
+javaExpToLExprAlgebra :: ExpAlgebra LExpr
+javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualInstanceCreation, fArrayCreate, fArrayCreateInit, fFieldAccess, fMethodInv, fArrayAccess, fExpName, fPostIncrement, fPostDecrement, fPreIncrement, fPreDecrement, fPrePlus, fPreMinus, fPreBitCompl, fPreNot, fCast, fBinOp, fInstanceOf, fCond, fAssign, fLambda, fMethodRef) where
+    fLit = undefined
+    fClassLit = undefined
+    fThis = undefined
+    fThisClass = undefined
+    fInstanceCreation = undefined
+    fQualInstanceCreation = undefined
+    fArrayCreate = undefined
+    fArrayCreateInit = undefined
+    fFieldAccess = undefined
+    fMethodInv = undefined
+    fArrayAccess = undefined
+    fExpName = undefined
+    fPostIncrement = undefined
+    fPostDecrement = undefined
+    fPreIncrement = undefined
+    fPreDecrement = undefined
+    fPrePlus = undefined
+    fPreMinus = undefined
+    fPreBitCompl = undefined
+    fPreNot = undefined
+    fCast = undefined
+    fBinOp = undefined
+    fInstanceOf = undefined
+    fCond = undefined
+    fAssign = undefined
+    fLambda = undefined
+    fMethodRef = undefined
\ No newline at end of file

src/SimpleFormulaChecker.hs

@@ -10,6 +10,10 @@ import Javawlp.Engine.Types
 import Javawlp.Engine.HelperFunctions
 import Javawlp.Engine.Verifier
 
+import LogicIR.Expr
+import LogicIR.Frontend.Java
+import LogicIR.Backend.Z3
+
 import Debug.Trace
 
 {-