summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Compiler.cs345
-rw-r--r--Source/Dafny/DafnyAst.cs7
-rw-r--r--Test/dafny0/Trait/TraitCompile.dfy71
-rw-r--r--Test/dafny0/Trait/TraitCompile.dfy.expect18
4 files changed, 252 insertions, 189 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index c3d82d06..7b63f65b 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -215,7 +215,7 @@ namespace Microsoft.Dafny {
Indent(indent);
wr.Write("public interface @{0}", trait.CompileName);
wr.WriteLine(" {");
- CompileClassMembers(trait, indent + IndentAmount);
+ CompileClassMembers(trait, false, indent + IndentAmount);
Indent(indent); wr.WriteLine("}");
//writing the _Companion class
@@ -239,7 +239,7 @@ namespace Microsoft.Dafny {
Indent(indent);
wr.Write("public class @_Companion_{0}", trait.CompileName);
wr.WriteLine(" {");
- CompileClassMembers(trait, indent + IndentAmount);
+ CompileClassMembers(trait, true, indent + IndentAmount);
Indent(indent); wr.WriteLine("}");
}
else if (d is ClassDecl) {
@@ -255,7 +255,7 @@ namespace Microsoft.Dafny {
sep = ", ";
}
wr.WriteLine(" {");
- CompileClassMembers(cl, indent+IndentAmount);
+ CompileClassMembers(cl, false, indent+IndentAmount);
Indent(indent); wr.WriteLine("}");
} else if (d is ModuleDecl) {
// nop
@@ -756,193 +756,151 @@ namespace Microsoft.Dafny {
}
}
-
- void CompileClassMembers(ClassDecl c, int indent)
- {
+ void CompileClassMembers(ClassDecl c, bool forCompanionClass, int indent) {
Contract.Requires(c != null);
+ Contract.Requires(!forCompanionClass || c is TraitDecl);
+ Contract.Requires(0 <= indent);
foreach (MemberDecl member in c.Members) {
if (member is Field) {
- Field f = (Field)member;
- if (!f.IsGhost) {
- if (c is TraitDecl)
- {
- {
- Indent(indent);
- wr.Write("{0} @{1}", TypeName(f.Type), f.CompileName);
- wr.Write(" {");
- wr.Write(" get; set; ");
- wr.WriteLine("}");
- }
- }
- else
- {
- if (f.Inherited)
- {
- Indent(indent);
- wr.WriteLine("public {0} @_{1};", TypeName(f.Type), f.CompileName);
- wr.Write("public {0} @{1}", TypeName(f.Type), f.CompileName);
- wr.WriteLine(" {");
- wr.WriteLine(" get { ");
- wr.Write("return this.@_{0};", f.CompileName);
- wr.WriteLine("}");
- wr.WriteLine(" set { ");
- wr.WriteLine("this.@_{0} = value;", f.CompileName);
- wr.WriteLine("}");
- wr.WriteLine("}");
- }
- else
- {
- Indent(indent);
- wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));
- }
- }
+ var f = (Field)member;
+ if (f.IsGhost || forCompanionClass) {
+ // emit nothing
+ } else if (c is TraitDecl) {
+ Indent(indent);
+ wr.Write("{0} @{1}", TypeName(f.Type), f.CompileName);
+ wr.WriteLine(" { get; set; }");
+ } else if (f.Inherited) {
+ Indent(indent);
+ wr.WriteLine("public {0} @_{1};", TypeName(f.Type), f.CompileName);
+ wr.Write("public {0} @{1}", TypeName(f.Type), f.CompileName);
+ wr.WriteLine(" {");
+ wr.WriteLine(" get { ");
+ wr.Write("return this.@_{0};", f.CompileName);
+ wr.WriteLine("}");
+ wr.WriteLine(" set { ");
+ wr.WriteLine("this.@_{0} = value;", f.CompileName);
+ wr.WriteLine("}");
+ wr.WriteLine("}");
+ } else {
+ Indent(indent);
+ wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));
}
} else if (member is Function) {
- Function f = (Function)member;
- if (c is TraitDecl)
- {
- if (member.IsStatic && f.Body == null)
- {
- Error("Function {0} has no body", f.FullName);
- }
- else if (!member.IsStatic && !member.IsGhost) //static and ghost members are not included in the target trait
- {
- Indent(indent);
- wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName);
- wr.Write("(");
- WriteFormals("", f.Formals);
- wr.WriteLine(");");
- }
- }
- else
- {
- if (f.Body == null)
- {
- if (!Attributes.Contains(f.Attributes, "axiom"))
- {
- Error("Function {0} has no body", f.FullName);
- }
- }
- else if (f.IsGhost)
- {
- var v = new CheckHasNoAssumes_Visitor(this);
- v.Visit(f.Body);
- }
- else
- {
- Indent(indent);
- wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);
- if (f.TypeArgs.Count != 0)
- {
- wr.Write("<{0}>", TypeParameters(f.TypeArgs));
- }
- wr.Write("(");
- WriteFormals("", f.Formals);
- wr.WriteLine(") {");
- CompileReturnBody(f.Body, indent + IndentAmount);
- Indent(indent); wr.WriteLine("}");
- }
+ var f = (Function)member;
+ if (f.Body == null && !(c is TraitDecl && !f.IsStatic)) {
+ // A (ghost or non-ghost) function must always have a body, except if it's an instance function in a trait.
+ 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);
+ }
+ } else if (f.IsGhost) {
+ // nothing to compile, but we do check for assumes
+ var v = new CheckHasNoAssumes_Visitor(this);
+ 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);
+ wr.Write("(");
+ WriteFormals("", f.Formals);
+ wr.WriteLine(");");
+ }
+ } else if (forCompanionClass && !f.IsStatic) {
+ // companion classes only has static members
+ } else {
+ Indent(indent);
+ wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);
+ if (f.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(f.TypeArgs));
+ }
+ wr.Write("(");
+ WriteFormals("", f.Formals);
+ wr.WriteLine(") {");
+ CompileReturnBody(f.Body, indent + IndentAmount);
+ Indent(indent); wr.WriteLine("}");
}
} else if (member is Method) {
- Method m = (Method)member;
- if (c is TraitDecl)
- {
- if (member.IsStatic && m.Body == null)
- {
- Error("Method {0} has no body", m.FullName);
- }
- else if (!member.IsStatic && !member.IsGhost) //static and ghost members are not included in the target trait
- {
- Indent(indent);
- wr.Write("void @{0}", m.CompileName);
- wr.Write("(");
- int nIns = WriteFormals("", m.Ins);
- WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
- wr.WriteLine(");");
- }
- }
- else
- {
- if (m.Body == null)
- {
- if (!Attributes.Contains(m.Attributes, "axiom"))
- {
- Error("Method {0} has no body", m.FullName);
- }
+ var m = (Method)member;
+ if (m.Body == null && !(c is TraitDecl && !m.IsStatic)) {
+ // A (ghost or non-ghost) method must always have a body, except if it's an instance method in a trait.
+ 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);
+ }
+ } else if (m.IsGhost) {
+ // nothing to compile, but we do check for assumes
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(m.Body);
+ } else if (c is TraitDecl && !forCompanionClass) {
+ // include it, unless it's static
+ if (!m.IsStatic) {
+ Indent(indent);
+ wr.Write("void @{0}", m.CompileName);
+ wr.Write("(");
+ int nIns = WriteFormals("", m.Ins);
+ WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
+ wr.WriteLine(");");
+ }
+ } else if (forCompanionClass && !m.IsStatic) {
+ // companion classes only has static members
+ } else {
+ Indent(indent);
+ 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);
+ wr.WriteLine(")");
+ Indent(indent); wr.WriteLine("{");
+ foreach (Formal p in m.Outs) {
+ if (!p.IsGhost) {
+ Indent(indent + IndentAmount);
+ wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));
}
- else if (m.IsGhost)
- {
- var v = new CheckHasNoAssumes_Visitor(this);
- v.Visit(m.Body);
+ }
+ if (m.Body == null) {
+ Error("Method {0} has no body", m.FullName);
+ } else {
+ if (m.IsTailRecursive) {
+ Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");
+ if (!m.IsStatic) {
+ Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");
+ }
}
- else
- {
- Indent(indent);
- 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);
- wr.WriteLine(")");
- Indent(indent); wr.WriteLine("{");
- foreach (Formal p in m.Outs)
- {
- if (!p.IsGhost)
- {
- Indent(indent + IndentAmount);
- wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));
- }
- }
- if (m.Body == null)
- {
- Error("Method {0} has no body", m.FullName);
- }
- else
- {
- if (m.IsTailRecursive)
- {
- Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");
- if (!m.IsStatic)
- {
- Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");
- }
- }
- Contract.Assert(enclosingMethod == null);
- enclosingMethod = m;
- TrStmtList(m.Body.Body, indent);
- Contract.Assert(enclosingMethod == m);
- enclosingMethod = null;
- }
- Indent(indent); wr.WriteLine("}");
-
-
- // allow the Main method to be an instance method
- if (!m.IsStatic && IsMain(m)) {
- Indent(indent);
- 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 = ", ";
- }
- wr.Write(">");
- }
- wr.WriteLine("();");
- Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");
- Indent(indent); wr.WriteLine("}");
- }
+ Contract.Assert(enclosingMethod == null);
+ enclosingMethod = m;
+ TrStmtList(m.Body.Body, indent);
+ Contract.Assert(enclosingMethod == m);
+ enclosingMethod = null;
+ }
+ Indent(indent); wr.WriteLine("}");
+
+ // allow the Main method to be an instance method
+ if (!m.IsStatic && IsMain(m)) {
+ Indent(indent);
+ 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 = ", ";
+ }
+ wr.Write(">");
}
+ wr.WriteLine("();");
+ Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");
+ Indent(indent); wr.WriteLine("}");
+ }
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member
@@ -974,6 +932,22 @@ namespace Microsoft.Dafny {
return null;
}
+ string TypeName_Companion(Type type) {
+ 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");
+ }
+ s += "<" + TypeNames(udt.TypeArgs) + ">";
+ }
+ return s;
+ } else {
+ return TypeName(type);
+ }
+ }
string TypeName(Type type)
{
Contract.Requires(type != null);
@@ -1881,14 +1855,7 @@ namespace Microsoft.Dafny {
wr.Write("@" + receiverReplacement);
} else if (s.Method.IsStatic) {
Indent(indent);
- if (s.Receiver.Type is UserDefinedType && ((UserDefinedType)s.Receiver.Type).ResolvedClass is TraitDecl)
- {
- wr.Write("@_Companion_{0}", TypeName(cce.NonNull(s.Receiver.Type)).Replace("@", string.Empty));
- }
- else
- {
- wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
- }
+ wr.Write(TypeName_Companion(s.Receiver.Type));
} else {
Indent(indent);
TrParenExpr(s.Receiver);
@@ -2956,7 +2923,7 @@ namespace Microsoft.Dafny {
void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, FCE_Arg_Translator tr) {
Function f = cce.NonNull(e.Function);
if (f.IsStatic) {
- twr.Write(TypeName(cce.NonNull(e.Receiver.Type)));
+ twr.Write(TypeName_Companion(e.Receiver.Type));
} else {
twr.Write("(");
tr(e.Receiver);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 6c498a59..02d729b4 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -994,6 +994,13 @@ namespace Microsoft.Dafny {
}
}
}
+ public string FullCompanionCompileName {
+ get {
+ Contract.Requires(ResolvedClass is TraitDecl);
+ var s = ResolvedClass.Module.IsDefaultModule ? "" : ResolvedClass.Module.CompileName + ".";
+ return s + "@_Companion_" + CompileName;
+ }
+ }
public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype/iterator and TypeArgs match the type parameters of that class/datatype/iterator
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
diff --git a/Test/dafny0/Trait/TraitCompile.dfy b/Test/dafny0/Trait/TraitCompile.dfy
new file mode 100644
index 00000000..cc667a9a
--- /dev/null
+++ b/Test/dafny0/Trait/TraitCompile.dfy
@@ -0,0 +1,71 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait TT
+{
+ function method Plus(x:int, y:int) : int
+ requires x > y
+ {
+ x + y
+ }
+ function method Times(x:int, y:int) : int
+ requires x > y
+ static function method StaticMinus(x:int, y:int) : int
+ requires x > y
+ {
+ x - y
+ }
+
+ method Double(x: int)
+ {
+ print "d=", x+x, "\n";
+ }
+ method AddFive(x: int)
+ static method StaticTriple(x: int)
+ {
+ print "t=", 3*x, "\n";
+ }
+}
+
+class CC extends TT
+{
+ function method Times(x:int, y:int) : int
+ requires x>y
+ {
+ x * y
+ }
+ method AddFive(x: int)
+ {
+ print "a5=", x+5, "\n";
+ }
+}
+
+method Client(t: TT)
+ requires t != null
+{
+ var x := t.Plus(10, 2);
+ print "x=", x, "\n";
+ t.Double(400);
+ t.AddFive(402);
+ t.StaticTriple(404);
+}
+
+method Main()
+{
+ var c := new CC;
+ var y := c.Plus(100, 20);
+ print "y=", y, "\n";
+ Client(c);
+ var z := TT.StaticMinus(50, 20);
+ print "z=", z, "\n";
+ var z' := CC.StaticMinus(50, 20);
+ print "z'=", z', "\n";
+ var w := c.StaticMinus(50, 20);
+ print "w=", w, "\n";
+
+ c.Double(500);
+ c.AddFive(502);
+ c.StaticTriple(504);
+ TT.StaticTriple(504);
+ CC.StaticTriple(505);
+}
diff --git a/Test/dafny0/Trait/TraitCompile.dfy.expect b/Test/dafny0/Trait/TraitCompile.dfy.expect
new file mode 100644
index 00000000..f4f346de
--- /dev/null
+++ b/Test/dafny0/Trait/TraitCompile.dfy.expect
@@ -0,0 +1,18 @@
+
+Dafny program verifier finished with 23 verified, 0 errors
+Program compiled successfully
+Running...
+
+y=120
+x=12
+d=800
+a5=407
+t=1212
+z=30
+z'=30
+w=30
+d=1000
+a5=507
+t=1512
+t=1512
+t=1515
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 13:28:18 +0000