refactor of LogicIR.Expr + implement quantifiers in LogicIR.Backend.Java

src/LogicIR/Backend/Pretty.hs

@@ -24,8 +24,8 @@ prettyCOp CGeq = ">="
 prettyLBinop :: LBinop -> String
 prettyLBinop LAnd = "&&"
 prettyLBinop LOr = "||"
-prettyLBinop LImpl = "=>"
-prettyLBinop LBicond = "<=>"
+prettyLBinop LImpl = "->"
+prettyLBinop LBicond = "<->"
 
 prettyNBinop :: NBinop -> String
 prettyNBinop NAdd = "+"
@@ -52,7 +52,7 @@ prettyLExprAlgebra = (flConst, prettyVar, flNot, flBinop, flComp, flQuant, flArr
     flNot a = '!' : a
     flBinop a o b = a ++ " " ++ prettyLBinop o ++ " " ++ b
     flComp a o b = a ++ " " ++ prettyCOp o ++ " " ++ b
-    flQuant o vs a = '(' : show o ++ intercalate "," (map prettyVar vs) ++ ": " ++ a ++ ")"
+    flQuant o v a = '(' : show o ++ " " ++ prettyVar v ++ " . " ++ a ++ ")"
     flArray v [a] = prettyVar v ++ "[" ++ (foldLExpr prettyLExprAlgebra a) ++ "]"
     flNil = "nil"
     fnConst n = show n

src/LogicIR/Expr.hs

@@ -63,7 +63,7 @@ data LExpr = LConst Bool -- True/False
            | LNot LExpr -- Logical negation/not
            | LBinop LExpr LBinop LExpr -- Logical operator
            | LComp NExpr COp NExpr -- Integer comparison
-           | LQuant QOp [Var] LExpr -- Logical quantifier
+           | LQuant QOp Var LExpr -- Logical quantifier
            | LArray Var [NExpr] -- Logical array access
            | LNil -- Nil constant
 

src/LogicIR/Fold.hs

@@ -8,7 +8,7 @@ type LExprAlgebra r = (Bool -> r, -- LConst
                        r -> r, -- LNot
                        r -> LBinop -> r -> r, -- LBinop
                        r -> COp -> r -> r, -- LComp
-                       QOp -> [Var] -> r -> r, -- LQuant
+                       QOp -> Var -> r -> r, -- LQuant
                        Var -> [NExpr] -> r, -- LArray
                        r, -- LNil
                        Int -> r, -- NConst
@@ -27,7 +27,7 @@ foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnCo
                   LNot e -> flNot (fold e)
                   LBinop a o b -> flBinop (fold a) o (fold b)
                   LComp a o b -> flComp (fold a) o (fold b)
-                  LQuant o vs e -> flQuant o vs (fold e)
+                  LQuant o v e -> flQuant o v (fold e)
                   LArray n e -> flArray n e
                   LNil -> flNil
                   NConst n -> fnConst n

src/LogicIR/Frontend/Java.hs

@@ -14,9 +14,17 @@ import Data.Typeable
 javaExpToLExpr :: Exp -> TypeEnv -> [TypeDecl] -> LExpr
 javaExpToLExpr = foldExp javaExpToLExprAlgebra
 
+nameToVar :: Name -> TypeEnv -> [TypeDecl] -> Var
+nameToVar name env decls = let (arrayType, symbol) = (lookupType decls env name, prettyPrint name) in
+    case arrayType of
+        PrimType BooleanT -> Var (TPrim PBool) symbol
+        PrimType IntT -> Var (TPrim PInt) symbol
+        RefType (ArrayType (PrimType IntT)) -> Var (TArray (TPrim PInt)) symbol
+        _ -> error $ "Unimplemented nameToVar for " ++ show (name, arrayType)
+
 javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> 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 lit _ _ = case lit of -- TODO: support more type literals
+    fLit lit _ _ = case lit of -- TODO: support more type literals?
                     Boolean b -> LConst b
                     Int n -> NConst (fromIntegral n)
                     Null -> LNil
@@ -29,28 +37,23 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
     fArrayCreate = undefined
     fArrayCreateInit = undefined
     fFieldAccess = undefined
-    fMethodInv = undefined
-    fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: better type checking + multiple dimension arrays + better abstractions
-                                             ArrayIndex (ExpName name) [ExpName index] ->
-                                                let (arrayType, indexType) = (lookupType decls env name, lookupType decls env index) in
-                                                    case arrayType of
-                                                         RefType (ArrayType (PrimType IntT)) ->
-                                                            case indexType of
-                                                                 PrimType IntT -> LArray (Var (TArray (TPrim PInt)) (prettyPrint name)) [LVar (Var (TPrim PInt) (prettyPrint index))]
-                                                                 _ -> error $ show (arrayIndex, indexType)
-                                                         _ -> error $ show (arrayIndex, arrayType)
-    fExpName name env decls = case name of -- TODO: better type checking + multiple dimension arrays + better abstractions
-                                   Name [Ident a, Ident "length"] -> let arrayType = lookupType decls env (Name [Ident a]) in
-                                                                     case arrayType of
-                                                                          RefType (ArrayType (PrimType IntT)) -> NLen (Var (TArray (TPrim PInt)) a)
-                                                                          _ -> error $ show (name, arrayType)
-                                   _ -> let symbol = prettyPrint name in let t = lookupType decls env name in
-                                        -- If we're not dealing with library methods, we should be able to get the type from the type environment
-                                        case t of
-                                             PrimType BooleanT -> LVar (Var (TPrim PBool) symbol)
-                                             PrimType IntT -> LVar (Var (TPrim PInt) symbol)
-                                             RefType (ArrayType (PrimType IntT)) -> LVar (Var (TArray (TPrim PInt)) symbol)
-                                             t -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
+    fMethodInv inv env decls = case inv of -- TODO: currently very hardcoded
+                                    MethodCall (Name [Ident "forall"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
+                                        -> let (i, arr) = (Var (TPrim PInt) 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))
+                                    MethodCall (Name [Ident "exists"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
+                                        -> let (i, arr) = (Var (TPrim PInt) 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))
+                                    _
+                                        -> error $ "Unimplemented fMethodInv: " ++ show inv
+    fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
+                                             ArrayIndex (ExpName name) [ExpName index]
+                                                -> LArray (nameToVar name env decls) [LVar (nameToVar index env decls)]
+                                             _
+                                                -> error $ "Multidimensional arrays are not supported: " ++ show (arrayIndex)
+    fExpName name env decls = case name of -- TODO: type checking
+                                   Name [Ident a, Ident "length"] -> NLen $ nameToVar (Name [Ident a]) env decls
+                                   _ -> LVar $ nameToVar name env decls
     fPostIncrement = error "fPostIncrement has side effects..."
     fPostDecrement = error "fPostDecrement has side effects..."
     fPreIncrement = error "fPreIncrement has side effects..."

src/SimpleFormulaChecker.hs

@@ -149,4 +149,4 @@ 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, "simple2") (edslSrc, "simple2")
\ No newline at end of file
+blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec1")
\ No newline at end of file