Skip to content

Commit

Permalink
Changing opaque type to abstract type (#3990)
Browse files Browse the repository at this point in the history 
Changing the ambiguous terminology 'opaque type' to 'abstract type'

<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>

---------

Co-authored-by: davidcok <[email protected]>
  • Loading branch information
@davidcok
davidcok and davidcok authored May 19, 2023
1 parent 33db038 commit 76dcc6b
Show file tree
Hide file tree
Showing 60 changed files with 234 additions and 235 deletions.
8 changes: 4 additions & 4 deletions Source/DafnyCore/AST/Cloner.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,9 +53,9 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m)
Contract.Requires(d != null);
Contract.Requires(m != null);

if (d is OpaqueTypeDecl) {
var dd = (OpaqueTypeDecl)d;
return new OpaqueTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
if (d is AbstractTypeDecl) {
var dd = (AbstractTypeDecl)d;
return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), m, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
} else if (d is SubsetTypeDecl) {
Contract.Assume(!(d is NonNullTypeDecl)); // don't clone the non-null type declaration; close the class, which will create a new non-null type declaration
var dd = (SubsetTypeDecl)d;
Expand Down Expand Up @@ -804,7 +804,7 @@ public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m
var tps = d.TypeArgs.ConvertAll(CloneTypeParam);
var characteristics = TypeParameter.GetExplicitCharacteristics(d);
var members = based is TopLevelDeclWithMembers tm ? tm.Members : new List<MemberDecl>();
var otd = new OpaqueTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), m, characteristics, tps, members, CloneAttributes(d.Attributes), d.IsRefining);
var otd = new AbstractTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), m, characteristics, tps, members, CloneAttributes(d.Attributes), d.IsRefining);
based = otd;
if (d is ClassDecl) {
reverseMap.Add(based, ((ClassDecl)d).NonNullTypeDecl);
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyCore/AST/Grammar/ParseErrors.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,7 @@ declared identifier.

Add(ErrorId.p_misplaced_ellipsis_in_newtype,
@"
There are limitations on refining a newtype, namely that the base type cannot be changed. You can change an opaque type into a newtype, however.
There are limitations on refining a newtype, namely that the base type cannot be changed. You can change an abstract type into a newtype, however.
");

Add(ErrorId.p_output_of_function_not_ghost,
Expand Down Expand Up @@ -282,7 +282,7 @@ its control flow produces (yields) a value, but the execution continues from tha
Add(ErrorId.p_unexpected_type_characteristic,
@"
[Type characteristics](https://dafny.org/latest/DafnyRef/DafnyRef#sec-type-parameters),
indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type.
indicated in parentheses after the type name, state properties of the otherwise uninterpreted or abstract type.
The currently defined type characteristics are designated by `==` (equality-supporting), `0` (auto-initializable), `00` (non-empty), and `!new` (non-reference).
", Replacements(new[] {
("==", "replace with '==' - this type supports equality"),
Expand All @@ -294,15 +294,15 @@ [Type characteristics](https://dafny.org/latest/DafnyRef/DafnyRef#sec-type-param
Add(ErrorId.p_missing_type_characteristic,
@"
[Type characteristics](https://dafny.org/latest/DafnyRef/DafnyRef#sec-type-parameters),
state properties of the otherwise uninterpreted or opaque type.
state properties of the otherwise uninterpreted or abstract type.
They are given in a parentheses-enclosed, comma-separated list after the type name.
The currently defined type characteristics are designated by `==` (equality - supporting), `0` (auto - initializable), `00` (non - empty), and `!new` (non - reference).
");

Add(ErrorId.p_illegal_type_characteristic,
@"
[Type characteristics](https://dafny.org/latest/DafnyRef/DafnyRef#sec-type-parameters),
indicated in parentheses after the type name, state properties of the otherwise uninterpreted or opaque type.
indicated in parentheses after the type name, state properties of the otherwise uninterpreted or abstract type.
The currently defined type characteristics are designated by `==` (equality - supporting), `0` (auto - initializable), `00` (non - empty), and `!new` (non - reference).
Type parameters are given in a parentheses-enclosed, comma-separated list after the type name.
");
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/AST/Grammar/Printer.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -276,8 +276,8 @@ public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent, List<IToken
foreach (TopLevelDecl d in decls) {
Contract.Assert(d != null);
if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; }
if (d is OpaqueTypeDecl) {
var at = (OpaqueTypeDecl)d;
if (d is AbstractTypeDecl) {
var at = (AbstractTypeDecl)d;
if (i++ != 0) { wr.WriteLine(); }
Indent(indent);
PrintClassMethodHelper("type", at.Attributes, at.Name + TPCharacteristicsSuffix(at.Characteristics), d.TypeArgs);
Expand Down
10 changes: 5 additions & 5 deletions Source/DafnyCore/AST/TopLevelDeclarations.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -347,8 +347,8 @@ public override string FullName {
public static TypeParameterCharacteristics GetExplicitCharacteristics(TopLevelDecl d) {
Contract.Requires(d != null);
TypeParameterCharacteristics characteristics = new TypeParameterCharacteristics(false);
if (d is OpaqueTypeDecl) {
var dd = (OpaqueTypeDecl)d;
if (d is AbstractTypeDecl) {
var dd = (AbstractTypeDecl)d;
characteristics = dd.Characteristics;
} else if (d is TypeSynonymDecl) {
var dd = (TypeSynonymDecl)d;
Expand Down Expand Up @@ -2081,15 +2081,15 @@ public NoContext(ModuleDefinition module) {
public bool AllowsAllocation => true;
}

public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring {
public override string WhatKind { get { return "opaque type"; } }
public class AbstractTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring {
public override string WhatKind { get { return "abstract type"; } }
public override bool CanBeRevealed() { return true; }
public readonly TypeParameter.TypeParameterCharacteristics Characteristics;
public bool SupportsEquality {
get { return Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified; }
}

public OpaqueTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, List<MemberDecl> members, Attributes attributes, bool isRefining)
public AbstractTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, List<MemberDecl> members, Attributes attributes, bool isRefining)
: base(rangeToken, name, module, typeArgs, members, attributes, isRefining) {
Contract.Requires(rangeToken != null);
Contract.Requires(name != null);
Expand Down
32 changes: 15 additions & 17 deletions Source/DafnyCore/AST/Types/Types.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ public Type NormalizeExpand(bool keepConstraints = false) {
Contract.Assert(cl.NonNullTypeDecl != null);
Contract.Assert(cl.NonNullTypeDecl.IsVisibleInScope(scope));
} else {
Contract.Assert(rtd is OpaqueTypeDecl);
Contract.Assert(rtd is AbstractTypeDecl);
}
}

Expand Down Expand Up @@ -354,8 +354,8 @@ AutoInitInfo CharacteristicToAutoInitInfo(TypeParameter.TypeParameterCharacteris
var udt = (UserDefinedType)t;
var cl = udt.ResolvedClass;
Contract.Assert(cl != null);
if (cl is OpaqueTypeDecl) {
var otd = (OpaqueTypeDecl)cl;
if (cl is AbstractTypeDecl) {
var otd = (AbstractTypeDecl)cl;
return CharacteristicToAutoInitInfo(otd.Characteristics);
} else if (cl is TypeParameter) {
var tp = (TypeParameter)cl;
Expand Down Expand Up @@ -814,13 +814,13 @@ public TypeParameter AsTypeParameter {
return ct?.ResolvedClass as TypeParameter;
}
}
public bool IsOpaqueType {
get { return AsOpaqueType != null; }
public bool IsAbstractType {
get { return AsAbstractType != null; }
}
public OpaqueTypeDecl AsOpaqueType {
public AbstractTypeDecl AsAbstractType {
get {
var udt = this.Normalize() as UserDefinedType; // note, it is important to use 'this.Normalize()' here, not 'this.NormalizeExpand()'
return udt?.ResolvedClass as OpaqueTypeDecl;
return udt?.ResolvedClass as AbstractTypeDecl;
}
}

Expand Down Expand Up @@ -869,7 +869,7 @@ public OpaqueTypeDecl AsOpaqueType {
public bool IsOrdered {
get {
var ct = NormalizeExpand();
return !ct.IsTypeParameter && !ct.IsOpaqueType && !ct.IsInternalTypeSynonym && !ct.IsCoDatatype && !ct.IsArrowType && !ct.IsIMapType && !ct.IsISetType;
return !ct.IsTypeParameter && !ct.IsAbstractType && !ct.IsInternalTypeSynonym && !ct.IsCoDatatype && !ct.IsArrowType && !ct.IsIMapType && !ct.IsISetType;
}
}

Expand Down Expand Up @@ -1423,7 +1423,7 @@ public static Type JoinX(Type a, Type b, BuiltIns builtIns) {
var udtA = (UserDefinedType)a;
return !b.IsRefType ? null : abNonNullTypes ? UserDefinedType.CreateNonNullType(udtA) : udtA;
} else {
// "a" is a class, trait, or opaque type
// "a" is a class, trait, or abstract type
var aa = ((UserDefinedType)a).ResolvedClass;
Contract.Assert(aa != null);
if (!(b is UserDefinedType)) {
Expand Down Expand Up @@ -1647,7 +1647,7 @@ public static Type MeetX(Type a, Type b, BuiltIns builtIns) {
} else if (a.IsObjectQ) {
return b.IsRefType ? b : null;
} else {
// "a" is a class, trait, or opaque type
// "a" is a class, trait, or abstract type
var aa = ((UserDefinedType)a).ResolvedClass;
Contract.Assert(aa != null);
if (!(b is UserDefinedType)) {
Expand Down Expand Up @@ -2370,9 +2370,7 @@ public UserDefinedType(TypeParameter tp)
}

/// <summary>
/// This constructor constructs a resolved type parameter (but shouldn't be called if "tp" denotes
/// the .TheType of an opaque type -- use the (OpaqueType_AsParameter, OpaqueTypeDecl, List(Type))
/// constructor for that).
/// This constructor constructs a resolved type parameter
/// </summary>
public UserDefinedType(IToken tok, TypeParameter tp) {
Contract.Requires(tok != null);
Expand Down Expand Up @@ -2549,8 +2547,8 @@ public override bool SupportsEquality {
}
} else if (ResolvedClass is TypeParameter) {
return ((TypeParameter)ResolvedClass).SupportsEquality;
} else if (ResolvedClass is OpaqueTypeDecl) {
return ((OpaqueTypeDecl)ResolvedClass).SupportsEquality;
} else if (ResolvedClass is AbstractTypeDecl) {
return ((AbstractTypeDecl)ResolvedClass).SupportsEquality;
}
Contract.Assume(false); // the SupportsEquality getter requires the Type to have been successfully resolved
return true;
Expand Down Expand Up @@ -2634,7 +2632,7 @@ public override bool ComputeMayInvolveReferences(ISet<DatatypeDecl> visitedDatat
} else {
return !typeParameter.Characteristics.ContainsNoReferenceTypes;
}
} else if (ResolvedClass is OpaqueTypeDecl opaqueTypeDecl) {
} else if (ResolvedClass is AbstractTypeDecl opaqueTypeDecl) {
return !opaqueTypeDecl.Characteristics.ContainsNoReferenceTypes;
}
Contract.Assume(false); // unexpected or not successfully resolved Type
Expand Down Expand Up @@ -2769,7 +2767,7 @@ public static Family GetFamily(Type t) {
return Family.ValueType;
} else if (t.IsRefType) {
return Family.Ref;
} else if (t.IsTypeParameter || t.IsOpaqueType || t.IsInternalTypeSynonym) {
} else if (t.IsTypeParameter || t.IsAbstractType || t.IsInternalTypeSynonym) {
return Family.Opaque;
} else if (t is TypeProxy) {
return ((TypeProxy)t).family;
Expand Down
12 changes: 6 additions & 6 deletions Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,15 +47,15 @@ public CsharpCompiler(DafnyOptions options, ErrorReporter reporter) : base(optio
const string TypeDescriptorMethodName = "_TypeDescriptor";

string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
Contract.Requires(tp is TypeParameter || tp is OpaqueTypeDecl);
if (tp is OpaqueTypeDecl) {
// This is unusual. Typically, the compiler never needs to compile an opaque type, but this opaque type
Contract.Requires(tp is TypeParameter || tp is AbstractTypeDecl);
if (tp is AbstractTypeDecl) {
// This is unusual. Typically, the compiler never needs to compile an abstract type, but this abstract type
// is apparently an :extern (or a compiler error has already been reported and we're just trying to get to
// the end of compilation without crashing). It's difficult to say what the compiler could do in this situation, since
// it doesn't know how to generate code that produces a legal value of the opaque type. If we don't do
// it doesn't know how to generate code that produces a legal value of the abstract type. If we don't do
// anything different from the common case (the "else" branch below), then the code emitted will not
// compile (see github issue #1151). So, to do something a wee bit better, we emit a placebo value. This
// will only work when the opaque type is in the same module and has no type parameters.
// will only work when the abstract type is in the same module and has no type parameters.
return $"default({tp.EnclosingModuleDefinition.GetCompileName(Options) + "." + tp.GetCompileName(Options)})";
} else {
// this is the common case
Expand Down Expand Up @@ -1511,7 +1511,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
} else {
return FormatDefaultTypeParameterValue(tp);
}
} else if (cl is OpaqueTypeDecl opaque) {
} else if (cl is AbstractTypeDecl opaque) {
return FormatDefaultTypeParameterValue(opaque);
} else if (cl is NewtypeDecl) {
var td = (NewtypeDecl)cl;
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -959,7 +959,7 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe
if (cl != null && Attributes.ContainsBool(cl.Attributes, "handle", ref isHandle) && isHandle) {
return "ulong";
}
if (class_name || xType.IsTypeParameter || xType.IsOpaqueType || xType.IsDatatype) { // Don't add pointer decorations to class names or type parameters
if (class_name || xType.IsTypeParameter || xType.IsAbstractType || xType.IsDatatype) { // Don't add pointer decorations to class names or type parameters
return IdProtect(s) + ActualTypeArgs(xType.TypeArgs);
} else {
return TypeName_UDT(s, udt, wr, udt.tok);
Expand Down Expand Up @@ -1035,8 +1035,8 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
var udt = (UserDefinedType)xType;
var cl = udt.ResolvedClass;
Contract.Assert(cl != null);
if (cl is TypeParameter || cl is OpaqueTypeDecl) {
var hasCompiledValue = (cl is TypeParameter ? ((TypeParameter)cl).Characteristics : ((OpaqueTypeDecl)cl).Characteristics).HasCompiledValue;
if (cl is TypeParameter || cl is AbstractTypeDecl) {
var hasCompiledValue = (cl is TypeParameter ? ((TypeParameter)cl).Characteristics : ((AbstractTypeDecl)cl).Characteristics).HasCompiledValue;
if (Attributes.Contains(udt.ResolvedClass.Attributes, "extern")) {
// Assume the external definition includes a default value
return String.Format("{1}::get_{0}_default()", IdProtect(udt.Name), udt.ResolvedClass.EnclosingModuleDefinition.GetCompileName(Options));
Expand Down Expand Up @@ -1134,7 +1134,7 @@ protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, I
}

// ----- Declarations -------------------------------------------------------------
protected override void DeclareExternType(OpaqueTypeDecl d, Expression compileTypeHint, ConcreteSyntaxTree wr) {
protected override void DeclareExternType(AbstractTypeDecl d, Expression compileTypeHint, ConcreteSyntaxTree wr) {
if (compileTypeHint.AsStringLiteral() == "struct") {
modDeclWr.WriteLine("// Extern declaration of {1}\n{0} struct {1};", DeclareTemplate(d.TypeArgs), d.Name);
} else {
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Compilers/GoLang/Compiler-go.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ public GoCompiler(DafnyOptions options, ErrorReporter reporter) : base(options,
};

string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
Contract.Requires(tp is TypeParameter || tp is OpaqueTypeDecl);
Contract.Requires(tp is TypeParameter || tp is AbstractTypeDecl);
return $"_default_{tp.GetCompileName(Options)}";
}

Expand Down Expand Up @@ -1516,7 +1516,7 @@ string nil() {
} else {
return FormatDefaultTypeParameterValue(tp);
}
} else if (cl is OpaqueTypeDecl opaque) {
} else if (cl is AbstractTypeDecl opaque) {
return FormatDefaultTypeParameterValue(opaque);
} else if (cl is NewtypeDecl) {
var td = (NewtypeDecl)cl;
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Compilers/Java/Compiler-java.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3073,7 +3073,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
} else {
return FormatDefaultTypeParameterValue(tp);
}
} else if (cl is OpaqueTypeDecl opaque) {
} else if (cl is AbstractTypeDecl opaque) {
return FormatDefaultTypeParameterValueName(opaque.GetCompileName(Options));
} else if (cl is NewtypeDecl) {
var td = (NewtypeDecl)cl;
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ public JavaScriptCompiler(DafnyOptions options, ErrorReporter reporter) : base(o
const string DafnyMapClass = "_dafny.Map";

string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
Contract.Requires(tp is TypeParameter || tp is OpaqueTypeDecl);
Contract.Requires(tp is TypeParameter || tp is AbstractTypeDecl);
return $"_default_{tp.GetCompileName(Options)}";
}

Expand Down Expand Up @@ -927,7 +927,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
} else {
return FormatDefaultTypeParameterValue((TypeParameter)udt.ResolvedClass);
}
} else if (cl is OpaqueTypeDecl opaque) {
} else if (cl is AbstractTypeDecl opaque) {
return FormatDefaultTypeParameterValue(opaque);
} else if (cl is NewtypeDecl) {
var td = (NewtypeDecl)cl;
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Compilers/Python/Compiler-python.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ public PythonCompiler(DafnyOptions options, ErrorReporter reporter) : base(optio
const string DafnyMapClass = $"{DafnyRuntimeModule}.Map";
const string DafnyDefaults = $"{DafnyRuntimeModule}.defaults";
string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
Contract.Requires(tp is TypeParameter or OpaqueTypeDecl);
Contract.Requires(tp is TypeParameter or AbstractTypeDecl);
return $"default_{tp.GetCompileName(Options)}";
}
protected override string StmtTerminator { get => ""; }
Expand Down Expand Up @@ -730,7 +730,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
? $"{TypeDescriptor(udt, wr, tok)}()"
: $"{FormatDefaultTypeParameterValue(tp)}()";

case OpaqueTypeDecl opaque:
case AbstractTypeDecl opaque:
return FormatDefaultTypeParameterValue(opaque);

case ClassDecl:
Expand Down
Loading

0 comments on commit 76dcc6b

Please sign in to comment.