feat: Datatype ghost constructors

RELEASE_NOTES.md

@@ -15,6 +15,7 @@
 - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
 - fix: Better messages on hovering failing postconditions in IDE (https://github.com/dafny-lang/dafny/pull/2654)
 - fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650)
+- feat: Introduced ghost constructors in datatypes. One use of these is when working with uninitialized storage, see https://github.com/dafny-lang/rfcs/pull/11. (https://github.com/dafny-lang/dafny/pull/2666)
 
 # 3.8.0
 

Source/Dafny/AST/DafnyAst.cs

@@ -1206,11 +1206,21 @@ public OpaqueTypeDecl AsOpaqueType {
  return udt?.ResolvedClass as OpaqueTypeDecl;
  }
  }
- public virtual bool SupportsEquality {
- get {
- return true;
- }
- }
+
+ /// <summary>
+ /// Returns whether or not any values of the type can be checked for equality in compiled contexts
+ /// </summary>
+ public virtual bool SupportsEquality => true;
+
+ /// <summary>
+ /// Returns whether or not some values of the type can be checked for equality in compiled contexts.
+ /// This differs from SupportsEquality for types where the equality operation is partial, e.g.,
+ /// for datatypes where some, but not all, constructors are ghost.
+ /// Note, whereas SupportsEquality sometimes consults some constituent type for SupportEquality
+ /// (e.g., seq<T> supports equality if T does), PartiallySupportsEquality does not (because the
+ /// semantic check would be more complicated and it currently doesn't seem worth the trouble).
+ /// </summary>
+ public virtual bool PartiallySupportsEquality => SupportsEquality;
 
  public bool MayInvolveReferences => ComputeMayInvolveReferences(null);
 
@@ -2875,6 +2885,29 @@ public override bool SupportsEquality {
  }
  }
 
+ public override bool PartiallySupportsEquality {
+ get {
+ var totalEqualitySupport = SupportsEquality;
+ if (!totalEqualitySupport && ResolvedClass is IndDatatypeDecl dt && dt.IsRevealedInScope(Type.GetScope())) {
+ // Equality is partially supported for:
+ // an inductive datatype with at least one non-ghost constructor where every argument of a non-ghost constructor
+ // totally supports equality.
+ var hasNonGhostConstructor = false;
+ foreach (var ctor in dt.Ctors) {
+ if (!ctor.IsGhost) {
+ hasNonGhostConstructor = true;
+ if (!ctor.Formals.All(formal => !formal.IsGhost && formal.Type.SupportsEquality)) {
+ return false;
+ }
+ }
+ }
+ Contract.Assert(dt.HasGhostVariant); // sanity check (if the types of all formals support equality, then either .SupportsEquality or there is a ghost constructor)
+ return hasNonGhostConstructor;
+ }
+ return totalEqualitySupport;
+ }
+ }
+
  public override bool ComputeMayInvolveReferences(ISet<DatatypeDecl> visitedDatatypes) {
  if (ResolvedClass is ArrowTypeDecl) {
  return TypeArgs.Any(ta => ta.ComputeMayInvolveReferences(visitedDatatypes));
@@ -4474,14 +4507,17 @@ public DatatypeDecl(IToken tok, string name, ModuleDefinition module, List<TypeP
  }
  public bool HasFinitePossibleValues {
  get {
+ // Note, to determine finiteness, it doesn't matter if the constructors are ghost or non-ghost.
  return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0));
  }
  }
 
  public bool IsRecordType {
- get { return this is IndDatatypeDecl && Ctors.Count == 1; }
+ get { return this is IndDatatypeDecl && Ctors.Count == 1 && !Ctors[0].IsGhost; }
  }
 
+ public bool HasGhostVariant => Ctors.Any(ctor => ctor.IsGhost);
+
  public TopLevelDecl AsTopLevelDecl => this;
  public TypeDeclSynonymInfo SynonymInfo { get; set; }
 
@@ -4551,7 +4587,7 @@ public CoDatatypeDecl(IToken tok, string name, ModuleDefinition module, List<Typ
  }
 
  public override DatatypeCtor GetGroundingCtor() {
- return Ctors[0];
+ return Ctors.FirstOrDefault(ctor => ctor.IsGhost, Ctors[0]);
  }
  }
 
@@ -4593,6 +4629,7 @@ public Type CreateType(List<Type> typeArgs) {
  }
 
  public class DatatypeCtor : Declaration, TypeParameter.ParentType {
+ public readonly bool IsGhost;
  public readonly List<Formal> Formals;
  [ContractInvariantMethod]
  void ObjectInvariant() {
@@ -4608,12 +4645,13 @@ void ObjectInvariant() {
  [FilledInDuringResolution] public SpecialField QueryField;
  [FilledInDuringResolution] public List<DatatypeDestructor> Destructors = new List<DatatypeDestructor>(); // includes both implicit (not mentionable in source) and explicit destructors
 
- public DatatypeCtor(IToken tok, string name, [Captured] List<Formal> formals, Attributes attributes)
+ public DatatypeCtor(IToken tok, string name, bool isGhost, [Captured] List<Formal> formals, Attributes attributes)
  : base(tok, name, attributes, false) {
  Contract.Requires(tok != null);
  Contract.Requires(name != null);
  Contract.Requires(cce.NonNullElements(formals));
  this.Formals = formals;
+ this.IsGhost = isGhost;
  }
 
  public string FullName {
@@ -5096,6 +5134,16 @@ public override string CompileName {
  }
  }
 
+ public class DatatypeDiscriminator : SpecialField {
+ public override string WhatKind {
+ get { return "discriminator"; }
+ }
+
+ public DatatypeDiscriminator(IToken tok, string name, ID specialId, object idParam, bool isGhost, Type type, Attributes attributes)
+ : base(tok, name, specialId, idParam, isGhost, false, false, type, attributes) {
+ }
+ }
+
  public class DatatypeDestructor : SpecialField {
  public readonly List<DatatypeCtor> EnclosingCtors = new List<DatatypeCtor>(); // is always a nonempty list
  public readonly List<Formal> CorrespondingFormals = new List<Formal>(); // is always a nonempty list
@@ -5137,18 +5185,7 @@ internal string EnclosingCtorNames(string grammaticalConjunction) {
  static internal string PrintableCtorNameList(List<DatatypeCtor> ctors, string grammaticalConjunction) {
  Contract.Requires(ctors != null);
  Contract.Requires(grammaticalConjunction != null);
- var n = ctors.Count;
- if (n == 1) {
- return string.Format("'{0}'", ctors[0].Name);
- } else if (n == 2) {
- return string.Format("'{0}' {1} '{2}'", ctors[0].Name, grammaticalConjunction, ctors[1].Name);
- } else {
- var s = "";
- for (int i = 0; i < n - 1; i++) {
- s += string.Format("'{0}', ", ctors[i].Name);
- }
- return s + string.Format("{0} '{1}'", grammaticalConjunction, ctors[n - 1].Name);
- }
+ return Util.PrintableNameList(ctors.ConvertAll(ctor => ctor.Name), grammaticalConjunction);
  }
  }
 
@@ -10175,6 +10212,7 @@ public class MemberSelectExpr : Expression {
  public readonly string MemberName;
  [FilledInDuringResolution] public MemberDecl Member; // will be a Field or Function
  [FilledInDuringResolution] public Label /*?*/ AtLabel; // non-null for a two-state selection
+ [FilledInDuringResolution] public bool InCompiledContext;
 
  /// <summary>
  /// TypeApplication_AtEnclosingClass is the list of type arguments used to instantiate the type that
@@ -11177,6 +11215,8 @@ public static string OpcodeString(Opcode op) {
  public Expression E1;
  public enum AccumulationOperand { None, Left, Right }
  public AccumulationOperand AccumulatesForTailRecursion = AccumulationOperand.None; // set by Resolver
+ [FilledInDuringResolution] public bool InCompiledContext;
+
  [ContractInvariantMethod]
  void ObjectInvariant() {
  Contract.Invariant(E0 != null);
@@ -12820,7 +12860,11 @@ public static Expression MaybeTypeExpr(Expression e, Type t) {
  public class DatatypeUpdateExpr : ConcreteSyntaxExpression {
  public readonly Expression Root;
  public readonly List<Tuple<IToken, string, Expression>> Updates;
+ [FilledInDuringResolution] public List<MemberDecl> Members;
  [FilledInDuringResolution] public List<DatatypeCtor> LegalSourceConstructors;
+ [FilledInDuringResolution] public bool InCompiledContext;
+ [FilledInDuringResolution] public Expression ResolvedCompiledExpression; // see comment for Resolver.ResolveDatatypeUpdate
+
  public DatatypeUpdateExpr(IToken tok, Expression root, List<Tuple<IToken, string, Expression>> updates)
  : base(tok) {
  Contract.Requires(tok != null);

Source/Dafny/AST/Printer.cs

@@ -761,7 +761,7 @@ public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted)
  string sep = "";
  foreach (DatatypeCtor ctor in dt.Ctors) {
  wr.Write(sep);
- PrintClassMethodHelper("", ctor.Attributes, ctor.Name, new List<TypeParameter>());
+ PrintClassMethodHelper(ctor.IsGhost ? " ghost" : "", ctor.Attributes, ctor.Name, new List<TypeParameter>());
  if (ctor.Formals.Count != 0) {
  PrintFormals(ctor.Formals, null);
  }

Source/Dafny/AST/TupleTypeDecl.cs

@@ -73,7 +73,7 @@ private static List<DatatypeCtor> CreateConstructors(List<TypeParameter> typeArg
  formals.Add(f);
  }
  string ctorName = BuiltIns.TupleTypeCtorName(typeArgs.Count);
- var ctor = new DatatypeCtor(Token.NoToken, ctorName, formals, null);
+ var ctor = new DatatypeCtor(Token.NoToken, ctorName, false, formals, null);
  return new List<DatatypeCtor>() { ctor };
  }
 

Source/Dafny/Cloner.cs

@@ -137,7 +137,7 @@ public TypeParameter.TypeParameterCharacteristics CloneTPChar(TypeParameter.Type
  }
 
  public DatatypeCtor CloneCtor(DatatypeCtor ct) {
- return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes));
+ return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.IsGhost, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes));
  }
 
  public TypeParameter CloneTypeParam(TypeParameter tp) {

Source/Dafny/Compilers/Compiler-Csharp.cs

@@ -517,15 +517,19 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
  }
 
  var groundingCtor = dt.GetGroundingCtor();
- if (dt is CoDatatypeDecl) {
- var wCo = wDefault;
- wDefault = new ConcreteSyntaxTree();
- wCo.Format($"new {dt.CompileName}__Lazy{DtT_TypeArgs}(() => {{ return {wDefault}; }})");
- }
+ if (groundingCtor.IsGhost) {
+ wDefault.Write(ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wDefault, dt.tok));
+ } else {
+ if (dt is CoDatatypeDecl) {
+ var wCo = wDefault;
+ wDefault = new ConcreteSyntaxTree();
+ wCo.Format($"new {dt.CompileName}__Lazy{DtT_TypeArgs}(() => {{ return {wDefault}; }})");
+ }
 
- wDefault.Write(DtCreateName(groundingCtor));
- var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost);
- wDefault.Write($"({nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok))})");
+ wDefault.Write(DtCreateName(groundingCtor));
+ var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost);
+ wDefault.Write($"({nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok))})");
+ }
 
  EmitTypeDescriptorMethod(dt, wr);
 
@@ -536,6 +540,9 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
 
  // create methods
  foreach (var ctor in dt.Ctors) {
+ if (ctor.IsGhost) {
+ continue;
+ }
  wr.Write($"public static {DtTypeName(dt)} {DtCreateName(ctor)}(");
  WriteFormals("", ctor.Formals, wr);
  var w = wr.NewBlock(")");
@@ -548,6 +555,9 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
  // omit the is_ property for tuples, since it cannot be used syntactically in the language
  } else {
  foreach (var ctor in dt.Ctors) {
+ if (ctor.IsGhost) {
+ continue;
+ }
  interfaceTree.WriteLine($"bool is_{ctor.CompileName} {{ get; }}");
 
  var returnValue = dt.IsRecordType
@@ -566,7 +576,11 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
  var wGet = w.NewBlock("get");
  foreach (var ctor in dt.Ctors) {
  Contract.Assert(ctor.Formals.Count == 0);
- wGet.WriteLine($"yield return {DtT_protected}.{DtCreateName(ctor)}();");
+ if (ctor.IsGhost) {
+ wGet.WriteLine($"yield return {ForcePlaceboValue(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wGet, dt.tok)};");
+ } else {
+ wGet.WriteLine($"yield return {DtT_protected}.{DtCreateName(ctor)}();");
+ }
  }
  }
 
@@ -697,8 +711,9 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre
  ConcreteSyntaxTree interfaceTree, string DtT_TypeArgs) {
  foreach (var ctor in dt.Ctors) {
  var index = 0;
- foreach (var dtor in ctor.Destructors) {
- if (dtor.EnclosingCtors[0] == ctor) {
+ foreach (var dtor in ctor.Destructors.Where(dtor => dtor.EnclosingCtors[0] == ctor)) {
+ var compiledConstructorCount = dtor.EnclosingCtors.Count(constructor => !constructor.IsGhost);
+ if (compiledConstructorCount != 0) {
  var arg = dtor.CorrespondingFormals[0];
  if (!arg.IsGhost) {
  var DtorM = arg.HasName ? "_" + arg.CompileName : FieldName(arg, index);
@@ -730,18 +745,23 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre
  wGet.WriteLine("var d = this;");
  }
 
- var n = dtor.EnclosingCtors.Count;
- for (int i = 0; i < n - 1; i++) {
+ var compiledConstructorsProcessed = 0;
+ for (var i = 0; i < dtor.EnclosingCtors.Count; i++) {
  var ctor_i = dtor.EnclosingCtors[i];
  Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[i].CompileName);
+ if (ctor_i.IsGhost) {
+ continue;
+ }
  var type = $"{dt.CompileName}_{ctor_i.CompileName}{DtT_TypeArgs}";
  // TODO use pattern matching to replace cast.
- wGet.WriteLine($"if (d is {type}) {{ return (({type})d).{IdProtect(DtorM)}; }}");
+ var returnTheValue = $"return (({type})d).{IdProtect(DtorM)};";
+ if (compiledConstructorsProcessed < compiledConstructorCount - 1) {
+ wGet.WriteLine($"if (d is {type}) {{ {returnTheValue} }}");
+ } else {
+ wGet.WriteLine(returnTheValue);
+ }
+ compiledConstructorsProcessed++;
  }
-
- Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[n - 1].CompileName);
- wGet.WriteLine(
- $"return (({dt.CompileName}_{dtor.EnclosingCtors[n - 1].CompileName}{DtT_TypeArgs})d).{IdProtect(DtorM)};");
  }
  index++;
  }
@@ -836,6 +856,9 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx
 
  int constructorIndex = 0; // used to give each constructor a different name
  foreach (DatatypeCtor ctor in dt.Ctors) {
+ if (ctor.IsGhost) {
+ continue;
+ }
  var wr = wrx.NewNamedBlock(
  $"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {IdName(dt)}{typeParams}");
  DatatypeFieldsAndConstructor(ctor, constructorIndex, wr);
@@ -1029,6 +1052,7 @@ string DtCtorName(DatatypeCtor ctor) {
  }
 
  string DtCreateName(DatatypeCtor ctor) {
+ Contract.Assert(!ctor.IsGhost); // there should never be an occasion to ask for a ghost constructor
  if (ctor.EnclosingDatatype.IsRecordType) {
  return "create";
  } else {
@@ -1551,7 +1575,8 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
  }
  }
 
- protected override string TypeName_UDT(string fullCompileName, List<TypeParameter.TPVariance> variance, List<Type> typeArgs, ConcreteSyntaxTree wr, IToken tok) {
+ protected override string TypeName_UDT(string fullCompileName, List<TypeParameter.TPVariance> variance, List<Type> typeArgs,
+ ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments = false) {
  Contract.Assume(fullCompileName != null); // precondition; this ought to be declared as a Requires in the superclass
  Contract.Assume(variance != null); // precondition; this ought to be declared as a Requires in the superclass
  Contract.Assume(typeArgs != null); // precondition; this ought to be declared as a Requires in the superclass

Source/Dafny/Compilers/Compiler-cpp.cs

@@ -327,7 +327,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT
  }
 
  // Optimize a not-uncommon case
- if (dt.Ctors.Count == 1) {
+ if (dt.IsRecordType) {
  var ctor = dt.Ctors[0];
  var ws = wdecl.NewBlock(String.Format("{0}\nstruct {1}", DeclareTemplate(dt.TypeArgs), DtT_protected), ";");
 
@@ -394,6 +394,9 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT
 
  /*** Create one struct for each constructor ***/
  foreach (var ctor in dt.Ctors) {
+ if (ctor.IsGhost) {
+ continue;
+ }
  string structName = DatatypeSubStructName(ctor);
  var wstruct = wdecl.NewBlock(String.Format("{0}\nstruct {1}", DeclareTemplate(dt.TypeArgs), structName), ";");
  // Declare the struct members
@@ -1111,7 +1114,8 @@ private string ActualTypeArgs(List<Type> typeArgs) {
  ? String.Format(" <{0}> ", Util.Comma(typeArgs, tp => TypeName(tp, null, null))) : "";
  }
 
- protected override string TypeName_UDT(string fullCompileName, List<TypeParameter.TPVariance> variance, List<Type> typeArgs, ConcreteSyntaxTree wr, IToken tok) {
+ protected override string TypeName_UDT(string fullCompileName, List<TypeParameter.TPVariance> variance, List<Type> typeArgs,
+ ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments) {
  Contract.Assume(fullCompileName != null); // precondition; this ought to be declared as a Requires in the superclass
  Contract.Assume(typeArgs != null); // precondition; this ought to be declared as a Requires in the superclass
  string s = IdProtect(fullCompileName);