refactored the Analyzer code so that it generates a separate Dafny file for each

method to be synthesized.

5 files changed, 389 insertions, 365 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index d0597d5a..806a6ab5 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -1,188 +1,167 @@
-module Analyzer

-

-open Ast

-open AstUtils

-open Printer

-open TypeChecker

-

-let rec PrintType ty =

-  match ty with

-  | NamedType(id) -> printf "%s" id

-  | InstantiatedType(id,arg) -> printf "%s<" id ; PrintType arg ; printf ">"

-

-let rec PrintExpr ctx expr =

-  match expr with

-  | IntLiteral(n) -> printf "%O" n

-  | IdLiteral(id) -> printf "%s" id

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

-  | Dot(e,id) -> PrintExpr 100 e ; printf ".%s" id

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

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

-      let op =

-        match op with

-          | "=" -> "=="

-          | "div" -> "/"

-          | "mod" -> "%"

-          | _ -> op

-      let needParens = strength <= ctx

-      if needParens then printf "(" else ()

-      PrintExpr strength e0 ; printf " %s " op ; PrintExpr strength e1

-      if needParens then printf ")" else ()

-  | SelectExpr(e,i) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf "]"

-  | UpdateExpr(e,i,v) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf " := " ; PrintExpr 0 v ; printf "]"

-  | SequenceExpr(ee) -> printf "[" ; ee |> PrintSep ", " (PrintExpr 0) ; printf "]"

-  | SeqLength(e) -> printf "|" ; PrintExpr 0 e ; printf "|"

-  | ForallExpr(vv,e) ->

-      let needParens = true

-      if needParens then printf "(" else ()

-      printf "forall " ; vv |> PrintSep ", " PrintVarDecl ; printf " :: " ; PrintExpr 0 e

-      if needParens then printf ")" else ()

-

-let VarsAreDifferent aa bb =

-  printf "false"

-  List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb

-

-let Fields members =

-  members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)

-

-let Rename suffix vars =

-  vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))

-

-let ReplaceName substMap nm =

-  match Map.tryFind nm substMap with

-    | Some(Var(name, tp)) -> name

-    | None -> nm

-

-let rec Substitute substMap = function

-  | IdLiteral(s) -> IdLiteral(ReplaceName substMap s)

-  | Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f)

-  | UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e)

-  | BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1)

-  | SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1)

-  | UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2)

-  | SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee)

-  | SeqLength(e) -> SeqLength(Substitute substMap e)

-  | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)

-  | expr -> expr

-

-let rec PrintStmt stmt indent =

-  match stmt with

-  | Block(stmts) ->

-      Indent indent ; printfn "{"

-      PrintStmtList stmts (indent + 2)

-      Indent indent ; printfn "}"

-  | Assign(lhs,rhs) -> Indent indent ; PrintExpr 0 lhs ; printf " := " ; PrintExpr 0 rhs ; printfn ";"

-and PrintStmtList stmts indent =

-  stmts |> List.iter (fun s -> PrintStmt s indent)

-

-let GenerateCode methodName signature pre post inv assumeInvInitially =

-  printfn "  method %s()" methodName

-  printfn "    modifies this;"

-  printfn "  {"

-  if assumeInvInitially then

-    // assume invariant

-    printfn "    assume Valid();"

-  else ()

-  // print signature as local variables

-  match signature with

-    | Sig(ins,outs) ->

-        List.concat [ins; outs] |> List.iter (fun vd -> printf "    var " ; PrintVarDecl vd ; printfn ";")

-  // assume preconditions

-  printfn "    // assume precondition"

-  printf "    assume " ; PrintExpr 0 pre ; printfn ";"

-  // assume invariant and postcondition

-  printfn "    // assume invariant and postcondition"

-  printfn "    assume Valid();"

-  printf "    assume " ; PrintExpr 0 post ; printfn ";"

-  // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible

-  printfn "    // assert false to search for a model satisfying the assumed constraints"

-  printfn "    assert false;"

-  printfn "  }"

-

-let GetFieldValidExpr name = 

-  BinaryImplies (BinaryNeq (IdLiteral(name)) (IdLiteral("null"))) (Dot(IdLiteral(name), "Valid()"))

-

-let GetFieldsForValidExpr (allFields: VarDecl list) prog =

-  allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true

-                                     | _                                   -> false)

-

-let GenFieldsValidExprList (allFields: VarDecl list) prog =

-  let fields = GetFieldsForValidExpr allFields prog

-  fields |> List.map (function Var(name, _) -> GetFieldValidExpr name)

-

-let AnalyzeComponent (prog: Program) c =

-  match c with

-  | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->

-      let aVars = Fields members

-      let allVars = List.concat [aVars ; cVars];

-      // Now print it as a Dafny program

-      printf "class %s" name

-      match typeParams with

-        | [] -> ()

-        | _ -> printf "<" ; typeParams |> PrintSep ", " (fun tp -> printf "%s" tp) ; printf ">"

-      printfn " {"

-      // the fields: original abstract fields plus two more copies thereof, plus and concrete fields

-      allVars |> List.iter (function Var(nm,None) -> printfn "  var %s;" nm | Var(nm,Some(tp)) -> printf "  var %s: " nm ; PrintType tp ; printfn ";")

-      printfn ""

-      // generate the Valid function

-      let invMembers = members |> List.filter (function Invariant(_) -> true | _ -> false)

-      let clsInvs = invMembers |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat

-      let allInvs = inv :: clsInvs

-      let fieldsValid = GenFieldsValidExprList allVars prog

-      printfn "  function Valid(): bool"

-      printfn "    reads *;"

-      printfn "  {"

-      let dummy = List.concat [fieldsValid ; allInvs] |> List.fold (fun acc (e: Expr) -> 

-                                                                      if acc = "" then

-                                                                        printf "    " ; PrintExpr 0 e ; "nonempty"

-                                                                      else

-                                                                        printfn " &&" ; printf "    " ; PrintExpr 0 e; "nonempty") ""

-      printfn ""

-      printfn "  }"; printfn ""

-

-      // generate constructors and methods

-      members |> List.iter (function

-        | Constructor(methodName,signature,pre,post) -> GenerateCode methodName signature pre post inv false ; printfn ""

-        | Method(methodName,signature,pre,post)      -> GenerateCode methodName signature pre post inv true  ; printfn ""

-        | _ -> ())

-      // the end of the class

-      printfn "}" ; printfn ""

-  | _ -> assert false  // unexpected case

-

-let AnalyzeComponent_rustan c =

-  match c with

-  | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->

-      let aVars = Fields members

-      let aVars0 = Rename "0" aVars

-      let aVars1 = Rename "1" aVars

-      let allVars = List.concat [aVars; List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars]

-      let inv0 = Substitute (Map.ofList aVars0) inv

-      let inv1 = Substitute (Map.ofList aVars1) inv

-      // Now print it as a Dafny program

-      printf "class %s" name

-      match typeParams with

-        | [] -> ()

-        | _ -> printf "<" ; typeParams |> PrintSep ", " (fun tp -> printf "%s" tp) ; printf ">"

-      printfn " {"

-      // the fields: original abstract fields plus two more copies thereof, plus and concrete fields

-      allVars |> List.iter (function Var(nm,None) -> printfn "  var %s;" nm | Var(nm,Some(tp)) -> printf "  var %s: " nm ; PrintType tp ; printfn ";")

-      // the method

-      printfn "  method %s_checkInjective() {" name

-      printf "    assume " ; VarsAreDifferent aVars0 aVars1 ; printfn ";"

-      printf "    assume " ; PrintExpr 0 inv0 ; printfn ";"

-      printf "    assume " ; PrintExpr 0 inv1 ; printfn ";"

-      printfn "    assert false;" // {:msg "Two abstract states map to the same concrete state"}

-      printfn "  }"

-      // generate code

-      members |> List.iter (function

-        | Constructor(methodName,signature,pre,stmts) -> GenerateCode methodName signature pre stmts inv false

-        | Method(methodName,signature,pre,stmts) -> GenerateCode methodName signature pre stmts inv true

-        | _ -> ())

-      // the end of the class

-      printfn "}"

-  | _ -> assert false  // unexpected case

-

-let Analyze prog =

-  match prog with

-  | Program(components) ->

-      components |> List.iter (AnalyzeComponent prog)

+module Analyzer
+
+open Ast
+open AstUtils
+open Printer
+open DafnyPrinter
+open TypeChecker
+
+let VarsAreDifferent aa bb =
+  printf "false"
+  List.iter2 (fun (_,Var(a,_)) (_,Var(b,_)) -> printf " || %s != %s" a b) aa bb
+
+let Fields members =
+  members |> List.choose (function Field(vd) -> Some(vd) | _ -> None)
+
+let Methods prog = 
+  match prog with
+  | Program(components) ->
+      components |> List.fold (fun acc comp -> 
+        match comp with
+        | Component(Class(_,_,members), Model(_,_,_,_,_), _) -> List.concat [acc ; members]            
+        | _ -> acc) []
+
+let Rename suffix vars =
+  vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))
+
+let ReplaceName substMap nm =
+  match Map.tryFind nm substMap with
+    | Some(Var(name, tp)) -> name
+    | None -> nm
+
+let rec Substitute substMap = function
+  | IdLiteral(s) -> IdLiteral(ReplaceName substMap s)
+  | Dot(e,f) -> Dot(Substitute substMap e, ReplaceName substMap f)
+  | UnaryExpr(op,e) -> UnaryExpr(op, Substitute substMap e)
+  | BinaryExpr(n,op,e0,e1) -> BinaryExpr(n, op, Substitute substMap e0, Substitute substMap e1)
+  | SelectExpr(e0,e1) -> SelectExpr(Substitute substMap e0, Substitute substMap e1)
+  | UpdateExpr(e0,e1,e2) -> UpdateExpr(Substitute substMap e0, Substitute substMap e1, Substitute substMap e2)
+  | SequenceExpr(ee) -> SequenceExpr(List.map (Substitute substMap) ee)
+  | SeqLength(e) -> SeqLength(Substitute substMap e)
+  | ForallExpr(vv,e) -> ForallExpr(vv, Substitute substMap e)
+  | expr -> expr
+
+let GenerateMethodCode methodName signature pre post assumeInvInitially =
+  "  method " + methodName + "()" + newline +
+  "    modifies this;" + newline +
+  "  {" + newline + 
+  (if assumeInvInitially then "    assume Valid();" else "") +
+  // print signature as local variables
+  (match signature with
+    | Sig(ins,outs) ->
+        List.concat [ins; outs] |> List.fold (fun acc vd -> acc + (sprintf "    var %s;" (PrintVarDecl vd)) + newline) "") +
+  // assume preconditions
+  "    // assume precondition" + newline +
+  "    assume " + (PrintExpr 0 pre) + ";" + newline + 
+  // assume invariant and postcondition
+  "    // assume invariant and postcondition" + newline + 
+  "    assume Valid();" + newline +
+  "    assume " + (PrintExpr 0 post) + ";" + newline +
+  // if the following assert fails, the model hints at what code to generate; if the verification succeeds, an implementation would be infeasible
+  "    // assert false to search for a model satisfying the assumed constraints" + newline + 
+  "    assert false;" + newline + 
+  "  }" + newline                                      
+
+let GetFieldValidExpr (name: string) : Expr = 
+  BinaryImplies (BinaryNeq (IdLiteral(name)) (IdLiteral("null"))) (Dot(IdLiteral(name), "Valid()"))
+
+let GetFieldsForValidExpr (allFields: VarDecl list) prog : VarDecl list =
+  allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true
+                                     | _                                   -> false)
+
+let GetFieldsValidExprList (allFields: VarDecl list) prog : Expr list =
+  let fields = GetFieldsForValidExpr allFields prog
+  fields |> List.map (function Var(name, _) -> GetFieldValidExpr name)
+
+let GenValidFunctionCode clsMembers modelInv vars prog : string = 
+  let invMembers = clsMembers |> List.filter (function Invariant(_) -> true | _ -> false)
+  let clsInvs = invMembers |> List.choose (function Invariant(exprList) -> Some(exprList) | _ -> None) |> List.concat
+  let allInvs = modelInv :: clsInvs
+  let fieldsValid = GetFieldsValidExprList vars prog
+  let idt = "    "
+  let invsStr = List.concat [fieldsValid ; allInvs] |> List.fold (fun acc (e: Expr) -> 
+                                                                  if acc = "" then
+                                                                    sprintf "%s%s" idt (PrintExpr 0 e)
+                                                                  else
+                                                                    acc + " &&" + newline + sprintf "%s%s" idt (PrintExpr 0 e)) ""
+  "  function Valid(): bool" + newline +
+  "    reads *;" + newline +
+  "  {" + newline + 
+  invsStr + newline +
+  "  }" + newline
+
+let AnalyzeMethod prog mthd : string =
+  match prog with
+  | Program(components) -> components |> List.fold (fun acc comp -> 
+      match comp with  
+      | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
+        let aVars = Fields members
+        let allVars = List.concat [aVars ; cVars];
+        // Now print it as a Dafny program
+        acc + 
+        (sprintf "class %s%s {" name (PrintTypeParams typeParams)) + newline +       
+        // the fields: original abstract fields plus concrete fields
+        (sprintf "%s" (PrintFields allVars 2)) + newline +                           
+        // generate the Valid function
+        (sprintf "%s" (GenValidFunctionCode members inv allVars prog)) + newline +
+        // generate code for the given method
+        (if List.exists (fun a -> a = mthd) members then
+           match mthd with 
+           | Constructor(methodName,signature,pre,post) -> (GenerateMethodCode methodName signature pre post false) + newline
+           | Method(methodName,signature,pre,post)      -> (GenerateMethodCode methodName signature pre post true) + newline
+           | _ -> ""
+         else
+           "") +
+        // the end of the class
+        "}" + newline + newline
+      | _ -> assert false; "") ""
+
+let scratchFileName = "scratch.dfy"
+
+let Analyze prog =
+  let methods = Methods prog
+
+  // synthesize constructors
+  methods |> List.iter (fun m -> 
+    match m with
+    | Constructor(methodName,signature,pre,post) -> 
+        use file = System.IO.File.CreateText(scratchFileName)
+        let code = AnalyzeMethod prog m
+        printfn "printing code for method %s:\r\n%s" methodName code
+        printfn "-------------------------"
+        fprintf file "%s" code
+    | _ -> ())
+
+
+//let AnalyzeComponent_rustan c =
+//  match c with
+//  | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) ->
+//      let aVars = Fields members
+//      let aVars0 = Rename "0" aVars
+//      let aVars1 = Rename "1" aVars
+//      let allVars = List.concat [aVars; List.map (fun (a,b) -> b) aVars0; List.map (fun (a,b) -> b) aVars1; cVars]
+//      let inv0 = Substitute (Map.ofList aVars0) inv
+//      let inv1 = Substitute (Map.ofList aVars1) inv
+//      // Now print it as a Dafny program
+//      printf "class %s" name
+//      match typeParams with
+//        | [] -> ()
+//        | _  -> printf "<%s>"  (typeParams |> PrintSep ", " (fun tp -> tp))
+//      printfn " {"
+//      // the fields: original abstract fields plus two more copies thereof, plus and concrete fields
+//      allVars |> List.iter (function Var(nm,None) -> printfn "  var %s;" nm | Var(nm,Some(tp)) -> printfn "  var %s: %s;" nm (PrintType tp))
+//      // the method
+//      printfn "  method %s_checkInjective() {" name
+//      printf "    assume " ; (VarsAreDifferent aVars0 aVars1) ; printfn ";"
+//      printfn "    assume %s;" (PrintExpr 0 inv0)
+//      printfn "    assume %s;" (PrintExpr 0 inv1)
+//      printfn "    assert false;" // {:msg "Two abstract states map to the same concrete state"}
+//      printfn "  }"
+//      // generate code
+//      members |> List.iter (function
+//        | Constructor(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv false)
+//        | Method(methodName,signature,pre,stmts) -> printf "%s" (GenerateCode methodName signature pre stmts inv true)
+//        | _ -> ())
+//      // the end of the class
+//      printfn "}"
+//  | _ -> assert false  // unexpected case
\ No newline at end of file
diff --git a/Jennisys/Jennisys/DafnyPrinter.fs b/Jennisys/Jennisys/DafnyPrinter.fs
new file mode 100644
index 00000000..d5fa6086
--- /dev/null
+++ b/Jennisys/Jennisys/DafnyPrinter.fs
@@ -0,0 +1,47 @@
+module DafnyPrinter
+
+open Ast
+open Printer
+
+let rec PrintType ty =
+  match ty with
+  | NamedType(id) -> id
+  | InstantiatedType(id,arg) -> sprintf "%s<%s>" id (PrintType arg) 
+
+let rec PrintExpr ctx expr =
+  match expr with
+  | IntLiteral(n) -> sprintf "%O" n
+  | IdLiteral(id) -> id
+  | Star -> assert false; "" // I hope this won't happen
+  | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id
+  | 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
+  | 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)
+  | 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 PrintTypeParams typeParams = 
+  match typeParams with
+  | [] -> ""
+  | _ -> sprintf "<%s>" (typeParams |> PrintSep ", " (fun tp -> tp))
+
+let PrintFields vars indent = 
+  vars |> List.fold (fun acc v -> match v with 
+                                  | Var(nm,None)     -> acc + (sprintf "%svar %s;%s" (Indent indent) nm newline)
+                                  | Var(nm,Some(tp)) -> acc + (sprintf "%svar %s: %s;%s" (Indent indent) nm (PrintType tp) newline)) ""
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs
index 34e3b611..d58af665 100644
--- a/Jennisys/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys/Jennisys.fs
@@ -1,64 +1,64 @@
-// This project type requires the F# PowerPack at http://fsharppowerpack.codeplex.com/releases

-// Learn more about F# at http://fsharp.net

-// Original project template by Jomo Fisher based on work of Brian McNamara, Don Syme and Matt Valerio

-// This posting is provided "AS IS" with no warranties, and confers no rights.

-module Main

-

-open System

-open System.IO

-open Microsoft.FSharp.Text.Lexing

-

-open Ast

-open Lexer

-open Parser

-open Printer

-open TypeChecker

-open Analyzer

-

-let readAndProcess tracing analyzing (filename: string) =

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

-        try

-            // parse

-            let sprog = Parser.start Lexer.tokenize lexbuf

-            // print the given Jennisys program

-            if tracing then

-                printfn "---------- Given Jennisys program ----------"

-                Print sprog

-            else ()

-            match TypeCheck sprog with

-              | None -> ()  // errors have already been reported

-              | Some(prog) ->

-                  if analyzing then

-                    // output a Dafny program with the constraints to be solved

-                    Analyze prog

-                  else ()

-            // that's it

-            if tracing then printfn "----------" else ()

-        with

-        | ex ->

-            let pos = lexbuf.EndPos

-            printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message

-

-    with

-     | ex ->

-        printfn "Unhandled Exception: %s" ex.Message

-

-let rec start n (args: string []) tracing analyzing filename =

-  if n < args.Length then

-    let arg = args.[n]

-    if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else ()

-    let filename = if arg.StartsWith "/" then filename else arg

-    start (n+1) args (tracing || arg = "/trace") (analyzing && arg <> "/noAnalysis") filename

-  else

-    readAndProcess tracing analyzing filename

-

-let args = Environment.GetCommandLineArgs()

-start 1 args false true null

+// This project type requires the F# PowerPack at http://fsharppowerpack.codeplex.com/releases
+// Learn more about F# at http://fsharp.net
+// Original project template by Jomo Fisher based on work of Brian McNamara, Don Syme and Matt Valerio
+// This posting is provided "AS IS" with no warranties, and confers no rights.
+module Main
+
+open System
+open System.IO
+open Microsoft.FSharp.Text.Lexing
+
+open Ast
+open Lexer
+open Parser
+open Printer
+open TypeChecker
+open Analyzer
+
+let readAndProcess tracing analyzing (filename: string) =
+    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 }
+        try
+            // parse
+            let sprog = Parser.start Lexer.tokenize lexbuf
+            // print the given Jennisys program
+            if tracing then
+                printfn "---------- Given Jennisys program ----------"
+                printfn "%s" (Print sprog)
+            else ()
+            match TypeCheck sprog with
+              | None -> ()  // errors have already been reported
+              | Some(prog) ->
+                  if analyzing then
+                    // output a Dafny program with the constraints to be solved
+                    Analyze prog
+                  else ()
+            // that's it
+            if tracing then printfn "----------" else ()
+        with
+        | ex ->
+            let pos = lexbuf.EndPos
+            printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
+
+    with
+     | ex ->
+        printfn "Unhandled Exception: %s" ex.Message
+
+let rec start n (args: string []) tracing analyzing filename =
+  if n < args.Length then
+    let arg = args.[n]
+    if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else ()
+    let filename = if arg.StartsWith "/" then filename else arg
+    start (n+1) args (tracing || arg = "/trace") (analyzing && arg <> "/noAnalysis") filename
+  else
+    readAndProcess tracing analyzing filename
+
+let args = Environment.GetCommandLineArgs()
+start 1 args false true null
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 159ed923..68369571 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -59,6 +59,7 @@
       <OtherFlags>--unicode</OtherFlags>

     </FsLex>

     <Compile Include="Printer.fs" />

+    <Compile Include="DafnyPrinter.fs" />

     <Compile Include="TypeChecker.fs" />

     <Compile Include="Analyzer.fs" />

     <Compile Include="Jennisys.fs" />

diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index f8434de5..77e462f3 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -1,113 +1,110 @@
-module Printer

-

-open Ast

-

-let rec PrintSep sep f list =

-  match list with

-  | [] -> ()

-  | [a] -> f a

-  | a :: more -> f a ; printf "%s" sep ; PrintSep sep f more

-  

-let rec PrintType ty =

-  match ty with

-  | NamedType(id) -> printf "%s" id

-  | InstantiatedType(id,arg) -> printf "%s[" id ; PrintType arg ; printf "]"

-

-let PrintVarDecl vd =

-  match vd with

-  | Var(id,None) -> printf "%s" id

-  | Var(id,Some(ty)) -> printf "%s: " id ; PrintType ty

-

-let rec PrintExpr ctx expr =

-  match expr with

-  | IntLiteral(n) -> printf "%O" n

-  | IdLiteral(id) -> printf "%s" id

-  | Star -> printf "*"

-  | Dot(e,id) -> PrintExpr 100 e ; printf ".%s" id

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

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

-      let needParens = strength <= ctx

-      if needParens then printf "(" else ()

-      PrintExpr strength e0 ; printf " %s " op ; PrintExpr strength e1

-      if needParens then printf ")" else ()

-  | SelectExpr(e,i) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf "]"

-  | UpdateExpr(e,i,v) -> PrintExpr 100 e ; printf "[" ; PrintExpr 0 i ; printf " := " ; PrintExpr 0 v ; printf "]"

-  | SequenceExpr(ee) -> printf "[" ; ee |> PrintSep ", " (PrintExpr 0) ; printf "]"

-  | SeqLength(e) -> printf "|" ; PrintExpr 0 e ; printf "|"

-  | ForallExpr(vv,e) ->

-      let needParens = ctx <> 0

-      if needParens then printf "(" else ()

-      printf "forall " ; vv |> PrintSep ", " PrintVarDecl ; printf " :: " ; PrintExpr 0 e

-      if needParens then printf ")" else ()

-

-let PrintSig signature =

-  match signature with

-  | Sig(ins, outs) ->

-      printf "("

-      ins |> PrintSep ", " PrintVarDecl

-      printf ")"

-      if outs <> [] then

-        printf " returns ("

-        outs |> PrintSep ", " PrintVarDecl

-        printf ")"

-      else ()

-

-let rec ForeachConjunct f expr =

-  match expr with

-  | IdLiteral("true") -> ()

-  | BinaryExpr(_,"&&",e0,e1) -> ForeachConjunct f e0 ; ForeachConjunct f e1

-  | _ -> f expr

-

-let rec Indent i =

-  if i = 0 then () else printf " " ; Indent (i-1)

-

-let rec PrintStmt stmt indent =

-  match stmt with

-  | Block(stmts) ->

-      Indent indent ; printfn "{"

-      PrintStmtList stmts (indent + 2)

-      Indent indent ; printfn "}"

-  | Assign(lhs,rhs) -> Indent indent ; PrintExpr 0 lhs ; printf " := " ; PrintExpr 0 rhs ; printfn ""

-and PrintStmtList stmts indent =

-  stmts |> List.iter (fun s -> PrintStmt s indent)

-

-let PrintRoutine signature pre body =

-  PrintSig signature

-  printfn ""

-  pre |> ForeachConjunct (fun e -> printf "    requires " ; PrintExpr 0 e ; printfn "")

-  PrintExpr 0 body  //  PrintStmtList body 4

-

-let PrintMember m =

-  match m with

-  | Field(vd) -> printf "  var " ; PrintVarDecl vd ; printfn ""

-  | Constructor(id,signature,pre,body) -> printf "  constructor %s" id ; PrintRoutine signature pre body

-  | Method(id,signature,pre,body) -> printf "  method %s" id ; PrintRoutine signature pre body

-      

-let PrintTopLevelDeclHeader kind id typeParams =

-  printf "%s %s" kind id

-  match typeParams with

-    | [] -> ()

-    | _ -> printf "[" ; typeParams |> PrintSep ", " (fun tp -> printf "%s" tp) ; printf "]"

-  printfn " {"

-

-let PrintDecl d =

-  match d with

-  | Class(id,typeParams,members) ->

-      PrintTopLevelDeclHeader "class" id typeParams

-      List.iter PrintMember members

-      printfn "}"

-  | Model(id,typeParams,vars,frame,inv) ->

-      PrintTopLevelDeclHeader "model" id typeParams

-      vars |> List.iter (fun vd -> printf "  var " ; PrintVarDecl vd ; printfn "")

-      printfn "  frame"

-      frame |> List.iter (fun fr -> printf "    " ; PrintExpr 0 fr ; printfn "")

-      printfn "  invariant"

-      inv |> ForeachConjunct (fun e -> printf "    " ; PrintExpr 0 e ; printfn "")

-      printfn "}"

-  | Code(id,typeParams) ->

-      PrintTopLevelDeclHeader "code" id typeParams

-      printfn "}"

-

-let Print prog =

-  match prog with

-  | SProgram(decls) -> List.iter PrintDecl decls

+module Printer
+
+open Ast
+
+let newline = System.Environment.NewLine // "\r\n"
+
+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
+  | NamedType(id) -> id
+  | InstantiatedType(id,arg) -> sprintf "%s[%s]" id (PrintType arg)
+
+let PrintVarDecl vd =
+  match vd with
+  | Var(id,None) -> id
+  | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)
+
+let rec PrintExpr ctx expr =
+  match expr with
+  | IntLiteral(n)     -> sprintf "%O" n
+  | IdLiteral(id)     -> id
+  | Star              -> "*"
+  | Dot(e,id)         -> sprintf "%s.%s" (PrintExpr 100 e) id
+  | UnaryExpr(op,e)   -> sprintf "%s%s" op (PrintExpr 90 e)
+  | BinaryExpr(strength,op,e0,e1) ->
+      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
+  | 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)
+  | ForallExpr(vv,e)  ->
+      let needParens = ctx <> 0
+      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 PrintSig signature =
+  match signature with
+  | Sig(ins, outs) ->
+      let returnClause = 
+        if outs <> [] then sprintf " returns (%s)" (outs |> PrintSep ", " PrintVarDecl)
+        else ""
+      sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause
+
+let rec ForeachConjunct f expr =
+  match expr with
+  | IdLiteral("true") -> ""
+  | BinaryExpr(_,"&&",e0,e1) -> (ForeachConjunct f e0) + (ForeachConjunct f e1)
+  | _ -> f expr
+
+let rec Indent i =
+  if i = 0 then "" else " " + (Indent (i-1))
+
+let rec PrintStmt stmt indent =
+  let idt = (Indent indent)
+  match stmt with
+  | Block(stmts) ->
+      idt + "{" + newline +
+      (PrintStmtList stmts (indent + 2)) +
+      idt + "}" + newline
+  | Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline
+and PrintStmtList stmts indent =
+  stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""
+
+let PrintRoutine signature pre body =
+  let preStr = pre |> ForeachConjunct (fun e -> sprintf "    requires %s%s" (PrintExpr 0 e) newline)
+  sprintf "%s%s%s%s" (PrintSig signature) newline preStr (PrintExpr 0 body)  
+  
+let PrintMember m =
+  match m with
+  | Field(vd) -> sprintf "  var %s%s" (PrintVarDecl vd) newline 
+  | Constructor(id,signature,pre,body) -> sprintf "  constructor %s%s" id (PrintRoutine signature pre body)
+  | Method(id,signature,pre,body) -> sprintf "  method %s%s" id (PrintRoutine signature pre body)
+  | Invariant(_) -> ""  // invariants are handled separately
+      
+let PrintTopLevelDeclHeader kind id typeParams =
+  let typeParamStr = 
+    match typeParams with
+    | [] -> ""
+    | _ -> sprintf "[%s]" (typeParams |> PrintSep ", " (fun tp -> tp))
+  sprintf "%s %s%s {%s" kind id typeParamStr newline
+  
+let PrintDecl d =
+  match d with
+  | Class(id,typeParams,members) ->
+      sprintf "%s%s}%s" (PrintTopLevelDeclHeader "class" id typeParams)
+                        (List.fold (fun acc m -> acc + (PrintMember m)) "" members)
+                        newline
+  | Model(id,typeParams,vars,frame,inv) ->
+      (PrintTopLevelDeclHeader "model" id typeParams) + 
+      (vars |> List.fold (fun acc vd -> acc + "  var " + (PrintVarDecl vd) + newline) "") +
+      "  frame" + newline +
+      (frame |> List.fold (fun acc fr -> acc + "    " + (PrintExpr 0 fr) + newline) "") +
+      "  invariant" + newline + 
+      (inv |> ForeachConjunct (fun e -> "    " + (PrintExpr 0 e) + newline)) +
+      "}" + newline
+  | Code(id,typeParams) ->
+      (PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline
+
+let Print prog =
+  match prog with
+  | SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls