diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 7 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 17 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 38 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 7 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 49 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 226 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitBasix.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitMultiModule.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitMultiModule.dfy.expect | 5 |
10 files changed, 151 insertions, 214 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 4972517b..74bdb63e 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -101,6 +101,13 @@ type ref; const null: ref;
// ---------------------------------------------------------------
+// -- Traits -----------------------------------------------------
+// ---------------------------------------------------------------
+
+const unique NoTraitAtAll: ClassName;
+function TraitParent(ClassName): ClassName;
+
+// ---------------------------------------------------------------
// -- Boxing and unboxing ----------------------------------------
// ---------------------------------------------------------------
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..c3d82d06 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -236,25 +236,24 @@ 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, 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);
Indent(indent); wr.WriteLine("}");
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ed089f10..6c498a59 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1865,12 +1865,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 +1884,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 +1912,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 +2196,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 727011e8..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) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index c9c900af..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)
@@ -11718,6 +11667,8 @@ namespace Microsoft.Dafny { Is, IsBox,
IsAlloc, IsAllocBox,
+ TraitParent,
+
SetCard,
SetEmpty,
SetUnionOne,
@@ -11895,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);
diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect index 5ebf1d5c..84465fea 100644 --- a/Test/dafny0/Trait/TraitBasix.dfy.expect +++ b/Test/dafny0/Trait/TraitBasix.dfy.expect @@ -1,4 +1,4 @@ -TraitBasix.dfy(91,24): Error: unresolved identifier: IX
+TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name?)
TraitBasix.dfy(77,8): Error: member in the class has been already inherited from its parent trait
TraitBasix.dfy(70,8): Error: class: I0Child does not implement trait member: Customizable
TraitBasix.dfy(80,8): Error: class: I0Child2 does not implement trait member: F
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy b/Test/dafny0/Trait/TraitMultiModule.dfy index b31e4b0d..81f4f401 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy +++ b/Test/dafny0/Trait/TraitMultiModule.dfy @@ -18,8 +18,16 @@ module M1 module M2
{
- class C2 extends T1
+ import opened M1
+ class C2 extends T1 // error: currently no support to implement trait in different module
+ {
+ }
+}
+
+module M3
+{
+ import M1
+ class C2 extends M1.T1 // error: currently no support to implement trait in different module
{
-
}
}
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect index a1617395..e991553a 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -1,2 +1,3 @@ -TraitMultiModule.dfy(21,19): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
-1 resolution/type errors detected in TraitMultiModule.dfy
+TraitMultiModule.dfy(22,19): Error: class 'C2' is in a different module than trait 'M1.T1'. A class may only extend a trait in the same module.
+TraitMultiModule.dfy(30,22): Error: class 'C2' is in a different module than trait 'M1.T1'. A class may only extend a trait in the same module.
+2 resolution/type errors detected in TraitMultiModule.dfy
|