Add comments to existing code #4
Conversation
This reverts commit 6011c93.
|
|
||
| namespace Microsoft.Dafny; | ||
|
|
||
| public class TypeRefinementWrapper : TypeProxy { |
There was a problem hiding this comment.
Can you add a comment to this class? The suffix Wrapper doesn't tell me anything. I think it has the same meaning as Proxy in TypeProxy. Consider renaming to RefinementTypeProxy.
Also it doesn't seem to have any members that TypeProxy does not have, apart from the debug field UniqueId. Is that not useful for TypeProxy as well? Why even have the class TypeRefinementWrapper ?
There was a problem hiding this comment.
Do the descriptions in docs/dev/TypeSystemRefresh.md help?
| } | ||
| } | ||
|
|
||
| public class BottomTypePlaceholder : TypeProxy { |
There was a problem hiding this comment.
Can you add an extensive comment to this class?
In debugging dafny-lang#5385
I see that the join of BottomTypePlaceholder(Bar?) and BottomTypePlaceholder(Bar) results in BottomTypePlaceholder(Bar), which seems incorrect to me.
The join code contains:
if (a is BottomTypePlaceholder) {
return b;
} else if (b is BottomTypePlaceholder) {
return a;
}
Also some code where BottomTypePlaceholder is created seems unfinished:
public static Type Meet(Type a, Type b, FlowContext context) {
Contract.Requires(a != null);
Contract.Requires(b != null);
// a crude implementation for now
if (Type.IsSupertype(a, b)) {
return b;
} else if (Type.IsSupertype(b, a)) {
return a;
} else {
// TODO: the following may not be correct in the face of traits
return new BottomTypePlaceholder(a.NormalizeExpand());
}
}
| /// | ||
| /// For more information about type refinements, flow, and the whole type inference process, see docs/dev/TypeSystemRefresh.md. | ||
| /// </summary> | ||
| abstract class Flow { |
There was a problem hiding this comment.
The term Flow has no meaning to me. Consider renaming to RefinementConstraint
| return a.Equals(b, true); | ||
| } | ||
|
|
||
| [CanBeNull] |
There was a problem hiding this comment.
For future PRs: Adding #nullable enable to the top of the file, so that ? syntax can be used, leads to much better language tooling support than using the [CanBeNull] attribute.
| } | ||
|
|
||
| var previousSink = (TypeRefinementWrapper.NormalizeSansRefinementWrappers(sink) as TypeRefinementWrapper)?.T ?? sink; | ||
| var join = JoinAndUpdate(sink, sourceType, context); |
There was a problem hiding this comment.
Do we have a picture that explains the relation of types in Dafny? Joining and meeting makes me think of a lattice of types, but I thought it is only the pretypes that are organized in a lattice, while a base type and its refinements are all part of the same lattice node in the pretype lattice.
What is a join doing in refinement code?
Also, if I have to imagine doing joins and meets during refinement, then I would expect to be doing meets since a refined type object is more specific than a pretype object?
| } | ||
| } | ||
|
|
||
| public class DPreType : PreType { |
There was a problem hiding this comment.
Can you rename this to something specific like ConcretePretype or ResolvedPretype?
| /// | ||
| /// See also the description of https://github.com/dafny-lang/dafny/pull/3795. | ||
| /// </summary> | ||
| public abstract class PreType { |
There was a problem hiding this comment.
What alternative names did we think of for PreType again? Is the essence of a pretype that for any program value we can say in time that is at worst linear to the size of the program, whether that value is part of the type?
Suggestions: StaticType, FastType, CompleteType (favorite)
| base.VisitExtendedPattern(pattern, context); | ||
| } | ||
|
|
||
| public void Solve(ErrorReporter reporter, bool debugPrint) { |
There was a problem hiding this comment.
This looks like it runs in O(N^2) time, since both the number of flows and the number of required iterations can be linear in the size of the program. I don't think we can afford to have any computations in our pipeline that are non-linear in the size of the source.
Thoughts?
There was a problem hiding this comment.
Yes, the complexity is bad. The code is not optimized and, as you point out, each iteration goes over the whole module. This would be good to improve.
This PR serves only to add comments to existing code
Partly for debugging dafny-lang#5385