diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2eaaca7f..04b8d9fa 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) {
@@ -273,6 +275,15 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> }
";"
.
+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;
|