summaryrefslogtreecommitdiff
path: root/Source/Dafny/Dafny.atg
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Dafny.atg')
-rw-r--r--Source/Dafny/Dafny.atg188
1 files changed, 106 insertions, 82 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 4b9e0c27..bfce5122 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -14,7 +14,7 @@ using System.IO;
using System.Text;
COMPILER Dafny
/*--------------------------------------------------------------------------*/
-static List<ModuleDecl/*!*/> theModules;
+static ModuleDecl theModule;
static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
@@ -28,51 +28,51 @@ struct MemberModifiers {
// helper routine for parsing call statements
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
-/// and appends them in appropriate form to "modules".
+/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns) /* throws System.IO.IOException */ {
+public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
- Contract.Requires(cce.NonNullElements(modules));
+ Contract.Requires(module != null);
string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());
- return Parse(s, filename, modules, builtIns);
+ return Parse(s, filename, module, builtIns);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());
- return Parse(s, filename, modules, builtIns);
+ return Parse(s, filename, module, builtIns);
}
}
}
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
-/// and appends them in appropriate form to "modules".
+/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns) {
+public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
- Contract.Requires(cce.NonNullElements(modules));
+ Contract.Requires(module != null);
Errors errors = new Errors();
- return Parse(s, filename, modules, builtIns, errors);
+ return Parse(s, filename, module, builtIns, errors);
}
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
-/// and appends them in appropriate form to "modules".
+/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner with the given Errors sink.
///</summary>
-public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns,
+public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns,
Errors/*!*/ errors) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
- Contract.Requires(cce.NonNullElements(modules));
+ Contract.Requires(module != null);
Contract.Requires(errors != null);
- List<ModuleDecl/*!*/> oldModules = theModules;
- theModules = modules;
+ var oldModule = theModule;
+ theModule = module;
BuiltIns oldBuiltIns = builtIns;
theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
@@ -80,7 +80,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Scanner scanner = new Scanner(ms, errors, filename);
Parser parser = new Parser(scanner, errors);
parser.Parse();
- theModules = oldModules;
+ theModule = oldModule;
theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
@@ -131,43 +131,19 @@ IGNORE cr + lf + tab
PRODUCTIONS
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;
- Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
- List<MemberDecl/*!*/> namedModuleDefaultClassMembers;
- ModuleDecl module;
- // to support multiple files, create a default module only if theModules doesn't already contain one
- DefaultModuleDecl defaultModule = null;
- foreach (ModuleDecl mdecl in theModules) {
- defaultModule = mdecl as DefaultModuleDecl;
- if (defaultModule != null) { break; }
- }
- bool defaultModuleCreatedHere = false;
- if (defaultModule == null) {
- defaultModuleCreatedHere = true;
- defaultModule = new DefaultModuleDecl();
- }
- IToken idRefined;
+ ModuleDecl submodule;
+ // to support multiple files, create a default module only if theModule is null
+ DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef;
+ // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
+ Contract.Assert(defaultModule != null);
bool isGhost;
.)
{ (. isGhost = false; .)
[ "ghost" (. isGhost = true; .) ]
- ( "module" (. attrs = null; idRefined = null; theImports = new List<string/*!*/>();
- namedModuleDefaultClassMembers = new List<MemberDecl>();
- .)
- { Attribute<ref attrs> }
- Ident<out id> (. defaultModule.ImportNames.Add(id.val); .)
- [ "refines" Ident<out idRefined> ]
- [ "imports" Idents<theImports> ] (. module = new ModuleDecl(id, id.val, isGhost, idRefined == null ? null : idRefined.val, theImports, attrs); .)
- "{" (. 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); .)
- | ClassMemberDecl<namedModuleDefaultClassMembers, false, false>
- }
- "}" (. module.BodyEndTok = t;
- module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
- theModules.Add(module); .)
+ ( SubModuleDecl<defaultModule, isGhost, out submodule>
+ (. defaultModule.TopLevelDecls.Add(submodule); .)
| (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .)
ClassDecl<defaultModule, out c> (. defaultModule.TopLevelDecls.Add(c); .)
| (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .)
@@ -177,23 +153,67 @@ Dafny
| ClassMemberDecl<membersDefaultClass, isGhost, false>
)
}
- (. if (defaultModuleCreatedHere) {
- defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
- theModules.Add(defaultModule);
- } else {
- // find the default class in the default module, then append membersDefaultClass to its member list
- foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
- DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;
- if (defaultClass != null) {
- defaultClass.Members.AddRange(membersDefaultClass);
- break;
- }
+ (. // find the default class in the default module, then append membersDefaultClass to its member list
+ DefaultClassDecl defaultClass = null;
+ foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
+ defaultClass = topleveldecl as DefaultClassDecl;
+ if (defaultClass != null) {
+ defaultClass.Members.AddRange(membersDefaultClass);
+ break;
}
}
- .)
+ if (defaultClass == null) { // create the default class here, because it wasn't found
+ defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);
+ defaultModule.TopLevelDecls.Add(defaultClass);
+ } .)
EOF
.
-ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
+SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule>
+= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at;
+ Attributes attrs = null; IToken/*!*/ id;
+ List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
+ List<IToken> idRefined = null, idPath = null;
+ bool isGhost = false;
+ ModuleDefinition module;
+ ModuleDecl sm;
+ submodule = null; // appease compiler
+ .)
+ "module"
+ { Attribute<ref attrs> }
+ NoUSIdent<out id>
+ ((
+ [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs); .)
+ "{" (. module.BodyStartTok = t; .)
+ { (. isGhost = false; .)
+ [ "ghost" (. isGhost = true; .) ]
+ ( SubModuleDecl<module, isGhost, out sm> (. module.TopLevelDecls.Add(sm); .)
+ | (. if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } .)
+ ClassDecl<module, out c> (. module.TopLevelDecls.Add(c); .)
+ | (. if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } .)
+ DatatypeDecl<module, out dt> (. module.TopLevelDecls.Add(dt); .)
+ | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .)
+ ArbitraryTypeDecl<module, out at> (. module.TopLevelDecls.Add(at); .)
+ | ClassMemberDecl<namedModuleDefaultClassMembers, isGhost, false>
+ )
+ }
+ "}" (. module.BodyEndTok = t;
+ module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
+ submodule = new LiteralModuleDecl(module, parent); .)
+ ) |
+ "=" QualifiedName<out idPath> ";" (. submodule = new AliasModuleDecl(idPath, id, parent); .)
+ |
+ "as" QualifiedName<out idPath> ";" (.submodule = new AbstractModuleDecl(idPath, id, parent); .)
+ )
+.
+
+QualifiedName<.out List<IToken> ids.>
+= (. IToken id; ids = new List<IToken>(); .)
+ Ident<out id> (. ids.Add(id); .)
+ { "." Ident<out id> (. ids.Add(id); .)
+ }
+ .
+
+ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
@@ -205,7 +225,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
SYNC
"class"
{ Attribute<ref attrs> }
- Ident<out id>
+ NoUSIdent<out id>
[ GenericParameters<typeArgs> ]
"{" (. bodyStart = t; .)
{ ClassMemberDecl<members, false, true>
@@ -231,7 +251,7 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool isAlreadyGhost, bool allowC
| MethodDecl<mmod, allowConstructors, out m> (. mm.Add(m); .)
)
.
-DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
+DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt>
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
IToken/*!*/ id;
@@ -246,7 +266,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
| "codatatype" (. co = true; .)
)
{ Attribute<ref attrs> }
- Ident<out id>
+ NoUSIdent<out id>
[ GenericParameters<typeArgs> ]
"=" (. bodyStart = t; .)
DatatypeMemberDecl<ctors>
@@ -268,7 +288,7 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
List<Formal/*!*/> formals = new List<Formal/*!*/>();
.)
{ Attribute<ref attrs> }
- Ident<out id>
+ NoUSIdent<out id>
[ FormalsOptionalIds<formals> ]
(. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
.
@@ -287,14 +307,14 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
}
SYNC ";"
.
-ArbitraryTypeDecl<ModuleDecl/*!*/ module, out ArbitraryTypeDecl at>
+ArbitraryTypeDecl<ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at>
= (. IToken/*!*/ id;
Attributes attrs = null;
var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
.)
"type"
{ Attribute<ref attrs> }
- Ident<out id>
+ NoUSIdent<out id>
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .)
SYNC ";"
@@ -310,14 +330,14 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo
.
IdentType<out IToken/*!*/ id, out Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
- Ident<out id>
+ NoUSIdent<out id>
":"
Type<out ty>
.
LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
= (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
- Ident<out id>
+ NoUSIdent<out id>
[ ":" Type<out ty> (. optType = ty; .)
]
(. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
@@ -325,7 +345,7 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
IdentTypeOptional<out BoundVar/*!*/ var>
= (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
- Ident<out id>
+ NoUSIdent<out id>
[ ":" Type<out ty> (. optType = ty; .)
]
(. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
@@ -363,10 +383,10 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
TypeParameter.EqualitySupportValue eqSupport;
.)
"<"
- Ident<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
- { "," Ident<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ { "," NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
}
@@ -412,7 +432,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
}
.)
{ Attribute<ref attrs> }
- Ident<out id>
+ NoUSIdent<out id>
(
[ GenericParameters<typeArgs> ]
Formals<true, !mmod.IsGhost, ins, out openParen>
@@ -572,7 +592,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
(. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute<ref attrs> }
- Ident<out id>
+ NoUSIdent<out id>
(
[ GenericParameters<typeArgs> ]
Formals<true, isFunctionMethod, formals, out openParen>
@@ -589,7 +609,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
(. if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute<ref attrs> }
- Ident<out id>
+ NoUSIdent<out id>
(
[ GenericParameters<typeArgs> ]
[ Formals<true, isFunctionMethod, formals, out openParen>
@@ -699,10 +719,10 @@ OneStmt<out Statement/*!*/ s>
| MatchStmt<out s>
| ParallelStmt<out s>
| "label" (. x = t; .)
- Ident<out id> ":"
+ NoUSIdent<out id> ":"
OneStmt<out s> (. s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); .)
| "break" (. x = t; breakCount = 1; label = null; .)
- ( Ident<out id> (. label = id.val; .)
+ ( NoUSIdent<out id> (. label = id.val; .)
| { "break" (. breakCount++; .)
}
)
@@ -1643,16 +1663,20 @@ AttributeArg<out Attributes.Argument/*!*/ arg>
)
.
/*------------------------------------------------------------------------*/
-Idents<.List<string/*!*/>/*!*/ ids.>
-= (. IToken/*!*/ id; .)
- Ident<out id> (. ids.Add(id.val); .)
- { "," Ident<out id> (. ids.Add(id.val); .)
- }
- .
Ident<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
ident (. x = t; .)
.
+// Identifier, disallowing leading underscores
+NoUSIdent<out IToken/*!*/ x>
+= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
+ ident (. x = t;
+ if (x.val.Length > 0 && x.val.StartsWith("_")) {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+ .)
+ .
+
Nat<out BigInteger n>
=
digits
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 08:14:38 +0000