diff options
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 1606 |
1 files changed, 960 insertions, 646 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 570ac30d..66765b34 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -14,18 +14,11 @@ using System.Text; namespace Microsoft.Dafny {
public class Compiler {
- public Compiler(TextWriter wr) {
- Contract.Requires(wr != null);
- this.wr = wr;
+ public Compiler() {
+
}
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(wr!=null);
- }
-
- TextWriter wr;
+ StringBuilder copyInstrWriter = new StringBuilder(); // a buffer that stores copy instructions generated by letExpr that uses out param.
Method enclosingMethod; // non-null when a method body is being translated
FreshIdGenerator idGenerator = new FreshIdGenerator();
@@ -50,7 +43,7 @@ namespace Microsoft.Dafny { public int ErrorCount;
public TextWriter ErrorWriter = Console.Out;
- void Error(string msg, params object[] args) {
+ void Error(string msg, TextWriter wr, params object[] args) {
Contract.Requires(msg != null);
Contract.Requires(args != null);
@@ -60,7 +53,7 @@ namespace Microsoft.Dafny { ErrorCount++;
}
- void ReadRuntimeSystem() {
+ void ReadRuntimeSystem(TextWriter wr) {
string codebase = cce.NonNull( System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
string path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");
using (TextReader rd = new StreamReader(new FileStream(path, System.IO.FileMode.Open, System.IO.FileAccess.Read)))
@@ -75,16 +68,16 @@ namespace Microsoft.Dafny { }
readonly int IndentAmount = 2;
- void Indent(int ind) {
+ void Indent(int ind, TextWriter wr) {
Contract.Requires(0 <= ind);
string spaces = " ";
for (; spaces.Length < ind; ind -= spaces.Length) {
wr.Write(spaces);
}
- wr.Write(spaces.Substring(0, ind));
+ wr.Write(spaces.Substring(0, ind));
}
- public void Compile(Program program) {
+ public void Compile(Program program, TextWriter wr) {
Contract.Requires(program != null);
wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);
wr.WriteLine("// To recompile, use 'csc' with: /r:System.Numerics.dll");
@@ -92,8 +85,8 @@ namespace Microsoft.Dafny { wr.WriteLine("// You might also want to include compiler switches like:");
wr.WriteLine("// /debug /nowarn:0164 /nowarn:0219");
wr.WriteLine();
- ReadRuntimeSystem();
- CompileBuiltIns(program.BuiltIns);
+ ReadRuntimeSystem(wr);
+ CompileBuiltIns(program.BuiltIns, wr);
foreach (ModuleDefinition m in program.CompileModules) {
if (m.IsAbstract) {
@@ -102,7 +95,11 @@ namespace Microsoft.Dafny { }
int indent = 0;
if (!m.IsDefaultModule) {
- wr.WriteLine("namespace @{0} {{", m.CompileName);
+ var m_prime = m;
+ while (DafnyOptions.O.IronDafny && m_prime.ClonedFrom != null) {
+ m_prime = m.ClonedFrom;
+ }
+ wr.WriteLine("namespace @{0} {{", m_prime.CompileName);
indent += IndentAmount;
}
foreach (TopLevelDecl d in m.TopLevelDecls) {
@@ -113,21 +110,33 @@ namespace Microsoft.Dafny { wr.WriteLine();
if (d is OpaqueTypeDecl) {
var at = (OpaqueTypeDecl)d;
- Error("Opaque type ('{0}') cannot be compiled", at.FullName);
+ Error("Opaque type ('{0}') cannot be compiled", wr, at.FullName);
} else if (d is TypeSynonymDecl) {
// do nothing, just bypass type synonyms in the compiler
} else if (d is NewtypeDecl) {
- // do nothing, just bypass newtypes in the compiler
+ var nt = (NewtypeDecl)d;
+ Indent(indent, wr);
+ wr.WriteLine("public class @{0} {{", nt.CompileName);
+ if (nt.NativeType != null) {
+ Indent(indent + IndentAmount, wr);
+ wr.WriteLine("public static System.Collections.Generic.IEnumerable<{0}> IntegerRange(BigInteger lo, BigInteger hi) {{", nt.NativeType.Name);
+ Indent(indent + 2 * IndentAmount, wr);
+ wr.WriteLine("for (var j = lo; j < hi; j++) {{ yield return ({0})j; }}", nt.NativeType.Name);
+ Indent(indent + IndentAmount, wr);
+ wr.WriteLine("}");
+ }
+ Indent(indent, wr);
+ wr.WriteLine("}");
} else if (d is DatatypeDecl) {
var dt = (DatatypeDecl)d;
- Indent(indent);
+ Indent(indent, wr);
wr.Write("public abstract class Base_{0}", dt.CompileName);
if (dt.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
}
wr.WriteLine(" { }");
- CompileDatatypeConstructors(dt, indent);
- CompileDatatypeStruct(dt, indent);
+ CompileDatatypeConstructors(dt, indent, wr);
+ CompileDatatypeStruct(dt, indent, wr);
} else if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
// An iterator is compiled as follows:
@@ -153,7 +162,7 @@ namespace Microsoft.Dafny { // }
// }
- Indent(indent);
+ Indent(indent, wr);
wr.Write("public class @{0}", iter.CompileName);
if (iter.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(iter.TypeArgs));
@@ -165,58 +174,58 @@ namespace Microsoft.Dafny { foreach (var member in iter.Members) {
var f = member as Field;
if (f != null && !f.IsGhost) {
- Indent(ind);
- wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));
+ Indent(ind, wr);
+ wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type, wr), f.CompileName, DefaultValue(f.Type, wr));
} else if (member is Constructor) {
Contract.Assert(ct == null); // we're expecting just one constructor
ct = (Constructor)member;
}
}
Contract.Assert(ct != null); // we do expect a constructor
- Indent(ind); wr.WriteLine("System.Collections.Generic.IEnumerator<object> __iter;");
+ Indent(ind, wr); wr.WriteLine("System.Collections.Generic.IEnumerator<object> __iter;");
// here's the initializer method
- Indent(ind); wr.Write("public void @{0}(", ct.CompileName);
+ Indent(ind, wr); wr.Write("public void @{0}(", ct.CompileName);
string sep = "";
foreach (var p in ct.Ins) {
if (!p.IsGhost) {
// here we rely on the parameters and the corresponding fields having the same names
- wr.Write("{0}{1} @{2}", sep, TypeName(p.Type), p.CompileName);
+ wr.Write("{0}{1} @{2}", sep, TypeName(p.Type, wr), p.CompileName);
sep = ", ";
}
}
wr.WriteLine(") {");
foreach (var p in ct.Ins) {
if (!p.IsGhost) {
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("this.@{0} = @{0};", p.CompileName);
}
}
- Indent(ind + IndentAmount); wr.WriteLine("__iter = TheIterator();");
- Indent(ind); wr.WriteLine("}");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("__iter = TheIterator();");
+ Indent(ind, wr); wr.WriteLine("}");
// here are the enumerator methods
- Indent(ind); wr.WriteLine("public void MoveNext(out bool more) { more = __iter.MoveNext(); }");
- Indent(ind); wr.WriteLine("private System.Collections.Generic.IEnumerator<object> TheIterator() {");
+ Indent(ind, wr); wr.WriteLine("public void MoveNext(out bool more) { more = __iter.MoveNext(); }");
+ Indent(ind, wr); wr.WriteLine("private System.Collections.Generic.IEnumerator<object> TheIterator() {");
if (iter.Body == null) {
- Error("Iterator {0} has no body", iter.FullName);
+ Error("Iterator {0} has no body", wr, iter.FullName);
} else {
- TrStmt(iter.Body, ind + IndentAmount);
+ wr.Write(TrStmt(iter.Body, ind + IndentAmount).ToString());
}
- Indent(ind + IndentAmount); wr.WriteLine("yield break;");
- Indent(ind); wr.WriteLine("}");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("yield break;");
+ Indent(ind, wr); wr.WriteLine("}");
// end of the class
- Indent(indent); wr.WriteLine("}");
+ Indent(indent, wr); wr.WriteLine("}");
}
else if (d is TraitDecl)
{
//writing the trait
var trait = (TraitDecl)d;
- Indent(indent);
+ Indent(indent, wr);
wr.Write("public interface @{0}", trait.CompileName);
wr.WriteLine(" {");
- CompileClassMembers(trait, false, indent + IndentAmount);
- Indent(indent); wr.WriteLine("}");
+ CompileClassMembers(trait, false, indent + IndentAmount, wr);
+ Indent(indent, wr); wr.WriteLine("}");
//writing the _Companion class
List<MemberDecl> members = new List<MemberDecl>();
@@ -236,27 +245,27 @@ namespace Microsoft.Dafny { }
}
}
- Indent(indent);
+ Indent(indent, wr);
wr.Write("public class @_Companion_{0}", trait.CompileName);
wr.WriteLine(" {");
- CompileClassMembers(trait, true, indent + IndentAmount);
- Indent(indent); wr.WriteLine("}");
+ CompileClassMembers(trait, true, indent + IndentAmount, wr);
+ Indent(indent, wr); wr.WriteLine("}");
}
else if (d is ClassDecl) {
var cl = (ClassDecl)d;
- Indent(indent);
- wr.Write("public class @{0}", cl.CompileName);
+ Indent(indent, wr);
+ wr.Write("public partial class @{0}", cl.CompileName);
if (cl.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(cl.TypeArgs));
}
string sep = " : ";
foreach (var trait in cl.TraitsTyp) {
- wr.Write("{0}{1}", sep, TypeName(trait));
+ wr.Write("{0}{1}", sep, TypeName(trait, wr));
sep = ", ";
}
wr.WriteLine(" {");
- CompileClassMembers(cl, false, indent+IndentAmount);
- Indent(indent); wr.WriteLine("}");
+ CompileClassMembers(cl, false, indent+IndentAmount, wr);
+ Indent(indent, wr); wr.WriteLine("}");
} else if (d is ModuleDecl) {
// nop
} else { Contract.Assert(false); }
@@ -267,15 +276,15 @@ namespace Microsoft.Dafny { }
}
- void CompileBuiltIns(BuiltIns builtIns) {
+ void CompileBuiltIns(BuiltIns builtIns, TextWriter wr) {
wr.WriteLine("namespace Dafny {");
- Indent(IndentAmount);
+ Indent(IndentAmount, wr);
wr.WriteLine("public partial 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);
+ Indent(3 * IndentAmount, wr);
wr.Write("public static T[");
RepeatWrite(wr, dims, "", ",");
wr.Write("] InitNewArray{0}<T>(", dims);
@@ -283,52 +292,52 @@ namespace Microsoft.Dafny { wr.WriteLine(") {");
// int s0 = (int)size0;
for (int i = 0; i < dims; i++) {
- Indent(4 * IndentAmount);
+ Indent(4 * IndentAmount, wr);
wr.WriteLine("int s{0} = (int)size{0};", i);
}
// T[,] a = new T[s0, s1];
- Indent(4 * IndentAmount);
+ Indent(4 * IndentAmount, wr);
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);
+ Indent(4 * IndentAmount, wr);
wr.Write("BigInteger[");
RepeatWrite(wr, dims, "", ",");
wr.Write("] b = a as BigInteger[");
RepeatWrite(wr, dims, "", ",");
wr.WriteLine("];");
// if (b != null) {
- Indent(4 * IndentAmount);
+ Indent(4 * IndentAmount, wr);
wr.WriteLine("if (b != null) {");
// BigInteger z = new BigInteger(0);
- Indent(5 * IndentAmount);
+ Indent(5 * IndentAmount, wr);
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);
+ Indent((5+i) * IndentAmount, wr);
wr.WriteLine("for (int i{0} = 0; i{0} < s{0}; i{0}++)", i);
}
// b[i0,i1] = z;
- Indent((5+dims) * IndentAmount);
+ Indent((5+dims) * IndentAmount, wr);
wr.Write("b[");
RepeatWrite(wr, dims, "i{0}", ",");
wr.WriteLine("] = z;");
// }
- Indent(4 * IndentAmount);
+ Indent(4 * IndentAmount, wr);
wr.WriteLine("}");
// return a;
- Indent(4 * IndentAmount);
+ Indent(4 * IndentAmount, wr);
wr.WriteLine("return a;");
// }
- Indent(3 * IndentAmount);
+ Indent(3 * IndentAmount, wr);
wr.WriteLine("}"); // end of method
}
}
- Indent(IndentAmount);
+ Indent(IndentAmount, wr);
wr.WriteLine("}"); // end of class Helpers
wr.WriteLine("}"); // end of namespace
}
@@ -343,7 +352,7 @@ namespace Microsoft.Dafny { }
}
- void CompileDatatypeConstructors(DatatypeDecl dt, int indent)
+ void CompileDatatypeConstructors(DatatypeDecl dt, int indent, TextWriter wr)
{
Contract.Requires(dt != null);
@@ -356,20 +365,20 @@ namespace Microsoft.Dafny { // public Dt__Lazy(Computer c) { this.c = c; }
// public Base_Dt<T> Get() { return c(); }
// }
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("public class {0}__Lazy{1} : Base_{0}{1} {{", dt.CompileName, typeParams);
int ind = indent + IndentAmount;
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public delegate Base_{0}{1} Computer();", dt.CompileName, typeParams);
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public delegate Computer ComputerComputer();");
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("Computer c;");
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public {0}__Lazy(Computer c) {{ this.c = c; }}", dt.CompileName);
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public Base_{0}{1} Get() {{ return c(); }}", dt.CompileName, typeParams);
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("}");
}
@@ -391,7 +400,7 @@ namespace Microsoft.Dafny { // // ...
// }
// }
- Indent(indent);
+ Indent(indent, wr);
wr.Write("public class {0}", DtCtorDeclarationName(ctor, dt.TypeArgs));
wr.WriteLine(" : Base_{0}{1} {{", dt.CompileName, typeParams);
int ind = indent + IndentAmount;
@@ -399,32 +408,32 @@ namespace Microsoft.Dafny { int i = 0;
foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
- Indent(ind);
- wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type), FormalName(arg, i));
+ Indent(ind, wr);
+ wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type, wr), FormalName(arg, i));
i++;
}
}
- Indent(ind);
+ Indent(ind, wr);
wr.Write("public {0}(", DtCtorDeclartionName(ctor));
- WriteFormals("", ctor.Formals);
+ WriteFormals("", ctor.Formals, wr);
wr.WriteLine(") {");
i = 0;
foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("this.@{0} = @{0};", FormalName(arg, i));
i++;
}
}
- Indent(ind); wr.WriteLine("}");
+ Indent(ind, wr); wr.WriteLine("}");
// Equals method
- Indent(ind); wr.WriteLine("public override bool Equals(object other) {");
- Indent(ind + IndentAmount);
+ Indent(ind, wr); wr.WriteLine("public override bool Equals(object other) {");
+ Indent(ind + IndentAmount, wr);
wr.Write("var oth = other as {0}", DtCtorName(ctor, dt.TypeArgs));
wr.WriteLine(";");
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.Write("return oth != null");
i = 0;
foreach (Formal arg in ctor.Formals) {
@@ -439,56 +448,76 @@ namespace Microsoft.Dafny { }
}
wr.WriteLine(";");
- Indent(ind); wr.WriteLine("}");
-
- // GetHashCode method
- Indent(ind); wr.WriteLine("public override int GetHashCode() {");
- Indent(ind + IndentAmount); wr.Write("return " + constructorIndex);
+ Indent(ind, wr); wr.WriteLine("}");
+ // GetHashCode method (Uses the djb2 algorithm)
+ Indent(ind, wr); wr.WriteLine("public override int GetHashCode() {");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("ulong hash = 5381;");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("hash = ((hash << 5) + hash) + {0};", constructorIndex);
i = 0;
foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
string nm = FormalName(arg, i);
- wr.Write(" ^ this.@{0}.GetHashCode()", nm);
+ Indent(ind + IndentAmount, wr); wr.WriteLine("hash = ((hash << 5) + hash) + ((ulong)this.@{0}.GetHashCode());", nm);
i++;
}
}
- wr.WriteLine(";");
- Indent(ind); wr.WriteLine("}");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("return (int) hash;");
+ Indent(ind, wr); wr.WriteLine("}");
if (dt is IndDatatypeDecl) {
- Indent(ind); wr.WriteLine("public override string ToString() {");
+ Indent(ind, wr); wr.WriteLine("public override string ToString() {");
string nm;
if (dt is TupleTypeDecl) {
nm = "";
} else {
nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;
}
- Indent(ind + IndentAmount); wr.WriteLine("string s = \"{0}\";", nm);
+ var tempVar = GenVarName("s", ctor.Formals);
+ Indent(ind + IndentAmount, wr); wr.WriteLine("string {0} = \"{1}\";", tempVar, nm);
if (ctor.Formals.Count != 0) {
- Indent(ind + IndentAmount); wr.WriteLine("s += \"(\";");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("{0} += \"(\";", tempVar);
i = 0;
foreach (var arg in ctor.Formals) {
if (!arg.IsGhost) {
if (i != 0) {
- Indent(ind + IndentAmount); wr.WriteLine("s += \", \";");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("{0} += \", \";", tempVar);
}
- Indent(ind + IndentAmount); wr.WriteLine("s += @{0}.ToString();", FormalName(arg, i));
+ Indent(ind + IndentAmount, wr); wr.WriteLine("{0} += @{1}.ToString();", tempVar,FormalName(arg, i));
i++;
}
}
- Indent(ind + IndentAmount); wr.WriteLine("s += \")\";");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("{0} += \")\";", tempVar);
}
- Indent(ind + IndentAmount); wr.WriteLine("return s;");
- Indent(ind); wr.WriteLine("}");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("return {0};", tempVar);
+ Indent(ind, wr); wr.WriteLine("}");
}
- Indent(indent); wr.WriteLine("}");
+ Indent(indent, wr); wr.WriteLine("}");
}
constructorIndex++;
}
- void CompileDatatypeStruct(DatatypeDecl dt, int indent) {
+ // create a varName that is not a duplicate of formals' name
+ string GenVarName(string root, List<Formal> formals) {
+ bool finished = false;
+ while (!finished) {
+ finished = true;
+ int i = 0;
+ foreach (var arg in formals) {
+ if (!arg.IsGhost) {
+ if (root.Equals(FormalName(arg, i))) {
+ root += root;
+ finished = false;
+ }
+ i++;
+ }
+ }
+ }
+ return root;
+ }
+
+ void CompileDatatypeStruct(DatatypeDecl dt, int indent, TextWriter wr) {
Contract.Requires(dt != null);
// public struct Dt<T> : IDatatype{
@@ -532,46 +561,46 @@ namespace Microsoft.Dafny { DtT += DtT_TypeArgs;
}
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("public struct @{0} {{", DtT);
int ind = indent + IndentAmount;
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("Base_{0} _d;", DtT);
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public Base_{0} _D {{", DtT);
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("get {");
- Indent(ind + 2 * IndentAmount);
+ Indent(ind + 2 * IndentAmount, wr);
wr.WriteLine("if (_d == null) {");
- Indent(ind + 3 * IndentAmount);
+ Indent(ind + 3 * IndentAmount, wr);
wr.WriteLine("_d = Default;");
if (dt is CoDatatypeDecl) {
string typeParams = dt.TypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeParameters(dt.TypeArgs));
- Indent(ind + 2 * IndentAmount);
+ Indent(ind + 2 * IndentAmount, wr);
wr.WriteLine("}} else if (_d is {0}__Lazy{1}) {{", dt.CompileName, typeParams);
- Indent(ind + 3 * IndentAmount);
+ Indent(ind + 3 * IndentAmount, wr);
wr.WriteLine("_d = (({0}__Lazy{1})_d).Get();", dt.CompileName, typeParams);
}
- Indent(ind + 2 * IndentAmount); wr.WriteLine("}");
- Indent(ind + 2 * IndentAmount); wr.WriteLine("return _d;");
- Indent(ind + IndentAmount); wr.WriteLine("}");
- Indent(ind); wr.WriteLine("}");
+ Indent(ind + 2 * IndentAmount, wr); wr.WriteLine("}");
+ Indent(ind + 2 * IndentAmount, wr); wr.WriteLine("return _d;");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("}");
+ Indent(ind, wr); wr.WriteLine("}");
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public @{0}(Base_{1} d) {{ this._d = d; }}", dt.CompileName, DtT);
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("static Base_{0} theDefault;", DtT);
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public static Base_{0} Default {{", DtT);
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("get {");
- Indent(ind + 2 * IndentAmount);
+ Indent(ind + 2 * IndentAmount, wr);
wr.WriteLine("if (theDefault == null) {");
- Indent(ind + 3 * IndentAmount);
+ Indent(ind + 3 * IndentAmount, wr);
wr.Write("theDefault = ");
DatatypeCtor defaultCtor;
@@ -585,55 +614,55 @@ namespace Microsoft.Dafny { string sep = "";
foreach (Formal f in defaultCtor.Formals) {
if (!f.IsGhost) {
- wr.Write("{0}{1}", sep, DefaultValue(f.Type));
+ wr.Write("{0}{1}", sep, DefaultValue(f.Type, wr));
sep = ", ";
}
}
wr.Write(")");
wr.WriteLine(";");
- Indent(ind + 2 * IndentAmount);
+ Indent(ind + 2 * IndentAmount, wr);
wr.WriteLine("}");
- Indent(ind + 2 * IndentAmount);
+ Indent(ind + 2 * IndentAmount, wr);
wr.WriteLine("return theDefault;");
- Indent(ind + IndentAmount); wr.WriteLine("}");
+ Indent(ind + IndentAmount, wr); wr.WriteLine("}");
- Indent(ind); wr.WriteLine("}");
+ Indent(ind, wr); wr.WriteLine("}");
- Indent(ind); wr.WriteLine("public override bool Equals(object other) {");
- Indent(ind + IndentAmount);
+ Indent(ind, wr); wr.WriteLine("public override bool Equals(object other) {");
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("return other is @{0} && _D.Equals(((@{0})other)._D);", DtT);
- Indent(ind); wr.WriteLine("}");
+ Indent(ind, wr); wr.WriteLine("}");
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public override int GetHashCode() { return _D.GetHashCode(); }");
if (dt is IndDatatypeDecl) {
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public override string ToString() { return _D.ToString(); }");
}
// query properties
foreach (var ctor in dt.Ctors) {
// public bool is_Ctor0 { get { return _D is Dt_Ctor0; } }
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public bool is_{0} {{ get {{ return _D is {1}_{0}{2}; }} }}", ctor.CompileName, dt.CompileName, DtT_TypeArgs);
}
if (dt.HasFinitePossibleValues) {
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("public static System.Collections.Generic.IEnumerable<@{0}> AllSingletonConstructors {{", DtT);
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("get {");
foreach (var ctr in dt.Ctors) {
if (ctr.Formals.Count == 0) {
- Indent(ind + IndentAmount + IndentAmount);
+ Indent(ind + IndentAmount + IndentAmount, wr);
wr.WriteLine("yield return new @{0}(new {2}_{1}());", DtT, ctr.CompileName, dt.CompileName);
}
}
- Indent(ind + IndentAmount + IndentAmount);
+ Indent(ind + IndentAmount + IndentAmount, wr);
wr.WriteLine("yield break;");
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("}");
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("}");
}
@@ -642,17 +671,17 @@ namespace Microsoft.Dafny { foreach (var arg in ctor.Formals) {
if (!arg.IsGhost && arg.HasName) {
// public T0 @Dtor0 { get { return ((DT_Ctor)_D).@Dtor0; } }
- Indent(ind);
- wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3}{4})_D).@{1}; }} }}", TypeName(arg.Type), arg.CompileName, dt.CompileName, ctor.CompileName, DtT_TypeArgs);
+ Indent(ind, wr);
+ wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3}{4})_D).@{1}; }} }}", TypeName(arg.Type, wr), arg.CompileName, dt.CompileName, ctor.CompileName, DtT_TypeArgs);
}
}
}
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("}");
}
- int WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals)
+ int WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals, TextWriter wr)
{
Contract.Requires(sep != null);
Contract.Requires(cce.NonNullElements(formals));
@@ -660,7 +689,7 @@ namespace Microsoft.Dafny { foreach (Formal arg in formals) {
if (!arg.IsGhost) {
string name = FormalName(arg, i);
- wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);
+ wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type, wr), name);
sep = ", ";
i++;
}
@@ -676,7 +705,11 @@ namespace Microsoft.Dafny { }
string DtName(DatatypeDecl decl) {
- return decl.Module.IsDefaultModule ? decl.CompileName : decl.FullCompileName;
+ var d = (TopLevelDecl)decl;
+ while (DafnyOptions.O.IronDafny && d.ClonedFrom != null) {
+ d = (TopLevelDecl)d.ClonedFrom;
+ }
+ return d.Module.IsDefaultModule ? d.CompileName : d.FullCompileName;
}
string DtCtorName(DatatypeCtor ctor) {
Contract.Requires(ctor != null);
@@ -712,51 +745,80 @@ namespace Microsoft.Dafny { return s;
}
- string DtCtorName(DatatypeCtor ctor, List<Type> typeArgs) {
+ string DtCtorName(DatatypeCtor ctor, List<Type> typeArgs, TextWriter wr) {
Contract.Requires(ctor != null);
Contract.Ensures(Contract.Result<string>() != null);
var s = DtCtorName(ctor);
if (typeArgs != null && typeArgs.Count != 0) {
- s += "<" + TypeNames(typeArgs) + ">";
+ s += "<" + TypeNames(typeArgs, wr) + ">";
}
return s;
}
public bool HasMain(Program program) {
+ Method mainMethod = null;
+ bool hasMain = false;
foreach (var module in program.Modules) {
+ if (module.IsAbstract) {
+ // the purpose of an abstract module is to skip compilation
+ continue;
+ }
foreach (var decl in module.TopLevelDecls) {
var c = decl as ClassDecl;
if (c != null) {
foreach (var member in c.Members) {
var m = member as Method;
if (m != null && IsMain(m)) {
- return true;
+ if (mainMethod == null) {
+ mainMethod = m;
+ hasMain = true;
+ } else {
+ // more than one main in the program
+ ErrorWriter.WriteLine("More than one method is declared as \"main\"");
+ ErrorCount++;
+ hasMain = false;
+ }
}
}
}
}
}
- return false;
+ return hasMain;
}
public static bool IsMain(Method m) {
// In order to be a legal Main() method, the following must be true:
- // The method takes no parameters
+ // The method takes no parameters
// The method is not a ghost method
// The method has no requires clause
// The method has no modifies clause
// If the method is an instance (that is, non-static) method in a class, then the enclosing class must not declare any constructor
- if (!m.IsGhost && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0
+ // Or if a method is annotated with {:main} and the above restrictions apply, except it is allowed to take ghost arguments,
+ // and it is allowed to have preconditions and modifies. This lets the programmer add some explicit assumptions about the outside world,
+ // modeled, for example, via ghost parameters.
+ if (!m.IsGhost && m.Name == "Main" && m.TypeArgs.Count == 0 && m.Ins.Count == 0 && m.Outs.Count == 0 && m.Req.Count == 0
&& m.Mod.Expressions.Count == 0 && (m.IsStatic || (((ClassDecl)m.EnclosingClass) == null) || !((ClassDecl)m.EnclosingClass).HasConstructor)) {
return true;
- }
- else {
+ } else if (Attributes.Contains(m.Attributes, "main") && !m.IsGhost && m.TypeArgs.Count == 0 && m.Outs.Count == 0
+ && (m.IsStatic || (((ClassDecl)m.EnclosingClass) == null) || !((ClassDecl)m.EnclosingClass).HasConstructor)) {
+ if (m.Ins.Count == 0) {
+ return true;
+ } else {
+ bool isGhost = true;
+ foreach (var arg in m.Ins) {
+ if (!arg.IsGhost) {
+ isGhost = false;
+ }
+ }
+ return isGhost;
+ }
+ } else {
return false;
}
}
- void CompileClassMembers(ClassDecl c, bool forCompanionClass, int indent) {
+ void CompileClassMembers(ClassDecl c, bool forCompanionClass, int indent, TextWriter wr) {
Contract.Requires(c != null);
Contract.Requires(!forCompanionClass || c is TraitDecl);
Contract.Requires(0 <= indent);
@@ -765,9 +827,9 @@ namespace Microsoft.Dafny { if (member is Field) {
var f = (Field)member;
// every field is inherited
- Indent(indent);
- wr.WriteLine("public {0} @_{1};", TypeName(f.Type), f.CompileName);
- wr.Write("public {0} @{1}", TypeName(f.Type), f.CompileName);
+ Indent(indent, wr);
+ wr.WriteLine("public {0} @_{1};", TypeName(f.Type, wr), f.CompileName);
+ wr.Write("public {0} @{1}", TypeName(f.Type, wr), f.CompileName);
wr.WriteLine(" {");
wr.WriteLine(" get { ");
wr.Write("return this.@_{0};", f.CompileName);
@@ -779,11 +841,11 @@ namespace Microsoft.Dafny { } else if (member is Function) {
var f = (Function)member;
Contract.Assert(f.Body != null);
- CompileFunction(indent, f);
+ CompileFunction(indent, f, wr);
} else if (member is Method) {
var method = (Method)member;
Contract.Assert(method.Body != null);
- CompileMethod(c, indent, method);
+ CompileMethod(c, indent, method, wr);
} else {
Contract.Assert(false); // unexpected member
}
@@ -794,12 +856,12 @@ namespace Microsoft.Dafny { if (f.IsGhost || forCompanionClass) {
// emit nothing
} else if (c is TraitDecl) {
- Indent(indent);
- wr.Write("{0} @{1}", TypeName(f.Type), f.CompileName);
+ Indent(indent, wr);
+ wr.Write("{0} @{1}", TypeName(f.Type, wr), f.CompileName);
wr.WriteLine(" { get; set; }");
} else {
- Indent(indent);
- wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));
+ Indent(indent, wr);
+ wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type, wr), f.CompileName, DefaultValue(f.Type, wr));
}
} else if (member is Function) {
var f = (Function)member;
@@ -808,29 +870,29 @@ namespace Microsoft.Dafny { if (forCompanionClass || Attributes.Contains(f.Attributes, "axiom")) {
// suppress error message (in the case of "forCompanionClass", the non-forCompanionClass call will produce the error message)
} else {
- Error("Function {0} has no body", f.FullName);
+ Error("Function {0} has no body", wr, f.FullName);
}
} else if (f.IsGhost) {
// nothing to compile, but we do check for assumes
if (f.Body == null) {
Contract.Assert(c is TraitDecl && !f.IsStatic);
} else {
- var v = new CheckHasNoAssumes_Visitor(this);
+ var v = new CheckHasNoAssumes_Visitor(this, wr);
v.Visit(f.Body);
}
} else if (c is TraitDecl && !forCompanionClass) {
// include it, unless it's static
if (!f.IsStatic) {
- Indent(indent);
- wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName);
+ Indent(indent, wr);
+ wr.Write("{0} @{1}", TypeName(f.ResultType, wr), f.CompileName);
wr.Write("(");
- WriteFormals("", f.Formals);
+ WriteFormals("", f.Formals, wr);
wr.WriteLine(");");
}
} else if (forCompanionClass && !f.IsStatic) {
// companion classes only has static members
} else {
- CompileFunction(indent, f);
+ CompileFunction(indent, f, wr);
}
} else if (member is Method) {
var m = (Method)member;
@@ -839,30 +901,30 @@ namespace Microsoft.Dafny { if (forCompanionClass || Attributes.Contains(m.Attributes, "axiom")) {
// suppress error message (in the case of "forCompanionClass", the non-forCompanionClass call will produce the error message)
} else {
- Error("Method {0} has no body", m.FullName);
+ Error("Method {0} has no body", wr, m.FullName);
}
} else if (m.IsGhost) {
// nothing to compile, but we do check for assumes
if (m.Body == null) {
Contract.Assert(c is TraitDecl && !m.IsStatic);
} else {
- var v = new CheckHasNoAssumes_Visitor(this);
+ var v = new CheckHasNoAssumes_Visitor(this, wr);
v.Visit(m.Body);
}
} else if (c is TraitDecl && !forCompanionClass) {
// include it, unless it's static
if (!m.IsStatic) {
- Indent(indent);
+ Indent(indent, wr);
wr.Write("void @{0}", m.CompileName);
wr.Write("(");
- int nIns = WriteFormals("", m.Ins);
- WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
+ int nIns = WriteFormals("", m.Ins, wr);
+ WriteFormals(nIns == 0 ? "" : ", ", m.Outs, wr);
wr.WriteLine(");");
}
} else if (forCompanionClass && !m.IsStatic) {
// companion classes only has static members
} else {
- CompileMethod(c, indent, m);
+ CompileMethod(c, indent, m, wr);
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member
@@ -870,85 +932,218 @@ namespace Microsoft.Dafny { }
}
- private void CompileFunction(int indent, Function f) {
- Indent(indent);
- wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);
+ private void CompileFunction(int indent, Function f, TextWriter wr) {
+ Indent(indent, wr);
+ wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType, wr), f.CompileName);
if (f.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(f.TypeArgs));
}
wr.Write("(");
- WriteFormals("", f.Formals);
+ WriteFormals("", f.Formals, wr);
wr.WriteLine(") {");
- CompileReturnBody(f.Body, indent + IndentAmount);
- Indent(indent); wr.WriteLine("}");
+ CompileReturnBody(f.Body, indent + IndentAmount, wr);
+ Indent(indent, wr); wr.WriteLine("}");
}
- private void CompileMethod(ClassDecl c, int indent, Method m) {
- Indent(indent);
+ private void CompileMethod(ClassDecl c, int indent, Method m, TextWriter wr) {
+ Indent(indent, wr);
wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);
if (m.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(m.TypeArgs));
}
wr.Write("(");
- int nIns = WriteFormals("", m.Ins);
- WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
+ int nIns = WriteFormals("", m.Ins, wr);
+ WriteFormals(nIns == 0 ? "" : ", ", m.Outs, wr);
wr.WriteLine(")");
- Indent(indent); wr.WriteLine("{");
+ Indent(indent, wr); wr.WriteLine("{");
foreach (Formal p in m.Outs) {
if (!p.IsGhost) {
- Indent(indent + IndentAmount);
- wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));
+ Indent(indent + IndentAmount, wr);
+ wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type, wr));
}
}
if (m.Body == null) {
- Error("Method {0} has no body", m.FullName);
+ Error("Method {0} has no body", wr, m.FullName);
} else {
if (m.IsTailRecursive) {
- Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");
if (!m.IsStatic) {
- Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");
+ Indent(indent + IndentAmount, wr); wr.WriteLine("var _this = this;");
}
+ Indent(indent, wr); wr.WriteLine("TAIL_CALL_START: ;");
}
Contract.Assert(enclosingMethod == null);
enclosingMethod = m;
- TrStmtList(m.Body.Body, indent);
+ TrStmtList(m.Body.Body, indent, wr);
Contract.Assert(enclosingMethod == m);
enclosingMethod = null;
}
- Indent(indent); wr.WriteLine("}");
+ Indent(indent, wr); wr.WriteLine("}");
// allow the Main method to be an instance method
- if (!m.IsStatic && IsMain(m)) {
- Indent(indent);
+ if (IsMain(m) && (!m.IsStatic || m.CompileName != "Main")) {
+ Indent(indent, wr);
wr.WriteLine("public static void Main(string[] args) {");
- Contract.Assert(m.EnclosingClass == c);
- Indent(indent + IndentAmount);
- wr.Write("@{0} b = new @{0}", c.CompileName);
- if (c.TypeArgs.Count != 0) {
- // instantiate every parameter, it doesn't particularly matter how
- wr.Write("<");
- string sep = "";
- for (int i = 0; i < c.TypeArgs.Count; i++) {
- wr.Write("{0}int", sep);
- sep = ", ";
+ if (!m.IsStatic) {
+ Contract.Assert(m.EnclosingClass == c);
+ Indent(indent + IndentAmount, wr);
+ wr.Write("@{0} b = new @{0}", c.CompileName);
+ if (c.TypeArgs.Count != 0) {
+ // instantiate every parameter, it doesn't particularly matter how
+ wr.Write("<");
+ string sep = "";
+ for (int i = 0; i < c.TypeArgs.Count; i++) {
+ wr.Write("{0}int", sep);
+ sep = ", ";
+ }
+ wr.Write(">");
}
- wr.Write(">");
+ wr.WriteLine("();");
+ Indent(indent + IndentAmount, wr); wr.WriteLine("b.@{0}();", m.CompileName);
+ } else {
+ Indent(indent + IndentAmount, wr); wr.WriteLine("@{0}();", m.CompileName);
}
- wr.WriteLine("();");
- Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");
- Indent(indent); wr.WriteLine("}");
+ Indent(indent, wr); wr.WriteLine("}");
}
}
- void CompileReturnBody(Expression body, int indent) {
- Contract.Requires(0 <= indent);
- body = body.Resolved;
- Indent(indent);
+ void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string, int indent, TextWriter wr, bool inLetExprBody) {
+ Contract.Requires(pat != null);
+ Contract.Requires(pat.Var != null || rhs != null);
+ if (pat.Var != null) {
+ // The trivial Dafny "pattern" expression
+ // var x := G
+ // is translated into C# as:
+ // var x := G;
+ var bv = pat.Var;
+ if (!bv.IsGhost) {
+ Indent(indent, wr);
+ wr.Write("{0} {1} = ", TypeName(bv.Type, wr), "@" + bv.CompileName);
+ if (rhs != null) {
+ TrExpr(rhs, wr, inLetExprBody);
+ } else {
+ wr.Write(rhs_string);
+ }
+ wr.Write(";\n");
+ }
+ } else if (pat.Arguments != null) {
+ // The Dafny "pattern" expression
+ // var Pattern(x,y) := G
+ // is translated into C# as:
+ // var tmp := G;
+ // var x := dtorX(tmp);
+ // var y := dtorY(tmp);
+ var ctor = pat.Ctor;
+ Contract.Assert(ctor != null); // follows from successful resolution
+ Contract.Assert(pat.Arguments.Count == ctor.Formals.Count); // follows from successful resolution
+
+ // Create the temporary variable to hold G
+ var tmp_name = idGenerator.FreshId("_let_tmp_rhs");
+ Indent(indent, wr);
+ wr.Write("{0} {1} = ", TypeName(rhs.Type, wr), tmp_name);
+ TrExpr(rhs, wr, inLetExprBody);
+ wr.WriteLine(";");
+
+ var k = 0; // number of non-ghost formals processed
+ for (int i = 0; i < pat.Arguments.Count; i++) {
+ var arg = pat.Arguments[i];
+ var formal = ctor.Formals[i];
+ if (formal.IsGhost) {
+ // nothing to compile, but do a sanity check
+ Contract.Assert(!Contract.Exists(arg.Vars, bv => !bv.IsGhost));
+ } else {
+ TrCasePatternOpt(arg, null, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs, wr), tmp_name, FormalName(formal, k)), indent, wr, inLetExprBody);
+ k++;
+ }
+ }
+ }
+ }
+
+ void ReturnExpr(Expression expr, int indent, TextWriter wr, bool inLetExprBody) {
+ Indent(indent, wr);
wr.Write("return ");
- TrExpr(body);
+ TrExpr(expr, wr, inLetExprBody);
wr.WriteLine(";");
}
+ void TrExprOpt(Expression expr, int indent, TextWriter wr, bool inLetExprBody) {
+ Contract.Requires(expr != null);
+ if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ if (e.Exact) {
+ for (int i = 0; i < e.LHSs.Count; i++) {
+ var lhs = e.LHSs[i];
+ if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {
+ TrCasePatternOpt(lhs, e.RHSs[i], null, indent, wr, inLetExprBody);
+ }
+ }
+ TrExprOpt(e.Body, indent, wr, inLetExprBody);
+ } else {
+ // We haven't optimized the other cases, so fallback to normal compilation
+ ReturnExpr(e, indent, wr, inLetExprBody);
+ }
+ } else if (expr is ITEExpr) {
+ ITEExpr e = (ITEExpr)expr;
+ Indent(indent, wr);
+ wr.Write("if (");
+ TrExpr(e.Test, wr, inLetExprBody);
+ wr.Write(") {\n");
+ TrExprOpt(e.Thn, indent + IndentAmount, wr, inLetExprBody);
+ Indent(indent, wr);
+ wr.WriteLine("} else {");
+ TrExprOpt(e.Els, indent + IndentAmount, wr, inLetExprBody);
+ Indent(indent, wr);
+ wr.WriteLine("}");
+ } else if (expr is MatchExpr) {
+ var e = (MatchExpr)expr;
+ // var _source = E;
+ // if (source.is_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source._D).a0;
+ // ...
+ // return Body0;
+ // } else if (...) {
+ // ...
+ // } else if (true) {
+ // ...
+ // }
+ string source = idGenerator.FreshId("_source");
+ Indent(indent, wr);
+ wr.Write("{0} {1} = ", TypeName(e.Source.Type, wr), source);
+ TrExpr(e.Source, wr, inLetExprBody);
+ wr.WriteLine(";");
+
+ if (e.Cases.Count == 0) {
+ // the verifier would have proved we never get here; still, we need some code that will compile
+ wr.Write("throw new System.Exception();");
+ } else {
+ int i = 0;
+ var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();
+ foreach (MatchCaseExpr mc in e.Cases) {
+ //Indent(indent);
+ MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, indent, wr);
+ TrExprOpt(mc.Body, indent + IndentAmount, wr, inLetExprBody);
+ i++;
+ }
+ Indent(indent, wr);
+ wr.WriteLine("}");
+ }
+ } else if (expr is StmtExpr) {
+ var e = (StmtExpr)expr;
+ TrExprOpt(e.E, indent, wr, inLetExprBody);
+ } else {
+ // We haven't optimized any other cases, so fallback to normal compilation
+ ReturnExpr(expr, indent, wr, inLetExprBody);
+ }
+ }
+
+ void CompileReturnBody(Expression body, int indent, TextWriter wr) {
+ Contract.Requires(0 <= indent);
+ body = body.Resolved;
+ //Indent(indent);
+ //wr.Write("return ");
+ TrExprOpt(body, indent, wr, false);
+ //wr.WriteLine(";");
+ }
+
// ----- Type ---------------------------------------------------------------------------------
readonly string DafnySetClass = "Dafny.Set";
@@ -964,168 +1159,207 @@ namespace Microsoft.Dafny { return null;
}
- string TypeName_Companion(Type type) {
+ string TypeName_Companion(Type type, TextWriter wr) {
Contract.Requires(type != null);
var udt = type as UserDefinedType;
if (udt != null && udt.ResolvedClass is TraitDecl) {
string s = udt.FullCompanionCompileName;
if (udt.TypeArgs.Count != 0) {
if (udt.TypeArgs.Exists(argType => argType is ObjectType)) {
- Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");
+ Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost", wr);
}
- s += "<" + TypeNames(udt.TypeArgs) + ">";
+ s += "<" + TypeNames(udt.TypeArgs, wr) + ">";
}
return s;
} else {
- return TypeName(type);
+ return TypeName(type, wr);
}
}
- string TypeName(Type type)
+ string TypeName(Type type, TextWriter wr)
{
Contract.Requires(type != null);
Contract.Ensures(Contract.Result<string>() != null);
- type = type.NormalizeExpand();
- if (type is TypeProxy) {
+ var xType = type.NormalizeExpand();
+ if (xType is TypeProxy) {
// unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
return "object";
}
- if (type is BoolType) {
+ if (xType is BoolType) {
return "bool";
- } else if (type is CharType) {
+ } else if (xType is CharType) {
return "char";
- } else if (type is IntType) {
+ } else if (xType is IntType) {
return "BigInteger";
- } else if (type is RealType) {
+ } else if (xType is RealType) {
return "Dafny.BigRational";
- } else if (type.AsNewtype != null) {
- NativeType nativeType = type.AsNewtype.NativeType;
+ } else if (xType.AsNewtype != null) {
+ NativeType nativeType = xType.AsNewtype.NativeType;
if (nativeType != null) {
return nativeType.Name;
}
- return TypeName(type.AsNewtype.BaseType);
- } else if (type is ObjectType) {
+ return TypeName(xType.AsNewtype.BaseType, wr);
+ } else if (xType is ObjectType) {
return "object";
- } else if (type.IsArrayType) {
- ArrayClassDecl at = type.AsArrayType;
+ } else if (xType.IsArrayType) {
+ ArrayClassDecl at = xType.AsArrayType;
Contract.Assert(at != null); // follows from type.IsArrayType
- Type elType = UserDefinedType.ArrayElementType(type);
- string name = TypeName(elType) + "[";
+ Type elType = UserDefinedType.ArrayElementType(xType);
+ string name = TypeName(elType, wr) + "[";
for (int i = 1; i < at.Dims; i++) {
name += ",";
}
return name + "]";
- } else if (type is UserDefinedType) {
- var udt = (UserDefinedType)type;
- return TypeName_UDT(udt.FullCompileName, udt.TypeArgs);
- } else if (type is SetType) {
- Type argType = ((SetType)type).Arg;
+ } else if (xType is UserDefinedType) {
+ var udt = (UserDefinedType)xType;
+ var s = udt.FullCompileName;
+ var rc = udt.ResolvedClass;
+ if (DafnyOptions.O.IronDafny &&
+ !(xType is ArrowType) &&
+ rc != null &&
+ rc.Module != null &&
+ !rc.Module.IsDefaultModule) {
+ while (rc.ClonedFrom != null || rc.ExclusiveRefinement != null) {
+ if (rc.ClonedFrom != null) {
+ rc = (TopLevelDecl)rc.ClonedFrom;
+ } else {
+ Contract.Assert(rc.ExclusiveRefinement != null);
+ rc = rc.ExclusiveRefinement;
+ }
+ }
+ s = rc.FullCompileName;
+ }
+ return TypeName_UDT(s, udt.TypeArgs, wr);
+ } else if (xType is SetType) {
+ Type argType = ((SetType)xType).Arg;
if (argType is ObjectType) {
- Error("compilation of set<object> is not supported; consider introducing a ghost");
+ Error("compilation of set<object> is not supported; consider introducing a ghost", wr);
}
- return DafnySetClass + "<" + TypeName(argType) + ">";
- } else if (type is SeqType) {
- Type argType = ((SeqType)type).Arg;
+ return DafnySetClass + "<" + TypeName(argType, wr) + ">";
+ } else if (xType is SeqType) {
+ Type argType = ((SeqType)xType).Arg;
if (argType is ObjectType) {
- Error("compilation of seq<object> is not supported; consider introducing a ghost");
+ Error("compilation of seq<object> is not supported; consider introducing a ghost", wr);
}
- return DafnySeqClass + "<" + TypeName(argType) + ">";
- } else if (type is MultiSetType) {
- Type argType = ((MultiSetType)type).Arg;
+ return DafnySeqClass + "<" + TypeName(argType, wr) + ">";
+ } else if (xType is MultiSetType) {
+ Type argType = ((MultiSetType)xType).Arg;
if (argType is ObjectType) {
- Error("compilation of seq<object> is not supported; consider introducing a ghost");
+ Error("compilation of seq<object> is not supported; consider introducing a ghost", wr);
}
- return DafnyMultiSetClass + "<" + TypeName(argType) + ">";
- } else if (type is MapType) {
- Type domType = ((MapType)type).Domain;
- Type ranType = ((MapType)type).Range;
+ return DafnyMultiSetClass + "<" + TypeName(argType, wr) + ">";
+ } else if (xType is MapType) {
+ Type domType = ((MapType)xType).Domain;
+ Type ranType = ((MapType)xType).Range;
if (domType is ObjectType || ranType is ObjectType) {
- Error("compilation of map<object, _> or map<_, object> is not supported; consider introducing a ghost");
+ Error("compilation of map<object, _> or map<_, object> is not supported; consider introducing a ghost", wr);
}
- return DafnyMapClass + "<" + TypeName(domType) + "," + TypeName(ranType) + ">";
+ return DafnyMapClass + "<" + TypeName(domType, wr) + "," + TypeName(ranType, wr) + ">";
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
- string TypeName_UDT(string fullCompileName, List<Type> typeArgs) {
+ string TypeName_UDT(string fullCompileName, List<Type> typeArgs, TextWriter wr) {
Contract.Requires(fullCompileName != null);
Contract.Requires(typeArgs != null);
string s = "@" + fullCompileName;
if (typeArgs.Count != 0) {
if (typeArgs.Exists(argType => argType is ObjectType)) {
- Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");
+ Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost", wr);
}
- s += "<" + TypeNames(typeArgs) + ">";
+ s += "<" + TypeNames(typeArgs, wr) + ">";
}
return s;
}
- string/*!*/ TypeNames(List<Type/*!*/>/*!*/ types) {
+ string/*!*/ TypeNames(List<Type/*!*/>/*!*/ types, TextWriter wr) {
Contract.Requires(cce.NonNullElements(types));
Contract.Ensures(Contract.Result<string>() != null);
- return Util.Comma(types, TypeName);
+ string res = "";
+ string c = "";
+ foreach (var t in types) {
+ res += c + TypeName(t, wr);
+ c = ",";
+ }
+ return res;
}
string/*!*/ TypeParameters(List<TypeParameter/*!*/>/*!*/ targs) {
Contract.Requires(cce.NonNullElements(targs));
Contract.Ensures(Contract.Result<string>() != null);
- string s = "";
- string sep = "";
- foreach (TypeParameter tp in targs) {
- s += sep + "@" + tp.CompileName;
- sep = ",";
- }
- return s;
+ return Util.Comma(targs, tp => "@" + tp.CompileName);
}
- string DefaultValue(Type type)
+ string DefaultValue(Type type, TextWriter wr)
{
Contract.Requires(type != null);
Contract.Ensures(Contract.Result<string>() != null);
- type = type.NormalizeExpand();
- if (type is TypeProxy) {
+ var xType = type.NormalizeExpand();
+ if (xType is TypeProxy) {
// unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
return "null";
}
- if (type is BoolType) {
+ if (xType is BoolType) {
return "false";
- } else if (type is CharType) {
+ } else if (xType is CharType) {
return "'D'";
- } else if (type is IntType) {
+ } else if (xType is IntType) {
return "BigInteger.Zero";
- } else if (type is RealType) {
+ } else if (xType is RealType) {
return "Dafny.BigRational.ZERO";
- } else if (type.AsNewtype != null) {
- if (type.AsNewtype.NativeType != null) {
+ } else if (xType.AsNewtype != null) {
+ if (xType.AsNewtype.NativeType != null) {
return "0";
}
- return DefaultValue(type.AsNewtype.BaseType);
- } else if (type.IsRefType) {
- return string.Format("({0})null", TypeName(type));
- } else if (type.IsDatatype) {
- UserDefinedType udt = (UserDefinedType)type;
- string s = "@" + udt.FullCompileName;
+ return DefaultValue(xType.AsNewtype.BaseType, wr);
+ } else if (xType.IsRefType) {
+ return string.Format("({0})null", TypeName(xType, wr));
+ } else if (xType.IsDatatype) {
+ var udt = (UserDefinedType)xType;
+ var s = "@" + udt.FullCompileName;
+ var rc = udt.ResolvedClass;
+ if (DafnyOptions.O.IronDafny &&
+ !(xType is ArrowType) &&
+ rc != null &&
+ rc.Module != null &&
+ !rc.Module.IsDefaultModule) {
+ while (rc.ClonedFrom != null || rc.ExclusiveRefinement != null) {
+ if (rc.ClonedFrom != null) {
+ rc = (TopLevelDecl)rc.ClonedFrom;
+ } else {
+ Contract.Assert(rc.ExclusiveRefinement != null);
+ rc = rc.ExclusiveRefinement;
+ }
+ }
+ s = "@" + rc.FullCompileName;
+ }
if (udt.TypeArgs.Count != 0) {
- s += "<" + TypeNames(udt.TypeArgs) + ">";
+ s += "<" + TypeNames(udt.TypeArgs, wr) + ">";
}
return string.Format("new {0}()", s);
- } else if (type.IsTypeParameter) {
- var udt = (UserDefinedType)type;
- return "default(@" + udt.FullCompileName + ")";
- } else if (type is SetType) {
- return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty";
- } else if (type is MultiSetType) {
- return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)type).Arg) + ">.Empty";
- } else if (type is SeqType) {
- return DafnySeqClass + "<" + TypeName(((SeqType)type).Arg) + ">.Empty";
- } else if (type is MapType) {
- return TypeName(type)+".Empty";
- } else if (type is ArrowType) {
+ } else if (xType.IsTypeParameter) {
+ var udt = (UserDefinedType)xType;
+ string s = "default(@" + udt.FullCompileName;
+ if (udt.TypeArgs.Count != 0)
+ {
+ s += "<" + TypeNames(udt.TypeArgs, wr) + ">";
+ }
+ s += ")";
+ return s;
+ } else if (xType is SetType) {
+ return DafnySetClass + "<" + TypeName(((SetType)xType).Arg, wr) + ">.Empty";
+ } else if (xType is MultiSetType) {
+ return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)xType).Arg, wr) + ">.Empty";
+ } else if (xType is SeqType) {
+ return DafnySeqClass + "<" + TypeName(((SeqType)xType).Arg, wr) + ">.Empty";
+ } else if (xType is MapType) {
+ return TypeName(xType, wr) + ".Empty";
+ } else if (xType is ArrowType) {
return "null";
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
@@ -1137,59 +1371,61 @@ namespace Microsoft.Dafny { public class CheckHasNoAssumes_Visitor : BottomUpVisitor
{
readonly Compiler compiler;
- public CheckHasNoAssumes_Visitor(Compiler c) {
+ TextWriter wr;
+ public CheckHasNoAssumes_Visitor(Compiler c, TextWriter wr) {
Contract.Requires(c != null);
compiler = c;
+ this.wr = wr;
}
protected override void VisitOneStmt(Statement stmt) {
if (stmt is AssumeStmt) {
- compiler.Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line);
+ compiler.Error("an assume statement cannot be compiled (line {0})", wr, stmt.Tok.line);
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
if (s.AssumeToken != null) {
- compiler.Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);
+ compiler.Error("an assume statement cannot be compiled (line {0})", wr, s.AssumeToken.line);
}
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
if (s.Body == null) {
- compiler.Error("a forall statement without a body cannot be compiled (line {0})", stmt.Tok.line);
+ compiler.Error("a forall statement without a body cannot be compiled (line {0})", wr, stmt.Tok.line);
}
} else if (stmt is WhileStmt) {
var s = (WhileStmt)stmt;
if (s.Body == null) {
- compiler.Error("a while statement without a body cannot be compiled (line {0})", stmt.Tok.line);
+ compiler.Error("a while statement without a body cannot be compiled (line {0})", wr, stmt.Tok.line);
}
}
}
}
- void TrStmt(Statement stmt, int indent)
+ TextWriter TrStmt(Statement stmt, int indent)
{
Contract.Requires(stmt != null);
+ TextWriter wr = new StringWriter();
if (stmt.IsGhost) {
- var v = new CheckHasNoAssumes_Visitor(this);
+ var v = new CheckHasNoAssumes_Visitor(this, wr);
v.Visit(stmt);
- Indent(indent); wr.WriteLine("{ }");
- return;
+ Indent(indent, wr); wr.WriteLine("{ }");
+ return wr;
}
-
if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
foreach (var arg in s.Args) {
- Indent(indent);
+ Indent(indent, wr);
wr.Write("System.Console.Write(");
- TrExpr(arg);
+ TrExpr(arg, wr, false);
wr.WriteLine(");");
}
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.Data.AssignUniqueId("after_", idGenerator));
} else if (stmt is ProduceStmt) {
var s = (ProduceStmt)stmt;
if (s.hiddenUpdate != null)
- TrStmt(s.hiddenUpdate, indent);
- Indent(indent);
+ wr.Write(TrStmt(s.hiddenUpdate, indent).ToString());
+ Indent(indent, wr);
if (s is YieldStmt) {
wr.WriteLine("yield return null;");
} else {
@@ -1199,7 +1435,7 @@ namespace Microsoft.Dafny { var s = (UpdateStmt)stmt;
var resolved = s.ResolvedStatements;
if (resolved.Count == 1) {
- TrStmt(resolved[0], indent);
+ wr.Write(TrStmt(resolved[0], indent).ToString());
} else {
// multi-assignment
Contract.Assert(s.Lhss.Count == resolved.Count);
@@ -1211,17 +1447,17 @@ namespace Microsoft.Dafny { var lhs = s.Lhss[i];
var rhs = s.Rhss[i];
if (!(rhs is HavocRhs)) {
- lvalues.Add(CreateLvalue(lhs, indent));
+ lvalues.Add(CreateLvalue(lhs, indent, wr));
string target = idGenerator.FreshId("_rhs");
rhss.Add(target);
- TrRhs("var " + target, null, rhs, indent);
+ TrRhs("var " + target, null, rhs, indent, wr);
}
}
}
Contract.Assert(lvalues.Count == rhss.Count);
for (int i = 0; i < lvalues.Count; i++) {
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("{0} = {1};", lvalues[i], rhss[i]);
}
}
@@ -1229,32 +1465,32 @@ namespace Microsoft.Dafny { } else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
Contract.Assert(!(s.Lhs is SeqSelectExpr) || ((SeqSelectExpr)s.Lhs).SelectOne); // multi-element array assignments are not allowed
- TrRhs(null, s.Lhs, s.Rhs, indent);
+ TrRhs(null, s.Lhs, s.Rhs, indent, wr);
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
if (s.AssumeToken != null) {
// Note, a non-ghost AssignSuchThatStmt may contain an assume
- Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);
+ Error("an assume statement cannot be compiled (line {0})", wr, s.AssumeToken.line);
} else if (s.MissingBounds != null) {
foreach (var bv in s.MissingBounds) {
- Error("this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", bv.Name, s.Tok.line);
+ Error("this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", wr, bv.Name, s.Tok.line);
}
} else {
Contract.Assert(s.Bounds != null); // follows from s.MissingBounds == null
TrAssignSuchThat(indent,
s.Lhss.ConvertAll(lhs => ((IdentifierExpr)lhs.Resolved).Var), // the resolver allows only IdentifierExpr left-hand sides
- s.Expr, s.Bounds, s.Tok.line);
+ s.Expr, s.Bounds, s.Tok.line, wr, false);
}
} else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
- TrCallStmt(s, null, indent);
+ wr.Write(TrCallStmt(s, null, indent).ToString());
} else if (stmt is BlockStmt) {
- Indent(indent); wr.WriteLine("{");
- TrStmtList(((BlockStmt)stmt).Body, indent);
- Indent(indent); wr.WriteLine("}");
+ Indent(indent, wr); wr.WriteLine("{");
+ TrStmtList(((BlockStmt)stmt).Body, indent, wr);
+ Indent(indent, wr); wr.WriteLine("}");
} else if (stmt is IfStmt) {
IfStmt s = (IfStmt)stmt;
@@ -1263,37 +1499,45 @@ namespace Microsoft.Dafny { if (s.Els == null) {
// let's compile the "else" branch, since that involves no work
// (still, let's leave a marker in the source code to indicate that this is what we did)
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("if (!false) { }");
} else {
// let's compile the "then" branch
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("if (true)");
- TrStmt(s.Thn, indent);
+ wr.Write(TrStmt(s.Thn, indent).ToString());
}
} else {
- Indent(indent); wr.Write("if (");
- TrExpr(s.Guard);
+ Indent(indent, wr); wr.Write("if (");
+ TrExpr(s.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)s.Guard, "eg_d", new Translator(null)) : s.Guard, wr, false);
wr.WriteLine(")");
- TrStmt(s.Thn, indent);
+ // We'd like to do "TrStmt(s.Thn, indent)", except we want the scope of any existential variables to come inside the block
+ Indent(indent, wr); wr.WriteLine("{");
+ if (s.IsExistentialGuard) {
+ IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)s.Guard, wr);
+ }
+ TrStmtList(s.Thn.Body, indent, wr);
+ Indent(indent, wr); wr.WriteLine("}");
+
if (s.Els != null) {
- Indent(indent); wr.WriteLine("else");
- TrStmt(s.Els, indent);
+ Indent(indent, wr); wr.WriteLine("else");
+ wr.Write(TrStmt(s.Els, indent).ToString());
}
}
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
- foreach (var alternative in s.Alternatives) {
- }
- Indent(indent);
+ Indent(indent, wr);
foreach (var alternative in s.Alternatives) {
wr.Write("if (");
- TrExpr(alternative.Guard);
+ TrExpr(alternative.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)alternative.Guard, "eg_d", new Translator(null)) : alternative.Guard, wr, false);
wr.WriteLine(") {");
- TrStmtList(alternative.Body, indent);
- Indent(indent);
+ if (alternative.IsExistentialGuard) {
+ IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)alternative.Guard, wr);
+ }
+ TrStmtList(alternative.Body, indent, wr);
+ Indent(indent, wr);
wr.Write("} else ");
}
wr.WriteLine("{ /*unreachable alternative*/ }");
@@ -1301,38 +1545,38 @@ namespace Microsoft.Dafny { } else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
if (s.Body == null) {
- return;
+ return wr;
}
if (s.Guard == null) {
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("while (false) { }");
} else {
- Indent(indent);
+ Indent(indent, wr);
wr.Write("while (");
- TrExpr(s.Guard);
+ TrExpr(s.Guard, wr, false);
wr.WriteLine(")");
- TrStmt(s.Body, indent);
+ wr.Write(TrStmt(s.Body, indent).ToString());
}
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
if (s.Alternatives.Count != 0) {
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("while (true) {");
int ind = indent + IndentAmount;
foreach (var alternative in s.Alternatives) {
}
- Indent(ind);
+ Indent(ind, wr);
foreach (var alternative in s.Alternatives) {
wr.Write("if (");
- TrExpr(alternative.Guard);
+ TrExpr(alternative.Guard, wr, false);
wr.WriteLine(") {");
- TrStmtList(alternative.Body, ind);
- Indent(ind);
+ TrStmtList(alternative.Body, ind, wr);
+ Indent(ind, wr);
wr.Write("} else ");
}
wr.WriteLine("{ break; }");
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("}");
}
@@ -1340,17 +1584,17 @@ namespace Microsoft.Dafny { var s = (ForallStmt)stmt;
if (s.Kind != ForallStmt.ParBodyKind.Assign) {
// Call and Proof have no side effects, so they can simply be optimized away.
- return;
+ return wr;
} else if (s.BoundVars.Count == 0) {
// the bound variables just spell out a single point, so the forall statement is equivalent to one execution of the body
- TrStmt(s.Body, indent);
- return;
+ wr.Write(TrStmt(s.Body, indent).ToString());
+ return wr;
}
var s0 = (AssignStmt)s.S0;
if (s0.Rhs is HavocRhs) {
// The forall statement says to havoc a bunch of things. This can be efficiently compiled
// into doing nothing.
- return;
+ return wr;
}
var rhs = ((ExprRhs)s0.Rhs).Expr;
@@ -1394,29 +1638,29 @@ namespace Microsoft.Dafny { if (s0.Lhs is MemberSelectExpr) {
var lhs = (MemberSelectExpr)s0.Lhs;
L = 2;
- tupleTypeArgs = TypeName(lhs.Obj.Type);
+ tupleTypeArgs = TypeName(lhs.Obj.Type, wr);
} else if (s0.Lhs is SeqSelectExpr) {
var lhs = (SeqSelectExpr)s0.Lhs;
L = 3;
// note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple
- tupleTypeArgs = TypeName(lhs.Seq.Type) + ",int";
+ tupleTypeArgs = TypeName(lhs.Seq.Type, wr) + ",int";
} else {
var lhs = (MultiSelectExpr)s0.Lhs;
L = 2 + lhs.Indices.Count;
if (8 < L) {
- Error("compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements");
- return;
+ Error("compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements", wr);
+ return wr;
}
- tupleTypeArgs = TypeName(lhs.Array.Type);
+ tupleTypeArgs = TypeName(lhs.Array.Type, wr);
for (int i = 0; i < lhs.Indices.Count; i++) {
// note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple
tupleTypeArgs += ",int";
}
}
- tupleTypeArgs += "," + TypeName(rhs.Type);
+ tupleTypeArgs += "," + TypeName(rhs.Type, wr);
// declare and construct "ingredients"
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("var {0} = new System.Collections.Generic.List<System.Tuple<{1}>>();", ingredients, tupleTypeArgs);
var n = s.BoundVars.Count;
@@ -1426,31 +1670,38 @@ namespace Microsoft.Dafny { var bound = s.Bounds[i];
var bv = s.BoundVars[i];
if (bound is ComprehensionExpr.BoolBoundedPool) {
- Indent(ind);
+ Indent(ind, wr);
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ Indent(ind, wr);
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
- Indent(ind);
- wr.Write("for (var @{0} = ", bv.CompileName);
- TrExpr(b.LowerBound);
- wr.Write("; @{0} < ", bv.CompileName);
- TrExpr(b.UpperBound);
- wr.Write("; @{0}++) {{ ", bv.CompileName);
+ Indent(ind, wr);
+ if (AsNativeType(bv.Type) != null) {
+ wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName);
+ } else {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);
+ }
+ TrExpr(b.LowerBound, wr, false);
+ wr.Write(", ");
+ TrExpr(b.UpperBound, wr, false);
+ wr.Write(")) { ");
} else if (bound is ComprehensionExpr.SetBoundedPool) {
var b = (ComprehensionExpr.SetBoundedPool)bound;
- Indent(ind);
+ Indent(ind, wr);
wr.Write("foreach (var @{0} in (", bv.CompileName);
- TrExpr(b.Set);
+ TrExpr(b.Set, wr, false);
wr.Write(").Elements) { ");
} else if (bound is ComprehensionExpr.SeqBoundedPool) {
var b = (ComprehensionExpr.SeqBoundedPool)bound;
- Indent(ind);
+ Indent(ind, wr);
wr.Write("foreach (var @{0} in (", bv.CompileName);
- TrExpr(b.Seq);
+ TrExpr(b.Seq, wr, false);
wr.Write(").UniqueElements) { ");
} else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
var b = (ComprehensionExpr.DatatypeBoundedPool)bound;
- wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));
+ wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type, wr));
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
}
@@ -1460,55 +1711,55 @@ namespace Microsoft.Dafny { // if (range) {
// ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));
// }
- Indent(indent + n * IndentAmount);
+ Indent(indent + n * IndentAmount, wr);
wr.Write("if (");
foreach (var bv in s.BoundVars) {
if (bv.Type.NormalizeExpand() is NatType) {
wr.Write("0 <= {0} && ", bv.CompileName);
}
}
- TrExpr(s.Range);
+ TrExpr(s.Range, wr, false);
wr.WriteLine(") {");
var indFinal = indent + (n + 1) * IndentAmount;
- Indent(indFinal);
+ Indent(indFinal, wr);
wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs);
if (s0.Lhs is MemberSelectExpr) {
var lhs = (MemberSelectExpr)s0.Lhs;
- TrExpr(lhs.Obj);
+ TrExpr(lhs.Obj, wr, false);
} else if (s0.Lhs is SeqSelectExpr) {
var lhs = (SeqSelectExpr)s0.Lhs;
- TrExpr(lhs.Seq);
+ TrExpr(lhs.Seq, wr, false);
wr.Write(", (int)(");
- TrExpr(lhs.E0);
+ TrExpr(lhs.E0, wr, false);
wr.Write(")");
} else {
var lhs = (MultiSelectExpr)s0.Lhs;
- TrExpr(lhs.Array);
+ TrExpr(lhs.Array, wr, false);
for (int i = 0; i < lhs.Indices.Count; i++) {
wr.Write(", (int)(");
- TrExpr(lhs.Indices[i]);
+ TrExpr(lhs.Indices[i], wr, false);
wr.Write(")");
}
}
wr.Write(", ");
- TrExpr(rhs);
+ TrExpr(rhs, wr, false);
wr.WriteLine("));");
- Indent(indent + n * IndentAmount);
+ Indent(indent + n * IndentAmount, wr);
wr.WriteLine("}");
for (int i = n; 0 <= --i; ) {
- Indent(indent + i * IndentAmount);
+ Indent(indent + i * IndentAmount, wr);
wr.WriteLine("}");
}
// foreach (L-Tuple l in ingredients) {
// LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1);
// }
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("foreach (var {0} in {1}) {{", tup, ingredients);
- Indent(indent + IndentAmount);
+ Indent(indent + IndentAmount, wr);
if (s0.Lhs is MemberSelectExpr) {
var lhs = (MemberSelectExpr)s0.Lhs;
wr.WriteLine("{0}.Item1.@{1} = {0}.Item2;", tup, lhs.MemberName);
@@ -1525,7 +1776,7 @@ namespace Microsoft.Dafny { }
wr.WriteLine("] = {0}.Item{1};", tup, L);
}
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("}");
} else if (stmt is MatchStmt) {
@@ -1542,42 +1793,64 @@ namespace Microsoft.Dafny { // }
if (s.Cases.Count != 0) {
string source = idGenerator.FreshId("_source");
- Indent(indent);
- wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type)), source);
- TrExpr(s.Source);
+ Indent(indent, wr);
+ wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type), wr), source);
+ TrExpr(s.Source, wr, false);
wr.WriteLine(";");
int i = 0;
var sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand();
foreach (MatchCaseStmt mc in s.Cases) {
- MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);
- TrStmtList(mc.Body, indent);
+ MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent, wr);
+ TrStmtList(mc.Body, indent, wr);
i++;
}
- Indent(indent); wr.WriteLine("}");
+ Indent(indent, wr); wr.WriteLine("}");
}
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
foreach (var local in s.Locals) {
- TrLocalVar(local, true, indent);
+ TrLocalVar(local, true, indent, wr);
}
if (s.Update != null) {
- TrStmt(s.Update, indent);
+ wr.Write(TrStmt(s.Update, indent).ToString());
}
+ } else if (stmt is LetStmt) {
+ var s = (LetStmt)stmt;
+ for (int i = 0; i < s.LHSs.Count; i++) {
+ var lhs = s.LHSs[i];
+ if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {
+ TrCasePatternOpt(lhs, s.RHSs[i], null, indent, wr, false);
+ }
+ }
} else if (stmt is ModifyStmt) {
var s = (ModifyStmt)stmt;
if (s.Body != null) {
- TrStmt(s.Body, indent);
+ wr.Write(TrStmt(s.Body, indent).ToString());
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
+
+ return wr;
}
- private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine) {
+ private void IntroduceAndAssignBoundVars(int indent, ExistsExpr exists, TextWriter wr) {
+ Contract.Requires(0 <= indent);
+ Contract.Requires(exists != null);
+ Contract.Assume(exists.Bounds != null); // follows from successful resolution
+ Contract.Assert(exists.Range == null); // follows from invariant of class IfStmt
+ foreach (var bv in exists.BoundVars) {
+ TrLocalVar(bv, false, indent, wr);
+ }
+ var ivars = exists.BoundVars.ConvertAll(bv => (IVariable)bv);
+ TrAssignSuchThat(indent, ivars, exists.Term, exists.Bounds, exists.tok.line, wr, false);
+ }
+
+ private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine, TextWriter wr, bool inLetExprBody) {
Contract.Requires(0 <= indent);
Contract.Requires(lhss != null);
Contract.Requires(constraint != null);
@@ -1619,7 +1892,7 @@ namespace Microsoft.Dafny { int ind = indent;
bool needIterLimit = lhss.Count != 1 && bounds.Exists(bnd => !bnd.IsFinite);
if (needIterLimit) {
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("for (var {0} = new BigInteger(5); ; {0} *= 2) {{", iterLimit);
ind += IndentAmount;
}
@@ -1628,89 +1901,87 @@ namespace Microsoft.Dafny { var bound = bounds[i];
var bv = lhss[i];
if (needIterLimit) {
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("var {0}_{1} = {0};", iterLimit, i);
}
var tmpVar = idGenerator.FreshId("_assign_such_that_");
- Indent(ind);
+ Indent(ind, wr);
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllChars) {{ @{1} = {0};", tmpVar, bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
- // (tmpVar is not used in this case)
- if (b.LowerBound != null) {
- wr.Write("@{0} = ", bv.CompileName);
- TrExpr(b.LowerBound);
- wr.WriteLine(";");
- Indent(ind);
- if (b.UpperBound != null) {
- wr.Write("for (; @{0} < ", bv.CompileName);
- TrExpr(b.UpperBound);
- wr.WriteLine("; @{0}++) {{ ", bv.CompileName);
- } else {
- wr.WriteLine("for (;; @{0}++) {{ ", bv.CompileName);
- }
+ if (AsNativeType(bv.Type) != null) {
+ wr.Write("foreach (var @{0} in @{1}.IntegerRange(", tmpVar, bv.Type.AsNewtype.FullCompileName);
} else {
- Contract.Assert(b.UpperBound != null);
- wr.Write("@{0} = ", bv.CompileName);
- TrExpr(b.UpperBound);
- wr.WriteLine(";");
- Indent(ind);
- wr.WriteLine("for (;; @{0}--) {{ ", bv.CompileName);
+ wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", tmpVar);
+ }
+ if (b.LowerBound == null) {
+ wr.Write("null");
+ } else {
+ TrExpr(b.LowerBound, wr, inLetExprBody);
+ }
+ wr.Write(", ");
+ if (b.UpperBound == null) {
+ wr.Write("null");
+ } else {
+ TrExpr(b.UpperBound, wr, inLetExprBody);
}
+ wr.WriteLine(")) {{ @{1} = {0};", tmpVar, bv.CompileName);
} else if (bound is AssignSuchThatStmt.WiggleWaggleBound) {
wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllIntegers) {{ @{1} = {0};", tmpVar, bv.CompileName);
} else if (bound is ComprehensionExpr.SetBoundedPool) {
var b = (ComprehensionExpr.SetBoundedPool)bound;
wr.Write("foreach (var {0} in (", tmpVar);
- TrExpr(b.Set);
+ TrExpr(b.Set, wr, inLetExprBody);
wr.WriteLine(").Elements) {{ @{0} = {1};", bv.CompileName, tmpVar);
} else if (bound is ComprehensionExpr.SubSetBoundedPool) {
var b = (ComprehensionExpr.SubSetBoundedPool)bound;
wr.Write("foreach (var {0} in (", tmpVar);
- TrExpr(b.UpperBound);
+ TrExpr(b.UpperBound, wr, inLetExprBody);
wr.WriteLine(").AllSubsets) {{ @{0} = {1};", bv.CompileName, tmpVar);
} else if (bound is ComprehensionExpr.MapBoundedPool) {
var b = (ComprehensionExpr.MapBoundedPool)bound;
wr.Write("foreach (var {0} in (", tmpVar);
- TrExpr(b.Map);
+ TrExpr(b.Map, wr, inLetExprBody);
wr.WriteLine(").Domain) {{ @{0} = {1};", bv.CompileName, tmpVar);
} else if (bound is ComprehensionExpr.SeqBoundedPool) {
var b = (ComprehensionExpr.SeqBoundedPool)bound;
wr.Write("foreach (var {0} in (", tmpVar);
- TrExpr(b.Seq);
+ TrExpr(b.Seq, wr, inLetExprBody);
wr.WriteLine(").Elements) {{ @{0} = {1};", bv.CompileName, tmpVar);
} else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
var b = (ComprehensionExpr.DatatypeBoundedPool)bound;
- wr.WriteLine("foreach (var {0} in {1}.AllSingletonConstructors) {{ @{2} = {0};", tmpVar, TypeName(bv.Type), bv.CompileName);
+ wr.WriteLine("foreach (var {0} in {1}.AllSingletonConstructors) {{ @{2} = {0};", tmpVar, TypeName(bv.Type, wr), bv.CompileName);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
}
if (needIterLimit) {
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("if ({0}_{1} == 0) {{ break; }} {0}_{1}--;", iterLimit, i);
}
}
- Indent(ind);
+ Indent(ind, wr);
wr.Write("if (");
- TrExpr(constraint);
+ TrExpr(constraint, wr, inLetExprBody);
wr.WriteLine(") {");
- Indent(ind + IndentAmount);
+ Indent(ind + IndentAmount, wr);
wr.WriteLine("goto {0};", doneLabel);
- Indent(ind);
+ Indent(ind, wr);
wr.WriteLine("}");
- Indent(indent);
+ Indent(indent, wr);
for (int i = 0; i < n; i++) {
wr.Write(i == 0 ? "}" : " }");
}
wr.WriteLine(needIterLimit ? " }" : "");
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("throw new System.Exception(\"assign-such-that search produced no value (line {0})\");", debuginfoLine);
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("{0}: ;", doneLabel);
}
- string CreateLvalue(Expression lhs, int indent) {
+ string CreateLvalue(Expression lhs, int indent, TextWriter wr) {
lhs = lhs.Resolved;
if (lhs is IdentifierExpr) {
var ll = (IdentifierExpr)lhs;
@@ -1718,9 +1989,9 @@ namespace Microsoft.Dafny { } else if (lhs is MemberSelectExpr) {
var ll = (MemberSelectExpr)lhs;
string obj = idGenerator.FreshId("_obj");
- Indent(indent);
+ Indent(indent, wr);
wr.Write("var {0} = ", obj);
- TrExpr(ll.Obj);
+ TrExpr(ll.Obj, wr, false);
wr.WriteLine(";");
return string.Format("{0}.@{1}", obj, ll.Member.CompileName);
} else if (lhs is SeqSelectExpr) {
@@ -1728,31 +1999,31 @@ namespace Microsoft.Dafny { var c = idGenerator.FreshNumericId("_arr+_index");
string arr = "_arr" + c;
string index = "_index" + c;
- Indent(indent);
+ Indent(indent, wr);
wr.Write("var {0} = ", arr);
- TrExpr(ll.Seq);
+ TrExpr(ll.Seq, wr, false);
wr.WriteLine(";");
- Indent(indent);
+ Indent(indent, wr);
wr.Write("var {0} = ", index);
- TrExpr(ll.E0);
+ TrExpr(ll.E0, wr, false);
wr.WriteLine(";");
return string.Format("{0}[(int){1}]", arr, index);
} else {
var ll = (MultiSelectExpr)lhs;
var c = idGenerator.FreshNumericId("_arr+_index");
string arr = "_arr" + c;
- Indent(indent);
+ Indent(indent, wr);
wr.Write("var {0} = ", arr);
- TrExpr(ll.Array);
+ TrExpr(ll.Array, wr, false);
wr.WriteLine(";");
string fullString = arr + "[";
string sep = "";
int i = 0;
foreach (var idx in ll.Indices) {
string index = "_index" + i + "_" + c;
- Indent(indent);
+ Indent(indent, wr);
wr.Write("var {0} = ", index);
- TrExpr(idx);
+ TrExpr(idx, wr, false);
wr.WriteLine(";");
fullString += sep + "(int)" + index;
sep = ", ";
@@ -1762,21 +2033,21 @@ namespace Microsoft.Dafny { }
}
- void TrRhs(string target, Expression targetExpr, AssignmentRhs rhs, int indent) {
+ void TrRhs(string target, Expression targetExpr, AssignmentRhs rhs, int indent, TextWriter wr) {
Contract.Requires((target == null) != (targetExpr == null));
var tRhs = rhs as TypeRhs;
if (tRhs != null && tRhs.InitCall != null) {
string nw = idGenerator.FreshId("_nw");
- Indent(indent);
+ Indent(indent, wr);
wr.Write("var {0} = ", nw);
- TrAssignmentRhs(rhs); // in this case, this call will not require us to spill any let variables first
+ TrAssignmentRhs(rhs, wr); // in this case, this call will not require us to spill any let variables first
wr.WriteLine(";");
- TrCallStmt(tRhs.InitCall, nw, indent);
- Indent(indent);
+ wr.Write(TrCallStmt(tRhs.InitCall, nw, indent).ToString());
+ Indent(indent, wr);
if (target != null) {
wr.Write(target);
} else {
- TrExpr(targetExpr);
+ TrExpr(targetExpr, wr, false);
}
wr.WriteLine(" = {0};", nw);
} else if (rhs is HavocRhs) {
@@ -1787,22 +2058,23 @@ namespace Microsoft.Dafny { foreach (Expression dim in tRhs.ArrayDimensions) {
}
}
- Indent(indent);
+ Indent(indent, wr);
if (target != null) {
wr.Write(target);
} else {
- TrExpr(targetExpr);
+ TrExpr(targetExpr, wr, false);
}
wr.Write(" = ");
- TrAssignmentRhs(rhs);
+ TrAssignmentRhs(rhs, wr);
wr.WriteLine(";");
}
}
- void TrCallStmt(CallStmt s, string receiverReplacement, int indent) {
+ TextWriter TrCallStmt(CallStmt s, string receiverReplacement, int indent) {
Contract.Requires(s != null);
Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved
+ StringWriter wr = new StringWriter();
if (s.Method == enclosingMethod && enclosingMethod.IsTailRecursive) {
// compile call as tail-recursive
@@ -1819,9 +2091,9 @@ namespace Microsoft.Dafny { string inTmp = idGenerator.FreshId("_in");
inTmps.Add(inTmp);
- Indent(indent);
+ Indent(indent, wr);
wr.Write("var {0} = ", inTmp);
- TrExpr(s.Receiver);
+ TrExpr(s.Receiver, wr, false);
wr.WriteLine(";");
}
for (int i = 0; i < s.Method.Ins.Count; i++) {
@@ -1829,29 +2101,29 @@ namespace Microsoft.Dafny { if (!p.IsGhost) {
string inTmp = idGenerator.FreshId("_in");
inTmps.Add(inTmp);
- Indent(indent);
+ Indent(indent, wr);
wr.Write("var {0} = ", inTmp);
- TrExpr(s.Args[i]);
+ TrExpr(s.Args[i], wr, false);
wr.WriteLine(";");
}
}
// Now, assign to the formals
int n = 0;
if (!s.Method.IsStatic) {
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("_this = {0};", inTmps[n]);
n++;
}
foreach (var p in s.Method.Ins) {
if (!p.IsGhost) {
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("{0} = {1};", p.CompileName, inTmps[n]);
n++;
}
}
Contract.Assert(n == inTmps.Count);
// finally, the jump back to the head of the method
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("goto TAIL_CALL_START;");
} else {
@@ -1862,7 +2134,7 @@ namespace Microsoft.Dafny { for (int i = 0; i < s.Method.Outs.Count; i++) {
Formal p = s.Method.Outs[i];
if (!p.IsGhost) {
- lvalues.Add(CreateLvalue(s.Lhs[i], indent));
+ lvalues.Add(CreateLvalue(s.Lhs[i], indent, wr));
}
}
var outTmps = new List<string>();
@@ -1871,8 +2143,8 @@ namespace Microsoft.Dafny { if (!p.IsGhost) {
string target = idGenerator.FreshId("_out");
outTmps.Add(target);
- Indent(indent);
- wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);
+ Indent(indent, wr);
+ wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type, wr), target);
}
}
Contract.Assert(lvalues.Count == outTmps.Count);
@@ -1883,14 +2155,14 @@ namespace Microsoft.Dafny { }
}
if (receiverReplacement != null) {
- Indent(indent);
+ Indent(indent, wr);
wr.Write("@" + receiverReplacement);
} else if (s.Method.IsStatic) {
- Indent(indent);
- wr.Write(TypeName_Companion(s.Receiver.Type));
+ Indent(indent, wr);
+ wr.Write(TypeName_Companion(s.Receiver.Type, wr));
} else {
- Indent(indent);
- TrParenExpr(s.Receiver);
+ Indent(indent, wr);
+ TrParenExpr(s.Receiver, wr, false);
}
wr.Write(".@{0}(", s.Method.CompileName);
@@ -1899,7 +2171,7 @@ namespace Microsoft.Dafny { Formal p = s.Method.Ins[i];
if (!p.IsGhost) {
wr.Write(sep);
- TrExpr(s.Args[i]);
+ TrExpr(s.Args[i], wr, false);
sep = ", ";
}
}
@@ -1912,44 +2184,45 @@ namespace Microsoft.Dafny { // assign to the actual LHSs
for (int j = 0; j < lvalues.Count; j++) {
- Indent(indent);
+ Indent(indent, wr);
wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);
}
}
+ return wr;
}
/// <summary>
/// Before calling TrAssignmentRhs(rhs), the caller must have spilled the let variables declared in "rhs".
/// </summary>
- void TrAssignmentRhs(AssignmentRhs rhs) {
+ void TrAssignmentRhs(AssignmentRhs rhs, TextWriter wr) {
Contract.Requires(rhs != null);
Contract.Requires(!(rhs is HavocRhs));
if (rhs is ExprRhs) {
ExprRhs e = (ExprRhs)rhs;
- TrExpr(e.Expr);
+ TrExpr(e.Expr, wr, false);
} else {
TypeRhs tp = (TypeRhs)rhs;
if (tp.ArrayDimensions == null) {
- wr.Write("new {0}()", TypeName(tp.EType));
+ wr.Write("new {0}()", TypeName(tp.EType, wr));
} else {
if (tp.EType.IsIntegerType || 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}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType));
+ wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType, wr));
string prefix = "(";
foreach (Expression dim in tp.ArrayDimensions) {
wr.Write(prefix);
- TrParenExpr(dim);
+ TrParenExpr(dim, wr, false);
prefix = ", ";
}
wr.Write(")");
} else {
- wr.Write("new {0}", TypeName(tp.EType));
+ wr.Write("new {0}", TypeName(tp.EType, wr));
string prefix = "[";
foreach (Expression dim in tp.ArrayDimensions) {
wr.Write("{0}(int)", prefix);
- TrParenExpr(dim);
+ TrParenExpr(dim, wr, false);
prefix = ", ";
}
wr.Write("]");
@@ -1958,34 +2231,43 @@ namespace Microsoft.Dafny { }
}
- void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent) {Contract.Requires(cce.NonNullElements(stmts));
+ void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent, TextWriter writer) {Contract.Requires(cce.NonNullElements(stmts));
foreach (Statement ss in stmts) {
- TrStmt(ss, indent + IndentAmount);
+ copyInstrWriter.Clear();
+ TextWriter wr = TrStmt(ss, indent + IndentAmount);
+ // write out any copy instructions that copies the out param
+ // used in letexpr to a local
+ string copyInstr = copyInstrWriter.ToString();
+ if (copyInstr != "") {
+ Indent(indent + IndentAmount, writer);
+ writer.Write(copyInstrWriter.ToString());
+ }
+ writer.Write(wr.ToString());
if (ss.Labels != null) {
- Indent(indent); // labels are not indented as much as the statements
- wr.WriteLine("after_{0}: ;", ss.Labels.Data.AssignUniqueId("after_", idGenerator));
+ Indent(indent, writer); // labels are not indented as much as the statements
+ writer.WriteLine("after_{0}: ;", ss.Labels.Data.AssignUniqueId("after_", idGenerator));
}
}
}
- void TrLocalVar(LocalVariable s, bool alwaysInitialize, int indent) {
- Contract.Requires(s != null);
- if (s.IsGhost) {
+ void TrLocalVar(IVariable v, bool alwaysInitialize, int indent, TextWriter wr) {
+ Contract.Requires(v != null);
+ if (v.IsGhost) {
// only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)
return;
}
- Indent(indent);
- wr.Write("{0} @{1}", TypeName(s.Type), s.CompileName);
+ Indent(indent, wr);
+ wr.Write("{0} @{1}", TypeName(v.Type, wr), v.CompileName);
if (alwaysInitialize) {
// produce a default value
- wr.WriteLine(" = {0};", DefaultValue(s.Type));
+ wr.WriteLine(" = {0};", DefaultValue(v.Type, wr));
} else {
wr.WriteLine(";");
}
}
- void MatchCasePrelude(string source, UserDefinedType sourceType, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent) {
+ void MatchCasePrelude(string source, UserDefinedType sourceType, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent, TextWriter wr) {
Contract.Requires(source != null);
Contract.Requires(sourceType != null);
Contract.Requires(ctor != null);
@@ -1994,7 +2276,7 @@ namespace Microsoft.Dafny { // if (source.is_Ctor0) {
// FormalType f0 = ((Dt_Ctor0)source._D).a0;
// ...
- Indent(indent);
+ Indent(indent, wr);
wr.Write("{0}if (", caseIndex == 0 ? "" : "} else ");
if (caseIndex == caseCount - 1) {
wr.Write("true");
@@ -2009,9 +2291,9 @@ namespace Microsoft.Dafny { if (!arg.IsGhost) {
BoundVar bv = arguments[m];
// FormalType f0 = ((Dt_Ctor0)source._D).a0;
- Indent(indent + IndentAmount);
+ Indent(indent + IndentAmount, wr);
wr.WriteLine("{0} @{1} = (({2}){3}._D).@{4};",
- TypeName(bv.Type), bv.CompileName, DtCtorName(ctor, sourceType.TypeArgs), source, FormalName(arg, k));
+ TypeName(bv.Type, wr), bv.CompileName, DtCtorName(ctor, sourceType.TypeArgs, wr), source, FormalName(arg, k));
k++;
}
}
@@ -2022,51 +2304,51 @@ namespace Microsoft.Dafny { /// <summary>
/// Before calling TrParenExpr(expr), the caller must have spilled the let variables declared in "expr".
/// </summary>
- void TrParenExpr(string prefix, Expression expr) {
+ void TrParenExpr(string prefix, Expression expr, TextWriter wr, bool inLetExprBody) {
Contract.Requires(prefix != null);
Contract.Requires(expr != null);
wr.Write(prefix);
- TrParenExpr(expr);
+ TrParenExpr(expr, wr, inLetExprBody);
}
/// <summary>
/// Before calling TrParenExpr(expr), the caller must have spilled the let variables declared in "expr".
/// </summary>
- void TrParenExpr(Expression expr) {
+ void TrParenExpr(Expression expr, TextWriter wr, bool inLetExprBody) {
Contract.Requires(expr != null);
wr.Write("(");
- TrExpr(expr);
+ TrExpr(expr, wr, inLetExprBody);
wr.Write(")");
}
/// <summary>
/// Before calling TrExprList(exprs), the caller must have spilled the let variables declared in expressions in "exprs".
/// </summary>
- void TrExprList(List<Expression/*!*/>/*!*/ exprs) {
+ void TrExprList(List<Expression/*!*/>/*!*/ exprs, TextWriter wr, bool inLetExprBody) {
Contract.Requires(cce.NonNullElements(exprs));
wr.Write("(");
string sep = "";
foreach (Expression e in exprs) {
wr.Write(sep);
- TrExpr(e);
+ TrExpr(e, wr, inLetExprBody);
sep = ", ";
}
wr.Write(")");
}
- void TrExprPairList(List<ExpressionPair/*!*/>/*!*/ exprs) {
+ void TrExprPairList(List<ExpressionPair/*!*/>/*!*/ exprs, TextWriter wr, bool inLetExprBody) {
Contract.Requires(cce.NonNullElements(exprs));
wr.Write("(");
string sep = "";
foreach (ExpressionPair p in exprs) {
wr.Write(sep);
wr.Write("new Dafny.Pair<");
- wr.Write(TypeName(p.A.Type));
+ wr.Write(TypeName(p.A.Type, wr));
wr.Write(",");
- wr.Write(TypeName(p.B.Type));
+ wr.Write(TypeName(p.B.Type, wr));
wr.Write(">(");
- TrExpr(p.A);
+ TrExpr(p.A, wr, inLetExprBody);
wr.Write(",");
- TrExpr(p.B);
+ TrExpr(p.B, wr, inLetExprBody);
wr.Write(")");
sep = ", ";
}
@@ -2076,13 +2358,15 @@ namespace Microsoft.Dafny { /// <summary>
/// Before calling TrExpr(expr), the caller must have spilled the let variables declared in "expr".
/// </summary>
- void TrExpr(Expression expr)
+ void TrExpr(Expression expr, TextWriter wr, bool inLetExprBody)
{
Contract.Requires(expr != null);
if (expr is LiteralExpr) {
LiteralExpr e = (LiteralExpr)expr;
- if (e.Value == null) {
- wr.Write("({0})null", TypeName(e.Type));
+ if (e is StaticReceiverExpr) {
+ wr.Write(TypeName(e.Type, wr));
+ } else if (e.Value == null) {
+ wr.Write("({0})null", TypeName(e.Type, wr));
} else if (e.Value is bool) {
wr.Write((bool)e.Value ? "true" : "false");
} else if (e is CharLiteralExpr) {
@@ -2123,41 +2407,49 @@ namespace Microsoft.Dafny { } else if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
- wr.Write("@" + e.Var.CompileName);
-
+ if (e.Var is Formal && inLetExprBody && !((Formal)e.Var).InParam) {
+ // out param in letExpr body, need to copy it to a temp since
+ // letExpr body is translated to an anonymous function that doesn't
+ // allow out parameters
+ var name = string.Format("_pat_let_tv{0}", GetUniqueAstNumber(e));
+ wr.Write("@" + name);
+ copyInstrWriter.Append("var @" + name + "= @" + e.Var.CompileName + ";\n");
+ } else {
+ wr.Write("@" + e.Var.CompileName);
+ }
} else if (expr is SetDisplayExpr) {
var e = (SetDisplayExpr)expr;
var elType = e.Type.AsSetType.Arg;
- wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));
- TrExprList(e.Elements);
+ wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType, wr));
+ TrExprList(e.Elements, wr, inLetExprBody);
} else if (expr is MultiSetDisplayExpr) {
var e = (MultiSetDisplayExpr)expr;
var elType = e.Type.AsMultiSetType.Arg;
- wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));
- TrExprList(e.Elements);
+ wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType, wr));
+ TrExprList(e.Elements, wr, inLetExprBody);
} else if (expr is SeqDisplayExpr) {
var e = (SeqDisplayExpr)expr;
var elType = e.Type.AsSeqType.Arg;
- wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));
- TrExprList(e.Elements);
+ wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType, wr));
+ TrExprList(e.Elements, wr, inLetExprBody);
} else if (expr is MapDisplayExpr) {
MapDisplayExpr e = (MapDisplayExpr)expr;
- wr.Write("{0}.FromElements", TypeName(e.Type));
- TrExprPairList(e.Elements);
+ wr.Write("{0}.FromElements", TypeName(e.Type, wr));
+ TrExprPairList(e.Elements, wr, inLetExprBody);
} else if (expr is MemberSelectExpr) {
MemberSelectExpr e = (MemberSelectExpr)expr;
SpecialField sf = e.Member as SpecialField;
if (sf != null) {
wr.Write(sf.PreString);
- TrParenExpr(e.Obj);
+ TrParenExpr(e.Obj, wr, inLetExprBody);
wr.Write(".@{0}", sf.CompiledName);
wr.Write(sf.PostString);
} else {
- TrParenExpr(e.Obj);
+ TrExpr(e.Obj, wr, inLetExprBody);
wr.Write(".@{0}", e.Member.CompileName);
}
@@ -2167,50 +2459,50 @@ namespace Microsoft.Dafny { if (e.Seq.Type.IsArrayType) {
if (e.SelectOne) {
Contract.Assert(e.E0 != null && e.E1 == null);
- TrParenExpr(e.Seq);
+ TrParenExpr(e.Seq, wr, inLetExprBody);
wr.Write("[(int)");
- TrParenExpr(e.E0);
+ TrParenExpr(e.E0, wr, inLetExprBody);
wr.Write("]");
} else {
- TrParenExpr("Dafny.Helpers.SeqFromArray", e.Seq);
+ TrParenExpr("Dafny.Helpers.SeqFromArray", e.Seq, wr, inLetExprBody);
if (e.E1 != null) {
- TrParenExpr(".Take", e.E1);
+ TrParenExpr(".Take", e.E1, wr, inLetExprBody);
}
if (e.E0 != null) {
- TrParenExpr(".Drop", e.E0);
+ TrParenExpr(".Drop", e.E0, wr, inLetExprBody);
}
}
} else if (e.SelectOne) {
Contract.Assert(e.E0 != null && e.E1 == null);
- TrParenExpr(e.Seq);
- TrParenExpr(".Select", e.E0);
+ TrParenExpr(e.Seq, wr, inLetExprBody);
+ TrParenExpr(".Select", e.E0, wr, inLetExprBody);
} else {
- TrParenExpr(e.Seq);
+ TrParenExpr(e.Seq, wr, inLetExprBody);
if (e.E1 != null) {
- TrParenExpr(".Take", e.E1);
+ TrParenExpr(".Take", e.E1, wr, inLetExprBody);
}
if (e.E0 != null) {
- TrParenExpr(".Drop", e.E0);
+ TrParenExpr(".Drop", e.E0, wr, inLetExprBody);
}
}
} else if (expr is MultiSetFormingExpr) {
var e = (MultiSetFormingExpr)expr;
- wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg));
+ wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg, wr));
var eeType = e.E.Type.NormalizeExpand();
if (eeType is SeqType) {
- TrParenExpr(".FromSeq", e.E);
+ TrParenExpr(".FromSeq", e.E, wr, inLetExprBody);
} else if (eeType is SetType) {
- TrParenExpr(".FromSet", e.E);
+ TrParenExpr(".FromSet", e.E, wr, inLetExprBody);
} else {
Contract.Assert(false); throw new cce.UnreachableException();
}
} else if (expr is MultiSelectExpr) {
MultiSelectExpr e = (MultiSelectExpr)expr;
- TrParenExpr(e.Array);
+ TrParenExpr(e.Array, wr, inLetExprBody);
string prefix = "[";
foreach (Expression idx in e.Indices) {
wr.Write("{0}(int)", prefix);
- TrParenExpr(idx);
+ TrParenExpr(idx, wr, inLetExprBody);
prefix = ", ";
}
wr.Write("]");
@@ -2219,47 +2511,46 @@ namespace Microsoft.Dafny { SeqUpdateExpr e = (SeqUpdateExpr)expr;
if (e.ResolvedUpdateExpr != null)
{
- TrExpr(e.ResolvedUpdateExpr);
+ TrExpr(e.ResolvedUpdateExpr, wr, inLetExprBody);
}
else
{
- TrParenExpr(e.Seq);
+ TrParenExpr(e.Seq, wr, inLetExprBody);
wr.Write(".Update(");
- TrExpr(e.Index);
+ TrExpr(e.Index, wr, inLetExprBody);
wr.Write(", ");
- TrExpr(e.Value);
+ TrExpr(e.Value, wr, inLetExprBody);
wr.Write(")");
}
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
- CompileFunctionCallExpr(e, wr, TrExpr);
+ CompileFunctionCallExpr(e, wr, wr, inLetExprBody, TrExpr);
} else if (expr is ApplyExpr) {
var e = expr as ApplyExpr;
wr.Write("Dafny.Helpers.Id<");
- wr.Write(TypeName(e.Function.Type));
+ wr.Write(TypeName(e.Function.Type, wr));
wr.Write(">(");
- TrExpr(e.Function);
+ TrExpr(e.Function, wr, inLetExprBody);
wr.Write(")");
- TrExprList(e.Args);
+ TrExprList(e.Args, wr, inLetExprBody);
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved
- var typeParams = dtv.InferredTypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeNames(dtv.InferredTypeArgs));
-
- wr.Write("new {0}{1}(", DtName(dtv.Ctor.EnclosingDatatype), typeParams);
+ var typeParams = dtv.InferredTypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeNames(dtv.InferredTypeArgs, wr));
+ wr.Write("new @{0}{1}(", DtName(dtv.Ctor.EnclosingDatatype), typeParams);
if (!dtv.IsCoCall) {
// For an ordinary constructor (that is, one that does not guard any co-recursive calls), generate:
// new Dt_Cons<T>( args )
- wr.Write("new {0}(", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs));
+ wr.Write("new {0}(", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs, wr));
string sep = "";
for (int i = 0; i < dtv.Arguments.Count; i++) {
Formal formal = dtv.Ctor.Formals[i];
if (!formal.IsGhost) {
wr.Write(sep);
- TrExpr(dtv.Arguments[i]);
+ TrExpr(dtv.Arguments[i], wr, inLetExprBody);
sep = ", ";
}
}
@@ -2288,17 +2579,17 @@ namespace Microsoft.Dafny { arg = varName;
wr.Write("var {0} = ", varName);
- TrExpr(actual);
+ TrExpr(actual, wr, inLetExprBody);
wr.Write("; ");
} else {
var sw = new StringWriter();
- CompileFunctionCallExpr(fce, sw, (exp) => {
+ CompileFunctionCallExpr(fce, sw, wr, inLetExprBody, (exp, wrr, inLetExpr) => {
string varName = idGenerator.FreshId("_ac");
sw.Write(varName);
- wr.Write("var {0} = ", varName);
- TrExpr(exp);
- wr.Write("; ");
+ wrr.Write("var {0} = ", varName);
+ TrExpr(exp, wrr, inLetExpr);
+ wrr.Write("; ");
});
arg = sw.ToString();
@@ -2310,7 +2601,7 @@ namespace Microsoft.Dafny { wr.Write("return () => { return ");
- wr.Write("new {0}({1}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs), args);
+ wr.Write("new {0}({1}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs, wr), args);
wr.Write("); }; })())");
}
wr.Write(")");
@@ -2323,11 +2614,11 @@ namespace Microsoft.Dafny { switch (e.Op) {
case UnaryOpExpr.Opcode.Not:
wr.Write("!");
- TrParenExpr(e.E);
+ TrParenExpr(e.E, wr, inLetExprBody);
break;
case UnaryOpExpr.Opcode.Cardinality:
wr.Write("new BigInteger(");
- TrParenExpr(e.E);
+ TrParenExpr(e.E, wr, inLetExprBody);
wr.Write(".Length)");
break;
default:
@@ -2345,7 +2636,7 @@ namespace Microsoft.Dafny { if (AsNativeType(e.E.Type) != null) {
wr.Write("new BigInteger");
}
- TrParenExpr(e.E);
+ TrParenExpr(e.E, wr, inLetExprBody);
};
Action toIntCast = () => {
Contract.Assert(toInt);
@@ -2361,7 +2652,7 @@ namespace Microsoft.Dafny { } else if (!fromInt && toInt) {
// real -> int
toIntCast();
- TrParenExpr(e.E);
+ TrParenExpr(e.E, wr, inLetExprBody);
wr.Write(".ToBigInteger()");
} else if (AsNativeType(e.ToType) != null) {
toIntCast();
@@ -2373,14 +2664,14 @@ namespace Microsoft.Dafny { wr.Write("(" + (BigInteger)lit.Value + AsNativeType(e.ToType).Suffix + ")");
} else if ((u != null && u.Op == UnaryOpExpr.Opcode.Cardinality) || (m != null && m.MemberName == "Length" && m.Obj.Type.IsArrayType)) {
// Optimize .Length to avoid intermediate BigInteger
- TrParenExpr((u != null) ? u.E : m.Obj);
+ TrParenExpr((u != null) ? u.E : m.Obj, wr, inLetExprBody);
if (AsNativeType(e.ToType).UpperBound <= new BigInteger(0x80000000U)) {
wr.Write(".Length");
} else {
wr.Write(".LongLength");
}
} else {
- TrParenExpr(e.E);
+ TrParenExpr(e.E, wr, inLetExprBody);
}
} else if (e.ToType.IsIntegerType && AsNativeType(e.E.Type) != null) {
fromIntAsBigInteger();
@@ -2388,7 +2679,7 @@ namespace Microsoft.Dafny { Contract.Assert(fromInt == toInt);
Contract.Assert(AsNativeType(e.ToType) == null);
Contract.Assert(AsNativeType(e.E.Type) == null);
- TrParenExpr(e.E);
+ TrParenExpr(e.E, wr, inLetExprBody);
}
} else if (expr is BinaryExpr) {
@@ -2408,27 +2699,27 @@ namespace Microsoft.Dafny { opString = "&&"; break;
case BinaryExpr.ResolvedOpcode.EqCommon: {
- if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
- callString = "Equals";
- } else if (e.E0.Type.IsRefType) {
+ if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
// For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
// type parameter.
opString = "== (object)";
+ } else if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
+ callString = "Equals";
} else {
opString = "==";
}
break;
}
case BinaryExpr.ResolvedOpcode.NeqCommon: {
- if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
- preOpString = "!";
- callString = "Equals";
- } else if (e.E0.Type.IsRefType) {
+ if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
// For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
// type parameter.
opString = "!= (object)";
+ } else if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
+ preOpString = "!";
+ callString = "Equals";
} else {
opString = "!=";
}
@@ -2457,9 +2748,9 @@ namespace Microsoft.Dafny { if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) {
string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : "";
wr.Write("Dafny.Helpers.EuclideanDivision" + suffix + "(");
- TrParenExpr(e.E0);
+ TrParenExpr(e.E0, wr, inLetExprBody);
wr.Write(", ");
- TrExpr(e.E1);
+ TrExpr(e.E1, wr, inLetExprBody);
wr.Write(")");
} else {
opString = "/"; // for reals
@@ -2469,9 +2760,9 @@ namespace Microsoft.Dafny { if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) {
string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : "";
wr.Write("Dafny.Helpers.EuclideanModulus" + suffix + "(");
- TrParenExpr(e.E0);
+ TrParenExpr(e.E0, wr, inLetExprBody);
wr.Write(", ");
- TrExpr(e.E1);
+ TrExpr(e.E1, wr, inLetExprBody);
wr.Write(")");
} else {
opString = "%"; // for reals
@@ -2506,18 +2797,18 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.InSet:
case BinaryExpr.ResolvedOpcode.InMultiSet:
case BinaryExpr.ResolvedOpcode.InMap:
- TrParenExpr(e.E1);
+ TrParenExpr(e.E1, wr, inLetExprBody);
wr.Write(".Contains(");
- TrExpr(e.E0);
+ TrExpr(e.E0, wr, inLetExprBody);
wr.Write(")");
break;
case BinaryExpr.ResolvedOpcode.NotInSet:
case BinaryExpr.ResolvedOpcode.NotInMultiSet:
case BinaryExpr.ResolvedOpcode.NotInMap:
wr.Write("!");
- TrParenExpr(e.E1);
+ TrParenExpr(e.E1, wr, inLetExprBody);
wr.Write(".Contains(");
- TrExpr(e.E0);
+ TrExpr(e.E0, wr, inLetExprBody);
wr.Write(")");
break;
case BinaryExpr.ResolvedOpcode.Union:
@@ -2537,16 +2828,16 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.Concat:
callString = "Concat"; break;
case BinaryExpr.ResolvedOpcode.InSeq:
- TrParenExpr(e.E1);
+ TrParenExpr(e.E1, wr, inLetExprBody);
wr.Write(".Contains(");
- TrExpr(e.E0);
+ TrExpr(e.E0, wr, inLetExprBody);
wr.Write(")");
break;
case BinaryExpr.ResolvedOpcode.NotInSeq:
wr.Write("!");
- TrParenExpr(e.E1);
+ TrParenExpr(e.E1, wr, inLetExprBody);
wr.Write(".Contains(");
- TrExpr(e.E0);
+ TrExpr(e.E0, wr, inLetExprBody);
wr.Write(")");
break;
@@ -2560,17 +2851,17 @@ namespace Microsoft.Dafny { wr.Write("(" + nativeType.Name + ")(");
}
wr.Write(preOpString);
- TrParenExpr(e.E0);
+ TrParenExpr(e.E0, wr, inLetExprBody);
wr.Write(" {0} ", opString);
- TrParenExpr(e.E1);
+ TrParenExpr(e.E1, wr, inLetExprBody);
if (needsCast) {
wr.Write(")");
}
} else if (callString != null) {
wr.Write(preOpString);
- TrParenExpr(e.E0);
+ TrParenExpr(e.E0, wr, inLetExprBody);
wr.Write(".@{0}(", callString);
- TrExpr(e.E1);
+ TrExpr(e.E1, wr, inLetExprBody);
wr.Write(")");
}
@@ -2593,17 +2884,18 @@ namespace Microsoft.Dafny { if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {
var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);
wr.Write("Dafny.Helpers.Let<");
- wr.Write(TypeName(e.RHSs[i].Type) + "," + TypeName(e.Body.Type));
+ wr.Write(TypeName(e.RHSs[i].Type, wr) + "," + TypeName(e.Body.Type, wr));
wr.Write(">(");
- TrExpr(e.RHSs[i]);
+ TrExpr(e.RHSs[i], wr, inLetExprBody);
wr.Write(", " + rhsName + " => ");
neededCloseParens++;
- var c = TrCasePattern(lhs, rhsName, e.Body.Type);
+ var c = TrCasePattern(lhs, rhsName, e.Body.Type, wr);
Contract.Assert(c != 0); // we already checked that there's at least one non-ghost
neededCloseParens += c;
}
}
- TrExpr(e.Body);
+
+ TrExpr(e.Body, wr, true);
for (int i = 0; i < neededCloseParens; i++) {
wr.Write(")");
}
@@ -2612,7 +2904,7 @@ namespace Microsoft.Dafny { // ghost var x,y :| Constraint; E
// is compiled just like E is, because the resolver has already checked that x,y (or other ghost variables, for that matter) don't
// occur in E (moreover, the verifier has checked that values for x,y satisfying Constraint exist).
- TrExpr(e.Body);
+ TrExpr(e.Body, wr, inLetExprBody);
} else {
// The Dafny "let" expression
// var x,y :| Constraint; E
@@ -2627,17 +2919,17 @@ namespace Microsoft.Dafny { Contract.Assert(e.RHSs.Count == 1); // checked by resolution
if (e.Constraint_MissingBounds != null) {
foreach (var bv in e.Constraint_MissingBounds) {
- Error("this let-such-that expression is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", bv.Name, e.tok.line);
+ Error("this let-such-that expression is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", wr, bv.Name, e.tok.line);
}
} else {
- wr.Write("Dafny.Helpers.Let<int," + TypeName(e.Body.Type) + ">(0, _let_dummy_" + GetUniqueAstNumber(e) + " => {");
+ wr.Write("Dafny.Helpers.Let<int," + TypeName(e.Body.Type, wr) + ">(0, _let_dummy_" + GetUniqueAstNumber(e) + " => {");
foreach (var bv in e.BoundVars) {
- wr.Write("{0} @{1}", TypeName(bv.Type), bv.CompileName);
- wr.WriteLine(" = {0};", DefaultValue(bv.Type));
+ wr.Write("{0} @{1}", TypeName(bv.Type, wr), bv.CompileName);
+ wr.WriteLine(" = {0};", DefaultValue(bv.Type, wr));
}
- TrAssignSuchThat(0, new List<IVariable>(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line);
+ TrAssignSuchThat(0, new List<IVariable>(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line, wr, inLetExprBody);
wr.Write(" return ");
- TrExpr(e.Body);
+ TrExpr(e.Body, wr, true);
wr.Write("; })");
}
}
@@ -2657,7 +2949,7 @@ namespace Microsoft.Dafny { // }(src)
string source = idGenerator.FreshId("_source");
- wr.Write("new Dafny.Helpers.Function<{0}, {1}>(delegate ({0} {2}) {{ ", TypeName(e.Source.Type), TypeName(e.Type), source);
+ wr.Write("new Dafny.Helpers.Function<{0}, {1}>(delegate ({0} {2}) {{ ", TypeName(e.Source.Type, wr), TypeName(e.Type, wr), source);
if (e.Cases.Count == 0) {
// the verifier would have proved we never get here; still, we need some code that will compile
@@ -2666,9 +2958,9 @@ namespace Microsoft.Dafny { int i = 0;
var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();
foreach (MatchCaseExpr mc in e.Cases) {
- MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0);
+ MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0, wr);
wr.Write("return ");
- TrExpr(mc.Body);
+ TrExpr(mc.Body, wr, inLetExprBody);
wr.Write("; ");
i++;
}
@@ -2676,11 +2968,14 @@ namespace Microsoft.Dafny { }
// We end with applying the source expression to the delegate we just built
wr.Write("})(");
- TrExpr(e.Source);
+ TrExpr(e.Source, wr, inLetExprBody);
wr.Write(")");
} else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
+
+ // Compilation does not check whether a quantifier was split.
+
Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds
var n = e.BoundVars.Count;
Contract.Assert(e.Bounds.Count == n);
@@ -2690,27 +2985,29 @@ namespace Microsoft.Dafny { // emit: Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("Dafny.Helpers.QuantBool(");
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("Dafny.Helpers.QuantChar(");
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantInt(");
- TrExpr(b.LowerBound);
+ TrExpr(b.LowerBound, wr, inLetExprBody);
wr.Write(", ");
- TrExpr(b.UpperBound);
+ TrExpr(b.UpperBound, wr, inLetExprBody);
wr.Write(", ");
} else if (bound is ComprehensionExpr.SetBoundedPool) {
var b = (ComprehensionExpr.SetBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantSet(");
- TrExpr(b.Set);
+ TrExpr(b.Set, wr, inLetExprBody);
wr.Write(", ");
} else if (bound is ComprehensionExpr.MapBoundedPool) {
var b = (ComprehensionExpr.MapBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantMap(");
- TrExpr(b.Map);
+ TrExpr(b.Map, wr, inLetExprBody);
wr.Write(", ");
} else if (bound is ComprehensionExpr.SeqBoundedPool) {
var b = (ComprehensionExpr.SeqBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantSeq(");
- TrExpr(b.Seq);
+ TrExpr(b.Seq, wr, inLetExprBody);
wr.Write(", ");
} else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
var b = (ComprehensionExpr.DatatypeBoundedPool)bound;
@@ -2723,7 +3020,7 @@ namespace Microsoft.Dafny { wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");
wr.Write("@{0} => ", bv.CompileName);
}
- TrExpr(e.LogicalBody());
+ TrExpr(e.LogicalBody(true), wr, inLetExprBody);
for (int i = 0; i < n; i++) {
wr.Write(")");
}
@@ -2747,9 +3044,10 @@ namespace Microsoft.Dafny { // return Dafny.Set<G>.FromCollection(_coll);
// })()
Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds
- var typeName = TypeName(e.Type.AsSetType.Arg);
+ var typeName = TypeName(e.Type.AsSetType.Arg, wr);
+ var collection_name = idGenerator.FreshId("_coll");
wr.Write("((Dafny.Helpers.ComprehensionDelegate<{0}>)delegate() {{ ", typeName);
- wr.Write("var _coll = new System.Collections.Generic.List<{0}>(); ", typeName);
+ wr.Write("var {0} = new System.Collections.Generic.List<{1}>(); ", collection_name, typeName);
var n = e.BoundVars.Count;
Contract.Assert(e.Bounds.Count == n);
for (int i = 0; i < n; i++) {
@@ -2757,44 +3055,51 @@ namespace Microsoft.Dafny { var bv = e.BoundVars[i];
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
- wr.Write("for (var @{0} = ", bv.CompileName);
- TrExpr(b.LowerBound);
- wr.Write("; @{0} < ", bv.CompileName);
- TrExpr(b.UpperBound);
- wr.Write("; @{0}++) {{ ", bv.CompileName);
+ if (AsNativeType(bv.Type) != null) {
+ wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName);
+ } else {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);
+ }
+ TrExpr(b.LowerBound, wr, inLetExprBody);
+ wr.Write(", ");
+ TrExpr(b.UpperBound, wr, inLetExprBody);
+ wr.Write(")) { ");
} else if (bound is ComprehensionExpr.SetBoundedPool) {
var b = (ComprehensionExpr.SetBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
- TrExpr(b.Set);
+ TrExpr(b.Set, wr, inLetExprBody);
wr.Write(").Elements) { ");
} else if (bound is ComprehensionExpr.MapBoundedPool) {
var b = (ComprehensionExpr.MapBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
- TrExpr(b.Map);
+ TrExpr(b.Map, wr, inLetExprBody);
wr.Write(").Domain) { ");
} else if (bound is ComprehensionExpr.SeqBoundedPool) {
var b = (ComprehensionExpr.SeqBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
- TrExpr(b.Seq);
+ TrExpr(b.Seq, wr, inLetExprBody);
wr.Write(").Elements) { ");
} else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
var b = (ComprehensionExpr.DatatypeBoundedPool)bound;
- wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));
+ wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type, wr));
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
}
}
wr.Write("if (");
- TrExpr(e.Range);
- wr.Write(") { _coll.Add(");
- TrExpr(e.Term);
+ TrExpr(e.Range, wr, inLetExprBody);
+ wr.Write(") {");
+ wr.Write("{0}.Add(", collection_name);
+ TrExpr(e.Term, wr, inLetExprBody);
wr.Write("); }");
for (int i = 0; i < n; i++) {
wr.Write("}");
}
- wr.Write("return Dafny.Set<{0}>.FromCollection(_coll); ", typeName);
+ wr.Write("return Dafny.Set<{0}>.FromCollection({1}); ", typeName, collection_name);
wr.Write("})()");
} else if (expr is MapComprehension) {
@@ -2816,58 +3121,63 @@ namespace Microsoft.Dafny { // return Dafny.Map<U, V>.FromElements(_coll);
// })()
Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds
- var domtypeName = TypeName(e.Type.AsMapType.Domain);
- var rantypeName = TypeName(e.Type.AsMapType.Range);
+ var domtypeName = TypeName(e.Type.AsMapType.Domain, wr);
+ var rantypeName = TypeName(e.Type.AsMapType.Range, wr);
+ var collection_name = idGenerator.FreshId("_coll");
wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName);
- wr.Write("var _coll = new System.Collections.Generic.List<Dafny.Pair<{0},{1}>>(); ", domtypeName, rantypeName);
+ wr.Write("var {0} = new System.Collections.Generic.List<Dafny.Pair<{1},{2}>>(); ", collection_name, domtypeName, rantypeName);
var n = e.BoundVars.Count;
Contract.Assert(e.Bounds.Count == n && n == 1);
var bound = e.Bounds[0];
var bv = e.BoundVars[0];
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
- wr.Write("for (var @{0} = ", bv.CompileName);
- TrExpr(b.LowerBound);
- wr.Write("; @{0} < ", bv.CompileName);
- TrExpr(b.UpperBound);
- wr.Write("; @{0}++) {{ ", bv.CompileName);
+ if (AsNativeType(bv.Type) != null) {
+ wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName);
+ } else {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);
+ }
+ TrExpr(b.LowerBound, wr, inLetExprBody);
+ wr.Write(", ");
+ TrExpr(b.UpperBound, wr, inLetExprBody);
+ wr.Write(")) { ");
} else if (bound is ComprehensionExpr.SetBoundedPool) {
var b = (ComprehensionExpr.SetBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
- TrExpr(b.Set);
+ TrExpr(b.Set, wr, inLetExprBody);
wr.Write(").Elements) { ");
} else if (bound is ComprehensionExpr.MapBoundedPool) {
var b = (ComprehensionExpr.MapBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
- TrExpr(b.Map);
+ TrExpr(b.Map, wr, inLetExprBody);
wr.Write(").Domain) { ");
} else if (bound is ComprehensionExpr.SeqBoundedPool) {
var b = (ComprehensionExpr.SeqBoundedPool)bound;
wr.Write("foreach (var @{0} in (", bv.CompileName);
- TrExpr(b.Seq);
+ TrExpr(b.Seq, wr, inLetExprBody);
wr.Write(").Elements) { ");
} else {
+ // TODO: handle ComprehensionExpr.SubSetBoundedPool
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
}
wr.Write("if (");
- TrExpr(e.Range);
+ TrExpr(e.Range, wr, inLetExprBody);
wr.Write(") { ");
- wr.Write("_coll.Add(new Dafny.Pair<{0},{1}>(@{2},", domtypeName, rantypeName, bv.CompileName);
- TrExpr(e.Term);
+ wr.Write("{0}.Add(new Dafny.Pair<{1},{2}>(@{3},", collection_name, domtypeName, rantypeName, bv.CompileName);
+ TrExpr(e.Term, wr, inLetExprBody);
wr.Write(")); }");
wr.Write("}");
- wr.Write("return Dafny.Map<{0},{1}>.FromCollection(_coll); ", domtypeName, rantypeName);
+ wr.Write("return Dafny.Map<{0},{1}>.FromCollection({2}); ", domtypeName, rantypeName, collection_name);
wr.Write("})()");
} else if (expr is LambdaExpr) {
LambdaExpr e = (LambdaExpr)expr;
- ISet<IVariable> fvs = new HashSet<IVariable>();
- bool dontCare = false;
- Type dontCareT = null;
- Translator.ComputeFreeVariables(expr, fvs, ref dontCare, ref dontCare, ref dontCareT, false);
+ var fvs = Translator.ComputeFreeVariables(expr);
var sm = new Dictionary<IVariable, Expression>();
var bvars = new List<BoundVar>();
@@ -2887,46 +3197,46 @@ namespace Microsoft.Dafny { var su = new Translator.Substituter(null, sm, new Dictionary<TypeParameter, Type>(), null);
- BetaRedex(bvars, fexprs, expr.Type, () => {
+ BetaRedex(bvars, fexprs, expr.Type, wr, inLetExprBody, () => {
wr.Write("(");
wr.Write(Util.Comma(e.BoundVars, bv => "@" + bv.CompileName));
wr.Write(") => ");
- TrExpr(su.Substitute(e.Body));
+ TrExpr(su.Substitute(e.Body), wr, inLetExprBody);
});
} else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
- TrExpr(e.E);
+ TrExpr(e.E, wr, inLetExprBody);
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
wr.Write("(");
- TrExpr(e.Test);
+ TrExpr(e.Test, wr, inLetExprBody);
wr.Write(") ? (");
- TrExpr(e.Thn);
+ TrExpr(e.Thn, wr, inLetExprBody);
wr.Write(") : (");
- TrExpr(e.Els);
+ TrExpr(e.Els, wr, inLetExprBody);
wr.Write(")");
} else if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
- TrExpr(e.ResolvedExpression);
+ TrExpr(e.ResolvedExpression, wr, inLetExprBody);
} else if (expr is NamedExpr) {
- TrExpr(((NamedExpr)expr).Body);
+ TrExpr(((NamedExpr)expr).Body, wr, inLetExprBody);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
}
- int TrCasePattern(CasePattern pat, string rhsString, Type bodyType) {
+ int TrCasePattern(CasePattern pat, string rhsString, Type bodyType, TextWriter wr) {
Contract.Requires(pat != null);
Contract.Requires(rhsString != null);
int c = 0;
if (pat.Var != null) {
var bv = pat.Var;
if (!bv.IsGhost) {
- wr.Write("Dafny.Helpers.Let<" + TypeName(bv.Type) + "," + TypeName(bodyType) + ">");
+ wr.Write("Dafny.Helpers.Let<" + TypeName(bv.Type, wr) + "," + TypeName(bodyType, wr) + ">");
wr.Write("(" + rhsString + ", @" + bv.CompileName + " => ");
c++;
}
@@ -2942,7 +3252,7 @@ namespace Microsoft.Dafny { // nothing to compile, but do a sanity check
Contract.Assert(!Contract.Exists(arg.Vars, bv => !bv.IsGhost));
} else {
- c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs), rhsString, FormalName(formal, k)), bodyType);
+ c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs, wr), rhsString, FormalName(formal, k)), bodyType, wr);
k++;
}
}
@@ -2950,36 +3260,40 @@ namespace Microsoft.Dafny { return c;
}
- delegate void FCE_Arg_Translator(Expression e);
+ delegate void FCE_Arg_Translator(Expression e, TextWriter wr, bool inLetExpr=false);
- void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, FCE_Arg_Translator tr) {
+ void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, TextWriter wr, bool inLetExprBody, FCE_Arg_Translator tr) {
Function f = cce.NonNull(e.Function);
if (f.IsStatic) {
- twr.Write(TypeName_Companion(e.Receiver.Type));
+ twr.Write(TypeName_Companion(e.Receiver.Type, wr));
} else {
twr.Write("(");
- tr(e.Receiver);
+ tr(e.Receiver, wr, inLetExprBody);
twr.Write(")");
}
twr.Write(".@{0}", f.CompileName);
+ if (f.TypeArgs.Count != 0) {
+ List<Type> typeArgs = f.TypeArgs.ConvertAll(ta => e.TypeArgumentSubstitutions[ta]);
+ twr.Write("<" + TypeNames(typeArgs, wr) + ">");
+ }
twr.Write("(");
string sep = "";
for (int i = 0; i < e.Args.Count; i++) {
if (!e.Function.Formals[i].IsGhost) {
twr.Write(sep);
- tr(e.Args[i]);
+ tr(e.Args[i], wr);
sep = ", ";
}
}
twr.Write(")");
}
- void BetaRedex(List<BoundVar> bvars, List<Expression> exprs, Type bodyType, Action makeBody) {
+ void BetaRedex(List<BoundVar> bvars, List<Expression> exprs, Type bodyType, TextWriter wr, bool inLetExprBody, Action makeBody) {
Contract.Requires(bvars != null);
Contract.Requires(exprs != null);
Contract.Requires(bvars.Count == exprs.Count);
wr.Write("Dafny.Helpers.Id<");
- wr.Write(TypeName_UDT(ArrowType.Arrow_FullCompileName, Util.Snoc(bvars.ConvertAll(bv => bv.Type), bodyType)));
+ wr.Write(TypeName_UDT(ArrowType.Arrow_FullCompileName, Util.Snoc(bvars.ConvertAll(bv => bv.Type), bodyType), wr));
wr.Write(">((");
wr.Write(Util.Comma(bvars, bv => "@" + bv.CompileName));
wr.Write(") => ");
@@ -2987,7 +3301,7 @@ namespace Microsoft.Dafny { makeBody();
wr.Write(")");
- TrExprList(exprs);
+ TrExprList(exprs, wr, inLetExprBody);
}
}
|