moved the addition of selectors and testers to program.Resolve

1 files changed, 0 insertions, 33 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 8542ad01..5a1f8dc5 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -139,37 +139,6 @@ namespace Microsoft.Boogie {
       Dafny

     };

 

-    static void CreateDatatypeSelectors(Program program) {

-      List<Function> constructors = new List<Function>();

-      foreach (Declaration decl in program.TopLevelDeclarations) {

-        if (decl is Function && QKeyValue.FindBoolAttribute(decl.Attributes, "constructor"))

-          constructors.Add((Function)decl);

-      }

-

-      foreach (Function f in constructors) {

-        foreach (Variable v in f.InParams) {

-          Formal inVar = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

-          Formal outVar = new Formal(Token.NoToken, v.TypedIdent, false);

-          Function selector = new Function(f.tok, v.Name + "#" + f.Name, new VariableSeq(inVar), outVar);

-          selector.AddAttribute("selector");

-          for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

-            if (kv.Key == "constructor") continue;

-            selector.AddAttribute(kv.Key, kv.Params.ToArray());

-          }

-          program.TopLevelDeclarations.Add(selector);

-        }

-        Formal inv = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

-        Formal outv = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false);

-        Function isConstructor = new Function(f.tok, "is#" + f.Name, new VariableSeq(inv), outv);

-        for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

-          if (kv.Key == "constructor") continue;

-          isConstructor.AddAttribute(kv.Key, kv.Params.ToArray());

-        } 

-        isConstructor.AddAttribute("membership");

-        program.TopLevelDeclarations.Add(isConstructor);

-      }

-    }

-

     static void ProcessFiles(List<string> fileNames) {

       Contract.Requires(cce.NonNullElements(fileNames));

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) {

@@ -181,8 +150,6 @@ namespace Microsoft.Boogie {
           PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);

         }

 

-        CreateDatatypeSelectors(program);

-

         PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);

         if (oc != PipelineOutcome.ResolvedAndTypeChecked)

           return;