Dafny: Compilation of multi-dimensional arrays

2 files changed, 103 insertions, 5 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 6115f026..648be451 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -61,6 +61,7 @@ namespace Microsoft.Dafny {
       wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);

       wr.WriteLine();

       ReadRuntimeSystem();

+      CompileBuiltIns(program.BuiltIns);

 

       foreach (ModuleDecl m in program.Modules) {

         int indent = 0;

@@ -98,6 +99,82 @@ namespace Microsoft.Dafny {
       }

     }

 

+    void CompileBuiltIns(BuiltIns builtIns) {

+      wr.WriteLine("namespace Dafny {");

+      Indent(IndentAmount);

+      wr.WriteLine("public class Helpers {");

+      foreach (var decl in builtIns.SystemModule.TopLevelDecls) {

+        if (decl is ArrayClassDecl) {

+          int dims = ((ArrayClassDecl)decl).Dims;

+          // public static T[,] InitNewArray2<T>(BigInteger size0, BigInteger size1) {

+          Indent(3 * IndentAmount);

+          wr.Write("public static T[");

+          RepeatWrite(wr, dims, "", ",");

+          wr.Write("] InitNewArray{0}<T>(", dims);

+          RepeatWrite(wr, dims, "BigInteger size{0}", ", ");

+          wr.WriteLine(") {");

+          // int s0 = (int)size0;

+          for (int i = 0; i < dims; i++) {

+            Indent(4 * IndentAmount);

+            wr.WriteLine("int s{0} = (int)size{0};", i);

+          }

+          // T[,] a = new T[s0, s1];

+          Indent(4 * IndentAmount);

+          wr.Write("T[");

+          RepeatWrite(wr, dims, "", ",");

+          wr.Write("] a = new T[");

+          RepeatWrite(wr, dims, "s{0}", ",");

+          wr.WriteLine("];");

+          // BigInteger[,] b = a as BigInteger[,];

+          Indent(4 * IndentAmount);

+          wr.Write("BigInteger[");

+          RepeatWrite(wr, dims, "", ",");

+          wr.Write("] b = a as BigInteger[");

+          RepeatWrite(wr, dims, "", ",");

+          wr.WriteLine("];");

+          // if (b != null) {

+          Indent(4 * IndentAmount);

+          wr.WriteLine("if (b != null) {");

+          // BigInteger z = new BigInteger(0);

+          Indent(5 * IndentAmount);

+          wr.WriteLine("BigInteger z = new BigInteger(0);");

+          // for (int i0 = 0; i0 < s0; i0++)

+          //   for (int i1 = 0; i1 < s1; i1++)

+          for (int i = 0; i < dims; i++) {

+            Indent((5+i) * IndentAmount);

+            wr.WriteLine("for (int i{0} = 0; i{0} < s{0}; i{0}++)", i);

+          }

+          // b[i0,i1] = z;

+          Indent((5+dims) * IndentAmount);

+          wr.Write("b[");

+          RepeatWrite(wr, dims, "i{0}", ",");

+          wr.WriteLine("] = z;");

+          // }

+          Indent(4 * IndentAmount);

+          wr.WriteLine("}");

+          // return a;

+          Indent(4 * IndentAmount);

+          wr.WriteLine("return a;");

+          // }

+          Indent(3 * IndentAmount);

+          wr.WriteLine("}");  // end of method

+        }

+      }

+      Indent(IndentAmount);

+      wr.WriteLine("}");  // end of class Helpers

+      wr.WriteLine("}");  // end of namespace

+    }

+

+    static void RepeatWrite(TextWriter wr, int times, string template, string separator) {

+      Contract.Requires(1 <= times);

+      string s = "";

+      for (int i = 0; i < times; i++) {

+        wr.Write(s);

+        wr.Write(template, i);

+        s = separator;

+      }

+    }

+

     void CompileDatatypeConstructors(DatatypeDecl dt, int indent)

     {Contract.Requires(dt != null);

       foreach (DatatypeCtor ctor in dt.Ctors) {

@@ -767,8 +844,7 @@ namespace Microsoft.Dafny {
           if (tp.EType is IntType || tp.EType.IsTypeParameter) {

             // Because the default constructor for BigInteger does not generate a valid BigInteger, we have

             // to excplicitly initialize the elements of an integer array.  This is all done in a helper routine.

-            Contract.Assume(tp.ArrayDimensions.Count == 1);  // TODO: multi-dimensional arrays

-            wr.Write("Dafny.Helpers.InitNewArray<{0}>(", TypeName(tp.EType));

+            wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType));

             string prefix = "(";

             foreach (Expression dim in tp.ArrayDimensions) {

               wr.Write(prefix);

@@ -931,8 +1007,20 @@ namespace Microsoft.Dafny {
       

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

-        TrParenExpr(e.Obj);

-        wr.Write(".{0}", e.FieldName);

+        SpecialField sf = e.Field as SpecialField;

+        if (sf != null) {

+          if (sf.Type is IntType) {

+            wr.Write("new BigInteger(");

+          }

+          TrParenExpr(e.Obj);

+          wr.Write(".{0}", sf.CompiledName);

+          if (sf.Type is IntType) {

+            wr.Write(")");

+          }

+        } else {

+          TrParenExpr(e.Obj);

+          wr.Write(".{0}", e.Field.Name);

+        }

         

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index f21a5b3e..27f5e3a5 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -58,7 +58,8 @@ namespace Microsoft.Dafny {
         ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);

         for (int d = 0; d < dims; d++) {

           string name = dims == 1 ? "Length" : "Length" + d;

-          Field len = new Field(Token.NoToken, name, false, false, Type.Int, null);

+          string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")";

+          Field len = new SpecialField(Token.NoToken, name, compiledName, false, false, Type.Int, null);

           len.EnclosingClass = arrayClass;  // resolve here

           arrayClass.Members.Add(len);

         }

@@ -791,6 +792,15 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class SpecialField : Field

+  {

+    public readonly string CompiledName;

+    public SpecialField(IToken tok, string name, string compiledName, bool isGhost, bool isMutable, Type type, Attributes attributes)

+      : base(tok, name, isGhost, isMutable, type, attributes) {

+      CompiledName = compiledName;

+    }

+  }

+

   public class CouplingInvariant : MemberDecl {

     public readonly Expression Expr;

     public readonly List<IToken/*!*/>/*!*/ Toks;