Skip to content
Snippets Groups Projects
Verified Commit 152dbe6e authored by Ogilvie, D.H. (Duncan)'s avatar Ogilvie, D.H. (Duncan)
Browse files

implement ranged quantifiers 

closes #21
parent 83bf6565
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/LogicIR/Frontend/Java.hs
+ 27
− 18
View file @ 152dbe6e
...@@ -43,26 +43,35 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, ...@@ -43,26 +43,35 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
_ -> undefined _ -> undefined
SuperFieldAccess id -> mkStringSymbol (prettyPrint (Name [id])) >>= mkIntVar SuperFieldAccess id -> mkStringSymbol (prettyPrint (Name [id])) >>= mkIntVar
ClassFieldAccess (Name name) id -> mkStringSymbol (prettyPrint (Name (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 fMethodInv inv env decls = case inv of -- TODO: very hardcoded EDSL + lambdas cannot be { return expr; } + ranged
-- Java: forall(name, bound -> expr); -- Java: method(name, bound -> expr);
MethodCall (Name [Ident "forall"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)] MethodCall (Name [Ident method]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-> forall name bound expr -> quant method name bound expr
-- Java: exists(name, bound -> expr); -- Java: method(name, bound -> { return expr; });
MethodCall (Name [Ident "exists"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)] MethodCall (Name [Ident method]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
-> exists name bound expr -> quant method name bound expr
-- Java: forall(name, bound -> { return expr; }); -- Java: method(name, rbegin, rend, bound -> expr);
MethodCall (Name [Ident "forall"]) [ExpName name ,Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))] MethodCall (Name [Ident method]) [ExpName name, rbegin, rend, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-> forall name bound expr -> quantr method name rbegin rend bound expr
-- Java: exists(name, bound -> { return expr; }); -- Java: method(name, rbegin, rend, bound -> { return expr; });
MethodCall (Name [Ident "exists"]) [ExpName name ,Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))] MethodCall (Name [Ident method]) [ExpName name, rbegin, rend, Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
-> exists name bound expr -> quantr method name rbegin rend bound expr
_ _
-> error $ "Unimplemented fMethodInv: " ++ show inv -> error $ "Unimplemented fMethodInv: " ++ show inv
where quant method name bound expr = let (i) = (Var (TPrim PInt32) bound) in
where forall name bound expr = let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in let (zero, len) = (LConst (CInt 0), LLen (nameToVar name env decls)) in
LQuant QAll i (LBinop (LBinop (LVar i) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar i) CLess (LLen arr))) (foldExp javaExpToLExprAlgebra expr env decls) case method of
exists name bound expr = let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in "forall" -> lquantr QAll i zero len expr
LQuant QAny i (LBinop (LBinop (LVar i) CGeq (LConst (CInt 0))) LAnd (LBinop (LVar i) CLess (LLen arr))) (foldExp javaExpToLExprAlgebra expr env decls) "exists" -> lquantr QAny i zero len expr
_ -> error $ "Unimplemented fMethodInv: " ++ show inv
quantr method name rbegin rend bound expr = let (begin, end) = (refold rbegin, refold rend) in
let (i, arr) = (Var (TPrim PInt32) 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: " ++ show inv
lquantr op i begin end expr = LQuant op i (LBinop (LBinop (LVar i) CGeq begin) LAnd (LBinop (LVar i) CLess end)) (refold expr)
refold expr = foldExp javaExpToLExprAlgebra expr env decls
fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
ArrayIndex (ExpName name) [expr] ArrayIndex (ExpName name) [expr]
-> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls) -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment