diff options
Diffstat (limited to 'Source/Dafny')
-rw-r--r-- | Source/Dafny/Cloner.cs | 7 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 40 |
2 files changed, 28 insertions, 19 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 5dfc67d5..b462f983 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -137,8 +137,6 @@ namespace Microsoft.Dafny var f = (Field)member;
Field field = new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));
field.Inherited = member.Inherited; //we do need this information in ResolveClassMemberTypes method
- if (field.Type is UserDefinedType)
- ((UserDefinedType)field.Type).ResolvedClass = ((UserDefinedType)(((Field)(member)).Type)).ResolvedClass;
return field;
} else if (member is Function) {
var f = (Function)member;
@@ -184,7 +182,10 @@ namespace Microsoft.Dafny }
public Formal CloneFormal(Formal formal) {
- return new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
+ Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
+ if (f.Type is UserDefinedType && formal.Type is UserDefinedType)
+ ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(formal.Type)).ResolvedClass;
+ return f;
}
public BoundVar CloneBoundVar(BoundVar bv) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d503076c..9798e79f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2916,13 +2916,16 @@ namespace Microsoft.Dafny else //the member is not already in the class
{
MemberDecl classNewMember = cloner.CloneMember(traitMem.Value);
+ if (classNewMember is Field)
+ {
+ Field f = (Field)classNewMember;
+ if (f.Type is UserDefinedType)
+ ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(((Field)(traitMem.Value)).Type)).ResolvedClass;
+ }
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
@@ -2934,27 +2937,32 @@ namespace Microsoft.Dafny 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)
+ if (traitFunc.Body == null) //we do this check only if trait function body is null
{
- Function classFunc = (Function)classMem;
- refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc);
+ 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);
}
- 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)
+ if (traitMethod.Body == null) //we do this check only if trait method body is null
{
- Method classMethod = (Method)classMem;
- refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);
+ 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);
}
- if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)
- Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);
}
}
}
|