- 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.

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