implementing datatypes

1 files changed, 24 insertions, 0 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 5a1f8dc5..722bc99e 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -139,6 +139,28 @@ 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");

+          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);

+        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])) {

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

         }

 

+        CreateDatatypeSelectors(program);

+

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

         if (oc != PipelineOutcome.ResolvedAndTypeChecked)

           return;