diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 7 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 109 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 45 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 1373 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 18 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 24 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 366 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 38 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 19 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
13 files changed, 1152 insertions, 859 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 8e18f229..1069f419 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -668,6 +668,13 @@ function _System.array.Length(a: ref): int; axiom (forall o: ref :: 0 <= _System.array.Length(o));
// ---------------------------------------------------------------
+// -- Reals ------------------------------------------------------
+// ---------------------------------------------------------------
+
+function _System.Real.RealToInt(h: HeapType, x: real): int { int(x) }
+function _System.Real.IntToReal(h: HeapType, x: int): real { real(x) }
+
+// ---------------------------------------------------------------
// -- The heap ---------------------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 4a69e495..e81e5e67 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -206,6 +206,8 @@ namespace Microsoft.Dafny return new LiteralExpr(Tok(e.tok));
} else if (e.Value is bool) {
return new LiteralExpr(Tok(e.tok), (bool)e.Value);
+ } else if (e.Value is Basetypes.BigDec) {
+ return new LiteralExpr(Tok(e.tok), (Basetypes.BigDec)e.Value);
} else {
return new LiteralExpr(Tok(e.tok), (BigInteger)e.Value);
}
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index ad384895..4b57b1a4 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -869,6 +869,9 @@ namespace Microsoft.Dafny { return "bool";
} else if (type is IntType) {
return "BigInteger";
+ } else if (type is RealType) {
+ Error("compilation of real is not supported");
+ return "object";
} else if (type is ObjectType) {
return "object";
} else if (type.IsArrayType) {
@@ -967,6 +970,9 @@ namespace Microsoft.Dafny { return "false";
} else if (type is IntType) {
return "new BigInteger(0)";
+ } else if (type is RealType) {
+ Error("compilation of real is not supported");
+ return "null";
} else if (type.IsRefType) {
return string.Format("({0})null", TypeName(type));
} else if (type.IsDatatype) {
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5e84cb15..dc8b9640 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -163,8 +163,9 @@ TOKENS | 'a' 'r' 'r' 'a' 'y' idcharMinusPosDigit {idchar}
| 'a' 'r' 'r' 'a' 'y' posDigit {idchar} nondigit {idchar}.
digits = digit {digit}.
- hexdigits = '0' 'x' hexdigit {hexdigit}.
- arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].
+ hexdigits = "0x" hexdigit {hexdigit}.
+ decimaldigits = digit {digit} '.' digit {digit}.
+ arrayToken = "array" [posDigit {digit}].
string = quote {nonquote} quote.
colon = ':'.
semi = ';'.
@@ -274,9 +275,11 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule> .
QualifiedName<.out List<IToken> ids.>
-= (. IToken id; ids = new List<IToken>(); .)
- Ident<out id> (. ids.Add(id); .)
- { "." IdentOrDigits<out id> (. ids.Add(id); .)
+= (. IToken id; IToken idPrime; ids = new List<IToken>(); .)
+ Ident<out id> (. ids.Add(id); .)
+ { IdentOrDigitsSuffix<out id, out idPrime> (. ids.Add(id);
+ if (idPrime != null) { ids.Add(idPrime); }
+ .)
}
.
@@ -738,6 +741,7 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> ( "bool" (. tok = t; .)
| "nat" (. tok = t; ty = new NatType(); .)
| "int" (. tok = t; ty = new IntType(); .)
+ | "real" (. tok = t; ty = new RealType(); .)
| "set" (. tok = t; gt = new List<Type/*!*/>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("set type expects exactly one type argument");
@@ -787,7 +791,7 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty> { (. path.Add(tok); .)
"." Ident<out tok>
}
- [ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt, path); .)
+ [ GenericInstantiation<gt> ] (. ty = (tok.val == "real") ? (Type)Microsoft.Dafny.Type.Real : new UserDefinedType(tok, tok.val, gt, path); .)
)
.
GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
@@ -1809,13 +1813,14 @@ NegOp = "!" | '\u00ac'. */
ConstAtomExpression<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x; BigInteger n;
+ IToken/*!*/ x; BigInteger n; Basetypes.BigDec d;
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); .)
+ | Dec<out d> (. e = new LiteralExpr(t, d); .)
| "this" (. e = new ThisExpr(t); .)
| "fresh" (. x = t; .)
"(" Expression<out e, true> ")" (. e = new FreshExpr(x, e); .)
@@ -1827,6 +1832,22 @@ ConstAtomExpression<out Expression e> | "(" (. x = t; .)
Expression<out e, true> (. e = new ParensExpression(x, e); .)
")"
+ | "real" (. x = t; .)
+ "(" (. IToken openParen = t; .)
+ Expression<out e, true>
+ ")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
+ IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
+ .)
+ | "int" (. x = t; .)
+ "(" (. IToken openParen = t; .)
+ Expression<out e, true>
+ ")" (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
+ IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
+ .)
)
.
DisplayExpr<out Expression e>
@@ -2017,19 +2038,20 @@ CasePattern<out CasePattern pat> .
/*------------------------------------------------------------------------*/
DottedIdentifiersAndFunction<out Expression e>
-= (. IToken id; IToken openParen = null;
+= (. IToken id, idPrime; IToken openParen = null;
List<Expression> args = null;
List<IToken> idents = new List<IToken>();
.)
- Ident<out id> (. idents.Add(id); .)
- { "."
- IdentOrDigits<out id> (. idents.Add(id); .)
+ Ident<out id> (. idents.Add(id); .)
+ { IdentOrDigitsSuffix<out id, out idPrime> (. idents.Add(id);
+ if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
+ .)
}
- [ (. args = new List<Expression>(); .)
- [ "#" (. id.val = id.val + "#"; Expression k; .)
- "[" Expression<out k, true> "]" (. args.Add(k); .)
+ [ (. args = new List<Expression>(); .)
+ [ "#" (. id.val = id.val + "#"; Expression k; .)
+ "[" Expression<out k, true> "]" (. args.Add(k); .)
]
- "(" (. openParen = t; .)
+ "(" (. openParen = t; .)
[ Expressions<args> ]
")"
]
@@ -2041,8 +2063,12 @@ Suffix<ref Expression e> List<Expression> multipleIndices = null;
bool func = false;
.)
- ( "."
- IdentOrDigits<out id>
+ ( IdentOrDigitsSuffix<out id, out x> (. if (x != null) {
+ // process id as a Suffix in its own right
+ e = new ExprDotName(id, e, id.val);
+ id = x; // move to the next Suffix
+ }
+ .)
[ (. args = new List<Expression/*!*/>(); func = true; .)
[ "#" (. id.val = id.val + "#"; Expression k; .)
"[" Expression<out k, true> "]" (. args.Add(k); .)
@@ -2196,10 +2222,41 @@ Ident<out IToken/*!*/ x> ident (. x = t; .)
.
// Identifier or sequence of digits
-IdentOrDigits<out IToken/*!*/ x>
-= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; .)
- ( ident (. x = t; .)
+// Parse one of the following:
+// . ident
+// . digits
+// . digits . digits
+// In the first two cases, x returns as the token for the ident/digits and y returns as null.
+// In the third case, x and y return as the tokens for the first and second digits.
+// This parser production solves a problem where the scanner might parse a real number instead
+// of stopping at the decimal point.
+IdentOrDigitsSuffix<out IToken x, out IToken y>
+= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ x = Token.NoToken;
+ y = null;
+ .)
+ "."
+ ( ident (. x = t; .)
| digits (. x = t; .)
+ | decimaldigits (. x = t;
+ int exponent = x.val.IndexOf('e');
+ if (0 <= exponent) {
+ // this is not a legal field/destructor name
+ SemErr(x, "invalid IdentOrDigitsSuffix");
+ } else {
+ int dot = x.val.IndexOf('.');
+ if (0 <= dot) {
+ y = new Token();
+ y.pos = x.pos + dot + 1;
+ y.val = x.val.Substring(dot + 1);
+ x.val = x.val.Substring(0, dot);
+ y.col = x.col + dot + 1;
+ y.line = x.line;
+ y.filename = x.filename;
+ y.kind = x.kind;
+ }
+ }
+ .)
)
.
// Identifier, disallowing leading underscores
@@ -2247,4 +2304,16 @@ Nat<out BigInteger n> .)
)
.
+Dec<out Basetypes.BigDec d>
+= (. d = Basetypes.BigDec.ZERO; .)
+ (decimaldigits
+ (. try {
+ d = Basetypes.BigDec.FromString(t.val);
+ } catch (System.FormatException) {
+ SemErr("incorrectly formatted number");
+ d = Basetypes.BigDec.ZERO;
+ }
+ .)
+ )
+ .
END Dafny.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 0e023cab..ba05d6a8 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -71,12 +71,31 @@ namespace Microsoft.Dafny { public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true);
Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();
public readonly ClassDecl ObjectDecl;
+ public readonly ClassDecl RealClass;
+ //public readonly Function RealToInt;
+ //public readonly Function IntToReal;
public BuiltIns() {
// create class 'object'
ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), null);
SystemModule.TopLevelDecls.Add(ObjectDecl);
// add one-dimensional arrays, since they may arise during type checking
UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);
+ // add real number functions
+ Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List<TypeParameter>(), Token.NoToken,
+ new List<Formal> { new Formal(Token.NoToken, "x", Type.Real, true, true) }, Type.Int, new List<Expression>(),
+ new List<FrameExpression>(), new List<Expression>(), new Specification<Expression>(new List<Expression>(), null),
+ null, null, Token.NoToken);
+ Function IntToReal = new Function(Token.NoToken, "IntToReal", true, true, new List<TypeParameter>(), Token.NoToken,
+ new List<Formal> { new Formal(Token.NoToken, "x", Type.Int, true, true) }, Type.Real, new List<Expression>(),
+ new List<FrameExpression>(), new List<Expression>(), new Specification<Expression>(new List<Expression>(), null),
+ null, null, Token.NoToken);
+ RealClass = new ClassDecl(Token.NoToken, "Real", SystemModule, new List<TypeParameter>(),
+ new List<MemberDecl>() { RealToInt, IntToReal }, null);
+ RealToInt.EnclosingClass = RealClass;
+ IntToReal.EnclosingClass = RealClass;
+ RealToInt.IsBuiltin = true;
+ IntToReal.IsBuiltin = true;
+ SystemModule.TopLevelDecls.Add(RealClass);
}
public UserDefinedType ArrayType(int dims, Type arg) {
@@ -227,6 +246,7 @@ namespace Microsoft.Dafny { public abstract class Type {
public static readonly BoolType Bool = new BoolType();
public static readonly IntType Int = new IntType();
+ public static readonly RealType Real = new RealType();
/// <summary>
/// Used in error situations in order to reduce further error messages.
/// </summary>
@@ -404,6 +424,16 @@ namespace Microsoft.Dafny { }
}
+ public class RealType : BasicType {
+ [Pure]
+ public override string TypeName(ModuleDefinition context) {
+ return "real";
+ }
+ public override bool Equals(Type that) {
+ return that.Normalize() is RealType;
+ }
+ }
+
public class ObjectType : BasicType
{
[Pure]
@@ -803,9 +833,9 @@ namespace Microsoft.Dafny { /// <summary>
/// This proxy stands for either:
- /// int or set or multiset or seq
+ /// int or real or set or multiset or seq
/// if AllowSeq, or:
- /// int or set or multiset
+ /// int or real or set or multiset
/// if !AllowSeq.
/// </summary>
public class OperationTypeProxy : RestrictedTypeProxy {
@@ -1973,6 +2003,7 @@ namespace Microsoft.Dafny { public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } } // is "false" for all Function objects that survive into resolution
public readonly IToken SignatureEllipsis;
+ public bool IsBuiltin;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TypeArgs));
@@ -4246,6 +4277,14 @@ namespace Microsoft.Dafny { this.Value = n;
}
+ public LiteralExpr(IToken tok, Basetypes.BigDec n)
+ : base(tok) {
+ Contract.Requires(0 <= n.Mantissa.Sign);
+ Contract.Requires(tok != null);
+
+ this.Value = n;
+ }
+
public LiteralExpr(IToken tok, int n) :base(tok){
Contract.Requires(tok != null);
Contract.Requires(0 <= n);
@@ -4259,7 +4298,7 @@ namespace Microsoft.Dafny { this.Value = b;
}
}
-
+
public class DatatypeValue : Expression {
public readonly string DatatypeName;
public readonly string MemberName;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 6e59a2df..07211134 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -17,16 +17,17 @@ public class Parser { public const int _ident = 1;
public const int _digits = 2;
public const int _hexdigits = 3;
- public const int _arrayToken = 4;
- public const int _string = 5;
- public const int _colon = 6;
- public const int _semi = 7;
- public const int _lbrace = 8;
- public const int _rbrace = 9;
- public const int _openparen = 10;
- public const int _star = 11;
- public const int _notIn = 12;
- public const int maxT = 123;
+ public const int _decimaldigits = 4;
+ public const int _arrayToken = 5;
+ public const int _string = 6;
+ public const int _colon = 7;
+ public const int _semi = 8;
+ public const int _lbrace = 9;
+ public const int _rbrace = 10;
+ public const int _openparen = 11;
+ public const int _star = 12;
+ public const int _notIn = 13;
+ public const int maxT = 125;
const bool T = true;
const bool x = false;
@@ -235,9 +236,9 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
Contract.Assert(defaultModule != null);
- while (la.kind == 13) {
+ while (la.kind == 14) {
Get();
- Expect(5);
+ Expect(6);
{
string parsedFile = t.filename;
string includedFile = t.val.Substring(1, t.val.Length - 2);
@@ -251,7 +252,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
while (StartOf(1)) {
switch (la.kind) {
- case 14: case 15: case 17: {
+ case 15: case 16: case 18: {
SubModuleDecl(defaultModule, out submodule);
defaultModule.TopLevelDecls.Add(submodule);
break;
@@ -276,7 +277,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { defaultModule.TopLevelDecls.Add(iter);
break;
}
- case 24: case 25: case 29: case 40: case 41: case 42: case 43: case 44: case 60: case 61: case 62: {
+ case 24: case 25: case 29: case 40: case 41: case 42: case 43: case 44: case 62: case 63: case 64: {
ClassMemberDecl(membersDefaultClass, false);
break;
}
@@ -308,26 +309,26 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { bool isAbstract = false;
bool opened = false;
- if (la.kind == 14 || la.kind == 15) {
- if (la.kind == 14) {
+ if (la.kind == 15 || la.kind == 16) {
+ if (la.kind == 15) {
Get();
isAbstract = true;
}
- Expect(15);
- while (la.kind == 8) {
+ Expect(16);
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 16) {
+ if (la.kind == 17) {
Get();
QualifiedName(out idRefined);
}
module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false);
- Expect(8);
+ Expect(9);
module.BodyStartTok = t;
while (StartOf(1)) {
switch (la.kind) {
- case 14: case 15: case 17: {
+ case 15: case 16: case 18: {
SubModuleDecl(module, out sm);
module.TopLevelDecls.Add(sm);
break;
@@ -352,40 +353,40 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { module.TopLevelDecls.Add(iter);
break;
}
- case 24: case 25: case 29: case 40: case 41: case 42: case 43: case 44: case 60: case 61: case 62: {
+ case 24: case 25: case 29: case 40: case 41: case 42: case 43: case 44: case 62: case 63: case 64: {
ClassMemberDecl(namedModuleDefaultClassMembers, false);
break;
}
}
}
- Expect(9);
+ Expect(10);
module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
submodule = new LiteralModuleDecl(module, parent);
- } else if (la.kind == 17) {
+ } else if (la.kind == 18) {
Get();
- if (la.kind == 18) {
+ if (la.kind == 19) {
Get();
opened = true;
}
NoUSIdent(out id);
- if (la.kind == 19 || la.kind == 20) {
- if (la.kind == 19) {
+ if (la.kind == 20 || la.kind == 21) {
+ if (la.kind == 20) {
Get();
QualifiedName(out idPath);
submodule = new AliasModuleDecl(idPath, id, parent, opened);
} else {
Get();
QualifiedName(out idPath);
- if (la.kind == 21) {
+ if (la.kind == 22) {
Get();
QualifiedName(out idAssignment);
}
submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened);
}
}
- if (la.kind == 7) {
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(124); Get();}
+ if (la.kind == 8) {
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(126); Get();}
Get();
}
if (submodule == null) {
@@ -394,7 +395,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { submodule = new AliasModuleDecl(idPath, id, parent, opened);
}
- } else SynErr(125);
+ } else SynErr(127);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
@@ -406,21 +407,21 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 23)) {SynErr(126); Get();}
+ while (!(la.kind == 0 || la.kind == 23)) {SynErr(128); Get();}
Expect(23);
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 38) {
GenericParameters(typeArgs);
}
- Expect(8);
+ Expect(9);
bodyStart = t;
while (StartOf(2)) {
ClassMemberDecl(members, true);
}
- Expect(9);
+ Expect(10);
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
@@ -437,29 +438,29 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 26 || la.kind == 27)) {SynErr(127); Get();}
+ while (!(la.kind == 0 || la.kind == 26 || la.kind == 27)) {SynErr(129); Get();}
if (la.kind == 26) {
Get();
} else if (la.kind == 27) {
Get();
co = true;
- } else SynErr(128);
- while (la.kind == 8) {
+ } else SynErr(130);
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
if (la.kind == 38) {
GenericParameters(typeArgs);
}
- Expect(19);
+ Expect(20);
bodyStart = t;
DatatypeMemberDecl(ctors);
while (la.kind == 28) {
Get();
DatatypeMemberDecl(ctors);
}
- if (la.kind == 7) {
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(129); Get();}
+ if (la.kind == 8) {
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(131); Get();}
Get();
}
if (co) {
@@ -478,19 +479,19 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
Expect(31);
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
Expect(32);
Expect(33);
eqSupport = TypeParameter.EqualitySupportValue.Required;
}
at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
- if (la.kind == 7) {
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(130); Get();}
+ if (la.kind == 8) {
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(132); Get();}
Get();
}
}
@@ -519,13 +520,13 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 34)) {SynErr(131); Get();}
+ while (!(la.kind == 0 || la.kind == 34)) {SynErr(133); Get();}
Expect(34);
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 10 || la.kind == 38) {
+ if (la.kind == 11 || la.kind == 38) {
if (la.kind == 38) {
GenericParameters(typeArgs);
}
@@ -542,11 +543,11 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { } else if (la.kind == 37) {
Get();
signatureEllipsis = t; openParen = Token.NoToken;
- } else SynErr(132);
+ } else SynErr(134);
while (StartOf(3)) {
IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);
}
- if (la.kind == 8) {
+ if (la.kind == 9) {
BlockStmt(out body, out bodyStart, out bodyEnd);
}
iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
@@ -577,19 +578,19 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
if (la.kind == 29) {
FieldDecl(mmod, mm);
- } else if (la.kind == 60 || la.kind == 61 || la.kind == 62) {
+ } else if (la.kind == 62 || la.kind == 63 || la.kind == 64) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (StartOf(4)) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(133);
+ } else SynErr(135);
}
void Attribute(ref Attributes attrs) {
- Expect(8);
- AttributeBody(ref attrs);
Expect(9);
+ AttributeBody(ref attrs);
+ Expect(10);
}
void NoUSIdent(out IToken/*!*/ x) {
@@ -603,13 +604,14 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
void QualifiedName(out List<IToken> ids) {
- IToken id; ids = new List<IToken>();
+ IToken id; IToken idPrime; ids = new List<IToken>();
Ident(out id);
ids.Add(id);
- while (la.kind == 22) {
- Get();
- IdentOrDigits(out id);
- ids.Add(id);
+ while (la.kind == 61) {
+ IdentOrDigitsSuffix(out id, out idPrime);
+ ids.Add(id);
+ if (idPrime != null) { ids.Add(idPrime); }
+
}
}
@@ -619,15 +621,40 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { x = t;
}
- void IdentOrDigits(out IToken/*!*/ x) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;
+ void IdentOrDigitsSuffix(out IToken x, out IToken y) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ x = Token.NoToken;
+ y = null;
+
+ Expect(61);
if (la.kind == 1) {
Get();
x = t;
} else if (la.kind == 2) {
Get();
x = t;
- } else SynErr(134);
+ } else if (la.kind == 4) {
+ Get();
+ x = t;
+ int exponent = x.val.IndexOf('e');
+ if (0 <= exponent) {
+ // this is not a legal field/destructor name
+ SemErr(x, "invalid IdentOrDigitsSuffix");
+ } else {
+ int dot = x.val.IndexOf('.');
+ if (0 <= dot) {
+ y = new Token();
+ y.pos = x.pos + dot + 1;
+ y.val = x.val.Substring(dot + 1);
+ x.val = x.val.Substring(0, dot);
+ y.col = x.col + dot + 1;
+ y.line = x.line;
+ y.filename = x.filename;
+ y.kind = x.kind;
+ }
+ }
+
+ } else SynErr(136);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -638,7 +665,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Expect(38);
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
Expect(32);
Expect(33);
@@ -649,7 +676,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Get();
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
Expect(32);
Expect(33);
@@ -665,11 +692,11 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 29)) {SynErr(135); Get();}
+ while (!(la.kind == 0 || la.kind == 29)) {SynErr(137); Get();}
Expect(29);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
FIdentType(out id, out ty);
@@ -679,8 +706,8 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { FIdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(136); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(138); Get();}
+ Expect(8);
}
void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {
@@ -702,7 +729,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { IToken bodyEnd = Token.NoToken;
IToken signatureEllipsis = null;
- if (la.kind == 60) {
+ if (la.kind == 62) {
Get();
if (la.kind == 40) {
Get();
@@ -710,23 +737,23 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 10 || la.kind == 38) {
+ if (la.kind == 11 || la.kind == 38) {
if (la.kind == 38) {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals, out openParen);
- Expect(6);
+ Expect(7);
Type(out returnType);
} else if (la.kind == 37) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(137);
- } else if (la.kind == 61) {
+ } else SynErr(139);
+ } else if (la.kind == 63) {
Get();
isPredicate = true;
if (la.kind == 40) {
@@ -735,7 +762,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
@@ -743,9 +770,9 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { if (la.kind == 38) {
GenericParameters(typeArgs);
}
- if (la.kind == 10) {
+ if (la.kind == 11) {
Formals(true, isFunctionMethod, formals, out openParen);
- if (la.kind == 6) {
+ if (la.kind == 7) {
Get();
SemErr(t, "predicates do not have an explicitly declared return type; it is always bool");
}
@@ -754,13 +781,13 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(138);
- } else if (la.kind == 62) {
+ } else SynErr(140);
+ } else if (la.kind == 64) {
Get();
isCoPredicate = true;
if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
@@ -768,9 +795,9 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { if (la.kind == 38) {
GenericParameters(typeArgs);
}
- if (la.kind == 10) {
+ if (la.kind == 11) {
Formals(true, isFunctionMethod, formals, out openParen);
- if (la.kind == 6) {
+ if (la.kind == 7) {
Get();
SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool");
}
@@ -779,13 +806,13 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(139);
- } else SynErr(140);
+ } else SynErr(141);
+ } else SynErr(142);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(6)) {
FunctionSpec(reqs, reads, ens, decreases);
}
- if (la.kind == 8) {
+ if (la.kind == 9) {
FunctionBody(out body, out bodyStart, out bodyEnd);
}
if (!theVerifyThisFile) { // We still need the func bodies, but don't bother verifying their correctness
@@ -838,7 +865,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(StartOf(7))) {SynErr(141); Get();}
+ while (!(StartOf(7))) {SynErr(143); Get();}
if (la.kind == 40) {
Get();
} else if (la.kind == 41) {
@@ -858,7 +885,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(142);
+ } else SynErr(144);
keywordToken = t;
if (isLemma) {
if (mmod.IsGhost) {
@@ -877,7 +904,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
}
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
if (la.kind == 1) {
@@ -891,7 +918,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
}
- if (la.kind == 10 || la.kind == 38) {
+ if (la.kind == 11 || la.kind == 38) {
if (la.kind == 38) {
GenericParameters(typeArgs);
}
@@ -904,11 +931,11 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { } else if (la.kind == 37) {
Get();
signatureEllipsis = t; openParen = Token.NoToken;
- } else SynErr(143);
+ } else SynErr(145);
while (StartOf(8)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
- if (la.kind == 8) {
+ if (la.kind == 9) {
BlockStmt(out body, out bodyStart, out bodyEnd);
}
if (!theVerifyThisFile) {
@@ -953,11 +980,11 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { IToken/*!*/ id;
List<Formal/*!*/> formals = new List<Formal/*!*/>();
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 10) {
+ if (la.kind == 11) {
FormalsOptionalIds(formals);
}
ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
@@ -965,7 +992,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
- Expect(10);
+ Expect(11);
if (StartOf(9)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
@@ -987,8 +1014,8 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { } else if (la.kind == 2) {
Get();
id = t;
- } else SynErr(144);
- Expect(6);
+ } else SynErr(146);
+ Expect(7);
Type(out ty);
}
@@ -1006,7 +1033,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { void 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);
- Expect(6);
+ Expect(7);
Type(out ty);
}
@@ -1033,7 +1060,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { IToken id; Type ty; Type optType = null;
WildIdent(out id, true);
- if (la.kind == 6) {
+ if (la.kind == 7) {
Get();
Type(out ty);
optType = ty;
@@ -1046,7 +1073,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { IToken id; Type ty; Type optType = null;
WildIdent(out id, true);
- if (la.kind == 6) {
+ if (la.kind == 7) {
Get();
Type(out ty);
optType = ty;
@@ -1065,7 +1092,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
if (StartOf(10)) {
TypeAndToken(out id, out ty);
- if (la.kind == 6) {
+ if (la.kind == 7) {
Get();
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
@@ -1079,9 +1106,9 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { } else if (la.kind == 2) {
Get();
id = t; name = id.val;
- Expect(6);
+ Expect(7);
Type(out ty);
- } else SynErr(145);
+ } else SynErr(147);
if (name != null) {
identName = name;
} else {
@@ -1112,6 +1139,11 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { }
case 55: {
Get();
+ tok = t; ty = new RealType();
+ break;
+ }
+ case 56: {
+ Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
if (gt.Count != 1) {
@@ -1121,7 +1153,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { break;
}
- case 56: {
+ case 57: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -1132,7 +1164,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { break;
}
- case 57: {
+ case 58: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -1143,7 +1175,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { break;
}
- case 58: {
+ case 59: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -1154,17 +1186,17 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { break;
}
- case 1: case 4: case 59: {
+ case 1: case 5: case 60: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(146); break;
+ default: SynErr(148); break;
}
}
void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
- Expect(10);
+ Expect(11);
openParen = t;
if (la.kind == 1 || la.kind == 24) {
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
@@ -1184,7 +1216,7 @@ List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!* ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
- while (!(StartOf(11))) {SynErr(147); Get();}
+ while (!(StartOf(11))) {SynErr(149); Get();}
if (la.kind == 50) {
Get();
while (IsAttribute()) {
@@ -1199,8 +1231,8 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(148); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(150); Get();}
+ Expect(8);
} else if (la.kind == 45) {
Get();
while (IsAttribute()) {
@@ -1215,8 +1247,8 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(149); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(151); Get();}
+ Expect(8);
} else if (StartOf(13)) {
if (la.kind == 46) {
Get();
@@ -1229,8 +1261,8 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { if (la.kind == 47) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(150); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(152); Get();}
+ Expect(8);
if (isYield) {
yieldReq.Add(new MaybeFreeExpression(e, isFree));
} else {
@@ -1243,36 +1275,36 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Attribute(ref ensAttrs);
}
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(151); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(153); Get();}
+ Expect(8);
if (isYield) {
yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
} else {
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
- } else SynErr(152);
+ } else SynErr(154);
} else if (la.kind == 49) {
Get();
while (IsAttribute()) {
Attribute(ref decrAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(153); Get();}
- Expect(7);
- } else SynErr(154);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(155); Get();}
+ Expect(8);
+ } else SynErr(156);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(8);
+ Expect(9);
bodyStart = t;
while (StartOf(14)) {
Stmt(body);
}
- Expect(9);
+ Expect(10);
bodyEnd = t;
block = new BlockStmt(bodyStart, bodyEnd, body);
}
@@ -1282,7 +1314,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo 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;
- while (!(StartOf(15))) {SynErr(155); Get();}
+ while (!(StartOf(15))) {SynErr(157); Get();}
if (la.kind == 45) {
Get();
while (IsAttribute()) {
@@ -1297,8 +1329,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(156); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(158); Get();}
+ Expect(8);
} else if (la.kind == 46 || la.kind == 47 || la.kind == 48) {
if (la.kind == 46) {
Get();
@@ -1307,8 +1339,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 47) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(157); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(159); Get();}
+ Expect(8);
req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 48) {
Get();
@@ -1316,19 +1348,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref ensAttrs);
}
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(158); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(160); Get();}
+ Expect(8);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(159);
+ } else SynErr(161);
} else if (la.kind == 49) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(160); Get();}
- Expect(7);
- } else SynErr(161);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(162); Get();}
+ Expect(8);
+ } else SynErr(163);
}
void FrameExpression(out FrameExpression/*!*/ fe) {
@@ -1341,25 +1373,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(16)) {
Expression(out e, false);
feTok = e.tok;
- if (la.kind == 63) {
+ if (la.kind == 65) {
Get();
Ident(out id);
fieldName = id.val; feTok = id;
}
fe = new FrameExpression(feTok, e, fieldName);
- } else if (la.kind == 63) {
+ } else if (la.kind == 65) {
Get();
Ident(out id);
fieldName = id.val;
fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName);
- } else SynErr(162);
+ } else SynErr(164);
}
void Expression(out Expression e, bool allowSemi) {
Expression e0; IToken endTok;
EquivExpression(out e, allowSemi);
if (SemiFollowsCall(allowSemi, e)) {
- Expect(7);
+ Expect(8);
endTok = t;
Expression(out e0, allowSemi);
e = new StmtExpr(e.tok,
@@ -1409,10 +1441,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Type/*!*/>/*!*/ gt;
List<IToken> path;
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
tok = t; ty = new ObjectType();
- } else if (la.kind == 4) {
+ } else if (la.kind == 5) {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -1429,7 +1461,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out tok);
gt = new List<Type/*!*/>();
path = new List<IToken>();
- while (la.kind == 22) {
+ while (la.kind == 61) {
path.Add(tok);
Get();
Ident(out tok);
@@ -1437,8 +1469,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 38) {
GenericInstantiation(gt);
}
- ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(163);
+ ty = (tok.val == "real") ? (Type)Microsoft.Dafny.Type.Real : new UserDefinedType(tok, tok.val, gt, path);
+ } else SynErr(165);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1447,11 +1479,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 47) {
- while (!(la.kind == 0 || la.kind == 47)) {SynErr(164); Get();}
+ while (!(la.kind == 0 || la.kind == 47)) {SynErr(166); Get();}
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(165); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(167); Get();}
+ Expect(8);
reqs.Add(e);
} else if (la.kind == 50) {
Get();
@@ -1464,13 +1496,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(166); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(168); Get();}
+ Expect(8);
} else if (la.kind == 48) {
Get();
Expression(out e, false);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(167); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(169); Get();}
+ Expect(8);
ens.Add(e);
} else if (la.kind == 49) {
Get();
@@ -1480,39 +1512,39 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(168); Get();}
- Expect(7);
- } else SynErr(169);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(170); Get();}
+ Expect(8);
+ } else SynErr(171);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
- Expect(8);
+ Expect(9);
bodyStart = t;
Expression(out e, true);
- Expect(9);
+ Expect(10);
bodyEnd = t;
}
void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
fe = new FrameExpression(t, new WildcardExpr(t), null);
} else if (StartOf(12)) {
FrameExpression(out fe);
- } else SynErr(170);
+ } else SynErr(172);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(16)) {
Expression(out e, false);
- } else SynErr(171);
+ } else SynErr(173);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1529,26 +1561,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(18))) {SynErr(172); Get();}
+ while (!(StartOf(18))) {SynErr(174); Get();}
switch (la.kind) {
- case 8: {
+ case 9: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
s = bs;
break;
}
- case 81: {
+ case 83: {
AssertStmt(out s);
break;
}
- case 70: {
+ case 72: {
AssumeStmt(out s);
break;
}
- case 82: {
+ case 84: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 3: case 10: case 28: case 110: case 111: case 112: case 113: case 114: case 115: {
+ case 1: case 2: case 3: case 4: case 11: case 28: case 54: case 55: case 112: case 113: case 114: case 115: case 116: case 117: {
UpdateStmt(out s);
break;
}
@@ -1556,53 +1588,53 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s);
break;
}
- case 74: {
+ case 76: {
IfStmt(out s);
break;
}
- case 78: {
+ case 80: {
WhileStmt(out s);
break;
}
- case 80: {
+ case 82: {
MatchStmt(out s);
break;
}
- case 83: case 84: {
+ case 85: case 86: {
ForallStmt(out s);
break;
}
- case 85: {
+ case 87: {
CalcStmt(out s);
break;
}
- case 64: {
+ case 66: {
Get();
x = t;
NoUSIdent(out id);
- Expect(6);
+ Expect(7);
OneStmt(out s);
s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 65: {
+ case 67: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
NoUSIdent(out id);
label = id.val;
- } else if (la.kind == 7 || la.kind == 65) {
- while (la.kind == 65) {
+ } else if (la.kind == 8 || la.kind == 67) {
+ while (la.kind == 67) {
Get();
breakCount++;
}
- } else SynErr(173);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(174); Get();}
- Expect(7);
+ } else SynErr(175);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(176); Get();}
+ Expect(8);
s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount);
break;
}
- case 51: case 68: {
+ case 51: case 70: {
ReturnStmt(out s);
break;
}
@@ -1610,7 +1642,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo SkeletonStmt(out s);
break;
}
- default: SynErr(175); break;
+ default: SynErr(177); break;
}
}
@@ -1619,7 +1651,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e = null; Attributes attrs = null;
IToken dotdotdot = null;
- Expect(81);
+ Expect(83);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -1629,8 +1661,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 37) {
Get();
dotdotdot = t;
- } else SynErr(176);
- Expect(7);
+ } else SynErr(178);
+ Expect(8);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
} else {
@@ -1644,7 +1676,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e = null; Attributes attrs = null;
IToken dotdotdot = null;
- Expect(70);
+ Expect(72);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -1654,8 +1686,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 37) {
Get();
dotdotdot = t;
- } else SynErr(177);
- Expect(7);
+ } else SynErr(179);
+ Expect(8);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
} else {
@@ -1668,7 +1700,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(82);
+ Expect(84);
x = t;
AttributeArg(out arg, false);
args.Add(arg);
@@ -1677,7 +1709,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AttributeArg(out arg, false);
args.Add(arg);
}
- Expect(7);
+ Expect(8);
s = new PrintStmt(x, t, args);
}
@@ -1693,20 +1725,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Lhs(out e);
x = e.tok;
- if (la.kind == 7 || la.kind == 8) {
- while (la.kind == 8) {
+ if (la.kind == 8 || la.kind == 9) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
- Expect(7);
+ Expect(8);
endTok = t; rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 30 || la.kind == 67 || la.kind == 69) {
+ } else if (la.kind == 30 || la.kind == 69 || la.kind == 71) {
lhss.Add(e); lhs0 = e;
while (la.kind == 30) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 67) {
+ if (la.kind == 69) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1716,21 +1748,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 69) {
+ } else if (la.kind == 71) {
Get();
x = t;
- if (la.kind == 70) {
+ if (la.kind == 72) {
Get();
suchThatAssume = t;
}
Expression(out suchThat, false);
- } else SynErr(178);
- Expect(7);
+ } else SynErr(180);
+ Expect(8);
endTok = t;
- } else if (la.kind == 6) {
+ } else if (la.kind == 7) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(179);
+ } else SynErr(181);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
} else {
@@ -1760,21 +1792,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(29);
if (!isGhost) { x = t; }
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d); d.Attributes = attrs; attrs = null;
while (la.kind == 30) {
Get();
- while (la.kind == 8) {
+ while (la.kind == 9) {
Attribute(ref attrs);
}
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d); d.Attributes = attrs; attrs = null;
}
- if (la.kind == 67 || la.kind == 69) {
- if (la.kind == 67) {
+ if (la.kind == 69 || la.kind == 71) {
+ if (la.kind == 69) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1790,14 +1822,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else {
Get();
assignTok = t;
- if (la.kind == 70) {
+ if (la.kind == 72) {
Get();
suchThatAssume = t;
}
Expression(out suchThat, false);
}
}
- Expect(7);
+ Expect(8);
endTok = t;
ConcreteUpdateStatement update;
if (suchThat != null) {
@@ -1830,7 +1862,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(74);
+ Expect(76);
x = t;
if (IsAlternative()) {
AlternativeBlock(out alternatives, out endTok);
@@ -1844,15 +1876,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
BlockStmt(out thn, out bodyStart, out bodyEnd);
endTok = thn.EndTok;
- if (la.kind == 75) {
+ if (la.kind == 77) {
Get();
- if (la.kind == 74) {
+ if (la.kind == 76) {
IfStmt(out s);
els = s; endTok = s.EndTok;
- } else if (la.kind == 8) {
+ } else if (la.kind == 9) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs; endTok = bs.EndTok;
- } else SynErr(180);
+ } else SynErr(182);
}
if (guardEllipsis != null) {
ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);
@@ -1860,7 +1892,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ifStmt = new IfStmt(x, endTok, guard, thn, els);
}
- } else SynErr(181);
+ } else SynErr(183);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1876,7 +1908,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(78);
+ Expect(80);
x = t;
if (IsLoopSpecOrAlternative()) {
LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
@@ -1891,13 +1923,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo guardEllipsis = t;
}
LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
- if (la.kind == 8) {
+ if (la.kind == 9) {
BlockStmt(out body, out bodyStart, out bodyEnd);
endTok = body.EndTok;
} else if (la.kind == 37) {
Get();
bodyEllipsis = t; endTok = t;
- } else SynErr(182);
+ } else SynErr(184);
if (guardEllipsis != null || bodyEllipsis != null) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1913,22 +1945,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
- } else SynErr(183);
+ } else SynErr(185);
}
void MatchStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(80);
+ Expect(82);
x = t;
Expression(out e, true);
- Expect(8);
- while (la.kind == 76) {
+ Expect(9);
+ while (la.kind == 78) {
CaseStatement(out c);
cases.Add(c);
}
- Expect(9);
+ Expect(10);
s = new MatchStmt(x, t, e, cases);
}
@@ -1945,16 +1977,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
- if (la.kind == 83) {
+ if (la.kind == 85) {
Get();
x = t;
- } else if (la.kind == 84) {
+ } else if (la.kind == 86) {
Get();
x = t;
errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
- } else SynErr(184);
- if (la.kind == 10) {
+ } else SynErr(186);
+ if (la.kind == 11) {
Get();
usesOptionalParen = true;
}
@@ -1970,9 +2002,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 33) {
Get();
if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); }
- } else if (la.kind == 8 || la.kind == 46 || la.kind == 48) {
+ } else if (la.kind == 9 || la.kind == 46 || la.kind == 48) {
if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
- } else SynErr(185);
+ } else SynErr(187);
while (la.kind == 46 || la.kind == 48) {
isFree = false;
if (la.kind == 46) {
@@ -1981,7 +2013,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(48);
Expression(out e, false);
- Expect(7);
+ Expect(8);
ens.Add(new MaybeFreeExpression(e, isFree));
}
BlockStmt(out block, out bodyStart, out bodyEnd);
@@ -2002,7 +2034,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken opTok;
IToken danglingOperator = null;
- Expect(85);
+ Expect(87);
x = t;
if (StartOf(21)) {
CalcOp(out opTok, out calcOp);
@@ -2013,11 +2045,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo resOp = calcOp;
}
- Expect(8);
+ Expect(9);
while (StartOf(16)) {
Expression(out e, false);
lines.Add(e); stepOp = calcOp; danglingOperator = null;
- Expect(7);
+ Expect(8);
if (StartOf(21)) {
CalcOp(out opTok, out op);
maybeOp = resOp.ResultOp(op);
@@ -2036,7 +2068,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (h.Body.Count != 0) { danglingOperator = null; }
}
- Expect(9);
+ Expect(10);
if (danglingOperator != null) {
SemErr(danglingOperator, "a calculation cannot end with an operator");
}
@@ -2054,13 +2086,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssignmentRhs r;
bool isYield = false;
- if (la.kind == 68) {
+ if (la.kind == 70) {
Get();
returnTok = t;
} else if (la.kind == 51) {
Get();
returnTok = t; isYield = true;
- } else SynErr(186);
+ } else SynErr(188);
if (StartOf(22)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
@@ -2070,7 +2102,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo rhss.Add(r);
}
}
- Expect(7);
+ Expect(8);
if (isYield) {
s = new YieldStmt(returnTok, t, rhss);
} else {
@@ -2086,7 +2118,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e;
Expect(37);
dotdotdot = t;
- if (la.kind == 66) {
+ if (la.kind == 68) {
Get();
names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
Ident(out tok);
@@ -2096,7 +2128,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out tok);
names.Add(tok);
}
- Expect(67);
+ Expect(69);
Expression(out e, false);
exprs.Add(e);
while (la.kind == 30) {
@@ -2110,7 +2142,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- Expect(7);
+ Expect(8);
s = new SkeletonStatement(dotdotdot, t, names, exprs);
}
@@ -2123,25 +2155,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = dummyRhs; // to please compiler
Attributes attrs = null;
- if (la.kind == 71) {
+ if (la.kind == 73) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 10 || la.kind == 22 || la.kind == 72) {
- if (la.kind == 72) {
+ if (la.kind == 11 || la.kind == 61 || la.kind == 74) {
+ if (la.kind == 74) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(73);
+ Expect(75);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else {
x = null; args = new List<Expression/*!*/>();
- if (la.kind == 22) {
+ if (la.kind == 61) {
Get();
Ident(out x);
}
- Expect(10);
+ Expect(11);
if (StartOf(16)) {
Expressions(args);
}
@@ -2156,14 +2188,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty);
}
- } else if (la.kind == 11) {
+ } else if (la.kind == 12) {
Get();
r = new HavocRhs(t);
} else if (StartOf(16)) {
Expression(out e, false);
r = new ExprRhs(e);
- } else SynErr(187);
- while (la.kind == 8) {
+ } else SynErr(189);
+ while (la.kind == 9) {
Attribute(ref attrs);
}
r.Attributes = attrs;
@@ -2174,16 +2206,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 22 || la.kind == 72) {
+ while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
} else if (StartOf(23)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 22 || la.kind == 72) {
+ while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
- } else SynErr(188);
+ } else SynErr(190);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -2203,36 +2235,36 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e;
List<Statement> body;
- Expect(8);
- while (la.kind == 76) {
+ Expect(9);
+ while (la.kind == 78) {
Get();
x = t;
Expression(out e, true);
- Expect(77);
+ Expect(79);
body = new List<Statement>();
while (StartOf(14)) {
Stmt(body);
}
alternatives.Add(new GuardedAlternative(x, e, body));
}
- Expect(9);
+ Expect(10);
endTok = t;
}
void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
e = null;
} else if (IsParenStar()) {
- Expect(10);
Expect(11);
+ Expect(12);
Expect(33);
e = null;
} else if (StartOf(16)) {
Expression(out ee, true);
e = ee;
- } else SynErr(189);
+ } else SynErr(191);
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2243,22 +2275,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null;
while (StartOf(24)) {
- if (la.kind == 46 || la.kind == 79) {
+ if (la.kind == 46 || la.kind == 81) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(190); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(192); Get();}
+ Expect(8);
invariants.Add(invariant);
} else if (la.kind == 49) {
- while (!(la.kind == 0 || la.kind == 49)) {SynErr(191); Get();}
+ while (!(la.kind == 0 || la.kind == 49)) {SynErr(193); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(192); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(194); Get();}
+ Expect(8);
} else {
- while (!(la.kind == 0 || la.kind == 45)) {SynErr(193); Get();}
+ while (!(la.kind == 0 || la.kind == 45)) {SynErr(195); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -2273,20 +2305,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 7)) {SynErr(194); Get();}
- Expect(7);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(196); Get();}
+ Expect(8);
}
}
}
void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 46 || la.kind == 79)) {SynErr(195); Get();}
+ while (!(la.kind == 0 || la.kind == 46 || la.kind == 81)) {SynErr(197); Get();}
if (la.kind == 46) {
Get();
isFree = true;
}
- Expect(79);
+ Expect(81);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -2301,10 +2333,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(76);
+ Expect(78);
x = t;
Ident(out id);
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
@@ -2315,7 +2347,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(33);
}
- Expect(77);
+ Expect(79);
while (StartOf(14)) {
Stmt(body);
}
@@ -2324,13 +2356,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void AttributeArg(out Attributes.Argument arg, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg;
- if (la.kind == 5) {
+ if (la.kind == 6) {
Get();
arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2));
} else if (StartOf(16)) {
Expression(out e, allowSemi);
arg = new Attributes.Argument(t, e);
- } else SynErr(196);
+ } else SynErr(198);
}
void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {
@@ -2364,11 +2396,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 32: {
Get();
x = t; binOp = BinaryExpr.Opcode.Eq;
- if (la.kind == 86) {
+ if (la.kind == 88) {
Get();
- Expect(72);
+ Expect(74);
Expression(out k, true);
- Expect(73);
+ Expect(75);
}
break;
}
@@ -2382,52 +2414,52 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Gt;
break;
}
- case 87: {
+ case 89: {
Get();
x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 88: {
+ case 90: {
Get();
x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
- case 89: {
+ case 91: {
Get();
x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
- case 90: {
+ case 92: {
Get();
x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
- case 91: {
+ case 93: {
Get();
x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 92: {
+ case 94: {
Get();
x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
- case 93: case 94: {
+ case 95: case 96: {
EquivOp();
x = t; binOp = BinaryExpr.Opcode.Iff;
break;
}
- case 95: case 96: {
+ case 97: case 98: {
ImpliesOp();
x = t; binOp = BinaryExpr.Opcode.Imp;
break;
}
- case 97: case 98: {
+ case 99: case 100: {
ExpliesOp();
x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(197); break;
+ default: SynErr(199); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -2446,8 +2478,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Token x = la;
IToken endTok = x;
- while (la.kind == 8 || la.kind == 85) {
- if (la.kind == 8) {
+ while (la.kind == 9 || la.kind == 87) {
+ if (la.kind == 9) {
BlockStmt(out block, out bodyStart, out bodyEnd);
endTok = block.EndTok; subhints.Add(block);
} else {
@@ -2460,33 +2492,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 93) {
+ if (la.kind == 95) {
Get();
- } else if (la.kind == 94) {
+ } else if (la.kind == 96) {
Get();
- } else SynErr(198);
+ } else SynErr(200);
}
void ImpliesOp() {
- if (la.kind == 95) {
+ if (la.kind == 97) {
Get();
- } else if (la.kind == 96) {
+ } else if (la.kind == 98) {
Get();
- } else SynErr(199);
+ } else SynErr(201);
}
void ExpliesOp() {
- if (la.kind == 97) {
+ if (la.kind == 99) {
Get();
- } else if (la.kind == 98) {
+ } else if (la.kind == 100) {
Get();
- } else SynErr(200);
+ } else SynErr(202);
}
void EquivExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpliesExpression(out e0, allowSemi);
- while (la.kind == 93 || la.kind == 94) {
+ while (la.kind == 95 || la.kind == 96) {
EquivOp();
x = t;
ImpliesExpliesExpression(out e1, allowSemi);
@@ -2498,7 +2530,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi);
if (StartOf(25)) {
- if (la.kind == 95 || la.kind == 96) {
+ if (la.kind == 97 || la.kind == 98) {
ImpliesOp();
x = t;
ImpliesExpression(out e1, allowSemi);
@@ -2508,7 +2540,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
LogicalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
- while (la.kind == 97 || la.kind == 98) {
+ while (la.kind == 99 || la.kind == 100) {
ExpliesOp();
x = t;
LogicalExpression(out e1, allowSemi);
@@ -2522,12 +2554,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0, allowSemi);
if (StartOf(26)) {
- if (la.kind == 99 || la.kind == 100) {
+ if (la.kind == 101 || la.kind == 102) {
AndOp();
x = t;
RelationalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 99 || la.kind == 100) {
+ while (la.kind == 101 || la.kind == 102) {
AndOp();
x = t;
RelationalExpression(out e1, allowSemi);
@@ -2538,7 +2570,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
RelationalExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 101 || la.kind == 102) {
+ while (la.kind == 103 || la.kind == 104) {
OrOp();
x = t;
RelationalExpression(out e1, allowSemi);
@@ -2551,7 +2583,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi);
- if (la.kind == 95 || la.kind == 96) {
+ if (la.kind == 97 || la.kind == 98) {
ImpliesOp();
x = t;
ImpliesExpression(out e1, allowSemi);
@@ -2661,25 +2693,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 99) {
+ if (la.kind == 101) {
Get();
- } else if (la.kind == 100) {
+ } else if (la.kind == 102) {
Get();
- } else SynErr(201);
+ } else SynErr(203);
}
void OrOp() {
- if (la.kind == 101) {
+ if (la.kind == 103) {
Get();
- } else if (la.kind == 102) {
+ } else if (la.kind == 104) {
Get();
- } else SynErr(202);
+ } else SynErr(204);
}
void Term(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0, allowSemi);
- while (la.kind == 105 || la.kind == 106) {
+ while (la.kind == 107 || la.kind == 108) {
AddOp(out x, out op);
Factor(out e1, allowSemi);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2696,11 +2728,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 32: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
- if (la.kind == 86) {
+ if (la.kind == 88) {
Get();
- Expect(72);
+ Expect(74);
Expression(out k, true);
- Expect(73);
+ Expect(75);
}
break;
}
@@ -2714,41 +2746,41 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 87: {
+ case 89: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 88: {
+ case 90: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 89: {
+ case 91: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
- if (la.kind == 86) {
+ if (la.kind == 88) {
Get();
- Expect(72);
+ Expect(74);
Expression(out k, true);
- Expect(73);
+ Expect(75);
}
break;
}
- case 103: {
+ case 105: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 12: {
+ case 13: {
Get();
x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 104: {
+ case 106: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 104) {
+ if (la.kind == 106) {
Get();
y = t;
}
@@ -2763,29 +2795,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
- case 90: {
+ case 92: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 91: {
+ case 93: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 92: {
+ case 94: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(203); break;
+ default: SynErr(205); break;
}
}
void Factor(out Expression e0, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0, allowSemi);
- while (la.kind == 11 || la.kind == 107 || la.kind == 108) {
+ while (la.kind == 12 || la.kind == 109 || la.kind == 110) {
MulOp(out x, out op);
UnaryExpression(out e1, allowSemi);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2794,103 +2826,103 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void AddOp(out IToken x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 105) {
+ if (la.kind == 107) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 106) {
+ } else if (la.kind == 108) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(204);
+ } else SynErr(206);
}
void UnaryExpression(out Expression e, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 106: {
+ case 108: {
Get();
x = t;
UnaryExpression(out e, allowSemi);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 104: case 109: {
+ case 106: case 111: {
NegOp();
x = t;
UnaryExpression(out e, allowSemi);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 24: case 29: case 55: case 64: case 70: case 74: case 80: case 81: case 83: case 85: case 118: case 119: case 120: {
+ case 24: case 29: case 56: case 66: case 72: case 76: case 82: case 83: case 85: case 87: case 120: case 121: case 122: {
EndlessExpression(out e, allowSemi);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 22 || la.kind == 72) {
+ while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
break;
}
- case 8: case 72: {
+ case 9: case 74: {
DisplayExpr(out e);
- while (la.kind == 22 || la.kind == 72) {
+ while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
break;
}
- case 56: {
+ case 57: {
MultiSetExpr(out e);
- while (la.kind == 22 || la.kind == 72) {
+ while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
break;
}
- case 58: {
+ case 59: {
Get();
x = t;
- if (la.kind == 72) {
+ if (la.kind == 74) {
MapDisplayExpr(x, out e);
- while (la.kind == 22 || la.kind == 72) {
+ while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
} else if (la.kind == 1) {
MapComprehensionExpr(x, out e, allowSemi);
} else if (StartOf(28)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(205);
+ } else SynErr(207);
break;
}
- case 2: case 3: case 10: case 28: case 110: case 111: case 112: case 113: case 114: case 115: {
+ case 2: case 3: case 4: case 11: case 28: case 54: case 55: case 112: case 113: case 114: case 115: case 116: case 117: {
ConstAtomExpression(out e);
- while (la.kind == 22 || la.kind == 72) {
+ while (la.kind == 61 || la.kind == 74) {
Suffix(ref e);
}
break;
}
- default: SynErr(206); break;
+ default: SynErr(208); break;
}
}
void MulOp(out IToken x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 107) {
+ } else if (la.kind == 109) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 108) {
+ } else if (la.kind == 110) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(207);
+ } else SynErr(209);
}
void NegOp() {
- if (la.kind == 104) {
+ if (la.kind == 106) {
Get();
- } else if (la.kind == 109) {
+ } else if (la.kind == 111) {
Get();
- } else SynErr(208);
+ } else SynErr(210);
}
void EndlessExpression(out Expression e, bool allowSemi) {
@@ -2900,30 +2932,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
switch (la.kind) {
- case 74: {
+ case 76: {
Get();
x = t;
Expression(out e, true);
- Expect(116);
+ Expect(118);
Expression(out e0, true);
- Expect(75);
+ Expect(77);
Expression(out e1, allowSemi);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 80: {
+ case 82: {
MatchExpression(out e, allowSemi);
break;
}
- case 83: case 118: case 119: case 120: {
+ case 85: case 120: case 121: case 122: {
QuantifierGuts(out e, allowSemi);
break;
}
- case 55: {
+ case 56: {
ComprehensionExpr(out e, allowSemi);
break;
}
- case 70: case 81: case 85: {
+ case 72: case 83: case 87: {
StmtInExpr(out s);
Expression(out e, allowSemi);
e = new StmtExpr(s.Tok, s, e);
@@ -2933,37 +2965,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LetExpr(out e, allowSemi);
break;
}
- case 64: {
+ case 66: {
NamedExpr(out e, allowSemi);
break;
}
- default: SynErr(209); break;
+ default: SynErr(211); break;
}
}
void DottedIdentifiersAndFunction(out Expression e) {
- IToken id; IToken openParen = null;
+ IToken id, idPrime; IToken openParen = null;
List<Expression> args = null;
List<IToken> idents = new List<IToken>();
Ident(out id);
idents.Add(id);
- while (la.kind == 22) {
- Get();
- IdentOrDigits(out id);
- idents.Add(id);
+ while (la.kind == 61) {
+ IdentOrDigitsSuffix(out id, out idPrime);
+ idents.Add(id);
+ if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
+
}
- if (la.kind == 10 || la.kind == 86) {
+ if (la.kind == 11 || la.kind == 88) {
args = new List<Expression>();
- if (la.kind == 86) {
+ if (la.kind == 88) {
Get();
id.val = id.val + "#"; Expression k;
- Expect(72);
+ Expect(74);
Expression(out k, true);
- Expect(73);
+ Expect(75);
args.Add(k);
}
- Expect(10);
+ Expect(11);
openParen = t;
if (StartOf(16)) {
Expressions(args);
@@ -2979,20 +3012,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 22) {
- Get();
- IdentOrDigits(out id);
- if (la.kind == 10 || la.kind == 86) {
+ if (la.kind == 61) {
+ IdentOrDigitsSuffix(out id, out x);
+ if (x != null) {
+ // process id as a Suffix in its own right
+ e = new ExprDotName(id, e, id.val);
+ id = x; // move to the next Suffix
+ }
+
+ if (la.kind == 11 || la.kind == 88) {
args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 86) {
+ if (la.kind == 88) {
Get();
id.val = id.val + "#"; Expression k;
- Expect(72);
+ Expect(74);
Expression(out k, true);
- Expect(73);
+ Expect(75);
args.Add(k);
}
- Expect(10);
+ Expect(11);
IToken openParen = t;
if (StartOf(16)) {
Expressions(args);
@@ -3001,24 +3039,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 72) {
+ } else if (la.kind == 74) {
Get();
x = t;
if (StartOf(16)) {
Expression(out ee, true);
e0 = ee;
- if (la.kind == 117) {
+ if (la.kind == 119) {
Get();
anyDots = true;
if (StartOf(16)) {
Expression(out ee, true);
e1 = ee;
}
- } else if (la.kind == 67) {
+ } else if (la.kind == 69) {
Get();
Expression(out ee, true);
e1 = ee;
- } else if (la.kind == 30 || la.kind == 73) {
+ } else if (la.kind == 30 || la.kind == 75) {
while (la.kind == 30) {
Get();
Expression(out ee, true);
@@ -3029,15 +3067,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(210);
- } else if (la.kind == 117) {
+ } else SynErr(212);
+ } else if (la.kind == 119) {
Get();
anyDots = true;
if (StartOf(16)) {
Expression(out ee, true);
e1 = ee;
}
- } else SynErr(211);
+ } else SynErr(213);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -3060,8 +3098,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- Expect(73);
- } else SynErr(212);
+ Expect(75);
+ } else SynErr(214);
}
void DisplayExpr(out Expression e) {
@@ -3069,23 +3107,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- if (la.kind == 8) {
+ if (la.kind == 9) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(16)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
- Expect(9);
- } else if (la.kind == 72) {
+ Expect(10);
+ } else if (la.kind == 74) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(16)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(73);
- } else SynErr(213);
+ Expect(75);
+ } else SynErr(215);
}
void MultiSetExpr(out Expression e) {
@@ -3093,17 +3131,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(56);
+ Expect(57);
x = t;
- if (la.kind == 8) {
+ if (la.kind == 9) {
Get();
elements = new List<Expression/*!*/>();
if (StartOf(16)) {
Expressions(elements);
}
e = new MultiSetDisplayExpr(x, elements);
- Expect(9);
- } else if (la.kind == 10) {
+ Expect(10);
+ } else if (la.kind == 11) {
Get();
x = t; elements = new List<Expression/*!*/>();
Expression(out e, true);
@@ -3111,7 +3149,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(33);
} else if (StartOf(29)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(214);
+ } else SynErr(216);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -3119,12 +3157,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
e = dummyExpr;
- Expect(72);
+ Expect(74);
if (StartOf(16)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(mapToken, elements);
- Expect(73);
+ Expect(75);
}
void MapComprehensionExpr(IToken mapToken, out Expression e, bool allowSemi) {
@@ -3148,21 +3186,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ConstAtomExpression(out Expression e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null);
- IToken/*!*/ x; BigInteger n;
+ IToken/*!*/ x; BigInteger n; Basetypes.BigDec d;
e = dummyExpr;
switch (la.kind) {
- case 110: {
+ case 112: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 111: {
+ case 113: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 112: {
+ case 114: {
Get();
e = new LiteralExpr(t);
break;
@@ -3172,24 +3210,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, n);
break;
}
- case 113: {
+ case 4: {
+ Dec(out d);
+ e = new LiteralExpr(t, d);
+ break;
+ }
+ case 115: {
Get();
e = new ThisExpr(t);
break;
}
- case 114: {
+ case 116: {
Get();
x = t;
- Expect(10);
+ Expect(11);
Expression(out e, true);
Expect(33);
e = new FreshExpr(x, e);
break;
}
- case 115: {
+ case 117: {
Get();
x = t;
- Expect(10);
+ Expect(11);
Expression(out e, true);
Expect(33);
e = new OldExpr(x, e);
@@ -3203,7 +3246,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(28);
break;
}
- case 10: {
+ case 11: {
Get();
x = t;
Expression(out e, true);
@@ -3211,7 +3254,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(33);
break;
}
- default: SynErr(215); break;
+ case 55: {
+ Get();
+ x = t;
+ Expect(11);
+ IToken openParen = t;
+ Expression(out e, true);
+ Expect(33);
+ IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
+ IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
+
+ break;
+ }
+ case 54: {
+ Get();
+ x = t;
+ Expect(11);
+ IToken openParen = t;
+ Expression(out e, true);
+ Expect(33);
+ IToken classTok = new Token(t.line, t.col); classTok.val = "Real";
+ IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";
+ //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });
+ e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });
+
+ break;
+ }
+ default: SynErr(217); break;
}
}
@@ -3236,41 +3307,53 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero;
}
- } else SynErr(216);
+ } else SynErr(218);
+ }
+
+ void Dec(out Basetypes.BigDec d) {
+ d = Basetypes.BigDec.ZERO;
+ Expect(4);
+ try {
+ d = Basetypes.BigDec.FromString(t.val);
+ } catch (System.FormatException) {
+ SemErr("incorrectly formatted number");
+ d = Basetypes.BigDec.ZERO;
+ }
+
}
void MapLiteralExpressions(out List<ExpressionPair> elements) {
Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d, true);
- Expect(67);
+ Expect(69);
Expression(out r, true);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 30) {
Get();
Expression(out d, true);
- Expect(67);
+ Expect(69);
Expression(out r, true);
elements.Add(new ExpressionPair(d,r));
}
}
void QSep() {
- if (la.kind == 121) {
+ if (la.kind == 123) {
Get();
- } else if (la.kind == 122) {
+ } else if (la.kind == 124) {
Get();
- } else SynErr(217);
+ } else SynErr(219);
}
void MatchExpression(out Expression e, bool allowSemi) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(80);
+ Expect(82);
x = t;
Expression(out e, allowSemi);
- while (la.kind == 76) {
+ while (la.kind == 78) {
CaseExpression(out c, allowSemi);
cases.Add(c);
}
@@ -3285,13 +3368,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range;
Expression/*!*/ body;
- if (la.kind == 83 || la.kind == 118) {
+ if (la.kind == 85 || la.kind == 120) {
Forall();
x = t; univ = true;
- } else if (la.kind == 119 || la.kind == 120) {
+ } else if (la.kind == 121 || la.kind == 122) {
Exists();
x = t;
- } else SynErr(218);
+ } else SynErr(220);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi);
@@ -3311,7 +3394,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range;
Expression body = null;
- Expect(55);
+ Expect(56);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -3322,7 +3405,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(28);
Expression(out range, allowSemi);
- if (la.kind == 121 || la.kind == 122) {
+ if (la.kind == 123 || la.kind == 124) {
QSep();
Expression(out body, allowSemi);
}
@@ -3333,13 +3416,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void StmtInExpr(out Statement s) {
s = dummyStmt;
- if (la.kind == 81) {
+ if (la.kind == 83) {
AssertStmt(out s);
- } else if (la.kind == 70) {
+ } else if (la.kind == 72) {
AssumeStmt(out s);
- } else if (la.kind == 85) {
+ } else if (la.kind == 87) {
CalcStmt(out s);
- } else SynErr(219);
+ } else SynErr(221);
}
void LetExpr(out Expression e, bool allowSemi) {
@@ -3368,9 +3451,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo letLHSs.Add(pat);
}
- if (la.kind == 67) {
+ if (la.kind == 69) {
Get();
- } else if (la.kind == 69) {
+ } else if (la.kind == 71) {
Get();
exact = false;
foreach (var lhs in letLHSs) {
@@ -3379,7 +3462,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- } else SynErr(220);
+ } else SynErr(222);
Expression(out e, false);
letRHSs.Add(e);
while (la.kind == 30) {
@@ -3387,7 +3470,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false);
letRHSs.Add(e);
}
- Expect(7);
+ Expect(8);
Expression(out e, allowSemi);
e = new LetExpr(x, letLHSs, letRHSs, e, exact);
}
@@ -3397,10 +3480,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
Expression expr;
- Expect(64);
+ Expect(66);
x = t;
NoUSIdent(out d);
- Expect(6);
+ Expect(7);
Expression(out e, allowSemi);
expr = e;
e = new NamedExpr(x, d.val, expr);
@@ -3413,7 +3496,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (IsIdentParen()) {
Ident(out id);
- Expect(10);
+ Expect(11);
arguments = new List<CasePattern>();
if (la.kind == 1) {
CasePattern(out pat);
@@ -3430,7 +3513,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
pat = new CasePattern(bv.tok, bv);
- } else SynErr(221);
+ } else SynErr(223);
}
void CaseExpression(out MatchCaseExpr c, bool allowSemi) {
@@ -3439,10 +3522,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(76);
+ Expect(78);
x = t;
Ident(out id);
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
@@ -3453,25 +3536,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(33);
}
- Expect(77);
+ Expect(79);
Expression(out body, allowSemi);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
void Forall() {
- if (la.kind == 83) {
+ if (la.kind == 85) {
Get();
- } else if (la.kind == 118) {
+ } else if (la.kind == 120) {
Get();
- } else SynErr(222);
+ } else SynErr(224);
}
void Exists() {
- if (la.kind == 119) {
+ if (la.kind == 121) {
Get();
- } else if (la.kind == 120) {
+ } else if (la.kind == 122) {
Get();
- } else SynErr(223);
+ } else SynErr(225);
}
void AttributeBody(ref Attributes attrs) {
@@ -3479,7 +3562,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
Attributes.Argument/*!*/ aArg;
- Expect(6);
+ Expect(7);
Expect(1);
aName = t.val;
if (StartOf(30)) {
@@ -3507,37 +3590,37 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
static readonly bool[,]/*!*/ set = {
- {T,T,T,T, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,T, T,T,x,x, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,T,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,x,x, T,T,T,x, x,x,T,T, x,T,x,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,T,x, x,x,T,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},
- {x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},
- {T,T,T,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,T,x, x,x,T,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x},
- {x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},
- {x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},
- {x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,T, T,T,x,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,T,T,x, x},
- {x,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,T,x,T, T,T,x,T, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,T,T,x, x},
- {x,T,T,T, x,T,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x}
+ {T,T,T,T, T,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,T, T,T,x,x, x,x,T,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,T, T,x,T,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {T,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,x, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,T,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,x,T, x,T,T,T, x,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,T, T,x,x},
+ {x,x,x,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,x,x, x,x,T,T, x,T,T,T, x,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,T, T,x,x},
+ {x,T,T,T, T,x,T,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x}
};
} // end Parser
@@ -3566,25 +3649,25 @@ public class Errors { case 1: s = "ident expected"; break;
case 2: s = "digits expected"; break;
case 3: s = "hexdigits expected"; break;
- case 4: s = "arrayToken expected"; break;
- case 5: s = "string expected"; break;
- case 6: s = "colon expected"; break;
- case 7: s = "semi expected"; break;
- case 8: s = "lbrace expected"; break;
- case 9: s = "rbrace expected"; break;
- case 10: s = "openparen expected"; break;
- case 11: s = "star expected"; break;
- case 12: s = "notIn expected"; break;
- case 13: s = "\"include\" expected"; break;
- case 14: s = "\"abstract\" expected"; break;
- case 15: s = "\"module\" expected"; break;
- case 16: s = "\"refines\" expected"; break;
- case 17: s = "\"import\" expected"; break;
- case 18: s = "\"opened\" expected"; break;
- case 19: s = "\"=\" expected"; break;
- case 20: s = "\"as\" expected"; break;
- case 21: s = "\"default\" expected"; break;
- case 22: s = "\".\" expected"; break;
+ case 4: s = "decimaldigits expected"; break;
+ case 5: s = "arrayToken expected"; break;
+ case 6: s = "string expected"; break;
+ case 7: s = "colon expected"; break;
+ case 8: s = "semi expected"; break;
+ case 9: s = "lbrace expected"; break;
+ case 10: s = "rbrace expected"; break;
+ case 11: s = "openparen expected"; break;
+ case 12: s = "star expected"; break;
+ case 13: s = "notIn expected"; break;
+ case 14: s = "\"include\" expected"; break;
+ case 15: s = "\"abstract\" expected"; break;
+ case 16: s = "\"module\" expected"; break;
+ case 17: s = "\"refines\" expected"; break;
+ case 18: s = "\"import\" expected"; break;
+ case 19: s = "\"opened\" expected"; break;
+ case 20: s = "\"=\" expected"; break;
+ case 21: s = "\"as\" expected"; break;
+ case 22: s = "\"default\" expected"; break;
case 23: s = "\"class\" expected"; break;
case 24: s = "\"ghost\" expected"; break;
case 25: s = "\"static\" expected"; break;
@@ -3617,175 +3700,177 @@ public class Errors { case 52: s = "\"bool\" expected"; break;
case 53: s = "\"nat\" expected"; break;
case 54: s = "\"int\" expected"; break;
- case 55: s = "\"set\" expected"; break;
- case 56: s = "\"multiset\" expected"; break;
- case 57: s = "\"seq\" expected"; break;
- case 58: s = "\"map\" expected"; break;
- case 59: s = "\"object\" expected"; break;
- case 60: s = "\"function\" expected"; break;
- case 61: s = "\"predicate\" expected"; break;
- case 62: s = "\"copredicate\" expected"; break;
- case 63: s = "\"`\" expected"; break;
- case 64: s = "\"label\" expected"; break;
- case 65: s = "\"break\" expected"; break;
- case 66: s = "\"where\" expected"; break;
- case 67: s = "\":=\" expected"; break;
- case 68: s = "\"return\" expected"; break;
- case 69: s = "\":|\" expected"; break;
- case 70: s = "\"assume\" expected"; break;
- case 71: s = "\"new\" expected"; break;
- case 72: s = "\"[\" expected"; break;
- case 73: s = "\"]\" expected"; break;
- case 74: s = "\"if\" expected"; break;
- case 75: s = "\"else\" expected"; break;
- case 76: s = "\"case\" expected"; break;
- case 77: s = "\"=>\" expected"; break;
- case 78: s = "\"while\" expected"; break;
- case 79: s = "\"invariant\" expected"; break;
- case 80: s = "\"match\" expected"; break;
- case 81: s = "\"assert\" expected"; break;
- case 82: s = "\"print\" expected"; break;
- case 83: s = "\"forall\" expected"; break;
- case 84: s = "\"parallel\" expected"; break;
- case 85: s = "\"calc\" expected"; break;
- case 86: s = "\"#\" expected"; break;
- case 87: s = "\"<=\" expected"; break;
- case 88: s = "\">=\" expected"; break;
- case 89: s = "\"!=\" expected"; break;
- case 90: s = "\"\\u2260\" expected"; break;
- case 91: s = "\"\\u2264\" expected"; break;
- case 92: s = "\"\\u2265\" expected"; break;
- case 93: s = "\"<==>\" expected"; break;
- case 94: s = "\"\\u21d4\" expected"; break;
- case 95: s = "\"==>\" expected"; break;
- case 96: s = "\"\\u21d2\" expected"; break;
- case 97: s = "\"<==\" expected"; break;
- case 98: s = "\"\\u21d0\" expected"; break;
- case 99: s = "\"&&\" expected"; break;
- case 100: s = "\"\\u2227\" expected"; break;
- case 101: s = "\"||\" expected"; break;
- case 102: s = "\"\\u2228\" expected"; break;
- case 103: s = "\"in\" expected"; break;
- case 104: s = "\"!\" expected"; break;
- case 105: s = "\"+\" expected"; break;
- case 106: s = "\"-\" expected"; break;
- case 107: s = "\"/\" expected"; break;
- case 108: s = "\"%\" expected"; break;
- case 109: s = "\"\\u00ac\" expected"; break;
- case 110: s = "\"false\" expected"; break;
- case 111: s = "\"true\" expected"; break;
- case 112: s = "\"null\" expected"; break;
- case 113: s = "\"this\" expected"; break;
- case 114: s = "\"fresh\" expected"; break;
- case 115: s = "\"old\" expected"; break;
- case 116: s = "\"then\" expected"; break;
- case 117: s = "\"..\" expected"; break;
- case 118: s = "\"\\u2200\" expected"; break;
- case 119: s = "\"exists\" expected"; break;
- case 120: s = "\"\\u2203\" expected"; break;
- case 121: s = "\"::\" expected"; break;
- case 122: s = "\"\\u2022\" expected"; break;
- case 123: s = "??? expected"; break;
- case 124: s = "this symbol not expected in SubModuleDecl"; break;
- case 125: s = "invalid SubModuleDecl"; break;
- case 126: s = "this symbol not expected in ClassDecl"; break;
- case 127: s = "this symbol not expected in DatatypeDecl"; break;
- case 128: s = "invalid DatatypeDecl"; break;
+ case 55: s = "\"real\" expected"; break;
+ case 56: s = "\"set\" expected"; break;
+ case 57: s = "\"multiset\" expected"; break;
+ case 58: s = "\"seq\" expected"; break;
+ case 59: s = "\"map\" expected"; break;
+ case 60: s = "\"object\" expected"; break;
+ case 61: s = "\".\" expected"; break;
+ case 62: s = "\"function\" expected"; break;
+ case 63: s = "\"predicate\" expected"; break;
+ case 64: s = "\"copredicate\" expected"; break;
+ case 65: s = "\"`\" expected"; break;
+ case 66: s = "\"label\" expected"; break;
+ case 67: s = "\"break\" expected"; break;
+ case 68: s = "\"where\" expected"; break;
+ case 69: s = "\":=\" expected"; break;
+ case 70: s = "\"return\" expected"; break;
+ case 71: s = "\":|\" expected"; break;
+ case 72: s = "\"assume\" expected"; break;
+ case 73: s = "\"new\" expected"; break;
+ case 74: s = "\"[\" expected"; break;
+ case 75: s = "\"]\" expected"; break;
+ case 76: s = "\"if\" expected"; break;
+ case 77: s = "\"else\" expected"; break;
+ case 78: s = "\"case\" expected"; break;
+ case 79: s = "\"=>\" expected"; break;
+ case 80: s = "\"while\" expected"; break;
+ case 81: s = "\"invariant\" expected"; break;
+ case 82: s = "\"match\" expected"; break;
+ case 83: s = "\"assert\" expected"; break;
+ case 84: s = "\"print\" expected"; break;
+ case 85: s = "\"forall\" expected"; break;
+ case 86: s = "\"parallel\" expected"; break;
+ case 87: s = "\"calc\" expected"; break;
+ case 88: s = "\"#\" expected"; break;
+ case 89: s = "\"<=\" expected"; break;
+ case 90: s = "\">=\" expected"; break;
+ case 91: s = "\"!=\" expected"; break;
+ case 92: s = "\"\\u2260\" expected"; break;
+ case 93: s = "\"\\u2264\" expected"; break;
+ case 94: s = "\"\\u2265\" expected"; break;
+ case 95: s = "\"<==>\" expected"; break;
+ case 96: s = "\"\\u21d4\" expected"; break;
+ case 97: s = "\"==>\" expected"; break;
+ case 98: s = "\"\\u21d2\" expected"; break;
+ case 99: s = "\"<==\" expected"; break;
+ case 100: s = "\"\\u21d0\" expected"; break;
+ case 101: s = "\"&&\" expected"; break;
+ case 102: s = "\"\\u2227\" expected"; break;
+ case 103: s = "\"||\" expected"; break;
+ case 104: s = "\"\\u2228\" expected"; break;
+ case 105: s = "\"in\" expected"; break;
+ case 106: s = "\"!\" expected"; break;
+ case 107: s = "\"+\" expected"; break;
+ case 108: s = "\"-\" expected"; break;
+ case 109: s = "\"/\" expected"; break;
+ case 110: s = "\"%\" expected"; break;
+ case 111: s = "\"\\u00ac\" expected"; break;
+ case 112: s = "\"false\" expected"; break;
+ case 113: s = "\"true\" expected"; break;
+ case 114: s = "\"null\" expected"; break;
+ case 115: s = "\"this\" expected"; break;
+ case 116: s = "\"fresh\" expected"; break;
+ case 117: s = "\"old\" expected"; break;
+ case 118: s = "\"then\" expected"; break;
+ case 119: s = "\"..\" expected"; break;
+ case 120: s = "\"\\u2200\" expected"; break;
+ case 121: s = "\"exists\" expected"; break;
+ case 122: s = "\"\\u2203\" expected"; break;
+ case 123: s = "\"::\" expected"; break;
+ case 124: s = "\"\\u2022\" expected"; break;
+ case 125: s = "??? expected"; break;
+ case 126: s = "this symbol not expected in SubModuleDecl"; break;
+ case 127: s = "invalid SubModuleDecl"; break;
+ case 128: s = "this symbol not expected in ClassDecl"; break;
case 129: s = "this symbol not expected in DatatypeDecl"; break;
- case 130: s = "this symbol not expected in ArbitraryTypeDecl"; break;
- case 131: s = "this symbol not expected in IteratorDecl"; break;
- case 132: s = "invalid IteratorDecl"; break;
- case 133: s = "invalid ClassMemberDecl"; break;
- case 134: s = "invalid IdentOrDigits"; break;
- case 135: s = "this symbol not expected in FieldDecl"; break;
- case 136: s = "this symbol not expected in FieldDecl"; break;
- case 137: s = "invalid FunctionDecl"; break;
- case 138: s = "invalid FunctionDecl"; break;
+ case 130: s = "invalid DatatypeDecl"; break;
+ case 131: s = "this symbol not expected in DatatypeDecl"; break;
+ case 132: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+ case 133: s = "this symbol not expected in IteratorDecl"; break;
+ case 134: s = "invalid IteratorDecl"; break;
+ case 135: s = "invalid ClassMemberDecl"; break;
+ case 136: s = "invalid IdentOrDigitsSuffix"; break;
+ case 137: s = "this symbol not expected in FieldDecl"; break;
+ case 138: s = "this symbol not expected in FieldDecl"; break;
case 139: s = "invalid FunctionDecl"; break;
case 140: s = "invalid FunctionDecl"; break;
- case 141: s = "this symbol not expected in MethodDecl"; break;
- case 142: s = "invalid MethodDecl"; break;
- case 143: s = "invalid MethodDecl"; break;
- case 144: s = "invalid FIdentType"; break;
- case 145: s = "invalid TypeIdentOptional"; break;
- case 146: s = "invalid TypeAndToken"; break;
- case 147: s = "this symbol not expected in IteratorSpec"; break;
- case 148: s = "this symbol not expected in IteratorSpec"; break;
+ case 141: s = "invalid FunctionDecl"; break;
+ case 142: s = "invalid FunctionDecl"; break;
+ case 143: s = "this symbol not expected in MethodDecl"; break;
+ case 144: s = "invalid MethodDecl"; break;
+ case 145: s = "invalid MethodDecl"; break;
+ case 146: s = "invalid FIdentType"; break;
+ case 147: s = "invalid TypeIdentOptional"; break;
+ case 148: s = "invalid TypeAndToken"; break;
case 149: s = "this symbol not expected in IteratorSpec"; break;
case 150: s = "this symbol not expected in IteratorSpec"; break;
case 151: s = "this symbol not expected in IteratorSpec"; break;
- case 152: s = "invalid IteratorSpec"; break;
+ case 152: s = "this symbol not expected in IteratorSpec"; break;
case 153: s = "this symbol not expected in IteratorSpec"; break;
case 154: s = "invalid IteratorSpec"; break;
- case 155: s = "this symbol not expected in MethodSpec"; break;
- case 156: s = "this symbol not expected in MethodSpec"; break;
+ case 155: s = "this symbol not expected in IteratorSpec"; break;
+ case 156: s = "invalid IteratorSpec"; break;
case 157: s = "this symbol not expected in MethodSpec"; break;
case 158: s = "this symbol not expected in MethodSpec"; break;
- case 159: s = "invalid MethodSpec"; break;
+ case 159: s = "this symbol not expected in MethodSpec"; break;
case 160: s = "this symbol not expected in MethodSpec"; break;
case 161: s = "invalid MethodSpec"; break;
- case 162: s = "invalid FrameExpression"; break;
- case 163: s = "invalid ReferenceType"; break;
- case 164: s = "this symbol not expected in FunctionSpec"; break;
- case 165: s = "this symbol not expected in FunctionSpec"; break;
+ case 162: s = "this symbol not expected in MethodSpec"; break;
+ case 163: s = "invalid MethodSpec"; break;
+ case 164: s = "invalid FrameExpression"; break;
+ case 165: s = "invalid ReferenceType"; break;
case 166: s = "this symbol not expected in FunctionSpec"; break;
case 167: s = "this symbol not expected in FunctionSpec"; break;
case 168: s = "this symbol not expected in FunctionSpec"; break;
- case 169: s = "invalid FunctionSpec"; break;
- case 170: s = "invalid PossiblyWildFrameExpression"; break;
- case 171: s = "invalid PossiblyWildExpression"; break;
- case 172: s = "this symbol not expected in OneStmt"; break;
- case 173: s = "invalid OneStmt"; break;
+ case 169: s = "this symbol not expected in FunctionSpec"; break;
+ case 170: s = "this symbol not expected in FunctionSpec"; break;
+ case 171: s = "invalid FunctionSpec"; break;
+ case 172: s = "invalid PossiblyWildFrameExpression"; break;
+ case 173: s = "invalid PossiblyWildExpression"; break;
case 174: s = "this symbol not expected in OneStmt"; break;
case 175: s = "invalid OneStmt"; break;
- case 176: s = "invalid AssertStmt"; break;
- case 177: s = "invalid AssumeStmt"; break;
- case 178: s = "invalid UpdateStmt"; break;
- case 179: s = "invalid UpdateStmt"; break;
- case 180: s = "invalid IfStmt"; break;
- case 181: s = "invalid IfStmt"; break;
- case 182: s = "invalid WhileStmt"; break;
- case 183: s = "invalid WhileStmt"; break;
- case 184: s = "invalid ForallStmt"; break;
- case 185: s = "invalid ForallStmt"; break;
- case 186: s = "invalid ReturnStmt"; break;
- case 187: s = "invalid Rhs"; break;
- case 188: s = "invalid Lhs"; break;
- case 189: s = "invalid Guard"; break;
- case 190: s = "this symbol not expected in LoopSpec"; break;
- case 191: s = "this symbol not expected in LoopSpec"; break;
+ case 176: s = "this symbol not expected in OneStmt"; break;
+ case 177: s = "invalid OneStmt"; break;
+ case 178: s = "invalid AssertStmt"; break;
+ case 179: s = "invalid AssumeStmt"; break;
+ case 180: s = "invalid UpdateStmt"; break;
+ case 181: s = "invalid UpdateStmt"; break;
+ case 182: s = "invalid IfStmt"; break;
+ case 183: s = "invalid IfStmt"; break;
+ case 184: s = "invalid WhileStmt"; break;
+ case 185: s = "invalid WhileStmt"; break;
+ case 186: s = "invalid ForallStmt"; break;
+ case 187: s = "invalid ForallStmt"; break;
+ case 188: s = "invalid ReturnStmt"; break;
+ case 189: s = "invalid Rhs"; break;
+ case 190: s = "invalid Lhs"; break;
+ case 191: s = "invalid Guard"; break;
case 192: s = "this symbol not expected in LoopSpec"; break;
case 193: s = "this symbol not expected in LoopSpec"; break;
case 194: s = "this symbol not expected in LoopSpec"; break;
- case 195: s = "this symbol not expected in Invariant"; break;
- case 196: s = "invalid AttributeArg"; break;
- case 197: s = "invalid CalcOp"; break;
- case 198: s = "invalid EquivOp"; break;
- case 199: s = "invalid ImpliesOp"; break;
- case 200: s = "invalid ExpliesOp"; break;
- case 201: s = "invalid AndOp"; break;
- case 202: s = "invalid OrOp"; break;
- case 203: s = "invalid RelOp"; break;
- case 204: s = "invalid AddOp"; break;
- case 205: s = "invalid UnaryExpression"; break;
- case 206: s = "invalid UnaryExpression"; break;
- case 207: s = "invalid MulOp"; break;
- case 208: s = "invalid NegOp"; break;
- case 209: s = "invalid EndlessExpression"; break;
- case 210: s = "invalid Suffix"; break;
- case 211: s = "invalid Suffix"; break;
+ case 195: s = "this symbol not expected in LoopSpec"; break;
+ case 196: s = "this symbol not expected in LoopSpec"; break;
+ case 197: s = "this symbol not expected in Invariant"; break;
+ case 198: s = "invalid AttributeArg"; break;
+ case 199: s = "invalid CalcOp"; break;
+ case 200: s = "invalid EquivOp"; break;
+ case 201: s = "invalid ImpliesOp"; break;
+ case 202: s = "invalid ExpliesOp"; break;
+ case 203: s = "invalid AndOp"; break;
+ case 204: s = "invalid OrOp"; break;
+ case 205: s = "invalid RelOp"; break;
+ case 206: s = "invalid AddOp"; break;
+ case 207: s = "invalid UnaryExpression"; break;
+ case 208: s = "invalid UnaryExpression"; break;
+ case 209: s = "invalid MulOp"; break;
+ case 210: s = "invalid NegOp"; break;
+ case 211: s = "invalid EndlessExpression"; break;
case 212: s = "invalid Suffix"; break;
- case 213: s = "invalid DisplayExpr"; break;
- case 214: s = "invalid MultiSetExpr"; break;
- case 215: s = "invalid ConstAtomExpression"; break;
- case 216: s = "invalid Nat"; break;
- case 217: s = "invalid QSep"; break;
- case 218: s = "invalid QuantifierGuts"; break;
- case 219: s = "invalid StmtInExpr"; break;
- case 220: s = "invalid LetExpr"; break;
- case 221: s = "invalid CasePattern"; break;
- case 222: s = "invalid Forall"; break;
- case 223: s = "invalid Exists"; break;
+ case 213: s = "invalid Suffix"; break;
+ case 214: s = "invalid Suffix"; break;
+ case 215: s = "invalid DisplayExpr"; break;
+ case 216: s = "invalid MultiSetExpr"; break;
+ case 217: s = "invalid ConstAtomExpression"; break;
+ case 218: s = "invalid Nat"; break;
+ case 219: s = "invalid QSep"; break;
+ case 220: s = "invalid QuantifierGuts"; break;
+ case 221: s = "invalid StmtInExpr"; break;
+ case 222: s = "invalid LetExpr"; break;
+ case 223: s = "invalid CasePattern"; break;
+ case 224: s = "invalid Forall"; break;
+ case 225: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index f4b4ccc8..952c8ef6 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1114,6 +1114,24 @@ namespace Microsoft.Dafny { wr.Write("null");
} else if (e.Value is bool) {
wr.Write((bool)e.Value ? "true" : "false");
+ } else if (e.Value is Basetypes.BigDec) {
+ Basetypes.BigDec dec = (Basetypes.BigDec)e.Value;
+ wr.Write((dec.Mantissa >= 0) ? "" : "-");
+ string s = BigInteger.Abs(dec.Mantissa).ToString();
+ int digits = s.Length;
+ if (dec.Exponent >= 0) {
+ wr.Write("{0}{1}.0", s, new string('0', dec.Exponent));
+ } else {
+ int exp = -dec.Exponent;
+ if (exp < digits) {
+ int intDigits = digits - exp;
+ int fracDigits = digits - intDigits;
+ wr.Write("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));
+ } else {
+ int fracDigits = digits;
+ wr.Write("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));
+ }
+ }
} else {
wr.Write((BigInteger)e.Value);
}
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 345c5fbb..acee1845 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -438,6 +438,8 @@ namespace Microsoft.Dafny if (next is IntType) {
return (prev is NatType) == (next is NatType);
} else return false;
+ } else if (prev is RealType) {
+ return next is RealType;
} else if (prev is ObjectType) {
return next is ObjectType;
} else if (prev is SetType) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d05c04d4..c18c30ea 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1159,6 +1159,8 @@ namespace Microsoft.Dafny return new LiteralExpr(e.tok);
} else if (e.Value is bool) {
return new LiteralExpr(e.tok, (bool)e.Value);
+ } else if (e.Value is Basetypes.BigDec) {
+ return new LiteralExpr(e.tok, (Basetypes.BigDec)e.Value);
} else {
return new LiteralExpr(e.tok, (BigInteger)e.Value);
}
@@ -3603,7 +3605,7 @@ namespace Microsoft.Dafny #if !NO_CHEAP_OBJECT_WORKAROUND
if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack
var other = a is ObjectType ? b : a;
- if (other is BoolType || other is IntType || other is SetType || other is SeqType || other.IsDatatype) {
+ if (other is BoolType || other is IntType || other is RealType || other is SetType || other is SeqType || other.IsDatatype) {
return false;
}
// allow anything else with object; this is BOGUS
@@ -3616,6 +3618,8 @@ namespace Microsoft.Dafny return b is BoolType;
} else if (a is IntType) {
return b is IntType;
+ } else if (a is RealType) {
+ return b is RealType;
} else if (a is ObjectType) {
return b is ObjectType;
} else if (a is SetType) {
@@ -3716,7 +3720,7 @@ namespace Microsoft.Dafny } else if (proxy is OperationTypeProxy) {
OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
- if (t is IntType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {
+ if (t is IntType || t is RealType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {
// this is the expected case
} else {
return false;
@@ -5518,6 +5522,8 @@ namespace Microsoft.Dafny e.Type = new ObjectTypeProxy();
} else if (e.Value is BigInteger) {
e.Type = Type.Int;
+ } else if (e.Value is Basetypes.BigDec) {
+ e.Type = Type.Real;
} else if (e.Value is bool) {
e.Type = Type.Bool;
} else {
@@ -5826,7 +5832,7 @@ namespace Microsoft.Dafny } else {
bool err = false;
if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) {
- Error(expr, "arguments to {0} must be int or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ Error(expr, "arguments to {0} must be int or real or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
err = true;
}
if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
@@ -5863,7 +5869,7 @@ namespace Microsoft.Dafny } else {
bool err = false;
if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) {
- Error(expr, "arguments to {0} must be int or a set (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ Error(expr, "arguments to {0} must be int or real or a set (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
err = true;
}
if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
@@ -5888,6 +5894,16 @@ namespace Microsoft.Dafny break;
case BinaryExpr.Opcode.Div:
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) {
+ // TODO: this should disallow OperationTypeProxy types except for int and real
+ Error(expr, "first argument to {0} must be of type int or real (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ }
+ if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
+ Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
+ }
+ expr.Type = e.E0.Type;
+ break;
+
case BinaryExpr.Opcode.Mod:
if (!UnifyTypes(e.E0.Type, Type.Int)) {
Error(expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 0c630934..a65a32eb 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 123;
- const int noSym = 123;
+ const int maxT = 125;
+ const int noSym = 125;
[ContractInvariantMethod]
@@ -255,45 +255,45 @@ public class Scanner { for (int i = 92; i <= 92; ++i) start[i] = 1;
for (int i = 95; i <= 95; ++i) start[i] = 1;
for (int i = 98; i <= 122; ++i) start[i] = 1;
- for (int i = 49; i <= 57; ++i) start[i] = 7;
- for (int i = 34; i <= 34; ++i) start[i] = 10;
- start[97] = 20;
- start[48] = 21;
- start[58] = 62;
- start[59] = 12;
- start[123] = 13;
- start[125] = 14;
- start[40] = 15;
- start[42] = 16;
- start[33] = 63;
- start[61] = 64;
- start[46] = 65;
- start[124] = 66;
- start[44] = 28;
- start[41] = 29;
- start[60] = 67;
- start[62] = 68;
- start[96] = 31;
- start[91] = 34;
- start[93] = 35;
- start[35] = 37;
- start[8800] = 40;
- start[8804] = 41;
- start[8805] = 42;
- start[8660] = 44;
- start[8658] = 46;
- start[8656] = 47;
- start[38] = 48;
- start[8743] = 50;
- start[8744] = 52;
- start[43] = 53;
- start[45] = 54;
- start[47] = 55;
- start[37] = 56;
- start[172] = 57;
- start[8704] = 58;
- start[8707] = 59;
- start[8226] = 61;
+ for (int i = 49; i <= 57; ++i) start[i] = 21;
+ for (int i = 34; i <= 34; ++i) start[i] = 11;
+ start[97] = 22;
+ start[48] = 23;
+ start[58] = 64;
+ start[59] = 13;
+ start[123] = 14;
+ start[125] = 15;
+ start[40] = 16;
+ start[42] = 17;
+ start[33] = 65;
+ start[61] = 66;
+ start[124] = 67;
+ start[44] = 30;
+ start[41] = 31;
+ start[46] = 68;
+ start[60] = 69;
+ start[62] = 70;
+ start[96] = 33;
+ start[91] = 36;
+ start[93] = 37;
+ start[35] = 39;
+ start[8800] = 42;
+ start[8804] = 43;
+ start[8805] = 44;
+ start[8660] = 46;
+ start[8658] = 48;
+ start[8656] = 49;
+ start[38] = 50;
+ start[8743] = 52;
+ start[8744] = 54;
+ start[43] = 55;
+ start[45] = 56;
+ start[47] = 57;
+ start[37] = 58;
+ start[172] = 59;
+ start[8704] = 60;
+ start[8707] = 61;
+ start[8226] = 63;
start[Buffer.EOF] = -1;
}
@@ -491,14 +491,14 @@ public class Scanner { void CheckLiteral() {
switch (t.val) {
- case "include": t.kind = 13; break;
- case "abstract": t.kind = 14; break;
- case "module": t.kind = 15; break;
- case "refines": t.kind = 16; break;
- case "import": t.kind = 17; break;
- case "opened": t.kind = 18; break;
- case "as": t.kind = 20; break;
- case "default": t.kind = 21; break;
+ case "include": t.kind = 14; break;
+ case "abstract": t.kind = 15; break;
+ case "module": t.kind = 16; break;
+ case "refines": t.kind = 17; break;
+ case "import": t.kind = 18; break;
+ case "opened": t.kind = 19; break;
+ case "as": t.kind = 21; break;
+ case "default": t.kind = 22; break;
case "class": t.kind = 23; break;
case "ghost": t.kind = 24; break;
case "static": t.kind = 25; break;
@@ -524,40 +524,41 @@ public class Scanner { case "bool": t.kind = 52; break;
case "nat": t.kind = 53; break;
case "int": t.kind = 54; break;
- case "set": t.kind = 55; break;
- case "multiset": t.kind = 56; break;
- case "seq": t.kind = 57; break;
- case "map": t.kind = 58; break;
- case "object": t.kind = 59; break;
- case "function": t.kind = 60; break;
- case "predicate": t.kind = 61; break;
- case "copredicate": t.kind = 62; break;
- case "label": t.kind = 64; break;
- case "break": t.kind = 65; break;
- case "where": t.kind = 66; break;
- case "return": t.kind = 68; break;
- case "assume": t.kind = 70; break;
- case "new": t.kind = 71; break;
- case "if": t.kind = 74; break;
- case "else": t.kind = 75; break;
- case "case": t.kind = 76; break;
- case "while": t.kind = 78; break;
- case "invariant": t.kind = 79; break;
- case "match": t.kind = 80; break;
- case "assert": t.kind = 81; break;
- case "print": t.kind = 82; break;
- case "forall": t.kind = 83; break;
- case "parallel": t.kind = 84; break;
- case "calc": t.kind = 85; break;
- case "in": t.kind = 103; break;
- case "false": t.kind = 110; break;
- case "true": t.kind = 111; break;
- case "null": t.kind = 112; break;
- case "this": t.kind = 113; break;
- case "fresh": t.kind = 114; break;
- case "old": t.kind = 115; break;
- case "then": t.kind = 116; break;
- case "exists": t.kind = 119; break;
+ case "real": t.kind = 55; break;
+ case "set": t.kind = 56; break;
+ case "multiset": t.kind = 57; break;
+ case "seq": t.kind = 58; break;
+ case "map": t.kind = 59; break;
+ case "object": t.kind = 60; break;
+ case "function": t.kind = 62; break;
+ case "predicate": t.kind = 63; break;
+ case "copredicate": t.kind = 64; break;
+ case "label": t.kind = 66; break;
+ case "break": t.kind = 67; break;
+ case "where": t.kind = 68; break;
+ case "return": t.kind = 70; break;
+ case "assume": t.kind = 72; break;
+ case "new": t.kind = 73; break;
+ case "if": t.kind = 76; break;
+ case "else": t.kind = 77; break;
+ case "case": t.kind = 78; break;
+ case "while": t.kind = 80; break;
+ case "invariant": t.kind = 81; break;
+ case "match": t.kind = 82; break;
+ case "assert": t.kind = 83; break;
+ case "print": t.kind = 84; break;
+ case "forall": t.kind = 85; break;
+ case "parallel": t.kind = 86; break;
+ case "calc": t.kind = 87; break;
+ case "in": t.kind = 105; break;
+ case "false": t.kind = 112; break;
+ case "true": t.kind = 113; break;
+ case "null": t.kind = 114; break;
+ case "this": t.kind = 115; break;
+ case "fresh": t.kind = 116; break;
+ case "old": t.kind = 117; break;
+ case "then": t.kind = 118; break;
+ case "exists": t.kind = 121; break;
default: break;
}
}
@@ -616,24 +617,25 @@ public class Scanner { if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 6;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 7:
- recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 7;}
- else {t.kind = 2; break;}
- case 8:
- if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 9;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 8;}
else {goto case 0;}
- case 9:
+ case 8:
recEnd = pos; recKind = 3;
- if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 9;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 8;}
else {t.kind = 3; break;}
- case 10:
- if (ch == '"') {AddCh(); goto case 11;}
- else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 10;}
+ case 9:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
else {goto case 0;}
+ case 10:
+ recEnd = pos; recKind = 4;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
+ else {t.kind = 4; break;}
case 11:
- {t.kind = 5; break;}
+ if (ch == '"') {AddCh(); goto case 12;}
+ else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 11;}
+ else {goto case 0;}
case 12:
- {t.kind = 7; break;}
+ {t.kind = 6; break;}
case 13:
{t.kind = 8; break;}
case 14:
@@ -643,79 +645,83 @@ public class Scanner { case 16:
{t.kind = 11; break;}
case 17:
- if (ch == 'n') {AddCh(); goto case 18;}
- else {goto case 0;}
+ {t.kind = 12; break;}
case 18:
- if (ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {apx++; AddCh(); goto case 19;}
+ if (ch == 'n') {AddCh(); goto case 19;}
else {goto case 0;}
case 19:
+ if (ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {apx++; AddCh(); goto case 20;}
+ else {goto case 0;}
+ case 20:
{
tlen -= apx;
SetScannerBehindT();
- t.kind = 12; break;}
- case 20:
- recEnd = pos; recKind = 1;
- if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 2;}
- else if (ch == 'r') {AddCh(); goto case 23;}
- else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
+ t.kind = 13; break;}
case 21:
recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 7;}
- else if (ch == 'x') {AddCh(); goto case 8;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 21;}
+ else if (ch == '.') {AddCh(); goto case 9;}
else {t.kind = 2; break;}
case 22:
recEnd = pos; recKind = 1;
- if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 22;}
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 2;}
+ else if (ch == 'r') {AddCh(); goto case 25;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 23:
+ recEnd = pos; recKind = 2;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 21;}
+ else if (ch == 'x') {AddCh(); goto case 7;}
+ else if (ch == '.') {AddCh(); goto case 9;}
+ else {t.kind = 2; break;}
+ case 24:
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 24;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
+ case 25:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 3;}
- else if (ch == 'r') {AddCh(); goto case 24;}
+ else if (ch == 'r') {AddCh(); goto case 26;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 24:
+ case 26:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'b' && ch <= 'z') {AddCh(); goto case 4;}
- else if (ch == 'a') {AddCh(); goto case 25;}
+ else if (ch == 'a') {AddCh(); goto case 27;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 25:
+ case 27:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'x' || ch == 'z') {AddCh(); goto case 5;}
- else if (ch == 'y') {AddCh(); goto case 26;}
+ else if (ch == 'y') {AddCh(); goto case 28;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 26:
- recEnd = pos; recKind = 4;
- if (ch == 39 || ch == '0' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 6;}
- else if (ch >= '1' && ch <= '9') {AddCh(); goto case 27;}
- else {t.kind = 4; break;}
- case 27:
- recEnd = pos; recKind = 4;
- if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 22;}
- else if (ch >= '0' && ch <= '9') {AddCh(); goto case 27;}
- else {t.kind = 4; break;}
case 28:
- {t.kind = 30; break;}
+ recEnd = pos; recKind = 5;
+ if (ch == 39 || ch == '0' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 6;}
+ else if (ch >= '1' && ch <= '9') {AddCh(); goto case 29;}
+ else {t.kind = 5; break;}
case 29:
- {t.kind = 33; break;}
+ recEnd = pos; recKind = 5;
+ if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 24;}
+ else if (ch >= '0' && ch <= '9') {AddCh(); goto case 29;}
+ else {t.kind = 5; break;}
case 30:
- {t.kind = 37; break;}
+ {t.kind = 30; break;}
case 31:
- {t.kind = 63; break;}
+ {t.kind = 33; break;}
case 32:
- {t.kind = 67; break;}
+ {t.kind = 37; break;}
case 33:
- {t.kind = 69; break;}
+ {t.kind = 65; break;}
case 34:
- {t.kind = 72; break;}
+ {t.kind = 69; break;}
case 35:
- {t.kind = 73; break;}
+ {t.kind = 71; break;}
case 36:
- {t.kind = 77; break;}
+ {t.kind = 74; break;}
case 37:
- {t.kind = 86; break;}
+ {t.kind = 75; break;}
case 38:
- {t.kind = 88; break;}
+ {t.kind = 79; break;}
case 39:
- {t.kind = 89; break;}
+ {t.kind = 88; break;}
case 40:
{t.kind = 90; break;}
case 41:
@@ -731,22 +737,22 @@ public class Scanner { case 46:
{t.kind = 96; break;}
case 47:
- {t.kind = 98; break;}
+ {t.kind = 97; break;}
case 48:
- if (ch == '&') {AddCh(); goto case 49;}
- else {goto case 0;}
+ {t.kind = 98; break;}
case 49:
- {t.kind = 99; break;}
- case 50:
{t.kind = 100; break;}
+ case 50:
+ if (ch == '&') {AddCh(); goto case 51;}
+ else {goto case 0;}
case 51:
{t.kind = 101; break;}
case 52:
{t.kind = 102; break;}
case 53:
- {t.kind = 105; break;}
+ {t.kind = 103; break;}
case 54:
- {t.kind = 106; break;}
+ {t.kind = 104; break;}
case 55:
{t.kind = 107; break;}
case 56:
@@ -754,61 +760,65 @@ public class Scanner { case 57:
{t.kind = 109; break;}
case 58:
- {t.kind = 118; break;}
+ {t.kind = 110; break;}
case 59:
- {t.kind = 120; break;}
+ {t.kind = 111; break;}
case 60:
- {t.kind = 121; break;}
+ {t.kind = 120; break;}
case 61:
{t.kind = 122; break;}
case 62:
- recEnd = pos; recKind = 6;
- if (ch == '=') {AddCh(); goto case 32;}
- else if (ch == '|') {AddCh(); goto case 33;}
- else if (ch == ':') {AddCh(); goto case 60;}
- else {t.kind = 6; break;}
+ {t.kind = 123; break;}
case 63:
- recEnd = pos; recKind = 104;
- if (ch == 'i') {AddCh(); goto case 17;}
- else if (ch == '=') {AddCh(); goto case 39;}
- else {t.kind = 104; break;}
+ {t.kind = 124; break;}
case 64:
- recEnd = pos; recKind = 19;
- if (ch == '=') {AddCh(); goto case 69;}
- else if (ch == '>') {AddCh(); goto case 36;}
- else {t.kind = 19; break;}
+ recEnd = pos; recKind = 7;
+ if (ch == '=') {AddCh(); goto case 34;}
+ else if (ch == '|') {AddCh(); goto case 35;}
+ else if (ch == ':') {AddCh(); goto case 62;}
+ else {t.kind = 7; break;}
case 65:
- recEnd = pos; recKind = 22;
- if (ch == '.') {AddCh(); goto case 70;}
- else {t.kind = 22; break;}
+ recEnd = pos; recKind = 106;
+ if (ch == 'i') {AddCh(); goto case 18;}
+ else if (ch == '=') {AddCh(); goto case 41;}
+ else {t.kind = 106; break;}
case 66:
+ recEnd = pos; recKind = 20;
+ if (ch == '=') {AddCh(); goto case 71;}
+ else if (ch == '>') {AddCh(); goto case 38;}
+ else {t.kind = 20; break;}
+ case 67:
recEnd = pos; recKind = 28;
- if (ch == '|') {AddCh(); goto case 51;}
+ if (ch == '|') {AddCh(); goto case 53;}
else {t.kind = 28; break;}
- case 67:
+ case 68:
+ recEnd = pos; recKind = 61;
+ if (ch == '.') {AddCh(); goto case 72;}
+ else {t.kind = 61; break;}
+ case 69:
recEnd = pos; recKind = 38;
- if (ch == '=') {AddCh(); goto case 71;}
+ if (ch == '=') {AddCh(); goto case 73;}
else {t.kind = 38; break;}
- case 68:
+ case 70:
recEnd = pos; recKind = 39;
- if (ch == '=') {AddCh(); goto case 38;}
+ if (ch == '=') {AddCh(); goto case 40;}
else {t.kind = 39; break;}
- case 69:
+ case 71:
recEnd = pos; recKind = 32;
- if (ch == '>') {AddCh(); goto case 45;}
+ if (ch == '>') {AddCh(); goto case 47;}
else {t.kind = 32; break;}
- case 70:
- recEnd = pos; recKind = 117;
- if (ch == '.') {AddCh(); goto case 30;}
- else {t.kind = 117; break;}
- case 71:
- recEnd = pos; recKind = 87;
- if (ch == '=') {AddCh(); goto case 72;}
- else {t.kind = 87; break;}
case 72:
- recEnd = pos; recKind = 97;
- if (ch == '>') {AddCh(); goto case 43;}
- else {t.kind = 97; break;}
+ recEnd = pos; recKind = 119;
+ if (ch == '.') {AddCh(); goto case 32;}
+ else {t.kind = 119; break;}
+ case 73:
+ recEnd = pos; recKind = 89;
+ if (ch == '=') {AddCh(); goto case 74;}
+ else {t.kind = 89; break;}
+ case 74:
+ recEnd = pos; recKind = 99;
+ if (ch == '>') {AddCh(); goto case 45;}
+ else {t.kind = 99; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 21aa2b60..8d472098 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1086,7 +1086,7 @@ namespace Microsoft.Dafny { } else if (member is Function) {
var f = (Function)member;
AddClassMember_Function(f);
- if (!IsOpaqueFunction(f)) { // Opaque function's well-formedness is checked on the full version
+ if (!IsOpaqueFunction(f) && !f.IsBuiltin) { // Opaque function's well-formedness is checked on the full version
AddWellformednessCheck(f);
}
var cop = f as CoPredicate;
@@ -3724,9 +3724,11 @@ namespace Microsoft.Dafny { }
break;
case BinaryExpr.ResolvedOpcode.Div:
- case BinaryExpr.ResolvedOpcode.Mod:
- CheckWellformed(e.E1, options, locals, builder, etran);
- builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0)), "possible division by zero", options.AssertKv));
+ case BinaryExpr.ResolvedOpcode.Mod: {
+ Bpl.Expr zero = (e.E1.Type is RealType) ? Bpl.Expr.Literal(Basetypes.BigDec.ZERO) : Bpl.Expr.Literal(0);
+ CheckWellformed(e.E1, options, locals, builder, etran);
+ builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), zero), "possible division by zero", options.AssertKv));
+ }
break;
default:
CheckWellformed(e.E1, options, locals, builder, etran);
@@ -3975,6 +3977,8 @@ namespace Microsoft.Dafny { return new Bpl.IdentifierExpr(tok, "class._System.bool", predef.ClassNameType);
} else if (type is IntType) {
return new Bpl.IdentifierExpr(tok, "class._System.int", predef.ClassNameType);
+ } else if (type is RealType) {
+ return new Bpl.IdentifierExpr(tok, "class._System.real", predef.ClassNameType);
} else if (type is ObjectType) {
return new Bpl.IdentifierExpr(tok, GetClass(program.BuiltIns.ObjectDecl));
} else if (type is CollectionType) {
@@ -4099,7 +4103,7 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null && sink != null);
// declare the function
- {
+ if (!f.IsBuiltin) {
var typeParams = TrTypeParamDecls(f.TypeArgs);
var formals = new List<Variable>();
if (f.IsRecursive) {
@@ -4739,6 +4743,8 @@ namespace Microsoft.Dafny { return Bpl.Type.Bool;
} else if (type is IntType) {
return Bpl.Type.Int;
+ } else if (type is RealType) {
+ return Bpl.Type.Real;
} else if (type is IteratorDecl.EverIncreasingType) {
return Bpl.Type.Int;
} else if (type.IsTypeParameter) {
@@ -5546,6 +5552,10 @@ namespace Microsoft.Dafny { var lit = new LiteralExpr(x.tok, 0);
lit.Type = Type.Int; // resolve here
yield return lit;
+ } else if (x.Type is RealType) {
+ var lit = new LiteralExpr(x.tok, Basetypes.BigDec.ZERO);
+ lit.Type = Type.Real; // resolve here
+ yield return lit;
}
var missingBounds = new List<BoundVar>();
@@ -6630,6 +6640,8 @@ namespace Microsoft.Dafny { return u is BoolType;
} else if (t is IntType) {
return u is IntType;
+ } else if (t is RealType) {
+ return false;
} else if (t is SetType) {
return u is SetType;
} else if (t is SeqType) {
@@ -6813,7 +6825,7 @@ namespace Microsoft.Dafny { // 0 <= x
return Bpl.Expr.Le(Bpl.Expr.Literal(0), x);
- } else if (type is BoolType || type is IntType) {
+ } else if (type is BoolType || type is IntType || type is RealType) {
// nothing to do
} else if (type is SetType) {
@@ -6939,6 +6951,8 @@ namespace Microsoft.Dafny { return Bpl.Expr.Literal(false);
} else if (type is IntType) {
return Bpl.Expr.Literal(0);
+ } else if (type is RealType) {
+ return Bpl.Expr.Literal(Basetypes.BigDec.ZERO);
} else if (type.IsRefType) {
return predef.Null;
} else {
@@ -7972,6 +7986,8 @@ namespace Microsoft.Dafny { return translator.Lit(new Bpl.LiteralExpr(e.tok, (bool)e.Value));
} else if (e.Value is BigInteger) {
return translator.Lit(Bpl.Expr.Literal(Microsoft.Basetypes.BigNum.FromBigInt((BigInteger)e.Value)));
+ } else if (e.Value is Basetypes.BigDec) {
+ return translator.Lit(Bpl.Expr.Literal((Basetypes.BigDec)e.Value));
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal
}
@@ -8253,6 +8269,7 @@ namespace Microsoft.Dafny { } else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
+ bool isReal = e.E0.Type is RealType;
Bpl.Expr e0 = TrExpr(e.E0);
if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) {
return TrInSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInSet translate e.E1
@@ -8330,8 +8347,13 @@ namespace Microsoft.Dafny { typ = Bpl.Type.Int;
bOpcode = BinaryOperator.Opcode.Mul; break;
case BinaryExpr.ResolvedOpcode.Div:
- typ = Bpl.Type.Int;
- bOpcode = BinaryOperator.Opcode.Div; break;
+ if (isReal) {
+ typ = Bpl.Type.Real;
+ bOpcode = BinaryOperator.Opcode.RealDiv; break;
+ } else {
+ typ = Bpl.Type.Int;
+ bOpcode = BinaryOperator.Opcode.Div; break;
+ }
case BinaryExpr.ResolvedOpcode.Mod:
typ = Bpl.Type.Int;
bOpcode = BinaryOperator.Opcode.Mod; break;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index b8ebb8e0..863d749c 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -143,6 +143,23 @@ Execution trace: Dafny program verifier finished with 15 verified, 9 errors
+-------------------- RealTypes.dfy --------------------
+RealTypes.dfy(5,23): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+RealTypes.dfy(11,12): Error: possible division by zero
+Execution trace:
+ (0,0): anon0
+ RealTypes.dfy(10,23): anon3_Else
+ (0,0): anon2
+RealTypes.dfy(11,20): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ RealTypes.dfy(10,23): anon3_Else
+ (0,0): anon2
+
+Dafny program verifier finished with 5 verified, 3 errors
+
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
Execution trace:
@@ -498,7 +515,7 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-ResolutionErrors.dfy(363,6): Error: arguments to + must be int or a collection type (instead got bool)
+ResolutionErrors.dfy(363,6): Error: arguments to + must be int or real or a collection type (instead got bool)
ResolutionErrors.dfy(368,6): Error: all lines in a calculation must have the same type (got int after bool)
ResolutionErrors.dfy(371,6): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(371,6): Error: second argument to ==> must be of type bool (instead got int)
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 3d4af611..581f5068 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -10,7 +10,7 @@ for %%f in (Simple.dfy) do ( %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f
)
-for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
+for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy
FunctionSpecifications.dfy ResolutionErrors.dfy ParseErrors.dfy
Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy
ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy
|