diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 184 |
1 files changed, 181 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 5e7381d9..d503076c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -144,6 +144,7 @@ namespace Microsoft.Dafny readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();
private ModuleSignature systemNameInfo = null;
private bool useCompileSignatures = false;
+ private RefinementTransformer refinementTransformer = null;
public Resolver(Program prog) {
Contract.Requires(prog != null);
@@ -956,7 +957,11 @@ namespace Microsoft.Dafny }
}
cl.HasConstructor = hasConstructor;
- if (cl.IsDefaultClass) {
+ if (cl is TraitDecl && cl.HasConstructor)
+ {
+ Error(cl, "a trait is not allowed to declare a constructor");
+ }
+ if (cl.IsDefaultClass) {
foreach (MemberDecl m in cl.Members) {
if (m.IsStatic && (m is Function || m is Method)) {
sig.StaticMembers[m.Name] = m;
@@ -1065,9 +1070,10 @@ namespace Microsoft.Dafny var dd = (ClassDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(CloneMember);
+ List<IToken> trait = null;
if (dd is DefaultClassDecl) {
return new DefaultClassDecl(m, mm);
- } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);
+ } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null,trait);
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);
@@ -1469,6 +1475,10 @@ namespace Microsoft.Dafny // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
+ if (d is TraitDecl && d.TypeArgs != null && d.TypeArgs.Count > 0)
+ {
+ Error(d, "a trait can not declare type parameters");
+ }
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, false, d);
if (!(d is IteratorDecl)) {
@@ -2758,6 +2768,7 @@ namespace Microsoft.Dafny Contract.Ensures(currentClass == null);
currentClass = cl;
+ RefinementCloner cloner = new RefinementCloner(cl.Module);
foreach (MemberDecl member in cl.Members) {
member.EnclosingClass = cl;
if (member is Field) {
@@ -2801,6 +2812,157 @@ namespace Microsoft.Dafny Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
}
}
+
+ //merging class members with parent members if any
+ if (cl.TraitId != null)
+ {
+ //resolving trait: making sure if the given qualifed name is a Trait
+ var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val);
+ if (trait != null && trait is TraitDecl)
+ {
+ //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(cl, 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.Trait = (TraitDecl)trait;
+ var traitMembers = classMembers[trait];
+ //merging current class members with the inheriting trait
+ foreach (KeyValuePair<string, MemberDecl> traitMem in traitMembers)
+ {
+ object clMember = cl.Members.FirstOrDefault(clMem => clMem.CompileName == traitMem.Key);
+ if (clMember != null)
+ {
+ //check if the signature of the members are equal and the member is body-less
+ if (traitMem.Value is Method)
+ {
+ Method traitMethod = (Method)traitMem.Value;
+ Method classMethod = (Method)clMember;
+ //refinementTransformer.CheckMethodsAreRefinements(classMethod, traitMethod);
+ if (traitMethod.Body != null && !classMembers[cl][classMethod.CompileName].Inherited) //if the existing method in the class is not that inherited one from the parent
+ Error(classMethod, "a class can not override implemented methods");
+ else
+ {
+ 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)
+ {
+ Function traitFunction = (Function)traitMem.Value;
+ Function classFunction = (Function)clMember;
+ //refinementTransformer.CheckFunctionsAreRefinements(classFunction, traitFunction);
+ if (traitFunction.Body != null && !classMembers[cl][classFunction.CompileName].Inherited)
+ Error(classFunction, "a class can not override implemented functions");
+ else
+ {
+ classFunction.OverriddenFunction = traitFunction;
+ //adding a call graph edge from the trait method 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)
+ {
+ Field traitField = (Field)traitMem.Value;
+ Field classField = (Field)clMember;
+ if (!classMembers[cl][classField.CompileName].Inherited)
+ Error(classField, "member in the class has been already inherited from its parent trait");
+ }
+ }
+ else //the member is not already in the class
+ {
+ MemberDecl classNewMember = cloner.CloneMember(traitMem.Value);
+ classNewMember.EnclosingClass = cl;
+ classNewMember.Inherited = true;
+ classMembers[cl].Add(traitMem.Key, classNewMember);
+ cl.Members.Add(classNewMember);
+ //traitMem.Value.Inherited = true;
+ //classMembers[cl].Add(traitMem.Key, traitMem.Value);
+ //cl.Members.Add(traitMem.Value);
+ }
+ }//foreach
+
+ //checking to make sure all body-less methods/functions have been implemented in the child class
+ if (refinementTransformer == null)
+ refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null);
+ foreach (MemberDecl traitMember in trait.Members.Where(mem => mem is Function || mem is Method))
+ {
+ if (traitMember is Function)
+ {
+ Function traitFunc = (Function)traitMember;
+ var classMem = cl.Members.Where(clMem => clMem is Function).FirstOrDefault(clMem => ((Function)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
+ if (classMem != null)
+ {
+ Function classFunc = (Function)classMem;
+ refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc);
+ }
+ else if (!cl.Module.IsAbstract && traitFunc.Body == null && classMem == null)
+ Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitFunc.CompileName);
+ }
+ if (traitMember is Method)
+ {
+ Method traitMethod = (Method)traitMember;
+
+ var classMem = cl.Members.Where(clMem => clMem is Method).FirstOrDefault(clMem => ((Method)clMem).Body != null && clMem.CompileName == traitMember.CompileName);
+ if (classMem != null)
+ {
+ Method classMethod = (Method)classMem;
+ refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);
+ }
+ if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)
+ Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);
+ }
+ }
+ }
+ }
+ else
+ Error(cl, string.Format("unresolved identifier: {0}", cl.TraitId.val));
+ }
+
currentClass = null;
}
@@ -3933,7 +4095,16 @@ namespace Microsoft.Dafny }
}
return successSoFar;
- } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {
+ }
+ else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl))
+ {
+ return ((ClassDecl)bb.ResolvedClass).Trait.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;
+ }
+ else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl))
+ {
+ return ((ClassDecl)aa.ResolvedClass).Trait.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName;
+ }
+ else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {
// type parameters
if (aa.TypeArgs.Count != bb.TypeArgs.Count) {
return false;
@@ -5690,6 +5861,13 @@ namespace Microsoft.Dafny // ---------- new C
Contract.Assert(rr.ArrayDimensions == null && rr.OptionalNameComponent == null && rr.InitCall == null);
}
+ if (rr.EType is UserDefinedType)
+ {
+ if (((UserDefinedType)rr.EType).ResolvedClass is TraitDecl)
+ {
+ Error(stmt, "new can not be applied to a trait");
+ }
+ }
if (!callsConstructor && rr.EType is UserDefinedType) {
var udt = (UserDefinedType)rr.EType;
var cl = (ClassDecl)udt.ResolvedClass; // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test
|