Fixed some bugs in override axioms (but still missing support for classes with type parameters).

Resolve ClassDecl.TraitsTyp as types.
Moved declaration of TraitParent and NoTraitAtAll to prelude.

3 files changed, 14 insertions, 5 deletions

diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect
index 5ebf1d5c..84465fea 100644
--- a/Test/dafny0/Trait/TraitBasix.dfy.expect
+++ b/Test/dafny0/Trait/TraitBasix.dfy.expect
@@ -1,4 +1,4 @@
-TraitBasix.dfy(91,24): Error: unresolved identifier: IX

+TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name?)

 TraitBasix.dfy(77,8): Error: member in the class has been already inherited from its parent trait

 TraitBasix.dfy(70,8): Error: class: I0Child does not implement trait member: Customizable

 TraitBasix.dfy(80,8): Error: class: I0Child2 does not implement trait member: F

diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy b/Test/dafny0/Trait/TraitMultiModule.dfy
index b31e4b0d..81f4f401 100644
--- a/Test/dafny0/Trait/TraitMultiModule.dfy
+++ b/Test/dafny0/Trait/TraitMultiModule.dfy
@@ -18,8 +18,16 @@ module M1
 

 module M2

 {

-  class C2 extends T1

+  import opened M1

+  class C2 extends T1  // error: currently no support to implement trait in different module

+  {

+  }

+}

+

+module M3

+{

+  import M1

+  class C2 extends M1.T1  // error: currently no support to implement trait in different module

   {

-   

   }

 }

diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect
index a1617395..e991553a 100644
--- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect
+++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect
@@ -1,2 +1,3 @@
-TraitMultiModule.dfy(21,19): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module

-1 resolution/type errors detected in TraitMultiModule.dfy

+TraitMultiModule.dfy(22,19): Error: class 'C2' is in a different module than trait 'M1.T1'. A class may only extend a trait in the same module.

+TraitMultiModule.dfy(30,22): Error: class 'C2' is in a different module than trait 'M1.T1'. A class may only extend a trait in the same module.

+2 resolution/type errors detected in TraitMultiModule.dfy