From 6eb7df44c4445a9f8ebd3ca1bef6aeb9923e74b8 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 3 Jun 2013 16:40:20 -0700
Subject: Did some refactoring of the Dafny drivers.

---
 Source/DafnyDriver/DafnyDriver.cs     | 18 ++++++------------
 Source/DafnyDriver/DafnyDriver.csproj |  3 +++
 2 files changed, 9 insertions(+), 12 deletions(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 4358eab9..8b587a86 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -11,18 +11,13 @@
 namespace Microsoft.Dafny
 {
   using System;
-  using System.IO;
-  using System.Collections;
+  using System.CodeDom.Compiler;
   using System.Collections.Generic;
   using System.Diagnostics.Contracts;
-  using PureCollections;
+  using System.IO;
   using Microsoft.Boogie;
-  using Bpl = Microsoft.Boogie;
-  using Microsoft.Boogie.AbstractInterpretation;
-  using System.Diagnostics;
   using VC;
-  using System.CodeDom.Compiler;
-  using Core;
+  using Bpl = Microsoft.Boogie;
 
   public class DafnyDriver
   {
@@ -113,7 +108,7 @@ namespace Microsoft.Dafny
           Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
           if (CommandLineOptions.Clo.PrintFile != null)
           {
-            PrintBplFile(CommandLineOptions.Clo.PrintFile, boogieProgram, false);
+            ExecutionEngine.PrintBplFile(CommandLineOptions.Clo.PrintFile, boogieProgram, false, false);
           }
 
           string bplFilename;
@@ -247,7 +242,7 @@ namespace Microsoft.Dafny
         case PipelineOutcome.ResolutionError:
         case PipelineOutcome.TypeCheckingError:
           {
-            PrintBplFile(bplFileName, program, false);
+            ExecutionEngine.PrintBplFile(bplFileName, program, false, false);
             Console.WriteLine();
             Console.WriteLine("*** Encountered internal translation error - re-running Boogie to get better debug information");
             Console.WriteLine();
@@ -307,7 +302,7 @@ namespace Microsoft.Dafny
       if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)
       {
         // if PrintDesugaring option is engaged, print the file here, after resolution and type checking
-        PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);
+        ExecutionEngine.PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true, false);
       }
 
       return PipelineOutcome.ResolvedAndTypeChecked;
@@ -418,7 +413,6 @@ namespace Microsoft.Dafny
 
       if (CommandLineOptions.Clo.ExpandLambdas) {
         LambdaHelper.ExpandLambdas(program);
-        //PrintBplFile ("-", program, true);
       }
 
       // ---------- Verify ------------------------------------------------------------
diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index 61ca8593..95d2b7bb 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -130,6 +130,9 @@
     <Reference Include="Core">
       <HintPath>..\..\..\boogie\Binaries\Core.dll</HintPath>
     </Reference>
+    <Reference Include="ExecutionEngine">
+      <HintPath>..\..\..\boogie\Binaries\ExecutionEngine.dll</HintPath>
+    </Reference>
     <Reference Include="Provers.SMTLib">
       <HintPath>..\..\..\boogie\Binaries\Provers.SMTLib.dll</HintPath>
     </Reference>
-- 
cgit v1.2.3