diff options
Diffstat (limited to 'Jennisys')
| -rw-r--r-- | Jennisys/Analyzer.fs | 6 | ||||
| -rw-r--r-- | Jennisys/Ast.fs | 3 | ||||
| -rw-r--r-- | Jennisys/AstUtils.fs | 322 | ||||
| -rw-r--r-- | Jennisys/Parser.fsy | 4 | ||||
| -rw-r--r-- | Jennisys/Resolver.fs | 23 |
5 files changed, 207 insertions, 151 deletions
diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs index e14d2d06..47313465 100644 --- a/Jennisys/Analyzer.fs +++ b/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/Ast.fs b/Jennisys/Ast.fs index eeb34a8d..7af1b6f6 100644 --- a/Jennisys/Ast.fs +++ b/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/AstUtils.fs b/Jennisys/AstUtils.fs index b81fd807..72bd189e 100644 --- a/Jennisys/AstUtils.fs +++ b/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/Parser.fsy b/Jennisys/Parser.fsy index 395ee223..15b27ddb 100644 --- a/Jennisys/Parser.fsy +++ b/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/Resolver.fs b/Jennisys/Resolver.fs index fac29fba..f87ce5bd 100644 --- a/Jennisys/Resolver.fs +++ b/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 |