Renamed "arbitrary type" to "opaque type"

7 files changed, 25 insertions, 25 deletions

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