made delegate a datatype

added a DatatypeConstructor class

4 files changed, 23 insertions, 10 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 500cb0ca..7ff0af6c 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -213,8 +213,8 @@ namespace Microsoft.Boogie {
       Emitter.Declarations(this.TopLevelDeclarations, stream);

     }

 

-    void CreateDatatypeSelectorsAndTesters() {

-      Dictionary<string, Function> constructors = new Dictionary<string, Function>();

+    public void ProcessDatatypeConstructors() {

+      Dictionary<string, DatatypeConstructor> constructors = new Dictionary<string, DatatypeConstructor>();

       List<Declaration> prunedTopLevelDeclarations = new List<Declaration>();

       foreach (Declaration decl in TopLevelDeclarations) {

         Function func = decl as Function;

@@ -223,17 +223,20 @@ namespace Microsoft.Boogie {
           continue;

         }

         if (constructors.ContainsKey(func.Name)) continue;

-        constructors.Add(func.Name, func);

-        prunedTopLevelDeclarations.Add(func);

+        DatatypeConstructor constructor = new DatatypeConstructor(func);

+        constructors.Add(func.Name, constructor);

+        prunedTopLevelDeclarations.Add(constructor);

       }

       TopLevelDeclarations = prunedTopLevelDeclarations;

-

-      foreach (Function f in constructors.Values) {

+    

+      foreach (DatatypeConstructor f in constructors.Values) {

         for (int i = 0; i < f.InParams.Length; i++) {

           DatatypeSelector selector = new DatatypeSelector(f, i);

+          f.selectors.Add(selector);

           TopLevelDeclarations.Add(selector);

         }

         DatatypeMembership membership = new DatatypeMembership(f);

+        f.membership = membership;

         TopLevelDeclarations.Add(membership);

       }

     }

@@ -256,8 +259,6 @@ namespace Microsoft.Boogie {
       //Contract.Requires(rc != null);

       Helpers.ExtraTraceInformation("Starting resolution");

 

-      CreateDatatypeSelectorsAndTesters();

-

       foreach (Declaration d in TopLevelDeclarations) {

         d.Register(rc);

       }

@@ -1791,6 +1792,17 @@ namespace Microsoft.Boogie {
     }

   }

 

+  public class DatatypeConstructor : Function {

+    public List<DatatypeSelector> selectors;

+    public DatatypeMembership membership;

+

+    public DatatypeConstructor(Function func) 

+    : base(func.tok, func.Name, func.TypeParameters, func.InParams, func.OutParams[0], func.Comment, func.Attributes)

+    {

+      selectors = new List<DatatypeSelector>();

+    }

+  }

+

   public class DatatypeSelector : Function {

     public Function constructor;

     public int index;

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 3602339e..fe77bcc1 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -85,6 +85,7 @@ Contract.Requires(cce.NonNullElements(defines,true));
     if (parser.errors.count == 0)

     {

       program = Pgm;

+      program.ProcessDatatypeConstructors();

       return 0;

     }

     else

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index dab0807f..e837b16f 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -841,7 +841,7 @@ namespace Microsoft.Boogie.SMTLib
     }

 

     public override void DeclareFunction(Function f, string attributes) {

-      if (QKeyValue.FindBoolAttribute(f.Attributes, "constructor")) {

+      if (f is DatatypeConstructor) {

         CtorType datatype = (CtorType) f.OutParams[0].TypedIdent.Type;

         if (!KnownDatatypeConstructors.ContainsKey(datatype))

           KnownDatatypeConstructors[datatype] = new List<Function>();

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 4a4ecfb6..40dc7cf6 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -266,7 +266,7 @@ void ObjectInvariant()
 

     public static bool IsDatatypeFunction(Function f) {

       return

-        QKeyValue.FindBoolAttribute(f.Attributes, "constructor") ||

+        f is DatatypeConstructor ||

         f is DatatypeSelector ||

         f is DatatypeMembership;

     }