- removed the "Constructor" discriminator from type Member, and added a

   boolean flag to the "Method" discriminator instead

 - added a new example called "List3.jen".  The difference between List2 is
   that the IntNode class has a "succ" field that returns a list of all
   successor nodes, instead of list of integers as in List2.  In this example,
   the invariant is very verbose because of the lack of better syntax, so
   maybe we can add some syntactic sugar to Jennisys (e.g. for transitive
   closure, comprehensions, etc.) and synthesize Dafny code from that.

 - reading from BVD models now also reads Seq#Append, because some lists are
   created only that way

1 files changed, 6 insertions, 6 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 30d4b85a..e3135cff 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -59,12 +59,12 @@ let MethodAnalysisPrinter onlyForThisCompMethod comp mthd =
   match onlyForThisCompMethod with
   | (c,m) when c = comp && m = mthd -> 
     match m with 
-    | Constructor(methodName, sign, pre, post) -> (GenMethodAnalysisCode methodName sign pre post false) + newline
+    | Method(methodName, sign, pre, post, true) -> (GenMethodAnalysisCode methodName sign pre post false) + newline
     | _ -> ""
   | _ -> ""
                            
 let AnalyzeConstructor prog comp methodName signature pre post =
-  let m = Constructor(methodName, signature, pre, post)
+  let m = Method(methodName, signature, pre, post, true)
   use file = System.IO.File.CreateText(dafnyScratchFile)
   file.AutoFlush <- true
   let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,m))
@@ -83,11 +83,11 @@ let AnalyzeConstructor prog comp methodName signature pre post =
     let model = models.[0]
     Some(ReadFieldValuesFromModel model prog comp m)
 
-let rec AnalyzeMethods prog methods = 
-  match methods with
+let rec AnalyzeMethods prog members = 
+  match members with
   | (comp,m) :: rest -> 
       match m with
-      | Constructor(methodName,signature,pre,post) -> 
+      | Method(methodName,signature,pre,post,true) -> 
           let solOpt = AnalyzeConstructor prog comp methodName signature pre post
           match solOpt with
           | Some(heap,env,ctx) -> AnalyzeMethods prog rest |> Map.add (comp,m) (heap,env,ctx)
@@ -96,7 +96,7 @@ let rec AnalyzeMethods prog methods =
   | [] -> Map.empty
 
 let Analyze prog =
-  let solutions = AnalyzeMethods prog (Methods prog)
+  let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)
   use file = System.IO.File.CreateText(dafnySynthFile)
   file.AutoFlush <- true
   let synthCode = PrintImplCode prog solutions