From a90b5d1fdf92e9f17eb8da23348d93bbbe46b88d Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 13 Jul 2011 01:24:27 -0700 Subject: - changed the parser to create VarLiteral instead of IdLiteral for method arguments in method pre/post conditions and quantiication variables in quantified expressions - refactoring: changed the EvalSym method to return an expression instead of a constant. --- Jennisys/Jennisys/Analyzer.fs | 6 +- Jennisys/Jennisys/Ast.fs | 3 +- Jennisys/Jennisys/AstUtils.fs | 322 ++++++++++++++++++++++++------------------ Jennisys/Jennisys/Parser.fsy | 4 +- Jennisys/Jennisys/Resolver.fs | 23 ++- 5 files changed, 207 insertions(+), 151 deletions(-) diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs index e14d2d06..47313465 100644 --- a/Jennisys/Jennisys/Analyzer.fs +++ b/Jennisys/Jennisys/Analyzer.fs @@ -97,7 +97,7 @@ let GetUnifications expr args (heap,env,ctx) = builder { let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption - let! v = Eval (heap,env,ctx) e + let! v = try Some(Eval (heap,env,ctx) true e |> Expr2Const) with ex -> None Logger.DebugLine (" - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v)); return Map.add e v unifMap } @@ -267,7 +267,7 @@ let TryInferConditionals prog comp m unifs (heap,env,ctx) = // - add pre and post conditions // - go through all objects on the heap and assert its invariant let pre,post = GetMethodPrePost m - let prepostExpr = post |> RewriteMethodArgs (GetMethodArgs m) //TODO: do we need the "pre" here as well? + let prepostExpr = post //TODO: do we need the "pre" here as well? let heapObjs = heap |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty let expr = heapObjs |> Set.fold (fun acc o -> let receiverOpt = GetObjRefExpr o (heap,env,ctx) @@ -283,7 +283,7 @@ let TryInferConditionals prog comp m unifs (heap,env,ctx) = ) prepostExpr expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "") // now evaluate and see what's left - let c = Eval (heap,env,ctx) expr + let c = Eval (heap2,env2,ctx2) false expr Some(heap2,env2,ctx2) // ============================================================================ diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs index eeb34a8d..7af1b6f6 100644 --- a/Jennisys/Jennisys/Ast.fs +++ b/Jennisys/Jennisys/Ast.fs @@ -39,7 +39,7 @@ type Expr = | UpdateExpr of Expr * Expr * Expr | SequenceExpr of Expr list | SeqLength of Expr - | SetExpr of Expr list + | SetExpr of Expr list //TODO: maybe this should really be a set instead of a list | ForallExpr of VarDecl list * Expr type Stmt = @@ -77,6 +77,5 @@ type Const = | NoneConst | ThisConst of (* loc id *) string * Type option | NewObj of (* loc id *) string * Type option - | VarConst of (* loc id *) string * Type option | ExprConst of Expr | Unresolved of (* loc id *) string \ No newline at end of file diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs index b81fd807..72bd189e 100644 --- a/Jennisys/Jennisys/AstUtils.fs +++ b/Jennisys/Jennisys/AstUtils.fs @@ -33,155 +33,172 @@ let rec VisitExpr visitorFunc expr acc = exception EvalFailed -let DefaultResolver e = ExprConst(e) +let DefaultResolver e = e + +let DefaultFallbackResolver resolverFunc e = + match resolverFunc e with + | Some(e') -> e' + | None -> e let EvalSym resolverFunc expr = let rec __EvalSym ctx expr = match expr with - | IntLiteral(n) -> IntConst(n) - | IdLiteral(_) | Dot(_) -> resolverFunc expr - | SeqLength(e) -> - match __EvalSym ctx e with - | SeqConst(clist) -> IntConst(List.length clist) - | _ -> resolverFunc expr + | IntLiteral(_) -> expr + | BoolLiteral(_) -> expr + | Star -> expr //TODO: can we do better? + | VarLiteral(_) -> resolverFunc expr + | IdLiteral(_) -> resolverFunc expr + | Dot(_) -> resolverFunc expr + | SeqLength(e) -> + let e' = __EvalSym ctx e + match e' with + | SequenceExpr(elist) -> IntLiteral(List.length elist) + | _ -> SeqLength(e') | SequenceExpr(elist) -> - let clist = elist |> List.fold (fun acc e -> __EvalSym ctx e :: acc) [] |> List.rev - SeqConst(clist) - | SetExpr(eset) -> - let cset = eset |> List.fold (fun acc e -> Set.add (__EvalSym ctx e) acc) Set.empty - SetConst(cset) + let elist' = elist |> List.fold (fun acc e -> __EvalSym ctx e :: acc) [] |> List.rev + SequenceExpr(elist') + | SetExpr(elist) -> + let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym ctx e) acc) Set.empty + SetExpr(Set.toList eset') | SelectExpr(lst, idx) -> - match __EvalSym ctx lst, __EvalSym ctx idx with - | SeqConst(clist), IntConst(n) -> clist.[n] - | _ -> resolverFunc expr + let lst', idx' = __EvalSym ctx lst, __EvalSym ctx idx + match lst', idx' with + | SequenceExpr(elist), IntLiteral(n) -> elist.[n] + | _ -> SelectExpr(lst', idx') | UpdateExpr(lst,idx,v) -> - match __EvalSym ctx lst, __EvalSym ctx idx, __EvalSym ctx v with - | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist) - | _ -> resolverFunc expr + let lst', idx', v' = __EvalSym ctx lst, __EvalSym ctx idx, __EvalSym ctx v + match lst', idx', v' with + | SequenceExpr(elist), IntLiteral(n), _ -> SequenceExpr(Utils.ListSet n v' elist) + | _ -> UpdateExpr(lst', idx', v') | IteExpr(c, e1, e2) -> - match __EvalSym ctx c with - | BoolConst(b) -> if b then __EvalSym ctx e1 else __EvalSym ctx e2 - | _ -> resolverFunc expr - | BinaryExpr(_,op,e1,e2) -> + let c', e1', e2' = __EvalSym ctx c, __EvalSym ctx e1, __EvalSym ctx e2 + match c' with + | BoolLiteral(b) -> if b then e1' else e2' + | _ -> IteExpr(c', e1', e2') + | BinaryExpr(p,op,e1,e2) -> + let e1' = __EvalSym ctx e1 + let e2' = __EvalSym ctx e2 + let recomposed = BinaryExpr(p,op,e1',e2') match op with | "=" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) - | IntConst(n1), IntConst(n2) -> BoolConst(n1 = n2) - | ExprConst(e1), ExprConst(e2) -> BoolConst(e1 = e2) - | _ -> resolverFunc expr + match e1', e2' with + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2) + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 = n2) + | _ when e1' = e2' -> BoolLiteral(true) + | _ -> recomposed | "!=" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2)) - | IntConst(n1), IntConst(n2) -> BoolConst(not (n1 = n2)) - | ExprConst(e1), ExprConst(e2) -> BoolConst(not (e1 = e2)) + match e1', e2' with + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(not (b1 = b2)) + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(not (n1 = n2)) + | _ when e1' = e2' -> BoolLiteral(false) | _ -> resolverFunc expr | "<" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 < n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) < (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) < (List.length s2)) - | _ -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 < n2) + | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2)) + | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) < (List.length s2)) + | _ -> recomposed | "<=" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 <= n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) <= (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) <= (List.length s2)) - | _ -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 <= n2) + | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2)) + | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) <= (List.length s2)) + | _ -> recomposed | ">" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 > n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) > (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) > (List.length s2)) - | _ -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 > n2) + | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2)) + | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) > (List.length s2)) + | _ -> recomposed | ">=" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> BoolConst(n1 >= n2) - | SetConst(s1), SetConst(s2) -> BoolConst((Set.count s1) >= (Set.count s2)) - | SeqConst(s1), SeqConst(s2) -> BoolConst((List.length s1) >= (List.length s2)) - | _ -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> BoolLiteral(n1 >= n2) + | SetExpr(s1), SetExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2)) + | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2)) + | _ -> recomposed | "in" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | _ as c, SetConst(s) -> BoolConst(Set.contains c s) - | _ as c, SeqConst(s) -> BoolConst(Utils.ListContains c s) - | _ -> resolverFunc expr + match e1', e2' with + | _, SetExpr(s) + | _, SequenceExpr(s) -> BoolLiteral(Utils.ListContains e1' s) + | _ -> recomposed | "!in" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | _ as c, SetConst(s) -> BoolConst(not (Set.contains c s)) - | _ as c, SeqConst(s) -> BoolConst(not (Utils.ListContains c s)) - | _ -> resolverFunc expr + match e1', e2' with + | _, SetExpr(s) + | _, SequenceExpr(s) -> BoolLiteral(not (Utils.ListContains e1' s)) + | _ -> recomposed | "+" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) - | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2) - | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2) - | q,w -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 + n2) + | SequenceExpr(l1), SequenceExpr(l2) -> SequenceExpr(List.append l1 l2) + | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.union (Set.ofList s1) (Set.ofList s2) |> Set.toList) + | _ -> recomposed | "-" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2) - | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2) - | _ -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 - n2) + | SetExpr(s1), SetExpr(s2) -> SetExpr(Set.difference (Set.ofList s1) (Set.ofList s2) |> Set.toList) + | _ -> recomposed | "*" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2) - | _ -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 * n2) + | _ -> recomposed | "div" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2) - | _ -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 / n2) + | _ -> recomposed | "mod" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2) - | _ -> resolverFunc expr + match e1', e2' with + | IntLiteral(n1), IntLiteral(n2) -> IntLiteral(n1 % n2) + | _ -> recomposed | "&&" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 && b2) - | _ -> resolverFunc expr + match e1', e2' with + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 && b2) + | _ -> recomposed | "||" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 || b2) - | _ -> resolverFunc expr + match e1', e2' with + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 || b2) + | _ -> recomposed | "==>" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst((not b1) || b2) - | _ -> resolverFunc expr + match e1', e2' with + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral((not b1) || b2) + | _ -> recomposed | "<==>" -> - match __EvalSym ctx e1, __EvalSym ctx e2 with - | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2) - | _ -> resolverFunc expr - | _ -> resolverFunc expr + match e1', e2' with + | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral(b1 = b2) + | _ -> recomposed + | _ -> recomposed | UnaryExpr(op, e) -> + let e' = __EvalSym ctx e + let recomposed = UnaryExpr(op, e') match op with | "!" -> - match __EvalSym ctx e with - | BoolConst(b) -> BoolConst(not b) - | _ -> resolverFunc expr + match e' with + | BoolLiteral(b) -> BoolLiteral(not b) + | _ -> recomposed | "-" -> - match __EvalSym ctx e with - | IntConst(n) -> IntConst(-n) - | _ -> resolverFunc expr - | _ -> resolverFunc expr + match e' with + | IntLiteral(n) -> IntLiteral(-n) + | _ -> recomposed + | _ -> recomposed | ForallExpr(vars, e) -> - let rec PrintSep sep f list = - match list with - | [] -> "" - | [a] -> f a + let rec PrintSep sep f list = + match list with + | [] -> "" + | [a] -> f a | a :: more -> (f a) + sep + (PrintSep sep f more) - let rec PrintType ty = - match ty with - | IntType -> "int" - | BoolType -> "bool" - | NamedType(id, args) -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args) - | SeqType(t) -> sprintf "seq[%s]" (PrintType t) - | SetType(t) -> sprintf "set[%s]" (PrintType t) + let rec PrintType ty = + match ty with + | IntType -> "int" + | BoolType -> "bool" + | NamedType(id, args) -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args) + | SeqType(t) -> sprintf "seq[%s]" (PrintType t) + | SetType(t) -> sprintf "set[%s]" (PrintType t) | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args) - let PrintVarDecl vd = - match vd with - | Var(id,None) -> id + let PrintVarDecl vd = + match vd with + | Var(id,None) -> id | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty) vars |> List.iter (fun v -> printfn "%s" (PrintVarDecl v)) - resolverFunc expr - | _ -> resolverFunc expr + resolverFunc expr //TODO __EvalSym [] expr // ======================================= @@ -198,7 +215,25 @@ let rec Const2Expr c = | Unresolved(name) -> IdLiteral(name) | NullConst -> IdLiteral("null") | ExprConst(e) -> e - | _ -> failwith "not implemented or not supported" + | _ -> failwithf "not implemented or not supported: %O" c + +let rec Expr2Const e = + match e with + | IntLiteral(n) -> IntConst(n) + | BoolLiteral(b) -> BoolConst(b) + | IdLiteral("this") -> ThisConst("this",None) + | IdLiteral("null") -> NullConst + | IdLiteral(id) -> Unresolved(id) + | VarLiteral(id) -> Unresolved(id) + | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const) + | SetExpr(elist) -> SetConst(elist |> List.map Expr2Const |> Set.ofList) + | _ -> failwithf "Not a constant: %O" e + +let TryExpr2Const e = + try + Some(Expr2Const e) + with + | ex -> None // ======================================================================= /// Returns a binary AND of the two given expressions with short-circuiting @@ -355,6 +390,10 @@ let GetMethodPrePost mthd = // ========================================================= /// Returns all arguments of a method (both input and output) // ========================================================= +let GetSigVars sign = + match sign with + | Sig(ins, outs) -> List.concat [ins; outs] + let GetMethodArgs mthd = match mthd with | Method(_,Sig(ins, outs),_,_,_) -> List.concat [ins; outs] @@ -448,20 +487,20 @@ let rec Desugar expr = match op with | "=" -> match EvalSym DefaultResolver e1, EvalSym DefaultResolver e2 with - | SeqConst(cl1), SeqConst(cl2) -> + | SequenceExpr(l1), SequenceExpr(l2) -> let rec __fff lst1 lst2 cnt = match lst1, lst2 with - | fs1 :: rest1, fs2 :: rest2 -> BinaryEq (Const2Expr cl1.[cnt]) (Const2Expr cl2.[cnt]) :: __fff rest1 rest2 (cnt+1) + | fs1 :: rest1, fs2 :: rest2 -> BinaryEq l1.[cnt] l2.[cnt] :: __fff rest1 rest2 (cnt+1) | [], [] -> [] | _ -> failwith "Lists are of different sizes" - __fff cl1 cl2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be - | c, SeqConst(clist) - | SeqConst(clist), c -> + __fff l1 l2 0 |> List.fold (fun acc e -> BinaryAnd acc e) be + | e, SequenceExpr(elist) + | SequenceExpr(elist), e -> let rec __fff lst cnt = match lst with - | fs :: rest -> BinaryEq (SelectExpr(Const2Expr c, IntLiteral(cnt))) (Const2Expr clist.[cnt]) :: __fff rest (cnt+1) + | fs :: rest -> BinaryEq (SelectExpr(e, IntLiteral(cnt))) elist.[cnt] :: __fff rest (cnt+1) | [] -> [] - __fff clist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be + __fff elist 0 |> List.fold (fun acc e -> BinaryAnd acc e) be | _ -> be | _ -> be with @@ -496,25 +535,34 @@ let ChangeThisReceiver receiver expr = (* function body starts here *) __ChangeThis Set.empty expr -let rec Rewrite rewriterFunc expr = +let rec Rewrite rewriterFunc expr = + let __RewriteOrRecurse e = + match rewriterFunc e with + | Some(ee) -> ee + | None -> Rewrite rewriterFunc e match expr with | IntLiteral(_) | BoolLiteral(_) | Star | VarLiteral(_) - | IdLiteral(_) -> rewriterFunc expr - | Dot(e, id) -> Dot(rewriterFunc e, id) - | ForallExpr(vars,e) -> ForallExpr(vars, rewriterFunc e) - | UnaryExpr(op,e) -> UnaryExpr(op, rewriterFunc e) - | SeqLength(e) -> SeqLength(rewriterFunc e) - | SelectExpr(e1, e2) -> SelectExpr(rewriterFunc e1, rewriterFunc e2) - | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, rewriterFunc e1, rewriterFunc e2) - | IteExpr(e1,e2,e3) -> IteExpr(rewriterFunc e1, rewriterFunc e2, rewriterFunc e3) - | UpdateExpr(e1,e2,e3) -> UpdateExpr(rewriterFunc e1, rewriterFunc e2, rewriterFunc e3) - | SequenceExpr(exs) -> SequenceExpr(exs |> List.map rewriterFunc) - | SetExpr(exs) -> SetExpr(exs |> List.map rewriterFunc) - -let RewriteMethodArgs args expr = - let __IdIsArg id = args |> List.exists (function Var(name,_) -> name = id) - Rewrite (function IdLiteral(id) when __IdIsArg id -> VarLiteral(id) | _ as e -> e) expr + | IdLiteral(_) -> match rewriterFunc expr with + | Some(e) -> e + | None -> expr + | Dot(e, id) -> Dot(__RewriteOrRecurse e, id) + | ForallExpr(vars,e) -> ForallExpr(vars, __RewriteOrRecurse e) + | UnaryExpr(op,e) -> UnaryExpr(op, __RewriteOrRecurse e) + | SeqLength(e) -> SeqLength(__RewriteOrRecurse e) + | SelectExpr(e1, e2) -> SelectExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2) + | BinaryExpr(p,op,e1,e2) -> BinaryExpr(p, op, __RewriteOrRecurse e1, __RewriteOrRecurse e2) + | IteExpr(e1,e2,e3) -> IteExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3) + | UpdateExpr(e1,e2,e3) -> UpdateExpr(__RewriteOrRecurse e1, __RewriteOrRecurse e2, __RewriteOrRecurse e3) + | SequenceExpr(exs) -> SequenceExpr(exs |> List.map __RewriteOrRecurse) + | SetExpr(exs) -> SetExpr(exs |> List.map __RewriteOrRecurse) + +let RewriteVars vars expr = + let __IdIsArg id = vars |> List.exists (function Var(name,_) -> name = id) + Rewrite (fun e -> + match e with + | IdLiteral(id) when __IdIsArg id -> Some(VarLiteral(id)) + | _ -> None) expr \ No newline at end of file diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy index 395ee223..15b27ddb 100644 --- a/Jennisys/Jennisys/Parser.fsy +++ b/Jennisys/Jennisys/Parser.fsy @@ -89,7 +89,7 @@ BlockStmt: Member: | VAR VarDecl { Field($2) } - | CONSTRUCTOR ID Signature Pre Post { Method($2, $3, $4, $5, true) } + | CONSTRUCTOR ID Signature Pre Post { Method($2, $3, RewriteVars (GetSigVars $3) $4, RewriteVars (GetSigVars $3) $5, true) } | METHOD ID Signature Pre Post { Method($2, $3, $4, $5, false) } | INVARIANT ExprList { Invariant($2) } @@ -188,7 +188,7 @@ Expr100: | LBRACKET ExprList RBRACKET { SequenceExpr($2) } | LCURLY ExprList RCURLY { SetExpr($2) } | VERTBAR Expr VERTBAR { SeqLength($2) } - | FORALL VarDeclList COLONCOLON Expr { ForallExpr($2, $4) } + | FORALL VarDeclList COLONCOLON Expr { ForallExpr($2, RewriteVars $2 $4) } StarExpr: | STAR { Star } diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs index fac29fba..f87ce5bd 100644 --- a/Jennisys/Jennisys/Resolver.fs +++ b/Jennisys/Jennisys/Resolver.fs @@ -67,11 +67,12 @@ let Resolve (env,ctx) cst = // ================================================================= /// Evaluates a given expression with respect to a given heap/env/ctx // ================================================================= -let Eval (heap,env,ctx) expr = +let Eval (heap,env,ctx) resolveVars expr = let rec __EvalResolver expr = match expr with - | VarLiteral(id) -> ExprConst(expr) + | VarLiteral(id) when not resolveVars -> ExprConst(expr) | IdLiteral("this") -> GetThisLoc env + | VarLiteral(id) | IdLiteral(id) -> match TryResolve (env,ctx) (Unresolved(id)) with | Unresolved(_) -> __EvalResolver (Dot(IdLiteral("this"), id)) @@ -84,8 +85,16 @@ let Eval (heap,env,ctx) expr = | _ :: _ -> failwithf "can't evaluate expression deterministically: %s.%s resolves to multiple locations." (PrintConst discr) str | [] -> failwithf "can't find value for %s.%s" (PrintConst discr) str | _ -> failwith "NOT IMPLEMENTED YET" - try - let unresolvedConst = EvalSym (fun e -> __EvalResolver e |> Resolve (env,ctx)) expr - Some(TryResolve (env,ctx) unresolvedConst) - with - ex -> None \ No newline at end of file +// try + EvalSym (fun e -> __EvalResolver e |> Resolve (env,ctx) |> Const2Expr) expr +// ccc |> Const2Expr +// match ccc with +// | ExprConst(eee) -> match Eval (heap,env,ctx) eee with +// | Some(c) -> c +// | None -> ccc +// | _ -> ccc +// ) expr + + //Some(TryResolve (env,ctx) unresolvedConst) +// with +// ex -> None \ No newline at end of file -- cgit v1.2.3