From bae256656129581b928b150e111573ce7571385d Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 3 Jun 2013 18:06:21 -0700
Subject: Did some refactoring of the Dafny drivers.

---
 Source/DafnyDriver/DafnyDriver.cs           | 47 ++---------------------------
 Source/DafnyExtension/DafnyExtension.csproj |  3 --
 2 files changed, 2 insertions(+), 48 deletions(-)

(limited to 'Source')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 2891ec2b..b959b561 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -161,7 +161,7 @@ namespace Microsoft.Dafny
       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
 
       errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
-      PipelineOutcome oc = ResolveAndTypecheck(program, bplFileName);
+      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName);
       switch (oc) {
         case PipelineOutcome.Done:
           return oc;
@@ -178,7 +178,7 @@ namespace Microsoft.Dafny
             fileNames.Add(bplFileName);
             Bpl.Program reparsedProgram = ExecutionEngine.ParseBoogieProgram(fileNames, true);
             if (reparsedProgram != null) {
-              ResolveAndTypecheck(reparsedProgram, bplFileName);
+              ExecutionEngine.ResolveAndTypecheck(reparsedProgram, bplFileName);
             }
           }
           return oc;
@@ -193,49 +193,6 @@ namespace Microsoft.Dafny
     }
 
 
-    // TODO(wuestholz): Use the definition in the Boogie driver.
-    /// <summary>
-    /// Resolves and type checks the given Boogie program.  Any errors are reported to the
-    /// console.  Returns:
-    ///  - Done if no errors occurred, and command line specified no resolution or no type checking.
-    ///  - ResolutionError if a resolution error occurred
-    ///  - TypeCheckingError if a type checking error occurred
-    ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded
-    /// </summary>
-    static PipelineOutcome ResolveAndTypecheck(Bpl.Program program, string bplFileName)
-    {
-      Contract.Requires(program != null);
-      Contract.Requires(bplFileName != null);
-      // ---------- Resolve ------------------------------------------------------------
-
-      if (CommandLineOptions.Clo.NoResolve) { return PipelineOutcome.Done; }
-
-      int errorCount = program.Resolve();
-      if (errorCount != 0) {
-        Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, bplFileName);
-        return PipelineOutcome.ResolutionError;
-      }
-
-      // ---------- Type check ------------------------------------------------------------
-
-      if (CommandLineOptions.Clo.NoTypecheck) { return PipelineOutcome.Done; }
-
-      errorCount = program.Typecheck();
-      if (errorCount != 0) {
-        Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);
-        return PipelineOutcome.TypeCheckingError;
-      }
-
-      if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)
-      {
-        // if PrintDesugaring option is engaged, print the file here, after resolution and type checking
-        ExecutionEngine.PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true, false);
-      }
-
-      return PipelineOutcome.ResolvedAndTypeChecked;
-    }
-
-
     /// <summary>
     /// Given a resolved and type checked Boogie program, infers invariants for the program
     /// and then attempts to verify it.  Returns:
diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 13045b13..eb50f698 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -206,9 +206,6 @@
       <SubType>Designer</SubType>
     </None>
   </ItemGroup>
-  <ItemGroup>
-    <WCFMetadata Include="Service References\" />
-  </ItemGroup>
   <PropertyGroup>
     <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">10.0</VisualStudioVersion>
     <VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>
-- 
cgit v1.2.3