chore: Rename adjustment to refinement (#5139)

This PR renames "adjustment type" to the better name "refinement type".
It also adds documentation to the class `Advice`.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Cloner.cs

@@ -256,9 +256,9 @@ public virtual Type CloneType(Type t) {
  return inferredTypeProxy;
  } else if (t is ParamTypeProxy) {
  return new ParamTypeProxy(CloneTypeParam(((ParamTypeProxy)t).orig));
- } else if (t is AdjustableType adjustableType) {
- // don't bother keeping AdjustableType wrappers
- return CloneType(adjustableType.T);
+ } else if (t is TypeRefinementWrapper typeRefinementWrapper) {
+ // don't bother keeping TypeRefinementWrapper wrappers
+ return CloneType(typeRefinementWrapper.T);
  } else {
  Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time)
  return null; // to please compiler

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -61,10 +61,11 @@ public Type Type {
  }
 
  /// <summary>
- /// The new type inference includes a "type adjustment" phase, which determines the best subset types for a program. This phase works
- /// by adjusting (mutating) types in place, using "AdjustableType" type proxies. During that phase, it is necessary to obtain the
+ /// The new type inference includes a "type refinement" phase, which determines the best subset types for a program. This phase works
+ /// by refining (mutating in the direction from bottom, meaning un ansatisfiable constraint, to top, meaning no constraint) types in place,
+ /// using "TypeRefinementWrapper" type proxies. During that phase, it is necessary to obtain the
  /// un-normalized type stored in each AST node, which is what the "UnnormalizedType" property does. This property should only be used
- /// during the type adjustment phase. After type inference is complete, use ".Type" instead.
+ /// during the type refinement phase. After type inference is complete, use ".Type" instead.
  /// </summary>
  public Type UnnormalizedType {
  get {

Source/DafnyCore/AST/Grammar/Printer/Printer.cs

@@ -1176,10 +1176,10 @@ public void PrintType(string prefix, Type ty) {
  Contract.Requires(prefix != null);
  Contract.Requires(ty != null);
  if (options.DafnyPrintResolvedFile != null) {
- ty = AdjustableType.NormalizeSansAdjustableType(ty);
+ ty = TypeRefinementWrapper.NormalizeSansRefinementWrappers(ty);
  }
  string s = ty.TypeName(options, null, true);
- if (ty is AdjustableType or not TypeProxy && !s.StartsWith("_")) {
+ if (ty is TypeRefinementWrapper or not TypeProxy && !s.StartsWith("_")) {
  wr.Write("{0}{1}", prefix, s);
  }
  }

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1094,7 +1094,7 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
  }
 
  if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
- var typeAdjustor = new TypeAdjustorVisitor(moduleDescription, SystemModuleManager);
+ var typeAdjustor = new TypeRefinementVisitor(moduleDescription, SystemModuleManager);
  typeAdjustor.VisitDeclarations(declarations);
  typeAdjustor.Solve(reporter, Options.Get(CommonOptionBag.NewTypeInferenceDebug));
  }

Source/DafnyCore/Resolver/PreType/Flows.cs

@@ -17,15 +17,15 @@ record FlowContext(SystemModuleManager SystemModuleManager, ErrorReporter Report
 }
 
 /// <summary>
-/// A "Flow" is a puzzle piece in recomputing types. The "type adjustment" phase defines a set of flows and then
+/// A "Flow" is a puzzle piece in recomputing types. The "type refinement" phase defines a set of flows and then
 /// recomputes types until it reaches a fix point.
 ///
-/// For example, the type adjustment phase will use a FlowIntoVariable to define a flow from the RHS of an assignment to
+/// For example, the type refinement phase will use a FlowIntoVariable to define a flow from the RHS of an assignment to
 /// the LHS. It will use a FlowBetweenExpressions to define a flow from the "then" branch of an "if-then-else" expression
 /// to the "if-then-else" expression itself, and will use another FlowBetweenExpressions to define the analogous flow from
 /// the "else" branch.
 ///
-/// For more information about type adjustments, flow, and the whole type inference process, see docs/dev/TypeSystemRefresh.md.
+/// For more information about type refinements, flow, and the whole type inference process, see docs/dev/TypeSystemRefresh.md.
 /// </summary>
 abstract class Flow {
  private readonly IToken tok;
@@ -48,15 +48,15 @@ protected Flow(IToken tok, string description) {
 
  public abstract void DebugPrint(TextWriter output);
 
- protected bool UpdateAdjustableType(Type sink, Type sourceType, FlowContext context) {
+ protected bool UpdateTypeHeldByRefinementWrapper(Type sink, Type sourceType, FlowContext context) {
  string previousLhs = null;
  string joinArguments = null;
  if (context.DebugPrint) {
- previousLhs = $"{AdjustableType.ToStringAsAdjustableType(sink)}";
- joinArguments = $"{AdjustableType.ToStringAsBottom(sink)} \\/ {AdjustableType.ToStringAsBottom(sourceType)}";
+ previousLhs = $"{TypeRefinementWrapper.ToStringShowingWrapper(sink)}";
+ joinArguments = $"{TypeRefinementWrapper.ToStringAsBottom(sink)} \\/ {TypeRefinementWrapper.ToStringAsBottom(sourceType)}";
  }
 
- var previousSink = (AdjustableType.NormalizeSansAdjustableType(sink) as AdjustableType)?.T ?? sink;
+ var previousSink = (TypeRefinementWrapper.NormalizeSansRefinementWrappers(sink) as TypeRefinementWrapper)?.T ?? sink;
  var join = JoinAndUpdate(sink, sourceType, context);
  if (join == null) {
  HasError = true;
@@ -66,62 +66,62 @@ protected bool UpdateAdjustableType(Type sink, Type sourceType, FlowContext cont
  return false;
  }
  if (context.DebugPrint) {
- context.OutputWriter.WriteLine($"DEBUG: adjusting {previousLhs} to {AdjustableType.ToStringAsBottom(sink)} ({joinArguments})");
+ context.OutputWriter.WriteLine($"DEBUG: refining {previousLhs} to {TypeRefinementWrapper.ToStringAsBottom(sink)} ({joinArguments})");
  }
  return true;
  }
 
  protected static bool EqualTypes(Type a, Type b) {
- if (AdjustableType.NormalizesToBottom(a) != AdjustableType.NormalizesToBottom(b)) {
+ if (TypeRefinementWrapper.NormalizesToBottom(a) != TypeRefinementWrapper.NormalizesToBottom(b)) {
  return false;
  }
  return a.Equals(b, true);
  }
 
  [CanBeNull]
  public static Type JoinAndUpdate(Type a, Type b, FlowContext context) {
- var adjustableA = AdjustableType.NormalizeSansAdjustableType(a) as AdjustableType;
- var adjustableB = AdjustableType.NormalizeSansAdjustableType(b) as AdjustableType;
- var join = Join(adjustableA?.T ?? a, adjustableB?.T ?? b, context);
+ var wrapperA = TypeRefinementWrapper.NormalizeSansRefinementWrappers(a) as TypeRefinementWrapper;
+ var wrapperB = TypeRefinementWrapper.NormalizeSansRefinementWrappers(b) as TypeRefinementWrapper;
+ var join = Join(wrapperA?.T ?? a, wrapperB?.T ?? b, context);
  if (join == null) {
  return null;
  }
- if (adjustableA == null) {
+ if (wrapperA == null) {
  return join;
  }
 
- if (AdjustableType.NormalizeSansAdjustableType(join) is AdjustableType adjustableJoin) {
- join = adjustableJoin.T;
+ if (TypeRefinementWrapper.NormalizeSansRefinementWrappers(join) is TypeRefinementWrapper wrapperJoin) {
+ join = wrapperJoin.T;
  }
- adjustableA.T = join;
- return adjustableA;
+ wrapperA.T = join;
+ return wrapperA;
  }
 
  [CanBeNull]
  public static Type CopyAndUpdate(Type a, Type b, FlowContext context) {
- var adjustableA = AdjustableType.NormalizeSansAdjustableType(a) as AdjustableType;
+ var wrapperA = TypeRefinementWrapper.NormalizeSansRefinementWrappers(a) as TypeRefinementWrapper;
  // compute the "copy" of aa and b:
  Type copy;
- if (AdjustableType.NormalizesToBottom(a)) {
+ if (TypeRefinementWrapper.NormalizesToBottom(a)) {
  copy = b;
- } else if (AdjustableType.NormalizesToBottom(b)) {
+ } else if (TypeRefinementWrapper.NormalizesToBottom(b)) {
  copy = a;
  } else if (a.Equals(b, true)) {
  copy = a;
  } else {
  return null;
  }
 
- if (adjustableA == null) {
+ if (wrapperA == null) {
  return copy;
  }
 
- copy = AdjustableType.NormalizeSansAdjustableType(copy);
- if (copy is AdjustableType adjustableCopy) {
- copy = adjustableCopy.T;
+ copy = TypeRefinementWrapper.NormalizeSansRefinementWrappers(copy);
+ if (copy is TypeRefinementWrapper wrapperCopy) {
+ copy = wrapperCopy.T;
  }
- adjustableA.T = copy;
- return adjustableA;
+ wrapperA.T = copy;
+ return wrapperA;
  }
 
  /// <summary>
@@ -305,19 +305,19 @@ class FlowIntoVariable : Flow {
 
  public FlowIntoVariable(IVariable variable, Expression source, IToken tok, string description = ":=")
  : base(tok, description) {
- this.sink = AdjustableType.NormalizeSansAdjustableType(variable.UnnormalizedType);
+ this.sink = TypeRefinementWrapper.NormalizeSansRefinementWrappers(variable.UnnormalizedType);
  this.source = source;
  }
 
  public override bool Update(FlowContext context) {
- return UpdateAdjustableType(sink, AdjustableType.NormalizeSansBottom(source), context);
+ return UpdateTypeHeldByRefinementWrapper(sink, TypeRefinementWrapper.NormalizeSansBottom(source), context);
  }
 
  public override void DebugPrint(TextWriter output) {
- var lhs = AdjustableType.ToStringAsAdjustableType(sink);
- var rhs = AdjustableType.ToStringAsAdjustableType(source.UnnormalizedType);
+ var lhs = TypeRefinementWrapper.ToStringShowingWrapper(sink);
+ var rhs = TypeRefinementWrapper.ToStringShowingWrapper(source.UnnormalizedType);
  var bound = PreTypeConstraints.Pad($"{lhs} :> {rhs}", 27);
- var value = PreTypeConstraints.Pad(AdjustableType.ToStringAsBottom(sink), 20);
+ var value = PreTypeConstraints.Pad(TypeRefinementWrapper.ToStringAsBottom(sink), 20);
  output.WriteLine($" {bound} {value} {TokDescription()}");
  }
 }
@@ -328,18 +328,18 @@ class FlowIntoVariableFromComputedType : Flow {
 
  public FlowIntoVariableFromComputedType(IVariable variable, System.Func<Type> getType, IToken tok, string description = ":=")
  : base(tok, description) {
- this.sink = AdjustableType.NormalizeSansAdjustableType(variable.UnnormalizedType);
+ this.sink = TypeRefinementWrapper.NormalizeSansRefinementWrappers(variable.UnnormalizedType);
  this.getType = getType;
  }
 
  public override bool Update(FlowContext context) {
- return UpdateAdjustableType(sink, getType(), context);
+ return UpdateTypeHeldByRefinementWrapper(sink, getType(), context);
  }
 
  public override void DebugPrint(TextWriter output) {
  var sourceType = getType();
- var bound = PreTypeConstraints.Pad($"{AdjustableType.ToStringAsAdjustableType(sink)} :> {AdjustableType.ToStringAsAdjustableType(sourceType)}", 27);
- var value = PreTypeConstraints.Pad(AdjustableType.ToStringAsBottom(sink), 20);
+ var bound = PreTypeConstraints.Pad($"{TypeRefinementWrapper.ToStringShowingWrapper(sink)} :> {TypeRefinementWrapper.ToStringShowingWrapper(sourceType)}", 27);
+ var value = PreTypeConstraints.Pad(TypeRefinementWrapper.ToStringAsBottom(sink), 20);
  output.WriteLine($" {bound} {value} {TokDescription()}");
  }
 }
@@ -354,13 +354,13 @@ public FlowBetweenComputedTypes(System.Func<(Type, Type)> getTypes, IToken tok,
 
  public override bool Update(FlowContext context) {
  var (sink, source) = getTypes();
- return UpdateAdjustableType(sink, source, context);
+ return UpdateTypeHeldByRefinementWrapper(sink, source, context);
  }
 
  public override void DebugPrint(TextWriter output) {
  var (sink, source) = getTypes();
- var bound = PreTypeConstraints.Pad($"{AdjustableType.ToStringAsAdjustableType(sink)} :> {AdjustableType.ToStringAsAdjustableType(source)}", 27);
- var value = PreTypeConstraints.Pad(AdjustableType.ToStringAsBottom(sink), 20);
+ var bound = PreTypeConstraints.Pad($"{TypeRefinementWrapper.ToStringShowingWrapper(sink)} :> {TypeRefinementWrapper.ToStringShowingWrapper(source)}", 27);
+ var value = PreTypeConstraints.Pad(TypeRefinementWrapper.ToStringAsBottom(sink), 20);
  output.WriteLine($" {bound} {value} {TokDescription()}");
  }
 }
@@ -370,7 +370,7 @@ abstract class FlowIntoExpr : Flow {
 
  protected FlowIntoExpr(Type sink, IToken tok, string description = "")
  : base(tok, description) {
- this.sink = AdjustableType.NormalizeSansAdjustableType(sink);
+ this.sink = TypeRefinementWrapper.NormalizeSansRefinementWrappers(sink);
  }
 
  protected FlowIntoExpr(Expression sink, IToken tok, string description = "")
@@ -381,13 +381,13 @@ protected FlowIntoExpr(Expression sink, IToken tok, string description = "")
  protected abstract Type GetSourceType();
 
  public override bool Update(FlowContext context) {
- return UpdateAdjustableType(sink, GetSourceType(), context);
+ return UpdateTypeHeldByRefinementWrapper(sink, GetSourceType(), context);
  }
 
  public override void DebugPrint(TextWriter output) {
  var sourceType = GetSourceType();
- var bound = PreTypeConstraints.Pad($"{AdjustableType.ToStringAsAdjustableType(sink)} :> {AdjustableType.ToStringAsAdjustableType(sourceType)}", 27);
- var value = PreTypeConstraints.Pad(AdjustableType.ToStringAsBottom(sink), 20);
+ var bound = PreTypeConstraints.Pad($"{TypeRefinementWrapper.ToStringShowingWrapper(sink)} :> {TypeRefinementWrapper.ToStringShowingWrapper(sourceType)}", 27);
+ var value = PreTypeConstraints.Pad(TypeRefinementWrapper.ToStringAsBottom(sink), 20);
  output.WriteLine($" {bound} {value} {TokDescription()}");
  }
 }
@@ -481,6 +481,6 @@ public FlowBetweenExpressions(Expression sink, Expression source, string descrip
  }
 
  protected override Type GetSourceType() {
- return AdjustableType.NormalizeSansBottom(source);
+ return TypeRefinementWrapper.NormalizeSansBottom(source);
  }
 }

Source/DafnyCore/Resolver/PreType/PreType2TypeUtil.cs

@@ -12,9 +12,9 @@
 namespace Microsoft.Dafny;
 
 public static class PreType2TypeUtil {
- public static Type PreType2Type(PreType preType, bool allowFutureAdjustments, TypeParameter.TPVariance futureAdjustments) {
- if (allowFutureAdjustments) {
- return PreType2AdjustableType(preType, futureAdjustments);
+ public static Type PreType2Type(PreType preType, bool allowFutureRefinements, TypeParameter.TPVariance futureRefinements) {
+ if (allowFutureRefinements) {
+ return PreType2RefinableType(preType, futureRefinements);
  } else {
  return PreType2FixedType(preType);
  }
@@ -24,30 +24,30 @@ public static Type PreType2FixedType(PreType preType) {
  return PreType2TypeCore(preType, false, TypeParameter.TPVariance.Co);
  }
 
- public static Type PreType2AdjustableType(PreType preType, TypeParameter.TPVariance futureAdjustments) {
- var ty = PreType2TypeCore(preType, true, futureAdjustments);
- switch (futureAdjustments) {
+ public static Type PreType2RefinableType(PreType preType, TypeParameter.TPVariance futureRefinements) {
+ var ty = PreType2TypeCore(preType, true, futureRefinements);
+ switch (futureRefinements) {
  case TypeParameter.TPVariance.Co:
  ty = new BottomTypePlaceholder(ty);
  break;
  default:
  break;
  }
 
- return new AdjustableType(ty);
+ return new TypeRefinementWrapper(ty);
  }
 
  /// <summary>
- /// The "futureAdjustment" parameter is relevant only if "allowFutureAdjustments" is "true".
+ /// The "futureRefinements" parameter is relevant only if "allowFutureRefinements" is "true".
  /// </summary>
- private static Type PreType2TypeCore(PreType preType, bool allowFutureAdjustments, TypeParameter.TPVariance futureAdjustments) {
+ private static Type PreType2TypeCore(PreType preType, bool allowFutureRefinements, TypeParameter.TPVariance futureRefinements) {
  var pt = (DPreType)preType.Normalize(); // all pre-types should have been filled in and resolved to a non-proxy
  if (pt.PrintablePreType != null) {
  pt = pt.PrintablePreType;
  }
 
  Type ArgumentAsCo(int i) {
- return PreType2Type(pt.Arguments[i], true, futureAdjustments);
+ return PreType2Type(pt.Arguments[i], true, futureRefinements);
  }
 
  switch (pt.Decl.Name) {
@@ -77,7 +77,7 @@ Type ArgumentAsCo(int i) {
  break;
  }
 
- var arguments = pt.Arguments.ConvertAll(preType => PreType2AdjustableType(preType, futureAdjustments));
+ var arguments = pt.Arguments.ConvertAll(preType => PreType2RefinableType(preType, futureRefinements));
  if (pt.Decl is ArrowTypeDecl arrowTypeDecl) {
  return new ArrowType(pt.Decl.tok, arrowTypeDecl, arguments);
  } else if (pt.Decl is ValuetypeDecl valuetypeDecl) {
@@ -89,8 +89,8 @@ Type ArgumentAsCo(int i) {
  }
  }
 
- public static void Combine(Type userSuppliedType, PreType preType, bool allowFutureAdjustments) {
- var preTypeConverted = PreType2Type(preType, allowFutureAdjustments, TypeParameter.TPVariance.Co);
+ public static void Combine(Type userSuppliedType, PreType preType, bool allowFutureRefinements) {
+ var preTypeConverted = PreType2Type(preType, allowFutureRefinements, TypeParameter.TPVariance.Co);
  Combine(userSuppliedType, preTypeConverted);
  }
 
@@ -102,19 +102,19 @@ public static void Combine(Type userSuppliedType, PreType preType, bool allowFut
  /// "preTypes" are expected to have the same length. The respective types and pre-types are combined in "types",
  /// and then "types" is returned.
  /// </summary>
- public static List<Type> Combine([CanBeNull] List<Type> types, List<PreType> preTypes, bool allowFutureAdjustments) {
+ public static List<Type> Combine([CanBeNull] List<Type> types, List<PreType> preTypes, bool allowFutureRefinements) {
  Contract.Requires(types == null || types.Count == preTypes.Count);
  if (types == null) {
- if (allowFutureAdjustments) {
- return preTypes.ConvertAll(preType => PreType2AdjustableType(preType, TypeParameter.TPVariance.Co));
+ if (allowFutureRefinements) {
+ return preTypes.ConvertAll(preType => PreType2RefinableType(preType, TypeParameter.TPVariance.Co));
  } else {
  return preTypes.ConvertAll(PreType2FixedType);
  }
  }
 
  Contract.Assert(types.Count == preTypes.Count);
  for (var i = 0; i < types.Count; i++) {
- Combine(types[i], preTypes[i], allowFutureAdjustments);
+ Combine(types[i], preTypes[i], allowFutureRefinements);
  }
  return types;
  }
@@ -127,7 +127,7 @@ private static void Combine(Type type, Type preTypeConverted) {
  if (type is TypeProxy { T: null } typeProxy) {
  typeProxy.T = preTypeConverted;
  } else {
- // Even if the head type of preTypeConverted is adjustable, we're going to stick with the user-defined type, so we Normalize() here.
+ // Even if the head type of preTypeConverted is a refinement wrapper, we're going to stick with the user-defined type, so we Normalize() here.
  preTypeConverted = preTypeConverted.Normalize();
 
  Contract.Assert((type as UserDefinedType)?.ResolvedClass == (preTypeConverted as UserDefinedType)?.ResolvedClass);