Jennisys:

   - finished the initial version of the modular code for constructors
     (excluding the unification part where it tries to find an existing function
     that meets the required spec)

10 files changed, 198 insertions, 118 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 7bc2e6cd..831fa0f6 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -125,7 +125,7 @@ let rec GetUnifications indent args heapInst unifs expr =
     let builder = new CascadingBuilder<_>(unifsAcc)

     builder {

       let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption

-      let! v = try Some(Eval heapInst true e |> Expr2Const) with ex -> None

+      let! v = try Some(Eval heapInst (fun _ -> true) e |> Expr2Const) with ex -> None

       return AddUnif indent e v unifsAcc

     }

   (* --- function body starts here --- *)

@@ -273,7 +273,7 @@ let rec DiscoverAliasing exprList heapInst =
   match exprList with

   | e1 :: rest -> 

       let eqExpr = rest |> List.fold (fun acc e -> 

-                                        if Eval heapInst true (BinaryEq e1 e) = TrueLiteral then

+                                        if Eval heapInst (fun _ -> true) (BinaryEq e1 e) = TrueLiteral then

                                           BinaryAnd acc (BinaryEq e1 e)

                                         else

                                           acc

@@ -281,6 +281,26 @@ let rec DiscoverAliasing exprList heapInst =
       BinaryAnd eqExpr (DiscoverAliasing rest heapInst)

   | [] -> TrueLiteral

 

+//  =============================================================================

+/// Returns an expression that combines the post-condition of a given method with

+/// invariants for all objects present on the heap

+//  =============================================================================

+let GetHeapExpr prog mthd heapInst = 

+  // get expressions to evaluate:

+  //   - add post (and pre?) conditions                                     

+  //   - go through all objects on the heap and assert their invariants  

+  let pre,post = GetMethodPrePost mthd

+  let prepostExpr = post //TODO: do we need the "pre" here as well?

+  let heapObjs = heapInst.assignments |> List.fold (fun acc ((o,_),_) -> acc |> Set.add o) Set.empty

+  heapObjs |> Set.fold (fun acc o -> 

+                          let receiverOpt = GetObjRefExpr o.name heapInst

+                          let receiver = Utils.ExtractOption receiverOpt

+                          let objComp = FindComponent prog (GetTypeShortName o.objType) |> Utils.ExtractOption

+                          let objInvs = GetInvariantsAsList objComp

+                          let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)

+                          objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

+                      ) prepostExpr

+

 // ------------------------------- Modularization stuff ---------------------------------

 

 let GetModularBranch prog comp meth hInst = 

@@ -294,6 +314,7 @@ let GetModularBranch prog comp meth hInst =
     let thisRhsExprs = hInst.assignments |> List.choose (function ((obj,_),e) when obj.name = "this" -> Some(e) | _ -> None)

     thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty 

                  |> Set.toList

+  let directChildren = lazy (__GetDirectChildren)

   let __IsAbstractField ty var = 

     let builder = CascadingBuilder<_>(false)

     let varName = GetVarName var

@@ -302,13 +323,32 @@ let GetModularBranch prog comp meth hInst =
       let! fld = GetAbstractFields comp |> List.fold (fun acc v -> if GetVarName v = varName then Some(varName) else acc) None

       return true

     }

-  let __GetSpecFor objLitName = 

-    let absFieldAssignments = hInst.assignments |> List.choose (fun ((obj,var),e) ->

-                                                                  if obj.name = objLitName && __IsAbstractField obj.objType var then

-                                                                    Some(var,e)

-                                                                  else

-                                                                    None)

-    absFieldAssignments |> List.fold (fun acc (Var(varName,_),e) -> BinaryAnd acc (BinaryEq (IdLiteral(varName)) e)) TrueLiteral

+  let __GetAbsFldAssignments objLitName = 

+    hInst.assignments |> List.choose (fun ((obj,var),e) ->

+                                        if obj.name = objLitName && __IsAbstractField obj.objType var then

+                                          Some(var,e)

+                                        else

+                                          None)

+  let rec __ExamineAndFix x e = 

+    match e with

+    | ObjLiteral(id) when not (Utils.ListContains e (directChildren.Force())) -> 

+        let absFlds = __GetAbsFldAssignments id

+        absFlds |> List.fold (fun acc (Var(vname,_),vval) -> BinaryAnd acc (BinaryEq (Dot(x, vname)) vval)) TrueLiteral

+    | SequenceExpr(elist) ->

+        let rec __fff lst acc cnt = 

+          match lst with

+          | fsExpr :: rest -> 

+              let acc = BinaryAnd acc (__ExamineAndFix (SelectExpr(x, IntLiteral(cnt))) fsExpr)

+              __fff rest acc (cnt+1)

+          | [] -> 

+              let lenExpr = BinaryEq (SeqLength(x)) (IntLiteral(cnt)) 

+              BinaryAnd lenExpr acc

+        __fff elist TrueLiteral 0

+    | _ -> BinaryEq x e

+

+  let __GetSpecFor objLitName =

+    let absFieldAssignments = __GetAbsFldAssignments objLitName

+    absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral

   let __GetArgsUsed expr = 

     let args = GetMethodArgs meth

     let argSet = DescendExpr2 (fun e acc ->

@@ -323,7 +363,7 @@ let GetModularBranch prog comp meth hInst =
   let rec __GetDelegateMethods objs acc = 

     match objs with

     | ObjLiteral(name) as obj :: rest ->

-        let mName = sprintf "_init_%s_%s" (GetMethodFullName comp meth |> String.map (fun c -> if c = '.' then '_' else c)) name

+        let mName = sprintf "_synth_%s_%s" (GetMethodFullName comp meth |> String.map (fun c -> if c = '.' then '_' else c)) name

         let pre = TrueLiteral

         let post = __GetSpecFor name

         let ins = __GetArgsUsed (BinaryAnd pre post)

@@ -338,8 +378,7 @@ let GetModularBranch prog comp meth hInst =
     with

       | ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth)

   (* --- function body starts here --- *)

-  let directChildren = __GetDirectChildren

-  let delegateMethods = __GetDelegateMethods directChildren Map.empty

+  let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty

   let initChildrenExprList = delegateMethods |> Map.toList

                                              |> List.map (fun (receiver, mthd) -> 

                                                             let key = __FindObj (PrintExpr 0 receiver), Var("", None)

@@ -360,6 +399,18 @@ let GetModularBranch prog comp meth hInst =
                                                                     ) (prog, comp, [])

   newProg, newComp, newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns }

 

+let rec MakeModular indent prog comp m cond heapInst = 

+  let idt = Indent indent

+  if Options.CONFIG.genMod then   

+    Logger.InfoLine (idt + "    - delegating to method calls     ...")

+    let newProg, newComp, newMthdLst, newHeapInst = GetModularBranch prog comp m heapInst

+    let msol = Utils.MapSingleton (newComp,m) [cond, newHeapInst]

+    newMthdLst |> List.fold (fun acc (c,m) -> 

+                                  acc |> MergeSolutions (Utils.MapSingleton (c,m) []) 

+                              ) msol     

+  else 

+    Utils.MapSingleton (comp,m) [cond, heapInst]

+

 //let GetModularSol prog sol = 

 //  let comp = fst (fst sol)

 //  let meth = snd (fst sol)

@@ -385,18 +436,6 @@ let GetModularBranch prog comp meth hInst =
 //  (* --- function body starts here --- *) 

 //  __Modularize prog (Map.toList solutions) Map.empty 

 

-let MakeModular indent prog comp m cond heapInst = 

-  let idt = Indent indent

-  if Options.CONFIG.genMod then   

-    Logger.InfoLine (idt + "    - delegating to method calls     ...")

-    let newProg, newComp, newMthdLst, newHeapInst = GetModularBranch prog comp m heapInst

-    let msol = Utils.MapSingleton (newComp,m) [cond, newHeapInst]

-    newMthdLst |> List.fold (fun acc (c,m) -> 

-                                  acc |> MergeSolutions (Utils.MapSingleton (c,m) []) //(AnalyzeConstructor (indent+2) newProg c m)

-                              ) msol     

-  else 

-    Utils.MapSingleton (comp,m) [cond, heapInst]

-

 // --------------------------------------------------------------------------------------

 

 //  ============================================================================

@@ -454,22 +493,9 @@ and TryInferConditionals indent prog comp m unifs heapInst =
   let idt = Indent indent

   let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]

   let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false

-  // get expressions to evaluate:

-  //   - add post (and pre?) conditions                                     

-  //   - go through all objects on the heap and assert their invariants  

-  let pre,post = GetMethodPrePost m

-  let prepostExpr = post //TODO: do we need the "pre" here as well?

-  let heapObjs = heapInst2.assignments |> List.fold (fun acc ((o,_),_) -> acc |> Set.add o) Set.empty

-  let expr = heapObjs |> Set.fold (fun acc o -> 

-                                     let receiverOpt = GetObjRefExpr o.name heapInst2

-                                     let receiver = Utils.ExtractOption receiverOpt

-                                     let objComp = FindComponent prog (GetTypeShortName o.objType) |> Utils.ExtractOption

-                                     let objInvs = GetInvariantsAsList objComp

-                                     let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)

-                                     objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

-                                  ) prepostExpr

+  let expr = GetHeapExpr prog m heapInst2

   // now evaluate and see what's left

-  let newCond = Eval heapInst2 false expr

+  let newCond = Eval heapInst2 (function VarLiteral(_) -> false | _ -> true) expr

   try

     if newCond = TrueLiteral then

       Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

@@ -505,7 +531,7 @@ and TryInferConditionals indent prog comp m unifs heapInst =
         wrongSol                     

   with

     ex -> raise ex

-  

+      

 let GetMethodsToAnalyze prog =

   let mOpt = Options.CONFIG.methodToSynth;

   if mOpt = "*" then

@@ -545,13 +571,21 @@ let GetMethodsToAnalyze prog =
 /// Returns a map from (component * method) |--> Expr * HeapInstance

 // ============================================================================

 let rec AnalyzeMethods prog members = 

+  let rec __AnalyzeConstructorDeep prog mList = 

+    match mList with

+    | (comp,mthd) :: rest -> 

+        let sol = AnalyzeConstructor 2 prog comp mthd

+        let unsolved = sol |> Map.filter (fun (c,m) lst -> lst = []) |> Utils.MapKeys

+        sol |> MergeSolutions (__AnalyzeConstructorDeep prog (rest@unsolved))

+    | [] -> Map.empty

+  (* --- function body starts here --- *)

   match members with

   | (comp,m) :: rest -> 

       match m with

       | Method(_,_,_,_,true) -> 

-          let solOpt = AnalyzeConstructor 2 prog comp m

+          let sol = __AnalyzeConstructorDeep prog [comp,m]

           Logger.InfoLine ""

-          AnalyzeMethods prog rest |> MergeSolutions solOpt

+          AnalyzeMethods prog rest |> MergeSolutions sol

       | _ -> AnalyzeMethods prog rest

   | [] -> Map.empty

 

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 42c1e74d..15c93047 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -480,8 +480,12 @@ let AddPrecondition prog comp m e =
 ////////////////////

 

 exception EvalFailed of string

+exception DomainNotInferred

 

-let DefaultResolver e = e

+let DefaultResolver e fldOpt = 

+  match fldOpt with

+  | None -> e

+  | Some(fldName) -> Dot(e, fldName)

 

 let DefaultFallbackResolver resolverFunc e = 

   match resolverFunc e with

@@ -515,9 +519,11 @@ let rec __EvalSym resolverFunc ctx expr =
         let _,e = ctx |> List.find (fun (v,e) -> GetVarName v = id)

         e

       with 

-      | ex -> resolverFunc expr

-  | IdLiteral(_)   -> resolverFunc expr

-  | Dot(_)         -> resolverFunc expr

+      | ex -> resolverFunc expr None

+  | IdLiteral(_)   -> resolverFunc expr None

+  | Dot(e, str)    -> 

+      let discr = __EvalSym resolverFunc ctx e

+      resolverFunc discr (Some(str))

   | SeqLength(e)   -> 

       let e' = __EvalSym resolverFunc ctx e

       match e' with

@@ -534,7 +540,8 @@ let rec __EvalSym resolverFunc ctx expr =
       let aparams' = aparams |> List.fold (fun acc e -> __EvalSym resolverFunc ctx e :: acc) [] |> List.rev

       MethodCall(rcv', name, aparams')

   | SelectExpr(lst, idx) ->

-      let lst', idx' = __EvalSym resolverFunc ctx lst, __EvalSym resolverFunc ctx idx 

+      let lst' = __EvalSym resolverFunc ctx lst

+      let idx' = __EvalSym resolverFunc ctx idx 

       match lst', idx' with

       | SequenceExpr(elist), IntLiteral(n) -> elist.[n] 

       | _ -> SelectExpr(lst', idx')

@@ -601,6 +608,12 @@ let rec __EvalSym resolverFunc ctx expr =
                  | SetExpr(s1), SetExpr(s2)           -> BoolLiteral((List.length s1) >= (List.length s2))

                  | SequenceExpr(s1), SequenceExpr(s2) -> BoolLiteral((List.length s1) >= (List.length s2))

                  | _ -> recomposed.Force()

+      | ".." ->

+          let e1'' = e1'.Force()

+          let e2'' = e2'.Force()

+          match e1'', e2'' with

+          | IntLiteral(lo), IntLiteral(hi)    -> SequenceExpr([lo .. hi] |> List.map (fun n -> IntLiteral(n)))

+          | _ -> recomposed.Force();

       | "in" -> 

           match e1'.Force(), e2'.Force() with

           | _, SetExpr(s)       

@@ -663,7 +676,9 @@ let rec __EvalSym resolverFunc ctx expr =
           match e1'.Force() with

           | BoolLiteral(false) -> BoolLiteral(true)

           | _ ->

-              match e1'.Force(), e2'.Force() with

+              let e1'' = e1'.Force()

+              let e2'' = e2'.Force()

+              match e1'', e2'' with

               | BoolLiteral(false), _            -> BoolLiteral(true)

               | _, BoolLiteral(true)             -> BoolLiteral(true)

               | BoolLiteral(b1), BoolLiteral(b2) -> BoolLiteral((not b1) || b2)

@@ -692,16 +707,23 @@ let rec __EvalSym resolverFunc ctx expr =
       let rec __ExhaustVar v restV vDomain = 

         match vDomain with

         | vv :: restD -> 

-            let newCtx = (v,vv) :: ctx

-            let e = __EvalSym resolverFunc newCtx (ForallExpr(restV, e))

+            let ctx' = (v,vv) :: ctx

+            let e' = __EvalSym resolverFunc ctx' (ForallExpr(restV, e))

             let erest = __ExhaustVar v restV restD

-            __EvalSym resolverFunc ctx (BinaryAnd e erest)

+            (* __EvalSym resolverFunc ctx' *) 

+            BinaryAnd e' erest

         | [] -> BoolLiteral(true)

-      match vars with

-      | v :: restV -> 

-          let vDom = GetVarDomain resolverFunc ctx v e

-          __ExhaustVar v restV vDom

-      | [] -> __EvalSym resolverFunc ctx e

+      let rec __TraverseVars vars =

+        match vars with

+        | v :: restV -> 

+            try 

+              let vDom = GetVarDomain resolverFunc ctx v e

+              __ExhaustVar v restV vDom

+            with

+              | ex -> ForallExpr([v], __TraverseVars restV) 

+        | [] -> __EvalSym resolverFunc ctx e

+      (* --- function body starts here --- *)

+      __TraverseVars vars

 and GetVarDomain resolverFunc ctx var expr = 

   match expr with 

   | BinaryExpr(_, "==>", lhs, rhs) -> 

@@ -712,14 +734,14 @@ and GetVarDomain resolverFunc ctx var expr =
                                 match __EvalSym resolverFunc ctx rhs with

                                 | SetExpr(elist)

                                 | SequenceExpr(elist) -> elist |> List.append acc

-                                | _ -> failwith "illegal 'in' expression"

+                                | _ -> raise DomainNotInferred

                             | BinaryExpr(_, op, VarLiteral(vn),oth)

                             | BinaryExpr(_, op, oth, VarLiteral(vn)) when GetVarName var = vn && Set.ofList ["<"; "<="; ">"; ">="] |> Set.contains op -> 

-                                failwith "not supported yet"

-                            | _ -> []) []

+                                failwith "Not implemented yet"

+                            | _ -> raise DomainNotInferred) []

   | _ -> 

       Logger.WarnLine ("unknown pattern for a quantified expression; cannot infer domain of quantified variable \"" + (GetVarName var) + "\"")

-      []

+      raise DomainNotInferred

 

 let EvalSym resolverFunc expr = 

   __EvalSym resolverFunc [] expr 

diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index 495daba9..43536ceb 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -24,6 +24,14 @@ let rec PrintExpr ctx expr =
   | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id

   | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))

   | UnaryExpr(op,e) -> sprintf "%s%s" op (PrintExpr 90 e)

+  | BinaryExpr(strength,"in",lhs,BinaryExpr(_,"..",lo,hi)) ->

+      let needParens = strength <= ctx

+      let openParen = if needParens then "(" else ""

+      let closeParen = if needParens then ")" else ""

+      let loStr = PrintExpr strength lo

+      let hiStr = PrintExpr strength hi

+      let lhsStr = PrintExpr strength lhs

+      sprintf "%s%s <= %s && %s <= %s%s" openParen loStr lhsStr lhsStr hiStr closeParen

   | BinaryExpr(strength,op,e0,e1) ->

       let op =

         match op with

diff --git a/Jennisys/Jennisys.fs b/Jennisys/Jennisys.fs
index 72c50b44..6dd2d26a 100644
--- a/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys.fs
@@ -18,26 +18,30 @@ open TypeChecker
 open Analyzer
 
 let readAndProcess (filename: string) =
-    printfn "// Jennisys, Copyright (c) 2011, Microsoft."
-    // lex
-    let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
-    let lexbuf = LexBuffer<char>.FromTextReader(f)
-    lexbuf.EndPos <- { pos_bol = 0;
-                       pos_fname=if filename = null then "stdin" else filename; 
-                       pos_cnum=0;
-                       pos_lnum=1 }
-//    try
+  printfn "// Jennisys, Copyright (c) 2011, Microsoft."
+  // lex
+  let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
+  let lexbuf = LexBuffer<char>.FromTextReader(f)
+  lexbuf.EndPos <- { pos_bol = 0;
+                     pos_fname=if filename = null then "stdin" else filename; 
+                     pos_cnum=0;
+                     pos_lnum=1 }
+  
+  let sprog = 
+    try 
       // parse
-    let sprog = Parser.start Lexer.tokenize lexbuf
-    match TypeCheck sprog with
-    | None -> ()  // errors have already been reported
-    | Some(prog) ->
-        Analyze prog filename
-//    with
-//      | ex ->
-//          let pos = lexbuf.EndPos
-//          printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
-//          printfn "%O" ex.StackTrace
+      Parser.start Lexer.tokenize lexbuf
+    with
+    | ex ->
+        let pos = lexbuf.EndPos
+        printfn "  [PARSE ERROR]: %s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
+        Environment.Exit(1)
+        failwith ""
+  match TypeCheck sprog with
+  | None -> ()  // errors have already been reported
+  | Some(prog) ->
+      Analyze prog filename
+  
 
 try 
   let args = Environment.GetCommandLineArgs()
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index fbeba9a5..79c273eb 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

     <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>

-    <StartArguments>examples/Set.jen /method:SetNode.Double /genRepr  /genMod</StartArguments>

+    <StartArguments>examples/List3.jen /method:IntList.OneTwo /genRepr  /genMod</StartArguments>

     <StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

diff --git a/Jennisys/Lexer.fsl b/Jennisys/Lexer.fsl
index 9eaf7421..d1b8ad91 100644
--- a/Jennisys/Lexer.fsl
+++ b/Jennisys/Lexer.fsl
@@ -39,6 +39,7 @@ rule tokenize = parse
 | "set"          { SETTYPE }

 // Operators

 | "."      { DOT }

+| ".."     { DOTDOT }

 | "+"      { PLUS }

 | "-"      { MINUS }

 | "*"      { STAR }

diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy
index c683e84c..e854d749 100644
--- a/Jennisys/Parser.fsy
+++ b/Jennisys/Parser.fsy
@@ -21,6 +21,7 @@ let rec MyFold ee acc =
 %token NOT

 %token STAR DIV MOD

 %token PLUS MINUS

+%token DOTDOT

 %token EQ NEQ LESS ATMOST ATLEAST GREATER IN NOTIN

 %token AND OR

 %token IMPLIES

@@ -141,16 +142,16 @@ Expr25:
     | Expr30                { $1 }

     | Expr30 QMARK Expr25 COLON Expr25 { IteExpr($1,$3,$5) }

 Expr30:

-    | Expr40               { $1 }

-    | Expr40 AND Expr30and { BinaryAnd $1 $3 }

-    | Expr40 OR Expr30or   { BinaryOr  $1 $3 }

+    | Expr40                { $1 }

+    | Expr40 AND Expr30and  { BinaryAnd $1 $3 }

+    | Expr40 OR Expr30or    { BinaryOr  $1 $3 }

 Expr30and:

-    | Expr40               { $1 }

-    | Expr40 AND Expr30and { BinaryAnd $1 $3 }

+    | Expr40                { $1 }

+    | Expr40 AND Expr30and  { BinaryAnd $1 $3 }

 Expr30or:

-    | Expr40               { $1 }

-    | Expr40 AND Expr30or  { BinaryOr $1 $3 }

-

+    | Expr40                { $1 }

+    | Expr40 AND Expr30or   { BinaryOr $1 $3 }

+                                           

 Expr40:

     | Expr50                { $1 }

     | Expr50 EQ Expr50      { BinaryExpr(40,"=",$1,$3) }

@@ -161,11 +162,15 @@ Expr40:
     | Expr50 GREATER Expr50 { BinaryExpr(40,">",$1,$3) }

     | Expr50 IN Expr50      { BinaryExpr(40,"in",$1,$3) }

     | Expr50 NOTIN Expr50   { BinaryExpr(40,"!in",$1,$3) }

-

+    

 Expr50:

+    | Expr55                { $1 }

+    | Expr55 DOTDOT Expr55  { BinaryExpr(50,"..",$1,$3) }

+

+Expr55:

     | Expr60               { $1 }

-    | Expr50 PLUS Expr60   { BinaryExpr(50,"+",$1,$3) }

-    | Expr50 MINUS Expr60  { BinaryExpr(50,"-",$1,$3) }

+    | Expr55 PLUS Expr60   { BinaryExpr(55,"+",$1,$3) }

+    | Expr55 MINUS Expr60  { BinaryExpr(55,"-",$1,$3) }

 

 Expr60:

     | Expr90              { $1 }

diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index d863cc7b..f4d31ccd 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -81,33 +81,38 @@ let Resolve hModel cst =
 //  ==================================================================

 /// Evaluates a given expression with respect to a given heap instance       

 //  ==================================================================

-let Eval heapInst resolveVars expr = 

-  let rec __EvalResolver expr = 

-    match expr with

-    | VarLiteral(id) when not resolveVars -> expr

-    | ObjLiteral("this") | ObjLiteral("null") -> expr

-    | IdLiteral("this")  | IdLiteral("null") -> failwith "should never happen anymore" //TODO

-    | VarLiteral(id) -> 

-        let argValue = heapInst.methodArgs |> Map.tryFind id |> Utils.ExtractOptionMsg ("cannot find value for method parameter " + id)

-        argValue |> Const2Expr

-    | IdLiteral(id) ->

-        let globalVal = heapInst.globals |> Map.tryFind id

-        match globalVal with

-        | Some(e) -> e

-        | None -> __EvalResolver (Dot(ObjLiteral("this"), id))

-    | Dot(e, str) -> 

-        let discr = __EvalResolver e

-        match discr with

-        | ObjLiteral(objName) -> 

-            let h2 = heapInst.assignments |> List.filter (fun ((o, Var(fldName,_)), v) -> o.name = objName && fldName = str)

-            match h2 with

-            | ((_,_),x) :: [] -> x

-            | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName str))

-            | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName str))  // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model???

-        | _ -> raise (EvalFailed(sprintf "Dot expression discriminator does not resolve to an object literal but %O" discr))

-    | _ -> failwith ("NOT IMPLEMENTED YET: " + (PrintExpr 0 expr))

+let Eval heapInst resolveExprFunc expr = 

+  let rec __EvalResolver expr fldNameOpt = 

+    if not (resolveExprFunc expr) then

+      match fldNameOpt with

+      | None -> expr

+      | Some(n) -> Dot(expr, n)

+    else

+      match fldNameOpt with

+      | None -> 

+          match expr with

+          | ObjLiteral("this") | ObjLiteral("null") -> expr

+          | IdLiteral("this")  | IdLiteral("null") -> failwith "should never happen anymore" //TODO

+          | VarLiteral(id) -> 

+              let argValue = heapInst.methodArgs |> Map.tryFind id |> Utils.ExtractOptionMsg ("cannot find value for method parameter " + id)

+              argValue |> Const2Expr

+          | IdLiteral(id) ->

+              let globalVal = heapInst.globals |> Map.tryFind id

+              match globalVal with

+              | Some(e) -> e

+              | None -> __EvalResolver ThisLiteral (Some(id))      

+          | _ -> raise (EvalFailed(sprintf "I'm not supposed to resolve %O" expr))

+      | Some(fldName) -> 

+          match expr with

+          | ObjLiteral(objName) -> 

+              let h2 = heapInst.assignments |> List.filter (fun ((o, Var(varName,_)), v) -> o.name = objName && varName = fldName)

+              match h2 with

+              | ((_,_),x) :: [] -> x

+              | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName fldName))

+              | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName fldName))  // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model???

+          | _ -> Dot(expr, fldName)

   (* --- function body starts here --- *)

-  EvalSym (fun e -> __EvalResolver e) expr

+  EvalSym __EvalResolver expr

 

 //  =====================================================================

 /// Takes an unresolved model of the heap (HeapModel), resolves all 

diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen
index d01300bb..f9828741 100644
--- a/Jennisys/examples/List3.jen
+++ b/Jennisys/examples/List3.jen
@@ -33,7 +33,7 @@ model IntList {
     root = null  ==> |list| = 0
     root != null ==> (|list| = |root.succ| + 1 && 
                       list[0] = root.data && 
-                      (forall i:int :: (0 < i && i <= |root.succ|) ==> (root.succ[i-1] != null && list[i] = root.succ[i-1].data)))
+                      (forall i :: i in 1 .. |root.succ| ==> (root.succ[i-1] != null && list[i] = root.succ[i-1].data)))
 }
 
 class IntNode {
diff --git a/Jennisys/examples/Number.jen b/Jennisys/examples/Number.jen
index 3d37e6a4..be33a00e 100644
--- a/Jennisys/examples/Number.jen
+++ b/Jennisys/examples/Number.jen
@@ -36,6 +36,7 @@ class Number {
 
   constructor Abs(a: int)  
     ensures num in {a (-a)} && num >= 0
+
 }
 
 model Number {