diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 1990 |
1 files changed, 0 insertions, 1990 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg deleted file mode 100644 index 4c425497..00000000 --- a/Source/Dafny/Dafny.atg +++ /dev/null @@ -1,1990 +0,0 @@ -/*-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------*/
-/*---------------------------------------------------------------------------
-// Dafny
-// Rustan Leino, first created 25 January 2008
-//--------------------------------------------------------------------------*/
-using System.Collections.Generic;
-using System.Numerics;
-using Microsoft.Boogie;
-using System.IO;
-using System.Text;
-COMPILER Dafny
-/*--------------------------------------------------------------------------*/
-readonly Expression/*!*/ dummyExpr;
-readonly AssignmentRhs/*!*/ dummyRhs;
-readonly FrameExpression/*!*/ dummyFrameExpr;
-readonly Statement/*!*/ dummyStmt;
-readonly Attributes.Argument/*!*/ dummyAttrArg;
-readonly ModuleDecl theModule;
-readonly BuiltIns theBuiltIns;
-int anonymousIds = 0;
-
-struct MemberModifiers {
- public bool IsGhost;
- public bool IsStatic;
-}
-// 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 "module".
-/// Returns the number of parsing errors encountered.
-/// Note: first initialize the Scanner.
-///</summary>
-public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns) /* throws System.IO.IOException */ {
- Contract.Requires(filename != null);
- 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, 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, module, builtIns);
- }
- }
-}
-///<summary>
-/// Parses top-level things (modules, classes, datatypes, class members)
-/// 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, ModuleDecl module, BuiltIns builtIns) {
- Contract.Requires(s != null);
- Contract.Requires(filename != null);
- Contract.Requires(module != null);
- Errors errors = new 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 "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, ModuleDecl module, BuiltIns builtIns,
- Errors/*!*/ errors) {
- Contract.Requires(s != null);
- Contract.Requires(filename != null);
- Contract.Requires(module != null);
- Contract.Requires(errors != null);
- byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
- MemoryStream ms = new MemoryStream(buffer,false);
- Scanner scanner = new Scanner(ms, errors, filename);
- Parser parser = new Parser(scanner, errors, module, builtIns);
- parser.Parse();
- return parser.errors.count;
-}
-public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns)
- : this(scanner, errors) // the real work
-{
- // initialize readonly fields
- dummyExpr = new LiteralExpr(Token.NoToken);
- dummyRhs = new ExprRhs(dummyExpr, null);
- dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
- dummyStmt = new ReturnStmt(Token.NoToken, null);
- dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
- theModule = module;
- theBuiltIns = builtIns;
-}
-
-bool IsAttribute() {
- Token x = scanner.Peek();
- return la.kind == _lbrace && x.kind == _colon;
-}
-/*--------------------------------------------------------------------------*/
-CHARACTERS
- letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
- digit = "0123456789".
- posDigit = "123456789".
- special = "'_?\\".
- glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
- cr = '\r'.
- lf = '\n'.
- tab = '\t'.
- space = ' '.
- quote = '"'.
- nondigit = letter + special.
- idchar = nondigit + digit.
- nonquote = letter + digit + space + glyph.
- /* exclude the characters in 'array' */
- nondigitMinusA = nondigit - 'a'.
- idcharMinusA = idchar - 'a'.
- idcharMinusR = idchar - 'r'.
- idcharMinusY = idchar - 'y'.
- idcharMinusPosDigit = idchar - posDigit.
-/*------------------------------------------------------------------------*/
-TOKENS
- ident = nondigitMinusA {idchar} /* if char 0 is not an 'a', then anything else is fine */
- | 'a' [ idcharMinusR {idchar} ] /* if char 0 is an 'a', then either there is no char 1 or char 1 is not an 'r' */
- | 'a' 'r' [ idcharMinusR {idchar} ] /* etc. */
- | 'a' 'r' 'r' [ idcharMinusA {idchar} ]
- | 'a' 'r' 'r' 'a' [ idcharMinusY {idchar} ]
- | 'a' 'r' 'r' 'a' 'y' idcharMinusPosDigit {idchar}
- | 'a' 'r' 'r' 'a' 'y' posDigit {idchar} nondigit {idchar}.
- digits = digit {digit}.
- arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].
- string = quote {nonquote} quote.
- colon = ':'.
- lbrace = '{'.
- rbrace = '}'.
-COMMENTS FROM "/*" TO "*/" NESTED
-COMMENTS FROM "//" TO lf
-IGNORE cr + lf + tab
-/*------------------------------------------------------------------------*/
-PRODUCTIONS
-Dafny
-= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;
- List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
- 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; .) ]
-
- ( 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'"); } .)
- DatatypeDecl<defaultModule, out dt> (. defaultModule.TopLevelDecls.Add(dt); .)
- | (. if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } .)
- ArbitraryTypeDecl<defaultModule, out at> (. defaultModule.TopLevelDecls.Add(at); .)
- | (. if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } .)
- IteratorDecl<defaultModule, out iter> (. defaultModule.TopLevelDecls.Add(iter); .)
- | ClassMemberDecl<membersDefaultClass, isGhost, false>
- )
- }
- (. // 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
- .
-SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule>
-= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;
- Attributes attrs = null; IToken/*!*/ id;
- List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;
- List<IToken> idRefined = null, idPath = null, idAssignment = null;
- bool isGhost = false;
- ModuleDefinition module;
- ModuleDecl sm;
- submodule = null; // appease compiler
- bool opened = false;
- .)
- ( "module"
- { Attribute<ref attrs> }
- NoUSIdent<out id>
-
- [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); .)
- "{" (. 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); .)
- | (. if (isGhost) { SemErr(t, "an iterator is not allowed to be declared as 'ghost'"); } .)
- IteratorDecl<module, out iter> (. module.TopLevelDecls.Add(iter); .)
- | ClassMemberDecl<namedModuleDefaultClassMembers, isGhost, false>
- )
- }
- "}" (. module.BodyEndTok = t;
- module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
- submodule = new LiteralModuleDecl(module, parent); .)
- |
- "import" ["opened" (.opened = true;.)]
- ( NoUSIdent<out id> ( "=" QualifiedName<out idPath> ";"
- (. submodule = new AliasModuleDecl(idPath, id, parent, opened); .)
- | ";"
- (. idPath = new List<IToken>(); idPath.Add(id); submodule = new AliasModuleDecl(idPath, id, parent, opened); .)
- | "as" QualifiedName<out idPath> ["default" QualifiedName<out idAssignment> ] ";"
- (.submodule = new AbstractModuleDecl(idPath, id, parent, idAssignment, opened); .)
- )
- )
- )
-.
-
-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;
- Attributes attrs = null;
- List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
- List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
- IToken bodyStart;
- .)
- SYNC
- "class"
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- [ GenericParameters<typeArgs> ]
- "{" (. bodyStart = t; .)
- { ClassMemberDecl<members, false, true>
- }
- "}"
- (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
- c.BodyStartTok = bodyStart;
- c.BodyEndTok = t;
- .)
- .
-ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool isAlreadyGhost, bool allowConstructors.>
-= (. Contract.Requires(cce.NonNullElements(mm));
- Method/*!*/ m;
- Function/*!*/ f;
- MemberModifiers mmod = new MemberModifiers();
- mmod.IsGhost = isAlreadyGhost;
- .)
- { "ghost" (. mmod.IsGhost = true; .)
- | "static" (. mmod.IsStatic = true; .)
- }
- ( FieldDecl<mmod, mm>
- | FunctionDecl<mmod, out f> (. mm.Add(f); .)
- | MethodDecl<mmod, allowConstructors, out m> (. mm.Add(m); .)
- )
- .
-DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt>
-= (. Contract.Requires(module != null);
- Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
- IToken/*!*/ id;
- Attributes attrs = null;
- List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
- List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
- IToken bodyStart = Token.NoToken; // dummy assignment
- bool co = false;
- .)
- SYNC
- ( "datatype"
- | "codatatype" (. co = true; .)
- )
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- [ GenericParameters<typeArgs> ]
- "=" (. bodyStart = t; .)
- DatatypeMemberDecl<ctors>
- { "|" DatatypeMemberDecl<ctors> }
- SYNC ";"
- (. if (co) {
- dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
- } else {
- dt = new IndDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
- }
- dt.BodyStartTok = bodyStart;
- dt.BodyEndTok = t;
- .)
- .
-DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
-= (. Contract.Requires(cce.NonNullElements(ctors));
- Attributes attrs = null;
- IToken/*!*/ id;
- List<Formal/*!*/> formals = new List<Formal/*!*/>();
- .)
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- [ FormalsOptionalIds<formals> ]
- (. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
- .
-FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
-= (. Contract.Requires(cce.NonNullElements(mm));
- Attributes attrs = null;
- IToken/*!*/ id; Type/*!*/ ty;
- .)
- SYNC
- "var"
- (. if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
- .)
- { Attribute<ref attrs> }
- IdentType<out id, out ty, false> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
- { "," IdentType<out id, out ty, false> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
- }
- SYNC ";"
- .
-ArbitraryTypeDecl<ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at>
-= (. IToken/*!*/ id;
- Attributes attrs = null;
- var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- .)
- "type"
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
- ] (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .)
- SYNC ";"
- .
-GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
-/* isGhost always returns as false if allowGhostKeyword is false */
-= (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
- Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
- isGhost = false; .)
- [ "ghost" (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
- ]
- IdentType<out id, out ty, true>
- .
-IdentType<out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId>
-= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
- WildIdent<out id, allowWildcardId>
- ":"
- Type<out ty>
- .
-LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
-= (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
- .)
- WildIdent<out id, true>
- [ ":" Type<out ty> (. optType = ty; .)
- ]
- (. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
- .
-IdentTypeOptional<out BoundVar/*!*/ var>
-= (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
- .)
- WildIdent<out id, true>
- [ ":" Type<out ty> (. optType = ty; .)
- ]
- (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
- .
-TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost>
-= (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
- Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
- Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
- string name = null; isGhost = false; .)
- [ "ghost" (. isGhost = true; .)
- ]
- TypeAndToken<out id, out ty>
- [ ":"
- (. /* try to convert ty to an identifier */
- UserDefinedType udt = ty as UserDefinedType;
- if (udt != null && udt.TypeArgs.Count == 0) {
- name = udt.Name;
- } else {
- SemErr(id, "invalid formal-parameter name in datatype constructor");
- }
- .)
- Type<out ty>
- ]
- (. if (name != null) {
- identName = name;
- } else {
- identName = "#" + anonymousIds++;
- }
- .)
- .
-/*------------------------------------------------------------------------*/
-IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter>
-= (. Contract.Ensures(Contract.ValueAtReturn(out iter) != null);
- IToken/*!*/ id;
- Attributes attrs = null;
- List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();
- IToken openParen;
- List<Formal/*!*/> ins = new List<Formal/*!*/>();
- List<Formal/*!*/> outs = new List<Formal/*!*/>();
- List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
- List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
- List<Expression/*!*/> decreases = new List<Expression>();
- List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();
- List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();
- List<MaybeFreeExpression/*!*/> yieldReq = new List<MaybeFreeExpression/*!*/>();
- List<MaybeFreeExpression/*!*/> yieldEns = new List<MaybeFreeExpression/*!*/>();
- List<Expression/*!*/> dec = new List<Expression/*!*/>();
- Attributes readsAttrs = null;
- Attributes modAttrs = null;
- Attributes decrAttrs = null;
- BlockStmt body = null;
- bool signatureOmitted = false;
- IToken bodyStart = Token.NoToken;
- IToken bodyEnd = Token.NoToken;
- .)
- SYNC
- "iterator"
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- (
- [ GenericParameters<typeArgs> ]
- Formals<true, true, ins, out openParen>
- [ "yields"
- Formals<false, true, outs, out openParen>
- ]
- | "..." (. signatureOmitted = true; openParen = Token.NoToken; .)
- )
- { IteratorSpec<reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs> }
- [ BlockStmt<out body, out bodyStart, out bodyEnd>
- ]
- (. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
- new Specification<FrameExpression>(reads, readsAttrs),
- new Specification<FrameExpression>(mod, modAttrs),
- new Specification<Expression>(decreases, decrAttrs),
- req, ens, yieldReq, yieldEns,
- body, attrs, signatureOmitted);
- iter.BodyStartTok = bodyStart;
- iter.BodyEndTok = bodyEnd;
- .)
- .
-/*------------------------------------------------------------------------*/
-GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
-= (. Contract.Requires(cce.NonNullElements(typeArgs));
- IToken/*!*/ id;
- TypeParameter.EqualitySupportValue eqSupport;
- .)
- "<"
- NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
- [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
- ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
- { "," NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
- [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
- ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
- }
- ">"
- .
-/*------------------------------------------------------------------------*/
-MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
-= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
- IToken/*!*/ id;
- Attributes attrs = null;
- List<TypeParameter/*!*/>/*!*/ typeArgs = new List<TypeParameter/*!*/>();
- IToken openParen;
- List<Formal/*!*/> ins = new List<Formal/*!*/>();
- List<Formal/*!*/> outs = new List<Formal/*!*/>();
- List<MaybeFreeExpression/*!*/> req = new List<MaybeFreeExpression/*!*/>();
- List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
- List<MaybeFreeExpression/*!*/> ens = new List<MaybeFreeExpression/*!*/>();
- List<Expression/*!*/> dec = new List<Expression/*!*/>();
- Attributes decAttrs = null;
- Attributes modAttrs = null;
- BlockStmt body = null;
- bool isConstructor = false;
- bool signatureOmitted = false;
- IToken bodyStart = Token.NoToken;
- IToken bodyEnd = Token.NoToken;
- .)
- SYNC
- ( "method"
- | "constructor" (. if (allowConstructor) {
- isConstructor = true;
- } else {
- SemErr(t, "constructors are only allowed in classes");
- }
- .)
- )
- (. if (isConstructor) {
- if (mmod.IsGhost) {
- SemErr(t, "constructors cannot be declared 'ghost'");
- }
- if (mmod.IsStatic) {
- SemErr(t, "constructors cannot be declared 'static'");
- }
- }
- .)
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- (
- [ GenericParameters<typeArgs> ]
- Formals<true, !mmod.IsGhost, ins, out openParen>
- [ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
- Formals<false, !mmod.IsGhost, outs, out openParen>
- ]
- | "..." (. signatureOmitted = true; openParen = Token.NoToken; .)
- )
- { MethodSpec<req, mod, ens, dec, ref decAttrs, ref modAttrs> }
- [ BlockStmt<out body, out bodyStart, out bodyEnd>
- ]
- (. if (isConstructor) {
- m = new Constructor(id, id.val, typeArgs, ins,
- req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
- } else {
- m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
- req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureOmitted);
- }
- m.BodyStartTok = bodyStart;
- m.BodyEndTok = bodyEnd;
- .)
- .
-MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
- List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes modAttrs.>
-= (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
- Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
- .)
- SYNC
- ( "modifies" { IF(IsAttribute()) Attribute<ref modAttrs> }
- [ FrameExpression<out fe> (. mod.Add(fe); .)
- { "," FrameExpression<out fe> (. mod.Add(fe); .)
- }
- ] SYNC ";"
- | [ "free" (. isFree = true; .)
- ]
- ( "requires" Expression<out e> SYNC ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
- | "ensures" { IF(IsAttribute()) Attribute<ref ensAttrs> } Expression<out e> SYNC ";" (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)
- )
- | "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, true> SYNC ";"
- )
- .
-IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/*!*/ mod, List<Expression/*!*/> decreases,
- List<MaybeFreeExpression/*!*/>/*!*/ req, List<MaybeFreeExpression/*!*/>/*!*/ ens,
- List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*/ yieldEns,
- ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs.>
-= (. Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
- .)
- SYNC
- ( "reads" { IF(IsAttribute()) Attribute<ref readsAttrs> }
- [ FrameExpression<out fe> (. reads.Add(fe); .)
- { "," FrameExpression<out fe> (. reads.Add(fe); .)
- }
- ] SYNC ";"
- | "modifies" { IF(IsAttribute()) Attribute<ref modAttrs> }
- [ FrameExpression<out fe> (. mod.Add(fe); .)
- { "," FrameExpression<out fe> (. mod.Add(fe); .)
- }
- ] SYNC ";"
- | [ "free" (. isFree = true; .)
- ]
- [ "yield" (. isYield = true; .)
- ]
- ( "requires" Expression<out e> SYNC ";" (. if (isYield) {
- yieldReq.Add(new MaybeFreeExpression(e, isFree));
- } else {
- req.Add(new MaybeFreeExpression(e, isFree));
- }
- .)
- | "ensures" { IF(IsAttribute()) Attribute<ref ensAttrs> }
- Expression<out e> SYNC ";" (. if (isYield) {
- yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else {
- ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- }
- .)
- )
- | "decreases" { IF(IsAttribute()) Attribute<ref decrAttrs> } DecreasesList<decreases, false> SYNC ";"
- )
- .
-Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen.>
-= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; .)
- "(" (. openParen = t; .)
- [
- GIdentType<allowGhostKeyword, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
- { "," GIdentType<allowGhostKeyword, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
- }
- ]
- ")"
- .
-FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
-= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; .)
- "("
- [
- TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
- { "," TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
- }
- ]
- ")"
- .
-/*------------------------------------------------------------------------*/
-Type<out Type/*!*/ ty>
-= (. Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; .)
- TypeAndToken<out tok, out ty>
- .
-TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
-= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
- List<Type/*!*/>/*!*/ gt;
- .)
- ( "bool" (. tok = t; .)
- | "nat" (. tok = t; ty = new NatType(); .)
- | "int" (. tok = t; ty = new IntType(); .)
- | "set" (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 1) {
- SemErr("set type expects exactly one type argument");
- }
- ty = new SetType(gt[0]);
- .)
- | "multiset" (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 1) {
- SemErr("multiset type expects exactly one type argument");
- }
- ty = new MultiSetType(gt[0]);
- .)
- | "seq" (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 1) {
- SemErr("seq type expects exactly one type argument");
- }
- ty = new SeqType(gt[0]);
- .)
- | "map" (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 2) {
- SemErr("map type expects exactly two type arguments");
- }
- else { ty = new MapType(gt[0], gt[1]); }
- .)
- | ReferenceType<out tok, out ty>
- )
- .
-ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
-= (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
- tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
- List<Type/*!*/>/*!*/ gt;
- List<IToken> path;
- .)
- ( "object" (. tok = t; ty = new ObjectType(); .)
- | arrayToken (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 1) {
- SemErr("array type expects exactly one type argument");
- }
- int dims = 1;
- if (tok.val.Length != 5) {
- dims = int.Parse(tok.val.Substring(5));
- }
- ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
- .)
- | Ident<out tok> (. gt = new List<Type/*!*/>();
- path = new List<IToken>(); .)
- { (. path.Add(tok); .)
- "." Ident<out tok>
- }
- [ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt, path); .)
- )
- .
-GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
-= (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)
- "<"
- Type<out ty> (. gt.Add(ty); .)
- { "," Type<out ty> (. gt.Add(ty); .)
- }
- ">"
- .
-/*------------------------------------------------------------------------*/
-FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
-= (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
- Attributes attrs = null;
- IToken/*!*/ id = Token.NoToken; // to please compiler
- List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
- List<Formal/*!*/> formals = new List<Formal/*!*/>();
- Type/*!*/ returnType = new BoolType();
- List<Expression/*!*/> reqs = new List<Expression/*!*/>();
- List<Expression/*!*/> ens = new List<Expression/*!*/>();
- List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
- List<Expression/*!*/> decreases;
- Expression body = null;
- bool isPredicate = false; bool isCoPredicate = false;
- bool isFunctionMethod = false;
- IToken openParen = null;
- IToken bodyStart = Token.NoToken;
- IToken bodyEnd = Token.NoToken;
- bool signatureOmitted = false;
- .)
- /* ----- function ----- */
- ( "function"
- [ "method" (. isFunctionMethod = true; .)
- ]
- (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
- .)
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- (
- [ GenericParameters<typeArgs> ]
- Formals<true, isFunctionMethod, formals, out openParen>
- ":"
- Type<out returnType>
- | "..." (. signatureOmitted = true;
- openParen = Token.NoToken; .)
- )
-
- /* ----- predicate ----- */
- | "predicate" (. isPredicate = true; .)
- [ "method" (. isFunctionMethod = true; .)
- ]
- (. if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
- .)
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- (
- [ GenericParameters<typeArgs> ]
- [ Formals<true, isFunctionMethod, formals, out openParen>
- [ ":" (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)
- ]
- ]
- | "..." (. signatureOmitted = true;
- openParen = Token.NoToken; .)
- )
-
- /* ----- copredicate ----- */
- | "copredicate" (. isCoPredicate = true; .)
- (. if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
- .)
- { Attribute<ref attrs> }
- NoUSIdent<out id>
- (
- [ GenericParameters<typeArgs> ]
- [ Formals<true, isFunctionMethod, formals, out openParen>
- [ ":" (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)
- ]
- ]
- | "..." (. signatureOmitted = true;
- openParen = Token.NoToken; .)
- )
- )
-
- (. decreases = isCoPredicate ? null : new List<Expression/*!*/>(); .)
- { FunctionSpec<reqs, reads, ens, decreases> }
- [ FunctionBody<out body, out bodyStart, out bodyEnd>
- ]
- (. if (isPredicate) {
- f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,
- reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);
- } else if (isCoPredicate) {
- f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,
- reqs, reads, ens, body, attrs, signatureOmitted);
- } else {
- f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,
- reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureOmitted);
- }
- f.BodyStartTok = bodyStart;
- f.BodyEndTok = bodyEnd;
- .)
- .
-FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases.>
-= (. Contract.Requires(cce.NonNullElements(reqs));
- Contract.Requires(cce.NonNullElements(reads));
- Contract.Requires(decreases == null || cce.NonNullElements(decreases));
- Expression/*!*/ e; FrameExpression/*!*/ fe; .)
- (
- SYNC
- "requires" Expression<out e> SYNC ";" (. reqs.Add(e); .)
- | "reads" [ PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
- { "," PossiblyWildFrameExpression<out fe> (. reads.Add(fe); .)
- }
- ] SYNC ";"
- | "ensures" Expression<out e> SYNC ";" (. ens.Add(e); .)
- | "decreases" (. if (decreases == null) {
- SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
- decreases = new List<Expression/*!*/>();
- }
- .)
- DecreasesList<decreases, false> SYNC ";"
- )
- .
-PossiblyWildExpression<out Expression/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
- e = dummyExpr; .)
- /* A decreases clause on a loop asks that no termination check be performed.
- * Use of this feature is sound only with respect to partial correctness.
- */
- ( "*" (. e = new WildcardExpr(t); .)
- | Expression<out e>
- )
- .
-PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
-= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .)
- /* A reads clause can list a wildcard, which allows the enclosing function to
- * read anything. In many cases, and in particular in all cases where
- * the function is defined recursively, this makes it next to impossible to make
- * any use of the function. Nevertheless, as an experimental feature, the
- * language allows it (and it is sound).
- */
- ( "*" (. fe = new FrameExpression(t, new WildcardExpr(t), null); .)
- | FrameExpression<out fe>
- )
- .
-FrameExpression<out FrameExpression/*!*/ fe>
-= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null);
- Expression/*!*/ e;
- IToken/*!*/ id;
- string fieldName = null; IToken feTok = null;
- fe = null;
- .)
- (( Expression<out e> (. feTok = e.tok; .)
- [ "`" Ident<out id> (. fieldName = id.val; feTok = id; .)
- ]
- (. fe = new FrameExpression(feTok, e, fieldName); .)
- ) |
- ( "`" Ident<out id> (. fieldName = id.val; .)
- (. fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); .)
- ))
- .
-FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
- "{" (. bodyStart = t; .)
- Expression<out e>
- "}" (. bodyEnd = t; .)
- .
-/*------------------------------------------------------------------------*/
-BlockStmt<out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
-= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);
- List<Statement/*!*/> body = new List<Statement/*!*/>();
- .)
- "{" (. bodyStart = t; .)
- { Stmt<body>
- }
- "}" (. bodyEnd = t;
- block = new BlockStmt(bodyStart, body); .)
- .
-Stmt<.List<Statement/*!*/>/*!*/ ss.>
-= (. Statement/*!*/ s;
- .)
- OneStmt<out s> (. ss.Add(s); .)
- .
-OneStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
- s = dummyStmt; /* to please the compiler */
- BlockStmt bs;
- IToken bodyStart, bodyEnd;
- int breakCount;
- .)
- SYNC
- ( BlockStmt<out bs, out bodyStart, out bodyEnd> (. s = bs; .)
- | AssertStmt<out s>
- | AssumeStmt<out s>
- | PrintStmt<out s>
- | UpdateStmt<out s>
- | VarDeclStatement<out s>
- | IfStmt<out s>
- | WhileStmt<out s>
- | MatchStmt<out s>
- | ParallelStmt<out s>
- | CalcStmt<out s>
- | "label" (. x = t; .)
- 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; .)
- ( NoUSIdent<out id> (. label = id.val; .)
- | { "break" (. breakCount++; .)
- }
- )
- SYNC
- ";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
- | ReturnStmt<out s>
- | SkeletonStmt<out s>
- ";"
- )
- .
-
-SkeletonStmt<out Statement s>
-= (. List<IToken> names = null;
- List<Expression> exprs = null;
- IToken tok, dotdotdot, whereTok;
- Expression e; .)
- "..." (. dotdotdot = t; .)
- ["where" (. names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;.)
- Ident<out tok> (. names.Add(tok); .)
- {"," Ident<out tok> (. names.Add(tok); .)
- }
- ":="
- Expression<out e> (. exprs.Add(e); .)
- {"," Expression<out e> (. exprs.Add(e); .)
- }
- (. if (exprs.Count != names.Count) {
- SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");
- names = null; exprs = null;
- }
- .)
- ]
- (. s = new SkeletonStatement(dotdotdot, names, exprs); .)
- .
-ReturnStmt<out Statement/*!*/ s>
-= (.
- IToken returnTok = null;
- List<AssignmentRhs> rhss = null;
- AssignmentRhs r;
- bool isYield = false;
- .)
- ( "return" (. returnTok = t; .)
- | "yield" (. returnTok = t; isYield = true; .)
- )
- [
- Rhs<out r, null> (. rhss = new List<AssignmentRhs>(); rhss.Add(r); .)
- { "," Rhs<out r, null> (. rhss.Add(r); .)
- }
- ]
- ";" (. if (isYield) {
- s = new YieldStmt(returnTok, rhss);
- } else {
- s = new ReturnStmt(returnTok, rhss);
- }
- .)
- .
-UpdateStmt<out Statement/*!*/ s>
-= (. List<Expression> lhss = new List<Expression>();
- List<AssignmentRhs> rhss = new List<AssignmentRhs>();
- Expression e; AssignmentRhs r;
- Expression lhs0;
- IToken x;
- Attributes attrs = null;
- IToken suchThatAssume = null;
- Expression suchThat = null;
- .)
- Lhs<out e> (. x = e.tok; .)
- ( { Attribute<ref attrs> }
- ";" (. rhss.Add(new ExprRhs(e, attrs)); .)
- | (. lhss.Add(e); lhs0 = e; .)
- { "," Lhs<out e> (. lhss.Add(e); .)
- }
- ( ":=" (. x = t; .)
- Rhs<out r, lhs0> (. rhss.Add(r); .)
- { "," Rhs<out r, lhs0> (. rhss.Add(r); .)
- }
- | ":|" (. x = t; .)
- [ "assume" (. suchThatAssume = t; .)
- ]
- Expression<out suchThat>
- )
- ";"
- | ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
- )
- (. if (suchThat != null) {
- s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
- } else {
- if (lhss.Count == 0 && rhss.Count == 0) {
- s = new BlockStmt(x, new List<Statement>()); // error, give empty statement
- } else {
- s = new UpdateStmt(x, lhss, rhss);
- }
- }
- .)
- .
-Rhs<out AssignmentRhs r, Expression receiverForInitCall>
-= (. Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);
- IToken/*!*/ x, newToken; Expression/*!*/ e;
- List<Expression> ee = null;
- Type ty = null;
- CallStmt initCall = null;
- List<Expression> args;
- r = dummyRhs; // to please compiler
- Attributes attrs = null;
- .)
- ( "new" (. newToken = t; .)
- TypeAndToken<out x, out ty>
- [ "[" (. ee = new List<Expression>(); .)
- Expressions<ee>
- "]" (. // make sure an array class with this dimensionality exists
- UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
- .)
- | "." Ident<out x>
- "(" (. // This case happens when we have type<typeargs>.Constructor(args)
- // There is no ambiguity about where the constructor is or whether one exists.
- args = new List<Expression/*!*/>(); .)
- [ Expressions<args> ]
- ")" (. initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); .)
- | "(" (. var udf = ty as UserDefinedType;
- if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {
- // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as
- // the name of the constructor that's being invoked.
- x = udf.tok;
- ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));
- } else {
- SemErr(t, "expected '.'");
- x = null;
- }
- args = new List<Expression/*!*/>(); .)
- [ Expressions<args> ]
- ")" (. if (x != null) {
- initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
- }
- .)
- ]
- (. if (ee != null) {
- r = new TypeRhs(newToken, ty, ee);
- } else {
- r = new TypeRhs(newToken, ty, initCall);
- }
- .)
- /* One day, the choose expression should be treated just as a special case of a method call. */
- | "choose" (. x = t; .)
- Expression<out e> (. r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); .)
- | "*" (. r = new HavocRhs(t); .)
- | Expression<out e> (. r = new ExprRhs(e); .)
- )
- { Attribute<ref attrs> } (. r.Attributes = attrs; .)
- .
-VarDeclStatement<.out Statement/*!*/ s.>
-= (. IToken x = null, assignTok = null; bool isGhost = false;
- VarDecl/*!*/ d;
- AssignmentRhs r; IdentifierExpr lhs0;
- List<VarDecl> lhss = new List<VarDecl>();
- List<AssignmentRhs> rhss = new List<AssignmentRhs>();
- IToken suchThatAssume = null;
- Expression suchThat = null;
- .)
- [ "ghost" (. isGhost = true; x = t; .)
- ]
- "var" (. if (!isGhost) { x = t; } .)
- LocalIdentTypeOptional<out d, isGhost> (. lhss.Add(d); .)
- { ","
- LocalIdentTypeOptional<out d, isGhost> (. lhss.Add(d); .)
- }
- [ ":=" (. assignTok = t;
- lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
- lhs0.Var = lhss[0]; lhs0.Type = lhss[0].OptionalType; // resolve here
- .)
- Rhs<out r, lhs0> (. rhss.Add(r); .)
- { "," Rhs<out r, lhs0> (. rhss.Add(r); .)
- }
- | ":|" (. assignTok = t; .)
- [ "assume" (. suchThatAssume = t; .)
- ]
- Expression<out suchThat>
- ]
- ";"
- (. ConcreteUpdateStatement update;
- if (suchThat != null) {
- var ies = new List<Expression>();
- foreach (var lhs in lhss) {
- ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));
- }
- update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);
- } else if (rhss.Count == 0) {
- update = null;
- } else {
- var ies = new List<Expression>();
- foreach (var lhs in lhss) {
- ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
- }
- update = new UpdateStmt(assignTok, ies, rhss);
- }
- s = new VarDeclStmt(x, lhss, update);
- .)
- .
-IfStmt<out Statement/*!*/ ifStmt>
-= (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
- Expression guard = null; bool guardOmitted = false;
- BlockStmt/*!*/ thn;
- BlockStmt/*!*/ bs;
- Statement/*!*/ s;
- Statement els = null;
- IToken bodyStart, bodyEnd;
- List<GuardedAlternative> alternatives;
- ifStmt = dummyStmt; // to please the compiler
- .)
- "if" (. x = t; .)
- (
- ( Guard<out guard>
- | "..." (. guardOmitted = true; .)
- )
- BlockStmt<out thn, out bodyStart, out bodyEnd>
- [ "else"
- ( IfStmt<out s> (. els = s; .)
- | BlockStmt<out bs, out bodyStart, out bodyEnd> (. els = bs; .)
- )
- ]
- (. if (guardOmitted) {
- ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
- } else {
- ifStmt = new IfStmt(x, guard, thn, els);
- }
- .)
- |
- AlternativeBlock<out alternatives>
- (. ifStmt = new AlternativeStmt(x, alternatives); .)
- )
- .
-AlternativeBlock<.out List<GuardedAlternative> alternatives.>
-= (. alternatives = new List<GuardedAlternative>();
- IToken x;
- Expression e;
- List<Statement> body;
- .)
- "{"
- { "case" (. x = t; .)
- Expression<out e>
- "=>"
- (. body = new List<Statement>(); .)
- { Stmt<body> }
- (. alternatives.Add(new GuardedAlternative(x, e, body)); .)
- }
- "}"
- .
-WhileStmt<out Statement/*!*/ stmt>
-= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
- Expression guard = null; bool guardOmitted = false;
- List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
- List<Expression/*!*/> decreases = new List<Expression/*!*/>();
- Attributes decAttrs = null;
- Attributes modAttrs = null;
- List<FrameExpression/*!*/> mod = null;
- BlockStmt/*!*/ body = null; bool bodyOmitted = false;
- IToken bodyStart = null, bodyEnd = null;
- List<GuardedAlternative> alternatives;
- stmt = dummyStmt; // to please the compiler
- .)
- "while" (. x = t; .)
- (
- ( Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
- | "..." (. guardOmitted = true; .)
- )
- LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
- ( BlockStmt<out body, out bodyStart, out bodyEnd>
- | "..." (. bodyOmitted = true; .)
- )
- (.
- if (guardOmitted || bodyOmitted) {
- if (mod != null) {
- SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
- }
- if (body == null) {
- body = new BlockStmt(x, new List<Statement>());
- }
- stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);
- stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);
- } else {
- // The following statement protects against crashes in case of parsing errors
- body = body ?? new BlockStmt(x, new List<Statement>());
- stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
- }
- .)
- |
- LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
- AlternativeBlock<out alternatives>
- (. stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); .)
- )
- .
-LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs.>
-= (. FrameExpression/*!*/ fe;
- invariants = new List<MaybeFreeExpression/*!*/>();
- MaybeFreeExpression invariant = null;
- decreases = new List<Expression/*!*/>();
- mod = null;
- .)
- {
- Invariant<out invariant> SYNC ";" (. invariants.Add(invariant); .)
- | SYNC "decreases"
- { IF(IsAttribute()) Attribute<ref decAttrs> }
- DecreasesList<decreases, true> SYNC ";"
- | SYNC "modifies"
- { IF(IsAttribute()) Attribute<ref modAttrs> } (. mod = mod ?? new List<FrameExpression>(); .)
- [ FrameExpression<out fe> (. mod.Add(fe); .)
- { "," FrameExpression<out fe> (. mod.Add(fe); .)
- }
- ] SYNC ";"
- }
- .
-Invariant<out MaybeFreeExpression/*!*/ invariant>
-= (. bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; .)
- SYNC
- ["free" (. isFree = true; .)
- ]
- "invariant" { IF(IsAttribute()) Attribute<ref attrs> } Expression<out e> (. invariant = new MaybeFreeExpression(e, isFree, attrs); .)
- .
-DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
-= (. Expression/*!*/ e; .)
- PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
- SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");
- } else {
- decreases.Add(e);
- }
- .)
- { "," PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
- SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");
- } else {
- decreases.Add(e);
- }
- .)
- }
- .
-Guard<out Expression e> /* null represents demonic-choice */
-= (. Expression/*!*/ ee; e = null; .)
- "("
- ( "*" (. e = null; .)
- | Expression<out ee> (. e = ee; .)
- )
- ")"
- .
-MatchStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
- List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); .)
- "match" (. x = t; .)
- Expression<out e>
- "{"
- { CaseStatement<out c> (. cases.Add(c); .)
- }
- "}"
- (. s = new MatchStmt(x, e, cases); .)
- .
-CaseStatement<out MatchCaseStmt/*!*/ c>
-= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
- IToken/*!*/ x, id;
- List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
- BoundVar/*!*/ bv;
- List<Statement/*!*/> body = new List<Statement/*!*/>();
- .)
- "case" (. x = t; .)
- Ident<out id>
- [ "("
- IdentTypeOptional<out bv> (. arguments.Add(bv); .)
- { "," IdentTypeOptional<out bv> (. arguments.Add(bv); .)
- }
- ")" ]
- "=>"
- { Stmt<body> }
- (. c = new MatchCaseStmt(x, id.val, arguments, body); .)
- .
-/*------------------------------------------------------------------------*/
-AssertStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
- Expression e = null; Attributes attrs = null;
- .)
- "assert" (. x = t; .)
- { IF(IsAttribute()) Attribute<ref attrs> }
- ( Expression<out e>
- | "..."
- )
- ";"
- (. if (e == null) {
- s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
- } else {
- s = new AssertStmt(x, e, attrs);
- }
- .)
- .
-AssumeStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
- Expression e = null; Attributes attrs = null;
- .)
- "assume" (. x = t; .)
- { IF(IsAttribute()) Attribute<ref attrs> }
- ( Expression<out e>
- | "..."
- )
- (. if (e == null) {
- s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
- } else {
- s = new AssumeStmt(x, e, attrs);
- }
- .)
- ";"
- .
-PrintStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
- List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- .)
- "print" (. x = t; .)
- AttributeArg<out arg> (. args.Add(arg); .)
- { "," AttributeArg<out arg> (. args.Add(arg); .)
- }
- ";" (. s = new PrintStmt(x, args); .)
- .
-
-ParallelStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- IToken/*!*/ x;
- List<BoundVar/*!*/> bvars = null;
- Attributes attrs = null;
- Expression range = null;
- var ens = new List<MaybeFreeExpression/*!*/>();
- bool isFree;
- Expression/*!*/ e;
- BlockStmt/*!*/ block;
- IToken bodyStart, bodyEnd;
- .)
- "parallel" (. x = t; .)
- "("
- [ (. List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX; .)
- QuantifierDomain<out bvarsX, out attrsX, out rangeX>
- (. bvars = bvarsX; attrs = attrsX; range = rangeX;
- .)
- ]
- (. if (bvars == null) { bvars = new List<BoundVar>(); }
- if (range == null) { range = new LiteralExpr(x, true); }
- .)
- ")"
- { (. isFree = false; .)
- [ "free" (. isFree = true; .)
- ]
- "ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
- }
- BlockStmt<out block, out bodyStart, out bodyEnd>
- (. s = new ParallelStmt(x, bvars, attrs, range, ens, block); .)
- .
-
-CalcStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- Token x;
- BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;
- var lines = new List<Expression/*!*/>();
- var hints = new List<BlockStmt/*!*/>();
- var customOps = new List<BinaryExpr.Opcode?>();
- BinaryExpr.Opcode? maybeOp;
- Expression/*!*/ e;
- BlockStmt/*!*/ h;
- IToken opTok;
- .)
- "calc" (. x = t; .)
- [ CalcOp<out opTok, out calcOp> (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(calcOp, calcOp); // guard against non-trasitive calcOp (like !=)
- if (maybeOp == null) {
- SemErr(opTok, "the main operator of a calculation must be transitive");
- }
- resOp = calcOp;
- .)
- ]
- "{"
- [ Expression<out e> (. lines.Add(e); .)
- ";"
- {
- Hint<out h> (. hints.Add(h); .)
- ( CalcOp<out opTok, out op> (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
- if (maybeOp == null) {
- customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor
- SemErr(opTok, "this operator cannot continue this calculation");
- } else {
- customOps.Add(op);
- resOp = (BinaryExpr.Opcode)maybeOp;
- }
- .)
- | (. customOps.Add(null); .)
- )
- Expression<out e> (. lines.Add(e); .)
- ";"
- }
- ]
- "}"
- (. s = new CalcStmt(x, calcOp, lines, hints, customOps); .)
- .
-CalcOp<out IToken x, out BinaryExpr.Opcode/*!*/ op>
-= (. Contract.Ensures(Microsoft.Dafny.CalcStmt.ValidOp(Contract.ValueAtReturn(out op)));
- op = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
- x = null;
- .)
- ( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
- | "<" (. x = t; op = BinaryExpr.Opcode.Lt; .)
- | ">" (. x = t; op = BinaryExpr.Opcode.Gt; .)
- | "<=" (. x = t; op = BinaryExpr.Opcode.Le; .)
- | ">=" (. x = t; op = BinaryExpr.Opcode.Ge; .)
- | "!=" (. x = t; op = BinaryExpr.Opcode.Neq; .)
- | '\u2260' (. x = t; op = BinaryExpr.Opcode.Neq; .)
- | '\u2264' (. x = t; op = BinaryExpr.Opcode.Le; .)
- | '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
- | EquivOp (. x = t; op = BinaryExpr.Opcode.Iff; .)
- | ImpliesOp (. x = t; op = BinaryExpr.Opcode.Imp; .)
- )
- .
-Hint<out BlockStmt s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
- var subhints = new List<Statement/*!*/>();
- IToken bodyStart, bodyEnd;
- BlockStmt/*!*/ block;
- Statement/*!*/ calc;
- Token x = la;
- .)
- { BlockStmt<out block, out bodyStart, out bodyEnd> (. subhints.Add(block); .)
- | CalcStmt<out calc> (. subhints.Add(calc); .)
- }
- (. s = new BlockStmt(x, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
- .)
- .
-/*------------------------------------------------------------------------*/
-Expression<out Expression/*!*/ e>
-=
- EquivExpression<out e>
- .
-/*------------------------------------------------------------------------*/
-EquivExpression<out Expression/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
- ImpliesExpression<out e0>
- { EquivOp (. x = t; .)
- ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
- }
- .
-EquivOp = "<==>" | '\u21d4'.
-/*------------------------------------------------------------------------*/
-ImpliesExpression<out Expression/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
- LogicalExpression<out e0>
- [ ImpliesOp (. x = t; .)
- ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
- ]
- .
-ImpliesOp = "==>" | '\u21d2'.
-/*------------------------------------------------------------------------*/
-LogicalExpression<out Expression/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
- RelationalExpression<out e0>
- [ AndOp (. x = t; .)
- RelationalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
- { AndOp (. x = t; .)
- RelationalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)
- }
- | OrOp (. x = t; .)
- RelationalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
- { OrOp (. x = t; .)
- RelationalExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)
- }
- ]
- .
-AndOp = "&&" | '\u2227'.
-OrOp = "||" | '\u2228'.
-/*------------------------------------------------------------------------*/
-RelationalExpression<out Expression/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken x, firstOpTok = null; Expression e0, e1, acc = null; BinaryExpr.Opcode op;
- List<Expression> chain = null;
- List<BinaryExpr.Opcode> ops = null;
- int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one !=
- // 1 ("ascending") indicates chain of ==, <, <=, possibly with one !=
- // 2 ("descending") indicates chain of ==, >, >=, possibly with one !=
- // 3 ("illegal") indicates illegal chain
- // 4 ("disjoint") indicates chain of disjoint set operators
- bool hasSeenNeq = false;
- .)
- Term<out e0> (. e = e0; .)
- [ RelOp<out x, out op> (. firstOpTok = x; .)
- Term<out e1> (. e = new BinaryExpr(x, op, e0, e1);
- if (op == BinaryExpr.Opcode.Disjoint)
- acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
- .)
- { (. if (chain == null) {
- chain = new List<Expression>();
- ops = new List<BinaryExpr.Opcode>();
- chain.Add(e0); ops.Add(op); chain.Add(e1);
- switch (op) {
- case BinaryExpr.Opcode.Eq:
- kind = 0; break;
- case BinaryExpr.Opcode.Neq:
- kind = 0; hasSeenNeq = true; break;
- case BinaryExpr.Opcode.Lt:
- case BinaryExpr.Opcode.Le:
- kind = 1; break;
- case BinaryExpr.Opcode.Gt:
- case BinaryExpr.Opcode.Ge:
- kind = 2; break;
- case BinaryExpr.Opcode.Disjoint:
- kind = 4; break;
- default:
- kind = 3; break;
- }
- }
- e0 = e1;
- .)
- RelOp<out x, out op> (. switch (op) {
- case BinaryExpr.Opcode.Eq:
- if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "chaining not allowed from the previous operator"); }
- break;
- case BinaryExpr.Opcode.Neq:
- if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }
- if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
- hasSeenNeq = true; break;
- case BinaryExpr.Opcode.Lt:
- case BinaryExpr.Opcode.Le:
- if (kind == 0) { kind = 1; }
- else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
- break;
- case BinaryExpr.Opcode.Gt:
- case BinaryExpr.Opcode.Ge:
- if (kind == 0) { kind = 2; }
- else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
- break;
- case BinaryExpr.Opcode.Disjoint:
- if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
- break;
- default:
- SemErr(x, "this operator cannot be part of a chain");
- kind = 3; break;
- }
- .)
- Term<out e1> (. ops.Add(op); chain.Add(e1);
- if (op == BinaryExpr.Opcode.Disjoint) {
- e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
- acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
- }
- else
- e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
- .)
- }
- ]
- (. if (chain != null) {
- e = new ChainingExpression(firstOpTok, chain, ops, e);
- }
- .)
- .
-RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
-= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null);
- x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- IToken y;
- .)
- ( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
- | "<" (. x = t; op = BinaryExpr.Opcode.Lt; .)
- | ">" (. x = t; op = BinaryExpr.Opcode.Gt; .)
- | "<=" (. x = t; op = BinaryExpr.Opcode.Le; .)
- | ">=" (. x = t; op = BinaryExpr.Opcode.Ge; .)
- | "!=" (. x = t; op = BinaryExpr.Opcode.Neq; .)
- | "!!" (. x = t; op = BinaryExpr.Opcode.Disjoint; .)
- | "in" (. x = t; op = BinaryExpr.Opcode.In; .)
- | /* The next operator is "!in", but Coco evidently parses "!in" even when it is a prefix of, say, "!initialized".
- * The reason for this seems to be that the first character of "!in" is not a letter. So, here is the workaround:
- */
- "!" (. x = t; y = Token.NoToken; .)
- [ "in" (. y = t; .)
- ] (. if (y == Token.NoToken) {
- SemErr(x, "invalid RelOp");
- } else if (y.pos != x.pos + 1) {
- SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");
- } else {
- x.val = "!in";
- op = BinaryExpr.Opcode.NotIn;
- }
- .)
- | '\u2260' (. x = t; op = BinaryExpr.Opcode.Neq; .)
- | '\u2264' (. x = t; op = BinaryExpr.Opcode.Le; .)
- | '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
- )
- .
-/*------------------------------------------------------------------------*/
-Term<out Expression/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
- Factor<out e0>
- { AddOp<out x, out op>
- Factor<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
- }
- .
-AddOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
-= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/; .)
- ( "+" (. x = t; op = BinaryExpr.Opcode.Add; .)
- | "-" (. x = t; op = BinaryExpr.Opcode.Sub; .)
- )
- .
-/*------------------------------------------------------------------------*/
-Factor<out Expression/*!*/ e0>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
- UnaryExpression<out e0>
- { MulOp<out x, out op>
- UnaryExpression<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
- }
- .
-MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
-= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
- ( "*" (. x = t; op = BinaryExpr.Opcode.Mul; .)
- | "/" (. x = t; op = BinaryExpr.Opcode.Div; .)
- | "%" (. x = t; op = BinaryExpr.Opcode.Mod; .)
- )
- .
-/*------------------------------------------------------------------------*/
-UnaryExpression<out Expression/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; .)
- ( "-" (. x = t; .)
- UnaryExpression<out e> (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)
- | NegOp (. x = t; .)
- UnaryExpression<out e> (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)
- | EndlessExpression<out e> /* these have no further suffix */
- | DottedIdentifiersAndFunction<out e>
- { Suffix<ref e> }
- | DisplayExpr<out e>
- { Suffix<ref e> }
- | MultiSetExpr<out e>
- { Suffix<ref e> }
- | "map" (. x = t; .)
- ( MapDisplayExpr<x, out e>
- { Suffix<ref e> }
- | MapComprehensionExpr<x, out e>
- | (. SemErr("map must be followed by literal in brackets or comprehension."); .)
- )
- | ConstAtomExpression<out e>
- { Suffix<ref e> }
- )
- .
-Lhs<out Expression e>
-= (. e = dummyExpr; // the assignment is to please the compiler, the dummy value to satisfy contracts in the event of a parse error
- .)
- ( DottedIdentifiersAndFunction<out e>
- { Suffix<ref e> }
- | ConstAtomExpression<out e>
- Suffix<ref e>
- { Suffix<ref e> }
- )
- .
-NegOp = "!" | '\u00ac'.
-/* A ConstAtomExpression is never an l-value. Also, a ConstAtomExpression is never followed by
- * an open paren (but could very well have a suffix that starts with a period or a square bracket).
- * (The "Also..." part may change if expressions in Dafny could yield functions.)
- */
-ConstAtomExpression<out Expression/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x; BigInteger n;
- e = dummyExpr;
- .)
- ( "false" (. e = new LiteralExpr(t, false); .)
- | "true" (. e = new LiteralExpr(t, true); .)
- | "null" (. e = new LiteralExpr(t); .)
- | Nat<out n> (. e = new LiteralExpr(t, n); .)
- | "this" (. e = new ThisExpr(t); .)
- | "fresh" (. x = t; .)
- "(" Expression<out e> ")" (. e = new FreshExpr(x, e); .)
- | "old" (. x = t; .)
- "(" Expression<out e> ")" (. e = new OldExpr(x, e); .)
- | "|" (. x = t; .)
- Expression<out e> (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)
- "|"
- | "(" (. x = t; .)
- Expression<out e> (. e = new ParensExpression(x, e); .)
- ")"
- )
- .
-DisplayExpr<out Expression e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
- e = dummyExpr;
- .)
- ( "{" (. x = t; elements = new List<Expression/*!*/>(); .)
- [ Expressions<elements> ] (. e = new SetDisplayExpr(x, elements);.)
- "}"
- | "[" (. x = t; elements = new List<Expression/*!*/>(); .)
- [ Expressions<elements> ] (. e = new SeqDisplayExpr(x, elements); .)
- "]"
- )
- .
-MultiSetExpr<out Expression e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
- e = dummyExpr;
- .)
- "multiset" (. x = t; .)
- ( "{" (. elements = new List<Expression/*!*/>(); .)
- [ Expressions<elements> ] (. e = new MultiSetDisplayExpr(x, elements);.)
- "}"
- | "(" (. x = t; elements = new List<Expression/*!*/>(); .)
- Expression<out e> (. e = new MultiSetFormingExpr(x, e); .)
- ")"
- | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)
- )
- .
-MapDisplayExpr<IToken/*!*/ mapToken, out Expression e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
- e = dummyExpr;
- .)
- "["
- [ MapLiteralExpressions<out elements> ] (. e = new MapDisplayExpr(mapToken, elements);.)
- "]"
- .
-MapLiteralExpressions<.out List<ExpressionPair> elements.>
-= (. Expression/*!*/ d, r;
- elements = new List<ExpressionPair/*!*/>(); .)
- Expression<out d> ":=" Expression<out r> (. elements.Add(new ExpressionPair(d,r)); .)
- { "," Expression<out d> ":=" Expression<out r>(. elements.Add(new ExpressionPair(d,r)); .)
- }
- .
-MapComprehensionExpr<IToken/*!*/ mapToken, out Expression e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- BoundVar/*!*/ bv;
- List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
- Expression range = null;
- Expression body;
- .)
- IdentTypeOptional<out bv> (. bvars.Add(bv); .)
- [ "|" Expression<out range> ]
- QSep
- Expression<out body>
- (. e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body);
- .)
- .
-EndlessExpression<out Expression e>
-= (. IToken/*!*/ x;
- Expression e0, e1;
- e = dummyExpr;
- .)
- ( "if" (. x = t; .)
- Expression<out e>
- "then" Expression<out e0>
- "else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
- | MatchExpression<out e>
- | QuantifierGuts<out e>
- | ComprehensionExpr<out e>
- | "assert" (. x = t; .)
- Expression<out e0> ";"
- Expression<out e1> (. e = new AssertExpr(x, e0, e1); .)
- | "assume" (. x = t; .)
- Expression<out e0> ";"
- Expression<out e1> (. e = new AssumeExpr(x, e0, e1); .)
- | LetExpr<out e>
- | NamedExpr<out e>
- )
- .
-
-LetExpr<out Expression e>
-= (. IToken/*!*/ x;
- e = dummyExpr;
- BoundVar d;
- List<BoundVar> letVars; List<Expression> letRHSs;
- .)
- "var" (. x = t;
- letVars = new List<BoundVar>();
- letRHSs = new List<Expression>(); .)
- IdentTypeOptional<out d> (. letVars.Add(d); .)
- { "," IdentTypeOptional<out d> (. letVars.Add(d); .)
- }
- ":="
- Expression<out e> (. letRHSs.Add(e); .)
- { "," Expression<out e> (. letRHSs.Add(e); .)
- }
- ";"
- Expression<out e> (. e = new LetExpr(x, letVars, letRHSs, e); .)
- .
-
-NamedExpr<out Expression e>
-= (. IToken/*!*/ x, d;
- e = dummyExpr;
- Expression expr;
- .)
- "label" (. x = t; .)
- NoUSIdent<out d>
- ":"
- Expression<out e> (. expr = e;
- e = new NamedExpr(x, d.val, expr); .)
- .
-
-MatchExpression<out Expression/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
- List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- .)
- "match" (. x = t; .)
- Expression<out e>
- /* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,
- but it's okay, because we want this closer match expression to bind as much as possible--use
- parens around it to limit its scope. */
- { CaseExpression<out c> (. cases.Add(c); .)
- }
- (. e = new MatchExpr(x, e, cases); .)
- .
-CaseExpression<out MatchCaseExpr/*!*/ c>
-= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;
- List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
- BoundVar/*!*/ bv;
- Expression/*!*/ body;
- .)
- "case" (. x = t; .)
- Ident<out id>
- [ "("
- IdentTypeOptional<out bv> (. arguments.Add(bv); .)
- { "," IdentTypeOptional<out bv> (. arguments.Add(bv); .)
- }
- ")" ]
- "=>"
- Expression<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
- .
-/*------------------------------------------------------------------------*/
-DottedIdentifiersAndFunction<out Expression e>
-= (. IToken id; IToken openParen = null;
- List<Expression> args = null;
- List<IToken> idents = new List<IToken>();
- .)
- Ident<out id> (. idents.Add(id); .)
- { "."
- Ident<out id> (. idents.Add(id); .)
- }
- [ "(" (. openParen = t; args = new List<Expression>(); .)
- [ Expressions<args> ]
- ")"
- ]
- (. e = new IdentifierSequence(idents, openParen, args); .)
- .
-Suffix<ref Expression/*!*/ e>
-= (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x; List<Expression/*!*/>/*!*/ args;
- Expression e0 = null; Expression e1 = null; Expression/*!*/ ee; bool anyDots = false;
- List<Expression> multipleIndices = null;
- bool func = false;
- .)
- ( "."
- Ident<out id>
- [ "(" (. IToken openParen = t; args = new List<Expression/*!*/>(); func = true; .)
- [ Expressions<args> ]
- ")" (. e = new FunctionCallExpr(id, id.val, e, openParen, args); .)
- ] (. if (!func) { e = new ExprDotName(id, e, id.val); } .)
- | "[" (. x = t; .)
- ( Expression<out ee> (. e0 = ee; .)
- ( ".." (. anyDots = true; .)
- [ Expression<out ee> (. e1 = ee; .)
- ]
- | ":="
- Expression<out ee> (. e1 = ee; .)
- | { "," Expression<out ee> (. if (multipleIndices == null) {
- multipleIndices = new List<Expression>();
- multipleIndices.Add(e0);
- }
- multipleIndices.Add(ee);
- .)
- }
- )
- | ".." (. anyDots = true; .)
- [ Expression<out ee> (. e1 = ee; .)
- ]
- )
- (. if (multipleIndices != null) {
- e = new MultiSelectExpr(x, e, multipleIndices);
- // make sure an array class with this dimensionality exists
- UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);
- } else {
- if (!anyDots && e0 == null) {
- /* a parsing error occurred */
- e0 = dummyExpr;
- }
- Contract.Assert(anyDots || e0 != null);
- if (anyDots) {
- //Contract.Assert(e0 != null || e1 != null);
- e = new SeqSelectExpr(x, false, e, e0, e1);
- } else if (e1 == null) {
- Contract.Assert(e0 != null);
- e = new SeqSelectExpr(x, true, e, e0, null);
- } else {
- Contract.Assert(e0 != null);
- e = new SeqUpdateExpr(x, e, e0, e1);
- }
- }
- .)
- "]"
- )
- .
-/*------------------------------------------------------------------------*/
-QuantifierGuts<out Expression/*!*/ q>
-= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
- bool univ = false;
- List<BoundVar/*!*/> bvars;
- Attributes attrs;
- Expression range;
- Expression/*!*/ body;
- .)
- ( Forall (. x = t; univ = true; .)
- | Exists (. x = t; .)
- )
- QuantifierDomain<out bvars, out attrs, out range>
- QSep
- Expression<out body>
- (. if (univ) {
- q = new ForallExpr(x, bvars, range, body, attrs);
- } else {
- q = new ExistsExpr(x, bvars, range, body, attrs);
- }
- .)
- .
-
-Forall = "forall" | '\u2200'.
-Exists = "exists" | '\u2203'.
-QSep = "::" | '\u2022'.
-
-QuantifierDomain<.out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range.>
-= (.
- bvars = new List<BoundVar/*!*/>();
- BoundVar/*!*/ bv;
- attrs = null;
- range = null;
- .)
- IdentTypeOptional<out bv> (. bvars.Add(bv); .)
- { ","
- IdentTypeOptional<out bv> (. bvars.Add(bv); .)
- }
- { Attribute<ref attrs> }
- [ "|"
- Expression<out range>
- ]
- .
-
-ComprehensionExpr<out Expression/*!*/ q>
-= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
- IToken/*!*/ x = Token.NoToken;
- BoundVar/*!*/ bv;
- List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
- Expression/*!*/ range;
- Expression body = null;
- .)
- "set" (. x = t; .)
- IdentTypeOptional<out bv> (. bvars.Add(bv); .)
- { ","
- IdentTypeOptional<out bv> (. bvars.Add(bv); .)
- }
- "|" Expression<out range>
- [
- QSep
- Expression<out body>
- ]
- (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }
- q = new SetComprehension(x, bvars, range, body);
- .)
- .
-Expressions<.List<Expression/*!*/>/*!*/ args.>
-= (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)
- Expression<out e> (. args.Add(e); .)
- { "," Expression<out e> (. args.Add(e); .)
- }
- .
-/*------------------------------------------------------------------------*/
-Attribute<ref Attributes attrs>
-= "{"
- AttributeBody<ref attrs>
- "}"
- .
-AttributeBody<ref Attributes attrs>
-= (. string aName;
- List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
- Attributes.Argument/*!*/ aArg;
- .)
- ":" ident (. aName = t.val; .)
- [ AttributeArg<out aArg> (. aArgs.Add(aArg); .)
- { "," AttributeArg<out aArg> (. aArgs.Add(aArg); .)
- }
- ] (. attrs = new Attributes(aName, aArgs, attrs); .)
- .
-AttributeArg<out Attributes.Argument/*!*/ arg>
-= (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg; .)
- ( string (. arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); .)
- | Expression<out e> (. arg = new Attributes.Argument(t, e); .)
- )
- .
-/*------------------------------------------------------------------------*/
-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.StartsWith("_")) {
- SemErr("cannot declare identifier beginning with underscore");
- }
- .)
- .
-
-// Identifier, disallowing leading underscores, except possibly the "wildcard" identifier "_"
-WildIdent<out IToken/*!*/ x, bool allowWildcardId>
-= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
- ident (. x = t;
- if (x.val.StartsWith("_")) {
- if (allowWildcardId && x.val.Length == 1) {
- t.val = "_v" + anonymousIds++;
- } else {
- SemErr("cannot declare identifier beginning with underscore");
- }
- }
- .)
- .
-
-Nat<out BigInteger n>
-=
- digits
- (. try {
- n = BigInteger.Parse(t.val);
- } catch (System.FormatException) {
- SemErr("incorrectly formatted number");
- n = BigInteger.Zero;
- }
- .)
- .
-END Dafny.
|