Jennisys:

  - implemented an initial version of modular code synthesis (where the
    initialization code is delegated to receiver objects instead of
    modifying their private stuff directly).  For now, it just generates
    stub methods with appropriate specification.  Another analysis can
    be called for such methods to synthesize their bodies.

7 files changed, 269 insertions, 120 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 0970a193..fffaa2bd 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -84,6 +84,7 @@ let rec IsArgsOnly args expr =
   | SequenceExpr(exprs) | SetExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true

   | SeqLength(e)                         -> IsArgsOnly args e

   | ForallExpr(vars,e)                   -> IsArgsOnly (List.concat [args; vars]) e

+  | MethodCall(rcv,_,aparams)            -> rcv :: aparams |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true

 

 let AddUnif indent e v unifMap =

   let idt = Indent indent

@@ -365,11 +366,14 @@ and TryInferConditionals indent prog comp m unifs heapInst =
   with

     ex -> raise ex

 

+let GetAllMethodsToAnalyze prog = 

+  FilterMembers prog FilterConstructorMembers

+

 let GetMethodsToAnalyze prog =

   let mOpt = Options.CONFIG.methodToSynth;

   if mOpt = "*" then

     (* all *)

-    FilterMembers prog FilterConstructorMembers   

+    GetAllMethodsToAnalyze prog

   elif mOpt = "paramsOnly" then

     (* only with parameters *)

     FilterMembers prog FilterConstructorMembersWithParams 

@@ -411,39 +415,121 @@ let rec AnalyzeMethods prog members =
       | _ -> AnalyzeMethods prog rest

   | [] -> Map.empty

 

+let GetModularBranch prog comp meth cond hInst = 

+  let rec __AddDirectChildren e acc = 

+    match e with

+    | ObjLiteral(_) when not (e = ThisLiteral || e = NullLiteral) -> acc |> Set.add e

+    | SequenceExpr(elist)

+    | SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc

+    | _ -> acc

+  let __GetDirectChildren = 

+    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 __IsAbstractField ty var = 

+    let builder = CascadingBuilder<_>(false)

+    let varName = GetVarName var

+    builder {

+      let! comp = FindComponent prog (GetTypeShortName ty)

+      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 __GetArgsUsed expr = 

+    let args = GetMethodArgs meth

+    let argSet = DescendExpr2 (fun e acc ->

+                                 match e with

+                                 | VarLiteral(vname) ->

+                                     match args |> List.tryFind (function Var(name,_) when vname = name -> true | _ -> false) with

+                                     | Some(var) -> acc |> Set.add var

+                                     | None -> acc

+                                 | _ -> acc

+                               ) expr Set.empty

+    argSet |> Set.toList

+  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 pre = TrueLiteral

+        let post = __GetSpecFor name

+        let ins = __GetArgsUsed (BinaryAnd pre post)

+        let sgn = Sig(ins, [])

+        let m = Method(mName, sgn, pre, post, true)

+        __GetDelegateMethods rest (acc |> Map.add obj m)

+    | _ :: rest -> failwith "internal error: expected to see only ObjLiterals"

+    | [] -> acc

+  let __FindObj objName = 

+    try 

+      hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst

+    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 initChildrenExprList = delegateMethods |> Map.toList

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

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

+                                                            let args = GetMethodArgs mthd |> List.map (fun (Var(name,_)) -> VarLiteral(name))

+                                                            let e = MethodCall(receiver, GetMethodName mthd, args)

+                                                            (key, e)

+                                                         )

+  let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)

+  let newProg = delegateMethods |> Map.fold (fun acc receiver mthd ->

+                                               let obj = __FindObj (PrintExpr 0 receiver)

+                                               let comp = FindComponent acc (GetTypeShortName obj.objType) |> Utils.ExtractOption

+                                               AddReplaceMethod acc comp mthd None |> fst

+                                            ) prog

+  newProg, { hInst with assignments = initChildrenExprList @ newAssgns }

+

 let GetModularSol prog sol = 

-  

-  sol

+  let comp = fst (fst sol)

+  let meth = snd (fst sol)

+  let rec __xxx prog lst = 

+    match lst with

+    | (cond, hInst) :: rest -> 

+        let newProg, newhInst = GetModularBranch prog comp meth cond hInst

+        let newProg, newRest = __xxx newProg rest

+        newProg, ((cond, newhInst) :: newRest)

+    | [] -> prog, []

+  let newProg, newSolutions = __xxx prog (snd sol)

+  let newComp = FindComponent newProg (GetComponentName comp) |> Utils.ExtractOption

+  newProg, ((newComp, meth), newSolutions)

 

 let Modularize prog solutions = 

-  let rec __Modularize sols acc = 

+  let rec __Modularize prog sols acc = 

     match sols with

     | sol :: rest -> 

-        let newSol = GetModularSol prog sol

+        let (newProg, newSol) = GetModularSol prog sol

         let newAcc = acc |> Map.add (fst newSol) (snd newSol)

-        __Modularize rest newAcc 

-    | [] -> acc

+        __Modularize newProg rest newAcc 

+    | [] -> (prog, acc)

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

-  __Modularize (Map.toList solutions) Map.empty 

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

 

 let Analyze prog filename =

   /// Prints given solutions to a file

-  let __PrintSolution outFileName solutions = 

+  let __PrintSolution prog outFileName solutions = 

     use file = System.IO.File.CreateText(outFileName)

     file.AutoFlush <- true  

-    let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze Options.CONFIG.genRepr

+    let synthCode = PrintImplCode prog solutions GetAllMethodsToAnalyze Options.CONFIG.genRepr

     fprintfn file "%s" synthCode

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

   let solutions = AnalyzeMethods prog (GetMethodsToAnalyze prog)

   let progName = System.IO.Path.GetFileNameWithoutExtension(filename)

   let outFlatSolFileName = dafnySynthFileNameTemplate.Replace("###", progName)

   Logger.InfoLine "Printing synthesized code"

-  __PrintSolution outFlatSolFileName solutions

+  __PrintSolution prog outFlatSolFileName solutions

   // try to modularize

-  let modularSolutions = Modularize prog solutions

+  let newProg, modularSolutions = Modularize prog solutions

   let outModSolFileName = dafnyModularSynthFileNameTemplate.Replace("###", progName)

   Logger.InfoLine "Printing modularized code"

-  __PrintSolution outModSolFileName modularSolutions

+  __PrintSolution newProg outModSolFileName modularSolutions

   ()

 

 //let AnalyzeComponent_rustan c =

diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index b9105254..ab3dc8bb 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -45,7 +45,7 @@ type Expr =
   | SeqLength of Expr

   | SetExpr of Expr list //TODO: maybe this should really be a set instead of a list

   | ForallExpr of VarDecl list * Expr

-

+  | MethodCall of (* receiver *) Expr * (* name *) string * (* actual parameters *) Expr list

 type Const = 

   | IntConst   of int

   | BoolConst  of bool

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 2c8c4440..5a8198d5 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -10,6 +10,9 @@ open Ast
 open Logger

 open Utils

 

+let ThisLiteral = ObjLiteral("this")

+let NullLiteral = ObjLiteral("null")

+

 let rec Rewrite rewriterFunc expr =

   let __RewriteOrRecurse e =

     match rewriterFunc e with

@@ -34,6 +37,7 @@ let rec Rewrite rewriterFunc expr =
   | 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)

+  | MethodCall(rcv,name,aparams)     -> MethodCall(__RewriteOrRecurse rcv, name, aparams |> List.map __RewriteOrRecurse)

 

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

 /// Substitutes all occurences of all IdLiterals having 

@@ -58,6 +62,10 @@ let Substitute e1 e2 expr =
                None) expr

 

 let rec DescendExpr visitorFunc composeFunc leafVal expr = 

+  let __Compose elist =

+    match elist with

+    | [] -> leafVal

+    | fs :: rest -> rest |> List.fold (fun acc e -> composeFunc (composeFunc acc (visitorFunc e)) (DescendExpr visitorFunc composeFunc leafVal e)) (visitorFunc fs)

   match expr with

   | IntLiteral(_)

   | BoolLiteral(_)                   

@@ -68,18 +76,18 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
   | Dot(e, _)

   | ForallExpr(_,e)

   | UnaryExpr(_,e)           

-  | SeqLength(e)                     -> composeFunc (visitorFunc e) (DescendExpr visitorFunc composeFunc leafVal e)

+  | SeqLength(e)                     -> __Compose (e :: [])

   | SelectExpr(e1, e2)

-  | BinaryExpr(_,_,e1,e2)            -> composeFunc (composeFunc (composeFunc (visitorFunc e1) (visitorFunc e2)) (DescendExpr visitorFunc composeFunc leafVal e1)) (DescendExpr visitorFunc composeFunc leafVal e2)

+  | BinaryExpr(_,_,e1,e2)            -> __Compose (e1 :: e2 :: [])

   | IteExpr(e1,e2,e3)                

-  | UpdateExpr(e1,e2,e3)             -> composeFunc (composeFunc (composeFunc (composeFunc (composeFunc (visitorFunc e1) (visitorFunc e2)) (visitorFunc e3)) (DescendExpr visitorFunc composeFunc leafVal e1)) (DescendExpr visitorFunc composeFunc leafVal e2)) (DescendExpr visitorFunc composeFunc leafVal e3)

+  | UpdateExpr(e1,e2,e3)             -> __Compose (e1 :: e2 :: e3 :: [])

+  | MethodCall(rcv,_,aparams)        -> __Compose (rcv :: aparams)

   | SequenceExpr(exs)                

-  | SetExpr(exs)                     -> match exs with

-                                        | [] -> leafVal

-                                        | fs :: rest -> rest |> List.fold (fun acc e -> composeFunc (composeFunc acc (visitorFunc e)) (DescendExpr visitorFunc composeFunc leafVal e)) (visitorFunc fs)

+  | SetExpr(exs)                     -> __Compose exs

               

 let rec DescendExpr2 visitorFunc expr acc = 

   let newAcc = acc |> visitorFunc expr

+  let __Pipe elist = elist |> List.fold (fun a e -> a |> DescendExpr2 visitorFunc e) newAcc

   match expr with

   | IntLiteral(_)

   | BoolLiteral(_)                   

@@ -90,13 +98,14 @@ let rec DescendExpr2 visitorFunc expr acc =
   | Dot(e, _)

   | ForallExpr(_,e)

   | UnaryExpr(_,e)           

-  | SeqLength(e)                     -> newAcc |> DescendExpr2 visitorFunc e

+  | SeqLength(e)                     -> __Pipe (e :: [])

   | SelectExpr(e1, e2)

-  | BinaryExpr(_,_,e1,e2)            -> newAcc |> DescendExpr2 visitorFunc e1 |> DescendExpr2 visitorFunc e2

+  | BinaryExpr(_,_,e1,e2)            -> __Pipe (e1 :: e2 :: [])

   | IteExpr(e1,e2,e3)

-  | UpdateExpr(e1,e2,e3)             -> newAcc |> DescendExpr2 visitorFunc e1 |> DescendExpr2 visitorFunc e2 |> DescendExpr2 visitorFunc e3

+  | UpdateExpr(e1,e2,e3)             -> __Pipe (e1 :: e2 :: e3 :: [])

+  | MethodCall(rcv,_,aparams)        -> __Pipe (rcv :: aparams)

   | SequenceExpr(exs)                

-  | SetExpr(exs)                     -> exs |> List.fold (fun a e -> a |> DescendExpr2 visitorFunc e) newAcc              

+  | SetExpr(exs)                     -> __Pipe exs

 

 let PrintGenSym name =

   sprintf "gensym%s" name

@@ -269,16 +278,22 @@ let FilterMembers prog filter =
         | Component(Class(_,_,members),_,_) -> List.concat [acc ; members |> filter |> List.choose (fun m -> Some(comp, m))]            

         | _ -> acc) []

 

+let GetAbstractFields comp = 

+  match comp with 

+  | Component(Class(_,_,members), _, _) -> FilterFieldMembers members

+  | _ -> failwithf "internal error: invalid component: %O" comp

+    

+let GetConcreteFields comp = 

+  match comp with 

+  | Component(_, Model(_,_,cVars,_,_), _) -> cVars

+  | _ -> failwithf "internal error: invalid component: %O" comp

+     

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

 /// Returns all fields of a component

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

 let GetAllFields comp = 

-  match comp with

-  | Component(Class(_,_,members), Model(_,_,cVars,_,_), _) ->

-      let aVars = FilterFieldMembers members

-      List.concat [aVars ; cVars]

-  | _ -> []

-

+  List.concat [GetAbstractFields comp; GetConcreteFields comp]

+  

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

 /// Returns a map (Type |--> Set<Var>) where all 

 /// the given fields are grouped by their type

@@ -374,6 +389,14 @@ let GetVarName var =
   | Var(name,_) -> name

 

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

+/// Returns component name

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

+let GetComponentName comp = 

+  match comp with

+  | Component(Class(name,_,_),_,_) -> name

+  | _ -> failwithf "invalid component %O" comp

+

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

 /// Returns all members of a component

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

 let GetMembers comp =

@@ -433,13 +456,24 @@ let GetFrameFields comp =
 

 ////////////////////////

 

-let AddPrecondition prog comp m e =

-  match prog, comp, m with

-  | Program(clist), Component(Class(cname, ctypeParams, members), model, code), Method(mn, sgn, pre, post, cstr) ->

-      let newMthd = Method(mn, sgn, BinaryAnd pre e, post, cstr)

-      let newCls = Class(cname, ctypeParams, Utils.ListReplace m newMthd members)

+let AddReplaceMethod prog comp newMthd oldMethod =

+  match prog, comp with

+  | Program(clist), Component(Class(cname, ctypeParams, members), model, code) ->

+      let newMembers = 

+        match oldMethod with

+        | None -> members @ [newMthd]

+        | Some(m) -> Utils.ListReplace m newMthd members

+      let newCls = Class(cname, ctypeParams, newMembers)

       let newComp = Component(newCls, model, code)

       let newProg = Program(Utils.ListReplace comp newComp clist)

+      newProg, newComp

+  | _ -> failwithf "Invalid component: %O" comp

+

+let AddPrecondition prog comp m e =

+  match m with

+  | Method(mn, sgn, pre, post, cstr) ->

+      let newMthd = Method(mn, sgn, BinaryAnd pre e, post, cstr)

+      let newProg, newComp = AddReplaceMethod prog comp newMthd (Some(m))

       newProg, newComp, newMthd

   | _ -> failwithf "Not a method: %O" m

 

@@ -495,6 +529,10 @@ let rec __EvalSym resolverFunc ctx expr =
   | SetExpr(elist) -> 

       let eset' = elist |> List.fold (fun acc e -> Set.add (__EvalSym resolverFunc ctx e) acc) Set.empty

       SetExpr(Set.toList eset')

+  | MethodCall(rcv,name,aparams) ->

+      let rcv' = __EvalSym resolverFunc ctx rcv

+      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 

       match lst', idx' with

@@ -702,7 +740,8 @@ let rec Desugar expr =
   | SelectExpr(_) 

   | SeqLength(_)           

   | UpdateExpr(_)     

-  | SetExpr(_)     

+  | SetExpr(_)

+  | MethodCall(_)     

   | SequenceExpr(_)        -> expr 

   // forall v :: v in {a1 a2 ... an} ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] 

   // forall v :: v in [a1 a2 ... an] ==> e  ~~~> e[v/a1] && e[v/a2] && ... && e[v/an] 

@@ -768,5 +807,6 @@ let ChangeThisReceiver receiver expr =
     | UpdateExpr(e1,e2,e3)             -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

     | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map (__ChangeThis locals))

     | SetExpr(exs)                     -> SetExpr(exs |> List.map (__ChangeThis locals))

+    | MethodCall(rcv,name,aparams)     -> MethodCall(__ChangeThis locals rcv, name, aparams |> List.map (__ChangeThis locals))

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

   __ChangeThis Set.empty expr

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 54c22053..5a1f108c 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -159,17 +159,22 @@ let PrintVarAssignments heapInst indent =
   let idt = Indent indent

   heapInst.assignments |> List.fold (fun acc ((o,f),e) ->

                                       let fldName = PrintVarName f

-                                      let value = PrintExpr 0 e

-                                      acc + (sprintf "%s%s.%s := %s;" idt o.name fldName value) + newline

+                                      let exprStr = 

+                                        if fldName = "" then

+                                          sprintf "%s;" (PrintExpr 0 e)

+                                        else

+                                          let value = PrintExpr 0 e

+                                          sprintf "%s.%s := %s;" o.name fldName value

+                                      acc + idt + exprStr + newline

                                     ) ""

 

 let PrintReprAssignments prog heapInst indent = 

   let __FollowsFunc o1 o2 = 

     heapInst.assignments |> List.fold (fun acc ((srcObj,fld),value) -> 

                                         acc || (srcObj = o1 && value = ObjLiteral(o2.name))

-                                     ) false

+                                      ) false

   let idt = Indent indent

-  let objs = heapInst.assignments |> List.fold (fun acc ((obj,fld),_) -> acc |> Set.add obj) Set.empty

+  let objs = heapInst.assignments |> List.fold (fun acc ((obj,(Var(fldName,_))),_) -> if fldName = "" then acc else acc |> Set.add obj) Set.empty

                                   |> Set.toList

                                   |> Utils.TopSort __FollowsFunc

                                   |> List.rev

@@ -224,18 +229,30 @@ let rec PrintHeapCreationCode prog sol indent genRepr =
           (__ReprAssignments indent)

   | [] -> ""

 

+let PrintPrePost pfix expr = 

+  SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")

+

+let GetPostconditionForMethod m genRepr = 

+  let validExpr = IdLiteral("Valid()");

+  match m with

+  | Method(_,_,_,post,_) ->

+      let postExpr = BinaryAnd validExpr post

+      if genRepr then

+        BinaryAnd (IdLiteral("fresh(Repr - {this})")) postExpr

+      else

+        postExpr

+  | _ -> failwithf "expected a method, got %O" m     

+      

 let GenConstructorCode mthd body genRepr =

   let validExpr = IdLiteral("Valid()");

   match mthd with

   | Method(methodName, sign, pre, post, _) -> 

-      let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")

       let preExpr = pre 

-      let postExpr = BinaryAnd validExpr post

+      let postExpr = GetPostconditionForMethod mthd genRepr

       "  method " + methodName + (PrintSig sign) + newline +

       "    modifies this;" + 

-      (__PrintPrePost (newline + "    requires ") preExpr) + 

-      Utils.Ite genRepr (newline + "    ensures fresh(Repr - {this});") "" +

-      (__PrintPrePost (newline + "    ensures ") postExpr) + 

+      (PrintPrePost (newline + "    requires ") preExpr) + 

+      (PrintPrePost (newline + "    ensures ") postExpr) + 

       newline +

       "  {" + newline + 

       body + 

@@ -249,7 +266,9 @@ let PrintImplCode prog solutions methodsToPrintFunc genRepr =
                                  if Utils.ListContains (comp,mthd) methods  then

                                    let mthdBody = match Map.tryFind (comp,mthd) solutions with

                                                   | Some(sol) -> PrintHeapCreationCode prog sol 4 genRepr

-                                                  | _ -> "    //unable to synthesize" + newline

+                                                  | _ -> 

+                                                      "    //unable to synthesize" +

+                                                      PrintPrePost (newline + "    assume ") (GetPostconditionForMethod mthd genRepr) + newline

                                    (GenConstructorCode mthd mthdBody genRepr) + newline

                                  else

                                    "") genRepr
\ No newline at end of file
diff --git a/Jennisys/Jennisys/DafnyPrinter.fs b/Jennisys/Jennisys/DafnyPrinter.fs
index 86974f20..495daba9 100644
--- a/Jennisys/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/Jennisys/DafnyPrinter.fs
@@ -1,76 +1,78 @@
-module DafnyPrinter
-
-open Ast
-open AstUtils
-open Printer
-
-let rec PrintType ty =
-  match ty with
-  | IntType                   -> "int"
-  | BoolType                  -> "bool"
-  | SeqType(t)                -> sprintf "seq<%s>" (PrintType t)
-  | SetType(t)                -> sprintf "set<%s>" (PrintType t)
-  | NamedType(id,args)        -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun s -> s) args)
-  | InstantiatedType(id,args) -> sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args)
-
-let rec PrintExpr ctx expr =
-  match expr with
-  | IntLiteral(d)     -> sprintf "%d" d
-  | BoolLiteral(b)    -> sprintf "%b" b
-  | ObjLiteral(id)
-  | VarLiteral(id)
-  | IdLiteral(id) -> id
-  | Star -> assert false; "" // I hope this won't happen
-  | 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,op,e0,e1) ->
-      let op =
-        match op with
-          | "=" -> "=="
-          | "div" -> "/"
-          | "mod" -> "%"
-          | _ -> op
-      let needParens = strength <= ctx
-      let openParen = if needParens then "(" else ""
-      let closeParen = if needParens then ")" else ""
-      sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen
-  | IteExpr(c,e1,e2)  -> sprintf "(if %s then %s else %s)" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)
-  | SelectExpr(e,i)   -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i)
-  | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)
-  | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0))
-  | SeqLength(e)      -> sprintf "|%s|" (PrintExpr 0 e)
-  | SetExpr(ee)       -> sprintf "{%s}" (ee |> PrintSep ", " (PrintExpr 0))
-  | ForallExpr(vv,e)  ->
-      let needParens = true
-      let openParen = if needParens then "(" else ""
-      let closeParen = if needParens then ")" else ""
-      sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
-
-let rec PrintConst cst = 
-  match cst with 
-  | IntConst(v)        -> sprintf "%d" v
-  | BoolConst(b)       -> sprintf "%b" b
-  | VarConst(v)        -> sprintf "%s" v
-  | SetConst(cset)     -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset))
-  | SeqConst(cseq)     -> sprintf "[%s]" (PrintSep ", " (fun c -> PrintConst c) cseq)
-  | NullConst          -> "null"
-  | NoneConst          -> "<none>"
-  | ThisConst(_,_)     -> "this"
-  | NewObj(name,_)     -> PrintGenSym name
-  | Unresolved(name)   -> sprintf "Unresolved(%s)" name
-
-let PrintTypeParams typeParams = 
-  match typeParams with
-  | [] -> ""
-  | _ -> sprintf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp))
-
-let PrintFields vars indent ghost = 
-  let ghostStr = if ghost then "ghost " else ""
-  vars |> List.fold (fun acc v -> match v with 
-                                  | Var(nm,None)     -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline)
-                                  | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""
-
+module DafnyPrinter

+

+open Ast

+open AstUtils

+open Printer

+

+let rec PrintType ty =

+  match ty with

+  | IntType                   -> "int"

+  | BoolType                  -> "bool"

+  | SeqType(t)                -> sprintf "seq<%s>" (PrintType t)

+  | SetType(t)                -> sprintf "set<%s>" (PrintType t)

+  | NamedType(id,args)        -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun s -> s) args)

+  | InstantiatedType(id,args) -> sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args)

+

+let rec PrintExpr ctx expr =

+  match expr with

+  | IntLiteral(d)     -> sprintf "%d" d

+  | BoolLiteral(b)    -> sprintf "%b" b

+  | ObjLiteral(id)

+  | VarLiteral(id)

+  | IdLiteral(id) -> id

+  | Star -> assert false; "" // I hope this won't happen

+  | 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,op,e0,e1) ->

+      let op =

+        match op with

+          | "=" -> "=="

+          | "div" -> "/"

+          | "mod" -> "%"

+          | _ -> op

+      let needParens = strength <= ctx

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

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

+      sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen

+  | IteExpr(c,e1,e2)  -> sprintf "(if %s then %s else %s)" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)

+  | SelectExpr(e,i)   -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i)

+  | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)

+  | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0))

+  | SeqLength(e)      -> sprintf "|%s|" (PrintExpr 0 e)

+  | SetExpr(ee)       -> sprintf "{%s}" (ee |> PrintSep ", " (PrintExpr 0))

+  | ForallExpr(vv,e)  ->

+      let needParens = true

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

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

+      sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen

+  | MethodCall(rcv, name, aparams) ->

+      sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))

+

+let rec PrintConst cst = 

+  match cst with 

+  | IntConst(v)        -> sprintf "%d" v

+  | BoolConst(b)       -> sprintf "%b" b

+  | VarConst(v)        -> sprintf "%s" v

+  | SetConst(cset)     -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset))

+  | SeqConst(cseq)     -> sprintf "[%s]" (PrintSep ", " (fun c -> PrintConst c) cseq)

+  | NullConst          -> "null"

+  | NoneConst          -> "<none>"

+  | ThisConst(_,_)     -> "this"

+  | NewObj(name,_)     -> PrintGenSym name

+  | Unresolved(name)   -> sprintf "Unresolved(%s)" name

+

+let PrintTypeParams typeParams = 

+  match typeParams with

+  | [] -> ""

+  | _ -> sprintf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp))

+

+let PrintFields vars indent ghost = 

+  let ghostStr = if ghost then "ghost " else ""

+  vars |> List.fold (fun acc v -> match v with 

+                                  | Var(nm,None)     -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline)

+                                  | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""

+

 let rec PrintStmt stmt indent =

   let idt = (Indent indent)

   match stmt with

diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 69ab0ff2..49696e58 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

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

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

+    <StartArguments>examples/List.jen /method:List.Double /genRepr</StartArguments>

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

   </PropertyGroup>

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

diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index f8f2933b..ca65f495 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -56,6 +56,8 @@ let rec PrintExpr ctx expr =
       let openParen = if needParens then "(" else ""

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

       sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen

+  | MethodCall(rcv,name,aparams) ->

+      sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))

 

 let rec PrintConst cst = 

   match cst with