summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-07-15 17:16:02 -0700
committerGravatar Rustan Leino <unknown>2014-07-15 17:16:02 -0700
commit17bd465d7950927d76080106db7ade928e5a8b4a (patch)
tree6cd72cca845197ea03536cce91a2f66cb1e88998
parent30cd666db7142297b7cd627cad34243b76e7291a (diff)
Renamed "arbitrary type" to "opaque type"
Diffstat
-rw-r--r--Source/Dafny/Cloner.cs6
-rw-r--r--Source/Dafny/Compiler.cs6
-rw-r--r--Source/Dafny/Dafny.atg4
-rw-r--r--Source/Dafny/DafnyAst.cs4
-rw-r--r--Source/Dafny/Parser.cs2
-rw-r--r--Source/Dafny/Printer.cs4
-rw-r--r--Source/Dafny/RefinementTransformer.cs36
-rw-r--r--Source/Dafny/Resolver.cs22
-rw-r--r--Source/Dafny/Translator.cs10
-rw-r--r--Test/cloudmake/CloudMake-ParallelBuilds.dfy2
-rw-r--r--Test/dafny0/CompilationErrors.dfy2
-rw-r--r--Test/dafny0/CompilationErrors.dfy.expect2
-rw-r--r--Test/dafny0/DisplayExpressions.dfy.expect10
-rw-r--r--Test/dafny0/EqualityTypes.dfy.expect10
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect6
-rw-r--r--Test/dafny0/TypeInstantiations.dfy.expect18
16 files changed, 72 insertions, 72 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index ebc547fb..bb644825 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -27,9 +27,9 @@ namespace Microsoft.Dafny
Contract.Requires(d != null);
Contract.Requires(m != null);
- if (d is ArbitraryTypeDecl) {
- var dd = (ArbitraryTypeDecl)d;
- return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), CloneAttributes(dd.Attributes));
+ if (d is OpaqueTypeDecl) {
+ var dd = (OpaqueTypeDecl)d;
+ return new OpaqueTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), CloneAttributes(dd.Attributes));
} else if (d is TypeSynonymDecl) {
var dd = (TypeSynonymDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index b5d145aa..c665026c 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -112,9 +112,9 @@ namespace Microsoft.Dafny {
continue;
}
wr.WriteLine();
- if (d is ArbitraryTypeDecl) {
- var at = (ArbitraryTypeDecl)d;
- Error("Arbitrary type ('{0}') cannot be compiled", at.FullName);
+ if (d is OpaqueTypeDecl) {
+ var at = (OpaqueTypeDecl)d;
+ Error("Opaque type ('{0}') cannot be compiled", at.FullName);
} else if (d is TypeSynonymDecl) {
// do nothing, just bypass type synonyms in the compiler
} else if (d is DatatypeDecl) {
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index fb68df7a..c870dc81 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -412,14 +412,14 @@ OtherTypeDecl<ModuleDefinition/*!*/ module, out TopLevelDecl td>
Type<out ty> (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)
]
) (. if (td == null) {
- td = new ArbitraryTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
+ td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
}
.)
[ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in a next big version of Dafny, including the following warning message:
- // (. errors.Warning(t, "the semi-colon that used to terminate an arbitrary-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
+ // (. errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
// And in a version after that, don't allow the semi-colon at all.
]
.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 227884f2..21227dd6 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1928,7 +1928,7 @@ namespace Microsoft.Dafny {
}
}
- public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType
+ public class OpaqueTypeDecl : TopLevelDecl, TypeParameter.ParentType
{
public readonly TypeParameter TheType;
public TypeParameter.EqualitySupportValue EqualitySupport {
@@ -1942,7 +1942,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(TheType != null && Name == TheType.Name);
}
- public ArbitraryTypeDecl(IToken tok, string name, ModuleDefinition module, TypeParameter.EqualitySupportValue equalitySupport, List<TypeParameter> typeArgs, Attributes attributes)
+ public OpaqueTypeDecl(IToken tok, string name, ModuleDefinition module, TypeParameter.EqualitySupportValue equalitySupport, List<TypeParameter> typeArgs, Attributes attributes)
: base(tok, name, module, typeArgs, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 6f5d8dc5..63c555aa 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -516,7 +516,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
} else SynErr(133);
if (td == null) {
- td = new ArbitraryTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
+ td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
}
if (la.kind == 8) {
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 49121848..1da5e7b2 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -133,8 +133,8 @@ namespace Microsoft.Dafny {
int i = 0;
foreach (TopLevelDecl d in decls) {
Contract.Assert(d != null);
- if (d is ArbitraryTypeDecl) {
- var at = (ArbitraryTypeDecl)d;
+ if (d is OpaqueTypeDecl) {
+ var at = (OpaqueTypeDecl)d;
if (i++ != 0) { wr.WriteLine(); }
Indent(indent);
PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 8fbb9d9b..d23aadc8 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -145,13 +145,13 @@ namespace Microsoft.Dafny
reporter.Error(nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name);
}
}
- } else if (d is ArbitraryTypeDecl) {
+ } else if (d is OpaqueTypeDecl) {
if (nw is ModuleDecl) {
reporter.Error(nw, "a module ({0}) must refine another module", nw.Name);
} else {
- bool dDemandsEqualitySupport = ((ArbitraryTypeDecl)d).MustSupportEquality;
- if (nw is ArbitraryTypeDecl) {
- if (dDemandsEqualitySupport != ((ArbitraryTypeDecl)nw).MustSupportEquality) {
+ bool dDemandsEqualitySupport = ((OpaqueTypeDecl)d).MustSupportEquality;
+ if (nw is OpaqueTypeDecl) {
+ if (dDemandsEqualitySupport != ((OpaqueTypeDecl)nw).MustSupportEquality) {
reporter.Error(nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);
}
if (nw.TypeArgs.Count != d.TypeArgs.Count) {
@@ -161,33 +161,33 @@ namespace Microsoft.Dafny
if (nw is ClassDecl) {
// fine, as long as "nw" does not take any type parameters
if (nw.TypeArgs.Count != d.TypeArgs.Count) {
- reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
+ reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
}
} else if (nw is CoDatatypeDecl) {
reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");
} else {
Contract.Assert(nw is IndDatatypeDecl || nw is TypeSynonymDecl);
if (nw.TypeArgs.Count != d.TypeArgs.Count) {
- reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
+ reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
} else {
// Here, we need to figure out if the new type supports equality. But we won't know about that until resolution has
// taken place, so we defer it until the PostResolve phase.
var udt = new UserDefinedType(nw.tok, nw.Name, nw, nw.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp)));
postTasks.Enqueue(() => {
if (!udt.SupportsEquality) {
- reporter.Error(udt.tok, "type '{0}' is used to refine an arbitrary type with equality support, but '{0}' does not support equality", udt.Name);
+ reporter.Error(udt.tok, "type '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", udt.Name);
}
});
}
}
} else if (d.TypeArgs.Count != nw.TypeArgs.Count) {
- reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
+ reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
}
}
- } else if (nw is ArbitraryTypeDecl) {
- reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);
+ } else if (nw is OpaqueTypeDecl) {
+ reporter.Error(nw, "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);
} else if (nw is DatatypeDecl) {
- reporter.Error(nw, "a datatype declaration ({0}) in a refinement module can only replace an arbitrary-type declaration", nw.Name);
+ reporter.Error(nw, "a datatype declaration ({0}) in a refinement module can only replace an opaque type declaration", nw.Name);
} else if (nw is IteratorDecl) {
if (d is IteratorDecl) {
m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d);
@@ -235,31 +235,31 @@ namespace Microsoft.Dafny
} else {
CheckIsRefinement(((ModuleDecl)nw).Signature, ((ModuleDecl)d).Signature);
}
- } else if (d is ArbitraryTypeDecl) {
+ } else if (d is OpaqueTypeDecl) {
if (nw is ModuleDecl) {
reporter.Error(nw, "a module ({0}) must refine another module", nw.Name);
} else {
- bool dDemandsEqualitySupport = ((ArbitraryTypeDecl)d).MustSupportEquality;
- if (nw is ArbitraryTypeDecl) {
- if (dDemandsEqualitySupport != ((ArbitraryTypeDecl)nw).MustSupportEquality) {
+ bool dDemandsEqualitySupport = ((OpaqueTypeDecl)d).MustSupportEquality;
+ if (nw is OpaqueTypeDecl) {
+ if (dDemandsEqualitySupport != ((OpaqueTypeDecl)nw).MustSupportEquality) {
reporter.Error(nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);
}
} else if (dDemandsEqualitySupport) {
if (nw is ClassDecl) {
// fine, as long as "nw" does not take any type parameters
if (nw.TypeArgs.Count != 0) {
- reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes type parameters", nw.Name);
+ reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a class that takes type parameters", nw.Name);
}
} else if (nw is CoDatatypeDecl) {
reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");
} else {
Contract.Assert(nw is IndDatatypeDecl);
if (nw.TypeArgs.Count != 0) {
- reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a datatype that takes type parameters", nw.Name);
+ reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a datatype that takes type parameters", nw.Name);
} else {
var udt = new UserDefinedType(nw.tok, nw.Name, nw, new List<Type>());
if (!(udt.SupportsEquality)) {
- reporter.Error(nw.tok, "datatype '{0}' is used to refine an arbitrary type with equality support, but '{0}' does not support equality", nw.Name);
+ reporter.Error(nw.tok, "datatype '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", nw.Name);
}
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 4b775017..5e7381d9 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -749,7 +749,7 @@ namespace Microsoft.Dafny
}
if (d is ModuleDecl) {
// nothing to do
- } else if (d is ArbitraryTypeDecl) {
+ } else if (d is OpaqueTypeDecl) {
// nothing more to register
} else if (d is TypeSynonymDecl) {
// nothing more to register
@@ -1039,9 +1039,9 @@ namespace Microsoft.Dafny
Contract.Requires(d != null);
Contract.Requires(m != null);
- if (d is ArbitraryTypeDecl) {
- var dd = (ArbitraryTypeDecl)d;
- return new ArbitraryTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), null);
+ if (d is OpaqueTypeDecl) {
+ var dd = (OpaqueTypeDecl)d;
+ return new OpaqueTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), null);
} else if (d is TypeSynonymDecl) {
var dd = (TypeSynonymDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
@@ -1415,7 +1415,7 @@ namespace Microsoft.Dafny
Contract.Assert(d != null);
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, true, d);
- if (d is ArbitraryTypeDecl) {
+ if (d is OpaqueTypeDecl) {
// nothing to do
} else if (d is TypeSynonymDecl) {
var syn = (TypeSynonymDecl)d;
@@ -2016,7 +2016,7 @@ namespace Microsoft.Dafny
Contract.Requires(what != null);
t = t.Normalize();
if (t is TypeProxy && (aggressive || !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy))) {
- Error(tok, "the type of this {0} is underspecified, but it cannot be an arbitrary type.", what);
+ Error(tok, "the type of this {0} is underspecified, but it cannot be an opaque type.", what);
return false;
} else if (aggressive && t is MapType) {
return CheckTypeIsDetermined(tok, ((MapType)t).Range, what, aggressive) &&
@@ -3810,9 +3810,9 @@ namespace Microsoft.Dafny
Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());
} else {
string what;
- if (d is ArbitraryTypeDecl) {
- what = "arbitrary type";
- t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType; // resolve like a type parameter, and it may have type parameters if it's an arbitrary-type
+ if (d is OpaqueTypeDecl) {
+ what = "opaque type";
+ t.ResolvedParam = ((OpaqueTypeDecl)d).TheType; // resolve like a type parameter, and it may have type parameters if it's an opaque type
} else {
// d is a class or datatype, and it may have type parameters
what = "class/datatype";
@@ -7154,7 +7154,7 @@ namespace Microsoft.Dafny
CallRhs ResolveIdentifierSequence(IdentifierSequence e, bool twoState, ICodeContext codeContext, bool allowMethodCall) {
// Look up "id" as follows:
// - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally)
- // - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)
+ // - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or opaque type)
// (if two imported types have the same name, an error message is produced here)
// - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)
// - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")
@@ -7267,7 +7267,7 @@ namespace Microsoft.Dafny
CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, bool twoState, ICodeContext codeContext, bool allowMethodCall) {
// Look up "id" as follows:
- // - unambiguous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)
+ // - unambiguous type/module name (class, datatype, sub-module (including submodules of imports) or opaque type)
// (if two imported types have the same name, an error message is produced here)
// - static function or method of sig.
// This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2c987b62..a936200e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -351,8 +351,8 @@ namespace Microsoft.Dafny {
foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) {
currentDeclaration = d;
- if (d is ArbitraryTypeDecl) {
- AddTypeDecl((ArbitraryTypeDecl)d);
+ if (d is OpaqueTypeDecl) {
+ AddTypeDecl((OpaqueTypeDecl)d);
} else if (d is DatatypeDecl) {
AddDatatype((DatatypeDecl)d);
} else {
@@ -362,8 +362,8 @@ namespace Microsoft.Dafny {
foreach (ModuleDefinition m in program.Modules) {
foreach (TopLevelDecl d in m.TopLevelDecls) {
currentDeclaration = d;
- if (d is ArbitraryTypeDecl) {
- AddTypeDecl((ArbitraryTypeDecl)d);
+ if (d is OpaqueTypeDecl) {
+ AddTypeDecl((OpaqueTypeDecl)d);
} else if (d is TypeSynonymDecl) {
// do nothing, just bypass type synonyms in the translation
} else if (d is DatatypeDecl) {
@@ -426,7 +426,7 @@ namespace Microsoft.Dafny {
return sink;
}
- void AddTypeDecl(ArbitraryTypeDecl td) {
+ void AddTypeDecl(OpaqueTypeDecl td) {
Contract.Requires(td != null);
string nm = nameTypeParam(td.TheType);
if (abstractTypes.Contains(nm)) {
diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy
index 19473b6a..a4f327ff 100644
--- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy
+++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy
@@ -761,7 +761,7 @@ abstract module M2 refines M1 {
}
}
-// Finally, this module defines any remaining arbitrary types and function bodies and proves any
+// Finally, this module defines any remaining opaque types and function bodies and proves any
// remaining lemmas about these. The actual definitions are not so interesting and are not meant
// to suggest that a deployed CloudMake use these definitions. Rather, these definitions are here
// only to establish mathematical feasibility of previously axiomatized properties.
diff --git a/Test/dafny0/CompilationErrors.dfy b/Test/dafny0/CompilationErrors.dfy
index 2f3325a1..80e5eeae 100644
--- a/Test/dafny0/CompilationErrors.dfy
+++ b/Test/dafny0/CompilationErrors.dfy
@@ -1,7 +1,7 @@
// RUN: %dafny "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-type MyType // compile error: arbitrary type
+type MyType // compile error: opaque type
iterator Iter() // compile error: body-less iterator
ghost method M() // compile error: body-less ghost method
method P() // compile error: body-less method
diff --git a/Test/dafny0/CompilationErrors.dfy.expect b/Test/dafny0/CompilationErrors.dfy.expect
index e0c7f11c..e5583f30 100644
--- a/Test/dafny0/CompilationErrors.dfy.expect
+++ b/Test/dafny0/CompilationErrors.dfy.expect
@@ -1,6 +1,6 @@
Dafny program verifier finished with 15 verified, 0 errors
-Compilation error: Arbitrary type ('_module.MyType') cannot be compiled
+Compilation error: Opaque type ('_module.MyType') cannot be compiled
Compilation error: Iterator _module.Iter has no body
Compilation error: Method _module._default.M has no body
Compilation error: Method _module._default.P has no body
diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect
index 1867ff3a..7374db2a 100644
--- a/Test/dafny0/DisplayExpressions.dfy.expect
+++ b/Test/dafny0/DisplayExpressions.dfy.expect
@@ -1,5 +1,5 @@
-DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an arbitrary type.
-DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
-DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
-DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type.
-4 resolution/type errors detected in DisplayExpressions.dfy
+DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an opaque type.
+DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
+DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
+DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
+4 resolution/type errors detected in DisplayExpressions.dfy
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index fde9aadf..410e4507 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -1,9 +1,9 @@
EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
-EqualityTypes.dfy(35,11): Error: type 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
-EqualityTypes.dfy(40,11): Error: arbitrary type 'X' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
-EqualityTypes.dfy(41,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters (got 1, expected 0)
-EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality
-EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(35,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(40,11): Error: opaque type 'X' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
+EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters (got 1, expected 0)
+EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality
+EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 38393b02..49cfe650 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -16,8 +16,8 @@ ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specifi
ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
-ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
+ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.
+ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.
ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops
@@ -66,7 +66,7 @@ ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
-ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to arbitrary type: P
+ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
ResolutionErrors.dfy(1072,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
ResolutionErrors.dfy(1077,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
diff --git a/Test/dafny0/TypeInstantiations.dfy.expect b/Test/dafny0/TypeInstantiations.dfy.expect
index 6c214970..30b74f8c 100644
--- a/Test/dafny0/TypeInstantiations.dfy.expect
+++ b/Test/dafny0/TypeInstantiations.dfy.expect
@@ -1,13 +1,13 @@
-TypeInstantiations.dfy(33,7): Error: an arbitrary type declaration (B) in a refining module cannot replace a more specific type declaration in the refinement base
+TypeInstantiations.dfy(33,7): Error: an opaque type declaration (B) in a refining module cannot replace a more specific type declaration in the refinement base
TypeInstantiations.dfy(36,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
-TypeInstantiations.dfy(40,7): Error: arbitrary type 'G' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
-TypeInstantiations.dfy(41,7): Error: arbitrary type 'H' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 2)
-TypeInstantiations.dfy(42,7): Error: arbitrary type 'J' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
-TypeInstantiations.dfy(51,8): Error: arbitrary type 'R' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
-TypeInstantiations.dfy(53,8): Error: arbitrary type 'T' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
+TypeInstantiations.dfy(40,7): Error: opaque type 'G' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
+TypeInstantiations.dfy(41,7): Error: opaque type 'H' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 2)
+TypeInstantiations.dfy(42,7): Error: opaque type 'J' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
+TypeInstantiations.dfy(51,8): Error: opaque type 'R' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
+TypeInstantiations.dfy(53,8): Error: opaque type 'T' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
TypeInstantiations.dfy(55,7): Error: type 'TP0' is not allowed to change its number of type parameters (got 1, expected 0)
TypeInstantiations.dfy(56,7): Error: type 'TP1' is not allowed to change its number of type parameters (got 0, expected 1)
-TypeInstantiations.dfy(34,11): Error: type 'C' is used to refine an arbitrary type with equality support, but 'C' does not support equality
-TypeInstantiations.dfy(35,7): Error: type 'D' is used to refine an arbitrary type with equality support, but 'D' does not support equality
-TypeInstantiations.dfy(48,7): Error: type 'N' is used to refine an arbitrary type with equality support, but 'N' does not support equality
+TypeInstantiations.dfy(34,11): Error: type 'C' is used to refine an opaque type with equality support, but 'C' does not support equality
+TypeInstantiations.dfy(35,7): Error: type 'D' is used to refine an opaque type with equality support, but 'D' does not support equality
+TypeInstantiations.dfy(48,7): Error: type 'N' is used to refine an opaque type with equality support, but 'N' does not support equality
12 resolution/type errors detected in TypeInstantiations.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 18:57:26 +0000