diff options
| author |  qunyanm <unknown> | 2015-04-06 10:35:55 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-04-06 10:35:55 -0700 |
| commit | 8cac7f02bde3364c92763c26b0f75c1b5feef944 (patch) | |
| tree | 6dad47174675c2209aae74cbbc92af43d928eed5 /Source | |
| parent | ce0649d4207ab1edeea2b26141ad45af7a5ee796 (diff) | |
| parent | 0aeab928abc85e646dc58c4dc4670a03a36cbc2f (diff) | |
Merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 360 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 45 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 7 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 92 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 313 |
6 files changed, 358 insertions, 461 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 8552e480..3c266a28 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -105,7 +105,7 @@ namespace Microsoft.Dafny if (d is DefaultClassDecl) {
return new DefaultClassDecl(m, mm);
} else {
- return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp);
+ return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType));
}
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index e557e509..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
@@ -236,27 +236,26 @@ namespace Microsoft.Dafny { }
}
}
- var cl = new ClassDecl(d.tok, d.Name, d.Module, d.TypeArgs, members, d.Attributes, null);
Indent(indent);
- wr.Write("public class @_Companion_{0}", cl.CompileName);
+ wr.Write("public class @_Companion_{0}", trait.CompileName);
wr.WriteLine(" {");
- CompileClassMembers(cl, indent + IndentAmount);
+ CompileClassMembers(trait, true, indent + IndentAmount);
Indent(indent); wr.WriteLine("}");
}
else if (d is ClassDecl) {
var cl = (ClassDecl)d;
Indent(indent);
- if (cl.TraitsObj != null && cl.TraitsObj.Count > 0)
- {
- wr.WriteLine("public class @{0} : @{1}", cl.CompileName, cl.TraitsStr);
- }
- else
- wr.Write("public class @{0}", cl.CompileName);
+ wr.Write("public 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));
+ sep = ", ";
+ }
wr.WriteLine(" {");
- CompileClassMembers(cl, indent+IndentAmount);
+ CompileClassMembers(cl, false, indent+IndentAmount);
Indent(indent); wr.WriteLine("}");
} else if (d is ModuleDecl) {
// nop
@@ -757,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
@@ -975,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);
@@ -1882,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);
@@ -2957,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 ed089f10..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
@@ -1865,12 +1872,14 @@ namespace Microsoft.Dafny { public class ClassDecl : TopLevelDecl {
public override string WhatKind { get { return "class"; } }
public readonly List<MemberDecl> Members;
- public List<TraitDecl> TraitsObj;
- public readonly List<Type> TraitsTyp;
+ public readonly List<Type> TraitsTyp; // these are the types that are parsed after the keyword 'extends'
+ public readonly List<TraitDecl> TraitsObj = new List<TraitDecl>(); // populated during resolution
public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Members));
+ Contract.Invariant(TraitsTyp != null);
+ Contract.Invariant(TraitsObj != null);
}
public ClassDecl(IToken tok, string name, ModuleDefinition module,
@@ -1882,42 +1891,18 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(members));
Members = members;
- //if (traits != null)
- TraitsTyp = traits;
+ TraitsTyp = traits ?? new List<Type>();
}
public virtual bool IsDefaultClass {
get {
return false;
}
}
-
- public string TraitsStr
- {
- get
- {
- if (TraitsTyp == null || TraitsTyp.Count == 0)
- return string.Empty;
- StringBuilder sb = new StringBuilder();
- foreach (Type ty in TraitsTyp)
- {
- if (ty is UserDefinedType)
- {
- sb.Append(((UserDefinedType)(ty)).Name);
- sb.Append(",");
- }
- }
- if (sb.Length > 0)
- {
- sb.Remove(sb.Length - 1, 1);
- }
- return sb.ToString();
- }
- }
}
public class DefaultClassDecl : ClassDecl {
public DefaultClassDecl(ModuleDefinition module, [Captured] List<MemberDecl> members)
- : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null,null) {
+ : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null, null) {
Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(members));
}
@@ -1934,7 +1919,7 @@ namespace Microsoft.Dafny { public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)
: base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,
new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),
- new List<MemberDecl>(), attrs,null)
+ new List<MemberDecl>(), attrs, null)
{
Contract.Requires(1 <= dims);
Contract.Requires(module != null);
@@ -2218,7 +2203,7 @@ namespace Microsoft.Dafny { List<MaybeFreeExpression> yieldRequires,
List<MaybeFreeExpression> yieldEnsures,
BlockStmt body, Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes,null)
+ : base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes, null)
{
Contract.Requires(tok != null);
Contract.Requires(name != null);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index b8c99b00..5fa232f1 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -319,8 +319,11 @@ namespace Microsoft.Dafny { Contract.Requires(c != null);
Indent(indent);
PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
- if (c.TraitsStr!=string.Empty) {
- wr.Write(" extends {0}", c.TraitsStr);
+ string sep = " extends ";
+ foreach (var trait in c.TraitsTyp) {
+ wr.Write(sep);
+ PrintType(trait);
+ sep = ", ";
}
if (c.Members.Count == 0) {
wr.WriteLine(" { }");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bf417de7..0e8e0ec3 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2837,39 +2837,24 @@ namespace Microsoft.Dafny currentClass = cl;
// Resolve names of traits extended
- if (cl.TraitsTyp != null)
- {
- cl.TraitsObj = new List<TraitDecl>();
- foreach (Type traitTyp in cl.TraitsTyp)
- {
- if (traitTyp is UserDefinedType)
- {
- var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == ((UserDefinedType)(traitTyp)).FullCompileName);
- if (trait == null)
- {
- Error(((UserDefinedType)(traitTyp)).tok, "unresolved identifier: {0}", ((UserDefinedType)(traitTyp)).tok.val);
- }
- else if (!(trait is TraitDecl))
- {
- Error(((UserDefinedType)(traitTyp)).tok, "identifier '{0}' does not denote a trait", ((UserDefinedType)(traitTyp)).tok.val);
- }
- else
- {
- //disallowing inheritance in multi module case
- string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty);
- string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty);
- if (clModName != traitModName)
- {
- Error(((UserDefinedType)(traitTyp)).tok, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module",
- cl.FullName, trait.FullName));
- }
- else
- {
- cl.TraitsObj.Add((TraitDecl)trait);
- }
- }
- }
+ foreach (var tt in cl.TraitsTyp) {
+ var prevErrorCount = ErrorCount;
+ ResolveType(cl.tok, tt, new NoContext(cl.Module), ResolveTypeOptionEnum.DontInfer, null);
+ if (ErrorCount == prevErrorCount) {
+ var udt = tt as UserDefinedType;
+ if (udt != null && udt.ResolvedClass is TraitDecl) {
+ var trait = (TraitDecl)udt.ResolvedClass;
+ //disallowing inheritance in multi module case
+ if (cl.Module != trait.Module) {
+ Error(udt.tok, "class '{0}' is in a different module than trait '{1}'. A class may only extend a trait in the same module.", cl.Name, trait.FullName);
+ } else {
+ // all is good
+ cl.TraitsObj.Add(trait);
+ }
+ } else {
+ Error(udt != null ? udt.tok : cl.tok, "a class can only extend traits (found '{0}')", tt);
}
+ }
}
foreach (MemberDecl member in cl.Members) {
@@ -2952,25 +2937,6 @@ namespace Microsoft.Dafny classMethod.OverriddenMethod = traitMethod;
//adding a call graph edge from the trait method to that of class
cl.Module.CallGraph.AddEdge(traitMethod, classMethod);
-
- //checking specifications
- //class method must provide its own specifications in case the overriden method has provided any
- if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req
- {
- Error(classMethod, "Method must provide its own Requires clauses anew");
- }
- if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens
- {
- Error(classMethod, "Method must provide its own Ensures clauses anew");
- }
- if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod
- {
- Error(classMethod, "Method must provide its own Modifies clauses anew");
- }
- if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases
- {
- Error(classMethod, "Method must provide its own Decreases clauses anew");
- }
}
}
else if (traitMem.Value is Function)
@@ -2985,25 +2951,6 @@ namespace Microsoft.Dafny classFunction.OverriddenFunction = traitFunction;
//adding a call graph edge from the trait function to that of class
cl.Module.CallGraph.AddEdge(traitFunction, classFunction);
-
- //checking specifications
- //class function must provide its own specifications in case the overriden function has provided any
- if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req
- {
- Error(classFunction, "Function must provide its own Requires clauses anew");
- }
- if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens
- {
- Error(classFunction, "Function must provide its own Ensures clauses anew");
- }
- if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod
- {
- Error(classFunction, "Function must provide its own Reads clauses anew");
- }
- if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases
- {
- Error(classFunction, "Function must provide its own Decreases clauses anew");
- }
}
}
else if (traitMem.Value is Field)
@@ -3058,6 +3005,11 @@ namespace Microsoft.Dafny {
Method classMethod = (Method)classMem;
refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);
+ var traitMethodAllowsNonTermination = Contract.Exists(traitMethod.Decreases.Expressions, e => e is WildcardExpr);
+ var classMethodAllowsNonTermination = Contract.Exists(classMethod.Decreases.Expressions, e => e is WildcardExpr);
+ if (classMethodAllowsNonTermination && !traitMethodAllowsNonTermination) {
+ Error(classMethod.tok, "not allowed to override a terminating method with a possibly non-terminating method ('{0}')", classMethod.Name);
+ }
}
if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)
Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 9160248c..2672258d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -155,6 +155,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Type Ty;
public readonly Bpl.Type TyTag;
public readonly Bpl.Expr Null;
+ public readonly Bpl.Expr NoTraitAtAll;
private readonly Bpl.Constant allocField;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -178,6 +179,7 @@ namespace Microsoft.Dafny { Contract.Invariant(Ty != null);
Contract.Invariant(TyTag != null);
Contract.Invariant(Null != null);
+ Contract.Invariant(NoTraitAtAll != null);
Contract.Invariant(allocField != null);
}
@@ -282,6 +284,7 @@ namespace Microsoft.Dafny { this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new List<Bpl.Type>());
this.allocField = allocField;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
+ this.NoTraitAtAll = new Bpl.IdentifierExpr(Token.NoToken, "NoTraitAtAll", ClassNameType);
}
}
@@ -537,8 +540,7 @@ namespace Microsoft.Dafny { }
}
- //adding TraitParent function and axioms
- AddTraitParentFuncAndAxioms();
+ AddTraitParentAxioms();
if (InsertChecksums)
{
@@ -561,35 +563,24 @@ namespace Microsoft.Dafny { return sink;
}
- //adding TraitParent function and axioms
- //if a class A extends trait J and B does not extned anything, then this method adds the followings to the sink:
- // const unique NoTraitAtAll: ClassName;
- // function TraitParent(ClassName): ClassName;
- // axiom TraitParent(class.A) == class.J;
- // axiom TraitParent(class.B) == NoTraitAtAll;
- private void AddTraitParentFuncAndAxioms()
+ /// <summary>
+ /// adding TraitParent axioms
+ /// if a class A extends trait J and B does not extend anything, then this method adds the followings to the sink:
+ /// axiom TraitParent(class.A) == class.J;
+ /// axiom TraitParent(class.B) == NoTraitAtAll;
+ /// </summary>
+ private void AddTraitParentAxioms()
{
foreach (ModuleDefinition m in program.Modules)
{
- if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitsObj != null && ((ClassDecl)d).TraitsObj.Count > 0) || (d is TraitDecl)))
+ if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitsObj.Count > 0) || (d is TraitDecl)))
{
- //adding const unique NoTraitAtAll: ClassName;
- Token tNoTrait = new Token();
- Token tTraitParent = new Token();
- Bpl.Constant cNoTrait = new Bpl.Constant(tNoTrait, new Bpl.TypedIdent(tNoTrait, "NoTraitAtAll", predef.ClassNameType), true);
- sink.AddTopLevelDeclaration(cNoTrait);
- //adding function TraitParent(ClassName): ClassName;
- var arg_ref = new Bpl.Formal(tTraitParent, new Bpl.TypedIdent(tTraitParent, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var res = new Bpl.Formal(tTraitParent, new Bpl.TypedIdent(tTraitParent, Bpl.TypedIdent.NoName, predef.ClassNameType), false);
- var fTraitParent = new Bpl.Function(tTraitParent, "TraitParent", new List<Variable> { arg_ref }, res);
- sink.AddTopLevelDeclaration(fTraitParent);
-
foreach (TopLevelDecl d in m.TopLevelDecls)
{
if (d is ClassDecl)
{
var c = (ClassDecl)d;
- if (c is ClassDecl && c.TraitsObj != null && c.TraitsObj.Count > 0)
+ if (c.TraitsObj.Count > 0)
{
foreach (TraitDecl traitObj in c.TraitsObj)
{
@@ -598,27 +589,18 @@ namespace Microsoft.Dafny { Bpl.Constant trait = new Bpl.Constant(traitObj.tok, trait_id, true);
Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(traitObj.tok, trait);
- var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), false);
- var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "TraitParent", new List<Variable> { args }, ret_value));
- var funCallExpr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
+ var id = new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType);
+ var funCallExpr = FunctionCall(c.tok, BuiltinFunction.TraitParent, null, id);
var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, traitId_expr));
sink.AddTopLevelDeclaration(traitParentAxiom);
}
}
- else if (c is ClassDecl && (c.TraitsObj == null || c.TraitsObj.Count == 0))
+ else
{
- //this adds: axiom TraitParent(class.B) == NoTraitAtAll; Where B does not extend any traits
- Bpl.TypedIdent noTraitAtAll_id = new Bpl.TypedIdent(c.tok, "NoTraitAtAll", predef.ClassNameType);
- Bpl.Constant noTraitAtAll = new Bpl.Constant(c.tok, noTraitAtAll_id, true);
- Bpl.Expr noTraitAtAll_expr = new Bpl.IdentifierExpr(c.tok, noTraitAtAll);
-
- var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), false);
- var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "TraitParent", new List<Variable> { args }, ret_value));
- var funCallExpr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
- var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, noTraitAtAll_expr));
+ var id = new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType);
+ var funCallExpr = FunctionCall(c.tok, BuiltinFunction.TraitParent, null, id);
+ var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, predef.NoTraitAtAll));
sink.AddTopLevelDeclaration(traitParentAxiom);
}
@@ -1365,7 +1347,7 @@ namespace Microsoft.Dafny { {
var t = (TraitDecl)c;
var dtypeFunc = FunctionCall(o.tok, BuiltinFunction.DynamicType, null, o);
- Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
+ Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.FullSanitizedName, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
rhs = BplOr(o_null, implementsFunc);
}
else
@@ -1380,34 +1362,20 @@ namespace Microsoft.Dafny { });
}
- //this adds: function implements$J(ClassName): bool;
- if (c is TraitDecl)
- {
- var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- var implement_intr = new Bpl.Function(c.tok, "implements$" + c.Name, new List<Variable> { arg_ref }, res);
- sink.AddTopLevelDeclaration(implement_intr);
- }
- //this adds: axiom implements$J(class.C);
- else if (c is ClassDecl)
- {
- if (c.TraitsObj != null && c.TraitsObj.Count > 0)
- {
- //var dtypeFunc = FunctionCall(c.tok, BuiltinFunction.DynamicType, null, o);
- //Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
- foreach (Type traitType in c.TraitsTyp)
- {
- if (traitType is UserDefinedType)
- {
- var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + ((UserDefinedType)(traitType)).tok, new List<Variable> { args }, ret_value));
- var expr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
- var implements_axiom = new Bpl.Axiom(c.tok, expr);
- sink.AddTopLevelDeclaration(implements_axiom);
- }
- }
- }
+ if (c is TraitDecl) {
+ //this adds: function implements$J(Ty): bool;
+ var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.Ty), true);
+ var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
+ var implement_intr = new Bpl.Function(c.tok, "implements$" + c.FullSanitizedName, new List<Variable> { arg_ref }, res);
+ sink.AddTopLevelDeclaration(implement_intr);
+ } else if (c is ClassDecl) {
+ //this adds: axiom implements$J(class.C);
+ foreach (var trait in c.TraitsObj) {
+ var arg = ClassTyCon(c, new List<Expr>()); // TODO: this needs more work if overridingClass has type parameters
+ var expr = FunctionCall(c.tok, "implements$" + trait.FullSanitizedName, Bpl.Type.Bool, arg);
+ var implements_axiom = new Bpl.Axiom(c.tok, expr);
+ sink.AddTopLevelDeclaration(implements_axiom);
+ }
}
foreach (MemberDecl member in c.Members) {
@@ -1514,7 +1482,7 @@ namespace Microsoft.Dafny { AddFrameAxiom(f);
// add consequence axiom
sink.AddTopLevelDeclaration(FunctionConsequenceAxiom(f, f.Ens));
- // add definition axioms, suitably specialized for "match" cases and for literals
+ // add definition axioms, suitably specialized for literals
if (f.Body != null && !IsOpaqueFunction(f)) {
AddFunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, f.Body.Resolved);
AddFunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, f.Body.Resolved);
@@ -2097,10 +2065,11 @@ namespace Microsoft.Dafny { }
}
- Bpl.Axiom FunctionAxiom(Function f, FunctionAxiomVisibility visibility, Expression body, ICollection<Formal> lits) {
+ Bpl.Axiom FunctionAxiom(Function f, FunctionAxiomVisibility visibility, Expression body, ICollection<Formal> lits, TopLevelDecl overridingClass = null) {
Contract.Requires(f != null);
Contract.Requires(predef != null);
Contract.Requires(f.EnclosingClass != null);
+ Contract.Requires(!f.IsStatic || overridingClass == null);
// only if body is null, we will return null:
Contract.Ensures((Contract.Result<Bpl.Axiom>() == null) == (body == null));
@@ -2114,7 +2083,8 @@ namespace Microsoft.Dafny { // ==>
// (forall s, $Heap, formals :: // let args := $Heap,formals
// { f(Succ(s), args) } // (*)
- // f#canCall(args) || USE_VIA_CONTEXT
+ // (f#canCall(args) || USE_VIA_CONTEXT) &&
+ // dtype(this) == overridingClass // if "overridingClass" != null
// ==>
// BODY-can-make-its-calls &&
// f(Succ(s), args) == BODY); // (*)
@@ -2178,6 +2148,7 @@ namespace Microsoft.Dafny { // ante: $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
+ Bpl.Expr additionalAntecedent = null;
if (!f.IsStatic) {
var bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, predef.RefType));
formals.Add(bvThis);
@@ -2189,6 +2160,10 @@ namespace Microsoft.Dafny { Bpl.Expr.Neq(bvThisIdExpr, predef.Null),
etran.GoodRef(f.tok, bvThisIdExpr, thisType));
ante = Bpl.Expr.And(ante, wh);
+ if (overridingClass != null) {
+ // additionalAntecednet := dtype(this) == overridingClass
+ additionalAntecedent = DType(bvThisIdExpr, ClassTyCon(overridingClass, new List<Expr>())); // TODO: this needs more work if overridingClass has type parameters
+ }
}
var substMap = new Dictionary<IVariable, Expression>();
@@ -2225,11 +2200,13 @@ namespace Microsoft.Dafny { // Add the precondition function and its axiom (which is equivalent to the ante)
if (body == null || (visibility == FunctionAxiomVisibility.IntraModuleOnly && lits == null)) {
- var precondF = new Bpl.Function(f.tok,
- RequiresName(f), new List<Bpl.TypeVariable>(),
- formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)),
- BplFormalVar(null, Bpl.Type.Bool, false));
- sink.AddTopLevelDeclaration(precondF);
+ if (overridingClass == null) {
+ var precondF = new Bpl.Function(f.tok,
+ RequiresName(f), new List<Bpl.TypeVariable>(),
+ formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)),
+ BplFormalVar(null, Bpl.Type.Bool, false));
+ sink.AddTopLevelDeclaration(precondF);
+ }
var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool,
formals.ConvertAll(x => (Bpl.Expr)(new Bpl.IdentifierExpr(f.tok, x))));
sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl), Bpl.Expr.Eq(appl, ante))));
@@ -2246,6 +2223,9 @@ namespace Microsoft.Dafny { // ante := useViaCanCall || (useViaContext && typeAnte && pre)
ante = Bpl.Expr.Or(useViaCanCall, ante);
+ if (additionalAntecedent != null) {
+ ante = Bpl.Expr.And(ante, additionalAntecedent);
+ }
Bpl.Expr funcAppl;
{
@@ -2287,7 +2267,11 @@ namespace Microsoft.Dafny { Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, kv, tr, Bpl.Expr.Imp(ante, meat));
var activate = AxiomActivation(f, visibility == FunctionAxiomVisibility.ForeignModuleOnly, visibility == FunctionAxiomVisibility.IntraModuleOnly, etran);
string comment;
- comment = "definition axiom for " + f.FullSanitizedName;
+ if (overridingClass == null) {
+ comment = "definition axiom for " + f.FullSanitizedName;
+ } else {
+ comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingClass.FullSanitizedName;
+ }
if (lits != null) {
if (lits.Count == f.Formals.Count) {
comment += " for all literals";
@@ -3056,67 +3040,32 @@ namespace Microsoft.Dafny { private void AddFunctionOverrideAxiom(Function f)
{
- Contract.Requires(f != null);
- Contract.Requires(sink != null && predef != null);
- // function override axiom
- // axiom (forall $heap: HeapType, this: ref, x#0: int ::
- // { J.F($heap, this, x#0) }
- // this != null && dtype(this) == class.C
- // ==>
- // J.F($heap, this, x#0) == C.F($heap, this, x#0));
-
- var formals = new List<Variable>();
- var argsC = new List<Bpl.Expr>();
- var argsT = new List<Bpl.Expr>();
-
- var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));
- var s = new Bpl.IdentifierExpr(f.tok, bv);
- if (f.IsRecursive)
- {
- formals.Add(bv);
- argsC.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s));
- argsT.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s));
- }
-
- bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
- formals.Add(bv);
- s = new Bpl.IdentifierExpr(f.tok, bv);
- argsC.Add(s);
- argsT.Add(s);
-
- if (!f.IsStatic)
- {
- bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
- formals.Add(bv);
- s = new Bpl.IdentifierExpr(f.tok, bv);
- argsC.Add(s);
- argsT.Add(s);
- }
- foreach (var p in f.Formals)
- {
- bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, f.FullSanitizedName + "_" + p.AssignUniqueName(f.IdGenerator), TrType(p.Type)));
- formals.Add(bv);
- s = new Bpl.IdentifierExpr(f.tok, bv);
- argsC.Add(s);
- }
- foreach (var p in f.OverriddenFunction.Formals)
- {
- bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, f.OverriddenFunction.FullSanitizedName + "_" + p.AssignUniqueName(f.OverriddenFunction.IdGenerator), TrType(p.Type)));
- formals.Add(bv);
- s = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, bv);
- argsT.Add(s);
- }
-
- var funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
- var funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));
- var funcApplC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
- var funcApplT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);
-
- var typeParams = TrTypeParamDecls(f.TypeArgs);
+ Contract.Requires(f != null);
+ Contract.Requires(!f.IsStatic); // only instance functions can be overridden
+ Contract.Requires(sink != null && predef != null);
- Bpl.Trigger tr = new Bpl.Trigger(f.OverriddenFunction.tok, true, new List<Bpl.Expr> { funcApplT, funcApplC });
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(funcApplC, funcApplT));
- sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax, "function override axiom"));
+ // Essentially, the function override axiom looks like:
+ // axiom (forall $heap: HeapType, this: ref, x#0: int ::
+ // { J.F($heap, this, x#0) }
+ // this != null && dtype(this) == class.C
+ // ==>
+ // J.F($heap, this, x#0) == C.F($heap, this, x#0));
+ // but it also has the various usual antecedents. Essentially, the override gives a part of the body of the
+ // trait's function, so we call FunctionAxiom to generate a conditional axiom (that is, we pass in the "overridingClass"
+ // parameter to FunctionAxiom, which will add 'dtype(this) == class.C' as an additional antecedent) for a
+ // body of 'C.F(this, x#0)'.
+ // TODO: More work needs to be done to support any type parameters that class C might have. These would
+ // need to be quantified (existentially?) in the axiom.
+ var receiver = new ThisExpr(f.tok);
+ receiver.Type = Resolver.GetReceiverType(f.tok, f);
+ var args = f.OverriddenFunction.Formals.ConvertAll(p => (Expression)new IdentifierExpr(p.tok, p.Name) { Var = p, Type = p.Type });
+ var pseudoBody = new FunctionCallExpr(f.tok, f.Name, new ThisExpr(f.tok), f.tok, args);
+ pseudoBody.Function = f; // resolve here
+ // TODO: the following two lines (incorrectly) assume there are no type parameters
+ pseudoBody.Type = f.ResultType; // resolve here
+ pseudoBody.TypeArgumentSubstitutions = new Dictionary<TypeParameter,Type>(); // resolve here
+ sink.AddTopLevelDeclaration(FunctionAxiom(f.OverriddenFunction, FunctionAxiomVisibility.IntraModuleOnly, pseudoBody, null, f.EnclosingClass));
+ sink.AddTopLevelDeclaration(FunctionAxiom(f.OverriddenFunction, FunctionAxiomVisibility.ForeignModuleOnly, pseudoBody, null, f.EnclosingClass));
}
private void AddFunctionOverrideEnsChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap, List<Variable> implInParams)
@@ -3405,33 +3354,68 @@ namespace Microsoft.Dafny { }
}
- private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)
- {
- var decrToks = new List<IToken>();
- var decrTypes1 = new List<Type>();
- var decrTypes2 = new List<Type>();
- var decrClass = new List<Expr>();
- var decrTrait = new List<Expr>();
- if (m.Decreases != null)
- {
- foreach (var decC in m.Decreases.Expressions)
- {
- decrToks.Add(decC.tok);
- decrTypes1.Add(decC.Type);
- decrClass.Add(etran.TrExpr(decC));
- }
- }
- if (m.OverriddenMethod.Decreases != null)
- {
- foreach (var decT in m.OverriddenMethod.Decreases.Expressions)
- {
- var decCNew = Substitute(decT, null, substMap);
- decrTypes2.Add(decCNew.Type);
- decrTrait.Add(etran.TrExpr(decCNew));
- }
+ private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap) {
+ Contract.Requires(m != null);
+ Contract.Requires(builder != null);
+ Contract.Requires(etran != null);
+ Contract.Requires(substMap != null);
+ // Note, it is as if the trait's method is calling the class's method.
+ var contextDecreases = m.OverriddenMethod.Decreases.Expressions;
+ var calleeDecreases = m.Decreases.Expressions;
+ // We want to check: calleeDecreases <= contextDecreases (note, we can allow equality, since there is a bounded, namely 1, number of dynamic dispatches)
+ if (Contract.Exists(contextDecreases, e => e is WildcardExpr)) {
+ // no check needed
+ return;
+ }
+
+ int N = Math.Min(contextDecreases.Count, calleeDecreases.Count);
+ var toks = new List<IToken>();
+ var types0 = new List<Type>();
+ var types1 = new List<Type>();
+ var callee = new List<Expr>();
+ var caller = new List<Expr>();
+
+ for (int i = 0; i < N; i++) {
+ Expression e0 = calleeDecreases[i];
+ Expression e1 = Substitute(contextDecreases[i], null, substMap);
+ if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {
+ N = i;
+ break;
}
- var decrChk = DecreasesCheck(decrToks, decrTypes1, decrTypes2, decrClass, decrTrait, null, null, true, false);
- builder.Add(new Bpl.AssertCmd(m.tok, decrChk));
+ toks.Add(new NestedToken(m.tok, e1.tok));
+ types0.Add(e0.Type.NormalizeExpand());
+ types1.Add(e1.Type.NormalizeExpand());
+ callee.Add(etran.TrExpr(e0));
+ caller.Add(etran.TrExpr(e1));
+ }
+
+ var decrCountT = contextDecreases.Count;
+ var decrCountC = calleeDecreases.Count;
+ // Generally, we want to produce a check "decrClass <= decrTrait", allowing (the common case where) they are equal.
+ // * If N < decrCountC && N < decrCountT, then "decrClass <= decrTrait" if the comparison ever gets beyond the
+ // parts that survived truncation. Thus, we compare with "allowNoChange" set to "false".
+ // Otherwise:
+ // * If decrCountC == decrCountT, then the truncation we did above had no effect and we pass in "allowNoChange" as "true".
+ // * If decrCountC > decrCountT, then we will have truncated decrClass above. Let x,y and x' denote decrClass and
+ // decrTrait, respectively, where x and x' have the same length. Considering how Dafny in effect pads the end of
+ // decreases tuples with a \top, we were supposed to evaluate (x,(y,\top)) <= (x',\top), which by lexicographic pairs
+ // we can expand to:
+ // x <= x' && (x == x' ==> (y,\top) <= \top)
+ // which is equivalent to just x <= x'. Thus, we called DecreasesCheck to compare x and x' and we pass in "allowNoChange"
+ // as "true".
+ // * If decrCountC < decrCountT, then we will have truncated decrTrait above. Let x and x',y' denote decrClass and
+ // decrTrait, respectively, where x and x' have the same length. We then want to check (x,\top) <= (x',(y',\top)), which
+ // expands to:
+ // x <= x' && (x == x' ==> \top <= (y',\top))
+ // = { \top is strictly larger than a pair }
+ // x <= x' && (x == x' ==> false)
+ // =
+ // x < x'
+ // So we perform our desired check by calling DecreasesCheck to strictly compare x and x', so we pass in "allowNoChange"
+ // as "false".
+ bool allowNoChange = N == decrCountT && decrCountT <= decrCountC;
+ var decrChk = DecreasesCheck(toks, types0, types1, callee, caller, null, null, allowNoChange, false);
+ builder.Add(Assert(m.tok, decrChk, "method's decreases clause must be below or equal to that in the trait"));
}
private void AddMethodOverrideSubsetChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables, Dictionary<IVariable, Expression> substMap)
@@ -11683,6 +11667,8 @@ namespace Microsoft.Dafny { Is, IsBox,
IsAlloc, IsAllocBox,
+ TraitParent,
+
SetCard,
SetEmpty,
SetUnionOne,
@@ -11860,6 +11846,11 @@ namespace Microsoft.Dafny { Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$IsAllocBox", Bpl.Type.Bool, args);
+ case BuiltinFunction.TraitParent:
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "TraitParent", predef.ClassNameType, args);
+
case BuiltinFunction.SetCard:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
|