diff options
Diffstat (limited to 'Source/Dafny/Compiler.ssc')
| -rw-r--r-- | Source/Dafny/Compiler.ssc | 94 |
1 files changed, 82 insertions, 12 deletions
diff --git a/Source/Dafny/Compiler.ssc b/Source/Dafny/Compiler.ssc index 155927c4..c7dc73eb 100644 --- a/Source/Dafny/Compiler.ssc +++ b/Source/Dafny/Compiler.ssc @@ -386,6 +386,9 @@ namespace Microsoft.Dafny { return "BigInteger";
} else if (type is ObjectType) {
return "object";
+ } else if (type.IsArrayType) {
+ Type elType = UserDefinedType.ArrayElementType(type);
+ return TypeName(elType) + "[]";
} else if (type is UserDefinedType) {
UserDefinedType udt = (UserDefinedType)type;
string s = udt.Name;
@@ -507,13 +510,54 @@ namespace Microsoft.Dafny { wr.WriteLine("return;");
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
- Indent(indent);
- TrExpr(s.Lhs);
- if (!(s.Rhs is HavocRhs)) {
- wr.Write(" = ");
- TrAssignmentRhs(s.Rhs);
+ if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {
+ SeqSelectExpr sel = (SeqSelectExpr)s.Lhs;
+ // Generate the following:
+ // tmpArr = sel.Seq;
+ // tmpLow = sel.E0; // or 0 if sel.E0==null
+ // tmpHigh = sel.Eq; // or arr.Length if sel.E1==null
+ // tmpRhs = s.Rhs;
+ // for (int tmpI = tmpLow; tmpI < tmpHigh; tmpI++) {
+ // tmpArr[tmpI] = tmpRhs;
+ // }
+ string arr = "_arr" + tmpVarCount;
+ string low = "_low" + tmpVarCount;
+ string high = "_high" + tmpVarCount;
+ string rhs = "_rhs" + tmpVarCount;
+ string i = "_i" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent); wr.Write("{0} {1} = ", TypeName((!)sel.Seq.Type), arr); TrExpr(sel.Seq); wr.WriteLine(";");
+ Indent(indent); wr.Write("int {0} = ", low);
+ if (sel.E0 == null) {
+ wr.Write("0");
+ } else {
+ TrExpr(sel.E0);
+ }
+ wr.WriteLine(";");
+ Indent(indent); wr.Write("int {0} = ", high);
+ if (sel.E1 == null) {
+ wr.Write("new BigInteger(arr.Length)");
+ } else {
+ TrExpr(sel.E1);
+ }
+ wr.WriteLine(";");
+ Indent(indent); wr.Write("{0} {1} = ", TypeName((!)sel.Type), rhs); TrAssignmentRhs(s.Rhs); wr.WriteLine(";");
+ Indent(indent);
+ wr.WriteLine("for (BigInteger {0} = {1}; {0} < {2}; {0}++) {{", i, low, high);
+ Indent(indent + IndentAmount);
+ wr.WriteLine("{0}[(int)({1})] = {2};", arr, i, rhs);
+ Indent(indent);
+ wr.WriteLine(";");
+
+ } else {
+ Indent(indent);
+ TrExpr(s.Lhs);
+ if (!(s.Rhs is HavocRhs)) {
+ wr.Write(" = ");
+ TrAssignmentRhs(s.Rhs);
+ }
+ wr.WriteLine(";");
}
- wr.WriteLine(";");
} else if (stmt is VarDecl) {
TrVarDecl((VarDecl)stmt, true, indent);
@@ -686,7 +730,21 @@ namespace Microsoft.Dafny { } else {
TypeRhs tp = (TypeRhs)rhs;
- wr.Write("new {0}()", TypeName(tp.Type));
+ if (tp.ArraySize == null) {
+ wr.Write("new {0}()", TypeName(tp.EType));
+ } else {
+ 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.
+ wr.Write("Dafny.Helpers.InitNewArray<{0}>(", TypeName(tp.EType));
+ TrExpr(tp.ArraySize);
+ wr.Write(")");
+ } else {
+ wr.Write("new {0}[(int)", TypeName(tp.EType));
+ TrExpr(tp.ArraySize);
+ wr.Write("]");
+ }
+ }
}
}
@@ -827,9 +885,15 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
TrParenExpr(e.Seq);
- if (e.SelectOne) {
- assert e.E0 != null;
- assert e.E1 == null;
+ assert e.Seq.Type != null;
+ if (e.Seq.Type.IsArrayType) {
+ assert e.SelectOne;
+ assert e.E0 != null && e.E1 == null;
+ wr.Write("[(int)");
+ TrParenExpr(e.E0);
+ wr.Write("]");
+ } else if (e.SelectOne) {
+ assert e.E0 != null && e.E1 == null;
TrParenExpr(".Select", e.E0);
} else {
if (e.E1 != null) {
@@ -902,8 +966,14 @@ namespace Microsoft.Dafny { TrParenExpr(e.E);
break;
case UnaryExpr.Opcode.SeqLength:
- TrParenExpr(e.E);
- wr.Write(".Length");
+ if (((!)e.E.Type).IsArrayType) {
+ wr.Write("new BigInteger(");
+ TrParenExpr(e.E);
+ wr.Write(".Length)");
+ } else {
+ TrParenExpr(e.E);
+ wr.Write(".Length");
+ }
break;
default:
assert false; // unexpected unary expression
|