LogicIR.Expr cleanup + swap_spec1 lifted correctly

src/LogicIR/Backend/Pretty.hs

@@ -47,16 +47,16 @@ prettyVar :: Var -> String
 prettyVar (Var t n) = prettyType t ++ ":" ++ n
 
 prettyLExprAlgebra :: LExprAlgebra String
-prettyLExprAlgebra = (flConst, prettyVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, prettyVar, fnUnop, fnBinop, fnArray, fnIf, fnLen) where
+prettyLExprAlgebra = (flConst, prettyVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) where
     flConst b = if b then "true" else "false"
     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 ++ ")"
     flArray v [a] = prettyVar v ++ "[" ++ (foldLExpr prettyLExprAlgebra a) ++ "]"
+    flNil = "nil"
     fnConst n = show n
     fnUnop o a = prettyNUnop o ++ a
     fnBinop a o b = a ++ " " ++ prettyNBinop o ++ " " ++ b
-    fnArray = flArray
     fnIf c a b = "(" ++ c ++ ") ? (" ++ a ++ ") : (" ++ b ++ ")"
     fnLen v = "len(" ++ prettyVar v ++ ")"
\ No newline at end of file

src/LogicIR/Backend/Z3.hs

@@ -9,7 +9,7 @@ lExprToZ3Ast :: LExpr -> Z3 AST
 lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
 
 lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
-lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray, fnIf, fnLen) where
+lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) where
     flConst = undefined
     flVar = undefined
     flNot = undefined
@@ -17,10 +17,9 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
     flComp = undefined
     flQuant = undefined
     flArray = undefined
+    flNil = undefined
     fnConst = undefined
-    fnVar = undefined
     fnUnop = undefined
     fnBinop = undefined
-    fnArray = undefined
     fnIf = undefined
     fnLen = undefined
\ No newline at end of file

src/LogicIR/Expr.hs

@@ -64,13 +64,12 @@ data LExpr = LConst Bool -- True/False
            | LBinop LExpr LBinop LExpr -- Logical operator
            | LComp NExpr COp NExpr -- Integer comparison
            | LQuant QOp [Var] LExpr -- Logical quantifier
-           | LArray Var [NExpr] -- Logical array access (TODO: remove?)
+           | LArray Var [NExpr] -- Logical array access
+           | LNil -- Nil constant
 
-           | NConst Int -- Integer constant
-           | NVar Var -- Variable
+           | NConst Int -- Integer constant (TODO: use Integer instead of Int?)
            | NUnop NUnop NExpr -- Unary operator
            | NBinop NExpr NBinop NExpr -- Binary operators
-           | NArray Var [NExpr] -- Integer array access
            | NIf LExpr NExpr NExpr -- if c then a else b
            | NLen Var -- len(array)
            deriving (Show, Eq, Read)
\ No newline at end of file

src/LogicIR/Fold.hs

@@ -10,18 +10,17 @@ type LExprAlgebra r = (Bool -> r, -- LConst
                        r -> COp -> r -> r, -- LComp
                        QOp -> [Var] -> r -> r, -- LQuant
                        Var -> [NExpr] -> r, -- LArray
+                       r, -- LNil
                        Int -> r, -- NConst
-                       Var -> r, -- NVar
                        NUnop -> r -> r, -- NUnop
                        r -> NBinop -> r -> r, -- NBinop
-                       Var -> [NExpr] -> r, -- NArray
                        r -> r -> r -> r, -- NIf
                        Var -> r -- NLen
                       )
 
 -- Fold for logical expressions
 foldLExpr :: LExprAlgebra r -> LExpr -> r
-foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray, fnIf, fnLen) = fold where
+foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) = fold where
     fold e = case e of
                   LConst c -> flConst c
                   LVar n -> flVar n
@@ -30,10 +29,9 @@ foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fn
                   LComp a o b -> flComp (fold a) o (fold b)
                   LQuant o vs e -> flQuant o vs (fold e)
                   LArray n e -> flArray n e
+                  LNil -> flNil
                   NConst n -> fnConst n
-                  NVar n -> fnVar n
                   NUnop o e -> fnUnop o (fold e)
                   NBinop a o b -> fnBinop (fold a) o (fold b)
-                  NArray n e -> fnArray n e
                   NIf c a b -> fnIf (fold c) (fold a) (fold b)
                   NLen v -> fnLen v
\ No newline at end of file

src/LogicIR/Frontend/Java.hs

@@ -18,8 +18,8 @@ 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
                     Boolean b -> LConst b
-                    Int n -> NConst (fromIntegral n) -- TODO: use Integer in LExpr?
-                    Null -> undefined -- TODO: null support
+                    Int n -> NConst (fromIntegral n)
+                    Null -> LNil
                     _ -> error $ show $ lit
     fClassLit = error "fClassLit not supported..."
     fThis = error "fThis not supported..."
@@ -34,22 +34,23 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
                                              ArrayIndex (ExpName name) [ExpName index] ->
                                                 let (arrayType, indexType) = (lookupType decls env name, lookupType decls env index) in
                                                     case arrayType of
-                                                         (RefType (ArrayType (PrimType IntT))) ->
+                                                         RefType (ArrayType (PrimType IntT)) ->
                                                             case indexType of
-                                                                 PrimType IntT -> NArray (Var (TArray (TPrim PInt)) (prettyPrint name)) [NVar (Var (TPrim PInt) (prettyPrint index))]
+                                                                 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)
+                                                                          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        -> NVar (Var (TPrim PInt) symbol)
-                                             t                    -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
+                                             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)
     fPostIncrement = error "fPostIncrement has side effects..."
     fPostDecrement = error "fPostDecrement has side effects..."
     fPreIncrement = error "fPreIncrement has side effects..."