EDSL: Fix 'with' var intros (with fresh vars)

impress_edsl/src/nl/uu/impress/Main.java

@@ -158,9 +158,7 @@ public class Main {
     }
 
     public static void blob1(int[] a) {
-        pre(forall(a, i -> {
-            return a[i] == 0;
-        }));
+        pre(forall(a, i -> a[i] == 0));
         post(true);
     }
 
@@ -226,13 +224,30 @@ public class Main {
       post(forall(b, i -> imp(i > 3, b[i] > 0)));
     }
 
-    public static void varIntro1(int[] b) {
+    public static void varIntro11(int[] b) {
       pre(b.length == 5);
-      post(forall(b, i -> imp(i > 2, with(b[i], x -> x > 0))));
+      post(forall(b, i -> imp(i > 3, with(b[i], y -> y >= 0))));
     }
-    public static void varIntro2(int[] b) {
+    public static void varIntro12(int[] b) {
       pre(b.length == 5);
       post(forall(b, i -> imp(i > 3, with(b[i], x -> x > 0))));
     }
 
+    public static void varIntro21(int y) {
+      pre(with(1, z -> (y == (z + 1))));
+      post();
+    }
+    public static void varIntro22(int y) {
+      pre(with(50 - 49 * (2/2), x -> (y == (x - 10 + 11))));
+      post();
+    }
+
+    public static void varIntro31(int y) {
+      pre(with(1, x -> x > 0));
+      post();
+    }
+    public static void varIntro32(int y) {
+      pre(with(10, x -> with(1, x -> with(0, y -> x > y))));
+      post();
+    }
 }

src/LogicIR/Frontend/Java.hs

@@ -7,40 +7,27 @@ import JavaHelpers.HelperFunctions
 import Language.Java.Pretty
 import Language.Java.Syntax
 
-import Data.String
+import           Control.Monad.State
+import qualified Data.Map            as M
+import           Data.String
+
 import LogicIR.Expr
 import LogicIR.Parser ()
 
+-- Convert a Java expression to a LIR expression.
+-- The transformation is stateful, since we need to generate fresh variables
+-- when introducing variables with the `with` construct.
 javaExpToLExpr :: Exp -> TypeEnv -> [TypeDecl] -> LExpr
-javaExpToLExpr = foldExp javaExpToLExprAlgebra
-
--- Converts a name to a LogicIR.Var, it queries the type environment to find the correct type.
-nameToVar :: Name -> TypeEnv -> [TypeDecl] -> Var
-nameToVar name env decls =
-    case type_ of
-        PrimType BooleanT                       -> fromString(symbol ++ ":bool")
-        PrimType ShortT                         -> fromString(symbol ++ ":int")
-        PrimType IntT                           -> fromString(symbol ++ ":int")
-        PrimType LongT                          -> fromString(symbol ++ ":int")
-        PrimType FloatT                         -> fromString(symbol ++ ":real")
-        PrimType DoubleT                        -> fromString(symbol ++ ":real")
-        RefType (ArrayType (PrimType ShortT))   -> fromString(symbol ++ ":[int]")
-        RefType (ArrayType (PrimType IntT))     -> fromString(symbol ++ ":[int]")
-        RefType (ArrayType (PrimType LongT))    -> fromString(symbol ++ ":[int]")
-        RefType (ArrayType (PrimType FloatT))   -> fromString(symbol ++ ":[real]")
-        RefType (ArrayType (PrimType DoubleT))  -> fromString(symbol ++ ":[real]")
-        _ -> error $ "Unsupported type: " ++ prettyPrint type_ ++ " " ++ prettyPrint name
-    where
-      (type_, symbol) = (lookupType decls env name, prettyPrint name)
+javaExpToLExpr e env d = evalState (foldExp javaExpToLExprAlgebra e env d) 0
 
-javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> LExpr)
+javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> State Int 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 _ _ =
+    fLit lit _ _ = return $
       case lit of
         Boolean t -> b t
         Int i     -> n $ fromInteger i
@@ -48,80 +35,12 @@ javaExpToLExprAlgebra =
         Double i  -> r i
         Null      -> "null"
         _         -> error $ "Unsupported type: " ++ show lit
-    fClassLit = error "fClassLit not supported..."
-    fThis = error "fThis not supported..."
-    fThisClass = error "fThisClass not supported..."
-    fInstanceCreation = error "fInstanceCreation not supported..."
-    fQualInstanceCreation = error "fQualInstanceCreation not supported..."
-    fArrayCreate = error "fArrayCreate not supported..."
-    fArrayCreateInit = error "fArrayCreateInit not supported..."
-    fFieldAccess = undefined {-case fieldAccess of -- TODO: implement field accesses
-                        PrimaryFieldAccess e id         -> case e of
-                                                                InstanceCreation _ t args _ -> undefined
-                                                                _ -> undefined
-                        SuperFieldAccess id             -> mkStringSymbol (prettyPrint (Name [id])) >>= mkIntVar
-                        ClassFieldAccess (Name name) id -> mkStringSymbol (prettyPrint (Name (name ++ [id]))) >>= mkIntVar -}
-    fMethodInv inv env decls =
-      case inv of -- TODO: very hardcoded EDSL + lambdas cannot be { return expr; } + ranged
-        -- Java: imp(exp1, exp2);
-        MethodCall (Name [Ident "imp"]) [exp1, exp2]
-            -> refold exp1 .==> refold exp2
-        -- Java: with(exp1, bound -> exp2);
-        MethodCall (Name [Ident "with"]) [exp1, Lambda (LambdaSingleParam bound) (LambdaExpression exp2)]
-            -> (LVar (nameToVar (Name [bound]) env decls) .== refold exp1) .==> refold exp2
-        -- Java: method(name, bound -> expr);
-        MethodCall (Name [Ident method]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-            -> quant method name bound expr
-        -- Java: method(name, bound -> { return expr; });
-        MethodCall (Name [Ident method]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
-            -> quant method name bound expr
-        -- Java: method(name, rbegin, rend, bound -> expr);
-        MethodCall (Name [Ident method]) [ExpName name, rbegin, rend, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-            -> quantr method name rbegin rend bound expr
-        -- Java: method(name, rbegin, rend, bound -> { return expr; });
-        MethodCall (Name [Ident method]) [ExpName name, rbegin, rend, Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
-            -> quantr method name rbegin rend bound expr
-        _
-            -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
-        where quant method name bound expr =
-                let i = Var (TPrim PInt) bound
-                    (zero, len) = (LConst (CInt 0), LLen (nameToVar name env decls))
-                in case method of
-                          "forall" -> lquantr QAll i zero len expr
-                          "exists" -> lquantr QAny i zero len expr
-                          _ -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
-              quantr method name rbegin rend bound expr =
-                let (begin, end) = (refold rbegin, refold rend)
-                    (i, _) = (Var (TPrim PInt) bound, nameToVar name env decls)
-                in case method of
-                          "forallr" -> lquantr QAll i begin end expr
-                          "existsr" -> lquantr QAny i begin end expr
-                          _ -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
-              lquantr op i begin end expr =
-                LQuant op i (LBinop (v i .>= begin) LAnd (LBinop (LVar i) CLess end)) (refold expr)
-              refold expr =
-                foldExp javaExpToLExprAlgebra expr env decls
-    fArrayAccess arrayIndex env decls =
-      case arrayIndex of
-        ArrayIndex (ExpName name) [expr]
-          -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)
-        _
-          -> error $ "Multidimensional arrays are not supported: " ++ prettyPrint arrayIndex
-    fExpName name env decls =
-      case name of
-        Name [Ident a, Ident "length"] -> LLen $ 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..."
-    fPreDecrement = error "fPreDecrement has side effects..."
     fPrePlus e = e
-    fPreMinus e env decls = LUnop NNeg (e env decls)
-    fPreBitCompl _ _ _ = error "Bitwise operations not supported..."
-    fPreNot e env decls = LUnop LNot (e env decls)
-    fCast = error "fCast is not supported..." -- TODO: perhaps support cast for some types?
-    fBinOp e1 op e2 env decls = -- TODO: type checking?
-      e1 env decls `bop` e2 env decls
+    fPreMinus e env decls = LUnop NNeg <$> e env decls
+    fPreNot e env decls = LUnop LNot <$> e env decls
+    fCond c a b_ env d = LIf <$> c env d <*> a env d <*> b_ env d
+    fBinOp e1 op e2 env decls =
+      bop <$> e1 env decls <*> e2 env decls
       where
         bop =
           case op of
@@ -143,8 +62,104 @@ javaExpToLExprAlgebra =
             Equal   -> (.==)
             NotEq   -> (.!=)
             _       -> error $ "Unsupported operation: " ++ prettyPrint op
-    fInstanceOf = error "fInstanceOf is not supported..."
-    fCond c a b_ env decls = LIf (c env decls) (a env decls) (b_ env decls)
-    fAssign = error "fAssign has side effects..."
-    fLambda = error "fLambda should be handled by fMethodInv..."
-    fMethodRef = undefined
+    fExpName name env decls = return $
+      case name of
+        Name [Ident a, Ident "length"] -> LLen $ nameToVar (Name [Ident a]) env decls
+        _ -> LVar $ nameToVar name env decls
+    fArrayAccess arrayIndex env decls =
+      case arrayIndex of
+        ArrayIndex (ExpName name) [expr] ->
+          LArray (nameToVar name env decls) <$>
+            foldExp javaExpToLExprAlgebra expr env decls
+        _ -> error $ "Multidimensional arrays are not supported: " ++ prettyPrint arrayIndex
+    fMethodInv inv env decls =
+      case inv of -- NOTE: EDSL only support single-param expression lambdas
+        -- Java: imp(exp1, exp2);
+        MethodCall (Name [Ident "imp"]) [exp1, exp2] ->
+          (.==>) <$> refold exp1 <*> refold exp2
+        -- Java: with(exp1, bound -> exp2);
+        -- NOTE: Need to introduce a fresh variable here
+        MethodCall (Name [Ident "with"]) [exp1, Lambda (LambdaSingleParam x) (LambdaExpression exp2)] -> do
+          x' <- (Ident . ("TEMP_" ++) . show) <$> get
+          modify (+ 1)
+          let sMap = M.singleton x x'
+          e1 <- refold $ substExp exp1 sMap
+          e2 <- refold $ substExp exp2 sMap
+          return $ (LVar (nameToVar (Name [x']) env decls) .== e1) .==> e2
+        -- Java: method(name, bound -> expr);
+        MethodCall (Name [Ident method]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
+            -> quant method name bound expr
+        -- Java: method(name, rbegin, rend, bound -> expr);
+        MethodCall (Name [Ident method]) [ExpName name, rbegin, rend, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
+            -> quantr method name rbegin rend bound expr
+        _ -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
+        where quant method name bound expr =
+                let i = Var (TPrim PInt) bound
+                    (zero, len) = (LConst (CInt 0), LLen (nameToVar name env decls))
+                in case method of
+                          "forall" -> lquantr QAll i zero len expr
+                          "exists" -> lquantr QAny i zero len expr
+                          _ -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
+              quantr method name rbegin rend bound expr = do
+                begin <- refold rbegin
+                end <- refold rend
+                let (i, _) = (Var (TPrim PInt) bound, nameToVar name env decls)
+                case method of
+                  "forallr" -> lquantr QAll i begin end expr
+                  "existsr" -> lquantr QAny i begin end expr
+                  _ -> error $ "Unimplemented fMethodInv: " ++ prettyPrint inv
+              lquantr op i begin end expr =
+                LQuant op i (LBinop (v i .>= begin) LAnd (LBinop (LVar i) CLess end)) <$> refold expr
+              refold expr =
+                foldExp javaExpToLExprAlgebra expr env decls
+    fPreBitCompl _ _ _ = no "PreBitCompl"; fFieldAccess = no "FieldAccess"
+    fInstanceOf = no "InstanceOf"; fAssign = no "Assign"; fLambda = no "Lambda"
+    fMethodRef = no "MethodRef"; fPostIncrement = no "PostIncrement"
+    fPostDecrement = no "PostDecrement"; fPreIncrement = no "PreIncrement"
+    fPreDecrement = no "PreDecrement"; fClassLit = no "ClassLit"
+    fThis = no "This"; fThisClass = no "ThisClass"
+    fInstanceCreation = no "InstanceCreation"; fArrayCreate = no "ArrayCreate"
+    fQualInstanceCreation = no "QualInstanceCreation"; fCast = no "Cast"
+    fArrayCreateInit = no "ArrayCreateInit"
+    no = error . ("[javaExpToLExp] " ++) . (++ " is not supported")
+
+-- Substitute a variable for another over a Java expression.
+type Substitution a = M.Map a a
+
+substExp :: Exp -> Substitution Ident -> Exp
+substExp e substMap =
+  let sb ex = substExp ex substMap
+  in case e of
+    Lit l              -> Lit l
+    ExpName (Name [x]) -> ExpName $ Name [M.findWithDefault x x substMap]
+    PrePlus e'         -> PrePlus (sb e')
+    PreMinus e'        -> PreMinus (sb e')
+    PreNot e'          -> PreNot (sb e')
+    BinOp e1 op e2     -> BinOp (sb e1) op (sb e2)
+    Cond e1 e2 e3      -> Cond (sb e1) (sb e2) (sb e3)
+    MethodInv (MethodCall f args) ->
+      MethodInv $ MethodCall f (sb <$> args)
+    ArrayAccess (ArrayIndex eArr eIs) ->
+      ArrayAccess $ ArrayIndex (sb eArr) (sb <$> eIs)
+    Lambda p@(LambdaSingleParam x) (LambdaExpression e') ->
+      Lambda p (LambdaExpression $ substExp e' (M.delete x substMap))
+    _ -> error "substExp: not supported"
+
+-- Converts a name to a LogicIR.Var, it queries the type environment to find the correct type.
+nameToVar :: Name -> TypeEnv -> [TypeDecl] -> Var
+nameToVar name env decls =
+    case type_ of
+        PrimType BooleanT                       -> fromString(symbol ++ ":bool")
+        PrimType ShortT                         -> fromString(symbol ++ ":int")
+        PrimType IntT                           -> fromString(symbol ++ ":int")
+        PrimType LongT                          -> fromString(symbol ++ ":int")
+        PrimType FloatT                         -> fromString(symbol ++ ":real")
+        PrimType DoubleT                        -> fromString(symbol ++ ":real")
+        RefType (ArrayType (PrimType ShortT))   -> fromString(symbol ++ ":[int]")
+        RefType (ArrayType (PrimType IntT))     -> fromString(symbol ++ ":[int]")
+        RefType (ArrayType (PrimType LongT))    -> fromString(symbol ++ ":[int]")
+        RefType (ArrayType (PrimType FloatT))   -> fromString(symbol ++ ":[real]")
+        RefType (ArrayType (PrimType DoubleT))  -> fromString(symbol ++ ":[real]")
+        _ -> error $ "Unsupported type: " ++ prettyPrint type_ ++ " " ++ prettyPrint name
+    where
+      (type_, symbol) = (lookupType decls env name, prettyPrint name)

test/TExamples.hs

@@ -43,5 +43,7 @@ examples =
   , "sorted3" .!= "sorted4"
   , "sorted1" .== "sorted4"
   , "imp1" .!= "imp2"
-  , "varIntro1" .!= "varIntro2"
+  , "varIntro11" .!= "varIntro12"
+  , "varIntro21" .== "varIntro22"
+  , "varIntro31" .== "varIntro32"
   ]

test/TIRParser.hs

 {-# LANGUAGE OverloadedStrings #-}
 module TIRParser where
 
-import System.IO.Unsafe (unsafePerformIO)
 import Test.HUnit
 
 import LogicIR.Expr
-import LogicIR.Parser
+import LogicIR.Parser ()
 
+parserTests :: [Assertion]
 parserTests =
   [ "1 + 1" @?= n 1 .+ n 1
   , "(1 == 1 ? 1 : 2)" @?=