Merge

1 files changed, 13 insertions, 3 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 7019a22b..6b12a288 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -134,7 +134,7 @@ IGNORE cr + lf + tab
 /*------------------------------------------------------------------------*/

 PRODUCTIONS

 Dafny

-= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

+= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;

      Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

      List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();

      ModuleDecl module;

@@ -157,11 +157,13 @@ Dafny
     "{"                                  (. module.BodyStartTok = t; .)

       { ClassDecl<module, out c>         (. module.TopLevelDecls.Add(c); .)

       | DatatypeDecl<module, out dt>     (. module.TopLevelDecls.Add(dt); .)

+      | ArbitraryTypeDecl<module, out at>(. module.TopLevelDecls.Add(at); .)

       }

     "}"                                  (. module.BodyEndTok = t;

                                             theModules.Add(module); .)

-  | ClassDecl<defaultModule, out c>      (. defaultModule.TopLevelDecls.Add(c); .)

-  | DatatypeDecl<defaultModule, out dt>  (. defaultModule.TopLevelDecls.Add(dt); .)

+  | ClassDecl<defaultModule, out c>           (. defaultModule.TopLevelDecls.Add(c); .)

+  | DatatypeDecl<defaultModule, out dt>       (. defaultModule.TopLevelDecls.Add(dt); .)

+  | ArbitraryTypeDecl<defaultModule, out at>  (. defaultModule.TopLevelDecls.Add(at); .)

   | ClassMemberDecl<membersDefaultClass, false>

   }

   (. if (defaultModuleCreatedHere) {

@@ -276,6 +278,14 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   }

   SYNC ";"

   .

+ArbitraryTypeDecl<ModuleDecl/*!*/ module, out ArbitraryTypeDecl at>

+= (. IToken/*!*/ id;

+     Attributes attrs = null;

+  .)

+  "type"

+  { Attribute<ref attrs> }

+  Ident<out id>               (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)

+  .

 CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>

 = (. Contract.Requires(cce.NonNullElements(mm));

      Attributes attrs = null;