diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 19 | ||||
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 23 | ||||
| -rw-r--r-- | Source/Dafny/Cloner.cs | 14 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 16 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 65 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 117 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 1057 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 14 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 25 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 16 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 411 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 91 | ||||
| -rw-r--r-- | Source/Dafny/Util.cs | 95 | ||||
| -rw-r--r-- | Source/DafnyExtension/TokenTagger.cs | 4 | ||||
| -rw-r--r-- | Test/cloudmake/CloudMake-CachedBuilds.dfy | 1 | ||||
| -rw-r--r-- | Test/cloudmake/CloudMake-ConsistentBuilds.dfy | 1 | ||||
| -rw-r--r-- | Test/cloudmake/CloudMake-ParallelBuilds.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/Strings.dfy | 57 | ||||
| -rw-r--r-- | Test/dafny0/Strings.dfy.expect | 11 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 4 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/dafny.vim | 2 |
23 files changed, 1181 insertions, 872 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 993ada51..4cdb21e9 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -15,6 +15,7 @@ axiom $$Language$Dafny; // coming from a Dafny program. type Ty;
const unique TBool : Ty;
+const unique TChar : Ty;
const unique TInt : Ty;
const unique TNat : Ty;
const unique TReal : Ty;
@@ -41,6 +42,7 @@ type TyTag; function Tag(Ty) : TyTag;
const unique TagBool : TyTag;
+const unique TagChar : TyTag;
const unique TagInt : TyTag;
const unique TagNat : TyTag;
const unique TagReal : TyTag;
@@ -51,6 +53,7 @@ const unique TagMap : TyTag; const unique TagClass : TyTag;
axiom Tag(TBool) == TagBool;
+axiom Tag(TChar) == TagChar;
axiom Tag(TInt) == TagInt;
axiom Tag(TNat) == TagNat;
axiom Tag(TReal) == TagReal;
@@ -70,6 +73,17 @@ function {:identity} Lit<T>(x: T): T { x } axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
// ---------------------------------------------------------------
+// -- Characters -------------------------------------------------
+// ---------------------------------------------------------------
+
+type char;
+function char#FromInt(int): char;
+function char#ToInt(char): int; // inverse of char#FromInt
+axiom (forall n: int ::
+ { char#FromInt(n) }
+ 0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n);
+
+// ---------------------------------------------------------------
// -- References -------------------------------------------------
// ---------------------------------------------------------------
@@ -115,6 +129,9 @@ axiom (forall bx : Box :: axiom (forall bx : Box ::
{ $IsBox(bx, TBool) }
( $IsBox(bx, TBool) ==> $Box($Unbox(bx) : bool) == bx && $Is($Unbox(bx) : bool, TBool)));
+axiom (forall bx : Box ::
+ { $IsBox(bx, TChar) }
+ ( $IsBox(bx, TChar) ==> $Box($Unbox(bx) : char) == bx && $Is($Unbox(bx) : char, TChar)));
axiom (forall bx : Box, t : Ty ::
{ $IsBox(bx, TSet(t)) }
( $IsBox(bx, TSet(t)) ==> $Box($Unbox(bx) : Set Box) == bx && $Is($Unbox(bx) : Set Box, TSet(t))));
@@ -169,11 +186,13 @@ axiom(forall v : int :: { $Is(v,TInt) } $Is(v,TInt)); axiom(forall v : int :: { $Is(v,TNat) } $Is(v,TNat) <==> v >= 0);
axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal));
axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool));
+axiom(forall v : char :: { $Is(v,TChar) } $Is(v,TChar));
axiom(forall h : Heap, v : int :: { $IsAlloc(v,TInt,h) } $IsAlloc(v,TInt,h));
axiom(forall h : Heap, v : int :: { $IsAlloc(v,TNat,h) } $IsAlloc(v,TNat,h));
axiom(forall h : Heap, v : real :: { $IsAlloc(v,TReal,h) } $IsAlloc(v,TReal,h));
axiom(forall h : Heap, v : bool :: { $IsAlloc(v,TBool,h) } $IsAlloc(v,TBool,h));
+axiom(forall h : Heap, v : char :: { $IsAlloc(v,TChar,h) } $IsAlloc(v,TChar,h));
axiom (forall v: Set Box, t0: Ty :: { $Is(v, TSet(t0)) }
$Is(v, TSet(t0)) <==>
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index f00db25a..661666ef 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -434,6 +434,9 @@ namespace Dafny public static Sequence<T> FromElements(params T[] values) {
return new Sequence<T>(values);
}
+ public static Sequence<char> FromString(string s) {
+ return new Sequence<char>(s.ToCharArray());
+ }
public BigInteger Length {
get { return new BigInteger(elmts.Length); }
}
@@ -467,13 +470,21 @@ namespace Dafny return elmts.GetHashCode();
}
public override string ToString() {
- var s = "[";
- var sep = "";
- foreach (var t in elmts) {
- s += sep + t.ToString();
- sep = ", ";
+ if (elmts is char[]) {
+ var s = "";
+ foreach (var t in elmts) {
+ s += t.ToString();
+ }
+ return s;
+ } else {
+ var s = "[";
+ var sep = "";
+ foreach (var t in elmts) {
+ s += sep + t.ToString();
+ sep = ", ";
+ }
+ return s + "]";
}
- return s + "]";
}
bool EqualUntil(Sequence<T> other, int n) {
for (int i = 0; i < n; i++) {
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index c195e14b..75c6ddfe 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -228,14 +228,7 @@ namespace Microsoft.Dafny if (attrs == null) {
return null;
} else {
- return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneAttrArg), CloneAttributes(attrs.Prev));
- }
- }
- public Attributes.Argument CloneAttrArg(Attributes.Argument aa) {
- if (aa.E != null) {
- return new Attributes.Argument(Tok(aa.Tok), CloneExpr(aa.E));
- } else {
- return new Attributes.Argument(Tok(aa.Tok), aa.S);
+ return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
}
}
@@ -256,6 +249,9 @@ 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 string) {
+ var str = (StringLiteralExpr)e;
+ return new StringLiteralExpr(Tok(e.tok), (string)e.Value, str.IsVerbatim);
} else if (e.Value is Basetypes.BigDec) {
return new LiteralExpr(Tok(e.tok), (Basetypes.BigDec)e.Value);
} else {
@@ -479,7 +475,7 @@ namespace Microsoft.Dafny } else if (stmt is PrintStmt) {
var s = (PrintStmt)stmt;
- r = new PrintStmt(Tok(s.Tok), Tok(s.EndTok), s.Args.ConvertAll(CloneAttrArg));
+ r = new PrintStmt(Tok(s.Tok), Tok(s.EndTok), s.Args.ConvertAll(CloneExpr));
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 59fa503e..6ea81d5b 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -966,6 +966,8 @@ namespace Microsoft.Dafny { if (type is BoolType) {
return "bool";
+ } else if (type is CharType) {
+ return "char";
} else if (type is IntType) {
return "BigInteger";
} else if (type is RealType) {
@@ -1061,6 +1063,8 @@ namespace Microsoft.Dafny { if (type is BoolType) {
return "false";
+ } else if (type is CharType) {
+ return "'D'";
} else if (type is IntType) {
return "BigInteger.Zero";
} else if (type is RealType) {
@@ -1132,15 +1136,10 @@ namespace Microsoft.Dafny { if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
- foreach (Attributes.Argument arg in s.Args) {
+ foreach (var arg in s.Args) {
Indent(indent);
wr.Write("System.Console.Write(");
- if (arg.S != null) {
- wr.Write("\"{0}\"", arg.S);
- } else {
- Contract.Assert(arg.E != null);
- TrExpr(arg.E);
- }
+ TrExpr(arg);
wr.WriteLine(");");
}
} else if (stmt is BreakStmt) {
@@ -2049,6 +2048,9 @@ namespace Microsoft.Dafny { wr.Write("({0})null", TypeName(e.Type));
} else if (e.Value is bool) {
wr.Write((bool)e.Value ? "true" : "false");
+ } else if (e.Value is string) {
+ var str = (StringLiteralExpr)e;
+ wr.Write("{0}<char>.FromString({1}\"{2}\")", DafnySeqClass, str.IsVerbatim ? "@" : "", (string)e.Value);
} else if (e.Value is BigInteger) {
BigInteger i = (BigInteger)e.Value;
if (new BigInteger(int.MinValue) <= i && i <= new BigInteger(int.MaxValue)) {
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d60b0b42..e330fc35 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -18,7 +18,6 @@ readonly Expression/*!*/ dummyExpr; readonly AssignmentRhs/*!*/ dummyRhs;
readonly FrameExpression/*!*/ dummyFrameExpr;
readonly Statement/*!*/ dummyStmt;
-readonly Attributes.Argument/*!*/ dummyAttrArg;
readonly ModuleDecl theModule;
readonly BuiltIns theBuiltIns;
readonly bool theVerifyThisFile;
@@ -89,7 +88,6 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, Built dummyRhs = new ExprRhs(dummyExpr, null);
dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null);
- dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
theModule = module;
theBuiltIns = builtIns;
theVerifyThisFile = verifyThisFile;
@@ -174,17 +172,19 @@ CHARACTERS lf = '\n'.
tab = '\t'.
space = ' '.
- quote = '"'.
nondigit = letter + special.
idchar = nondigit + digit.
nonidchar = ANY - idchar.
- nonquote = letter + digit + space + glyph.
/* exclude the characters in 'array' */
nondigitMinusA = nondigit - 'a'.
idcharMinusA = idchar - 'a'.
idcharMinusR = idchar - 'r'.
idcharMinusY = idchar - 'y'.
idcharMinusPosDigit = idchar - posDigit.
+ /* string literals */
+ stringChar = ANY - '"' - '\\' - cr - lf.
+ verbatimStringChar = ANY - '"'.
+
/*------------------------------------------------------------------------*/
TOKENS
ident = nondigitMinusA {idchar} /* if char 0 is not an 'a', then anything else is fine */
@@ -198,7 +198,14 @@ TOKENS hexdigits = "0x" hexdigit {hexdigit}.
decimaldigits = digit {digit} '.' digit {digit}.
arrayToken = "array" [posDigit {digit}].
- string = quote {nonquote} quote.
+ stringToken =
+ '"'
+ { stringChar
+ | "\\\'" | "\\\"" | "\\\\" | "\\0" | "\\n" | "\\r" | "\\t"
+ | "\\u" hexdigit hexdigit hexdigit hexdigit
+ }
+ '"'
+ | '@' '"' { verbatimStringChar | "\"\"" } '"'.
colon = ':'.
verticalbar = '|'.
semi = ';'.
@@ -227,18 +234,20 @@ Dafny TraitDecl/*!*/ trait;
Contract.Assert(defaultModule != null);
.)
- { "include" string (. {
- string parsedFile = t.filename;
- string includedFile = t.val.Substring(1, t.val.Length - 2);
- string fullPath = includedFile;
- if (!Path.IsPathRooted(includedFile)) {
- string basePath = Path.GetDirectoryName(parsedFile);
- includedFile = Path.Combine(basePath, includedFile);
- fullPath = Path.GetFullPath(includedFile);
- }
- defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
- }
- .)
+ { "include" stringToken (. {
+ string parsedFile = t.filename;
+ bool isVerbatimString;
+ string includedFile = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);
+ includedFile = Util.RemoveEscaping(includedFile, isVerbatimString);
+ string fullPath = includedFile;
+ if (!Path.IsPathRooted(includedFile)) {
+ string basePath = Path.GetDirectoryName(parsedFile);
+ includedFile = Path.Combine(basePath, includedFile);
+ fullPath = Path.GetFullPath(includedFile);
+ }
+ defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
+ }
+ .)
}
{ SubModuleDecl<defaultModule, out submodule> (. defaultModule.TopLevelDecls.Add(submodule); .)
| ClassDecl<defaultModule, out c> (. defaultModule.TopLevelDecls.Add(c); .)
@@ -840,6 +849,7 @@ TypeAndToken<out IToken tok, out Type ty> List<Type> gt = null;
.)
( "bool" (. tok = t; .)
+ | "char" (. tok = t; ty = new CharType(); .)
| "nat" (. tok = t; ty = new NatType(); .)
| "int" (. tok = t; ty = new IntType(); .)
| "real" (. tok = t; ty = new RealType(); .)
@@ -861,6 +871,7 @@ TypeAndToken<out IToken tok, out Type ty> }
ty = new SeqType(gt.Count == 1 ? gt[0] : null);
.)
+ | "string" (. tok = t; ty = new UserDefinedType(tok, tok.val, new List<Type>(), new List<IToken>()); .)
| "map" (. tok = t; gt = new List<Type/*!*/>(); .)
[ GenericInstantiation<gt> ] (. if (gt.Count == 0) {
ty = new MapType(null, null);
@@ -1546,8 +1557,8 @@ AssumeStmt<out Statement/*!*/ s> .)
.
PrintStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
- List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression arg;
+ List<Expression> args = new List<Expression>();
.)
"print" (. x = t; .)
AttributeArg<out arg, false> (. args.Add(arg); .)
@@ -2012,6 +2023,10 @@ ConstAtomExpression<out Expression e, bool allowSemi, bool allowLambda> | "null" (. e = new LiteralExpr(t); .)
| Nat<out n> (. e = new LiteralExpr(t, n); .)
| Dec<out d> (. e = new LiteralExpr(t, d); .)
+ | stringToken (. bool isVerbatimString;
+ string s = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);
+ e = new StringLiteralExpr(t, s, isVerbatimString);
+ .)
| "this" (. e = new ThisExpr(t); .)
| "fresh" (. x = t; .)
"(" Expression<out e, true, true> ")" (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e); .)
@@ -2553,8 +2568,8 @@ Attribute<ref Attributes attrs> .
AttributeBody<ref Attributes attrs>
= (. string aName;
- List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
- Attributes.Argument/*!*/ aArg;
+ List<Expression> aArgs = new List<Expression>();
+ Expression aArg;
.)
":" ident (. aName = t.val; .)
[ AttributeArg<out aArg, true> (. aArgs.Add(aArg); .)
@@ -2562,11 +2577,9 @@ AttributeBody<ref Attributes attrs> }
] (. attrs = new Attributes(aName, aArgs, attrs); .)
.
-AttributeArg<out Attributes.Argument arg, bool allowSemi>
-= (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg; .)
- ( string (. arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); .)
- | Expression<out e, allowSemi, true> (. arg = new Attributes.Argument(t, e); .)
- )
+AttributeArg<out Expression arg, bool allowSemi>
+= (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyExpr; .)
+ Expression<out e, allowSemi, true> (. arg = e; .)
.
/*------------------------------------------------------------------------*/
Ident<out IToken/*!*/ x>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 4b8ede60..906175c9 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -94,6 +94,9 @@ namespace Microsoft.Dafny { public readonly ClassDecl ObjectDecl;
public BuiltIns() {
SystemModule.Height = -1; // the system module doesn't get a height assigned later, so we set it here to something below everything else
+ // create type synonym 'string'
+ var str = new TypeSynonymDecl(Token.NoToken, "string", new List<TypeParameter>(), SystemModule, new SeqType(new CharType()), null);
+ SystemModule.TopLevelDecls.Add(str);
// create class 'object'
ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile(), null);
SystemModule.TopLevelDecls.Add(ObjectDecl);
@@ -108,8 +111,8 @@ namespace Microsoft.Dafny { }
private Attributes DontCompile() {
- var flse = new Attributes.Argument(Token.NoToken, Expression.CreateBoolLiteral(Token.NoToken, false));
- return new Attributes("compile", new List<Attributes.Argument>() { flse }, null);
+ var flse = Expression.CreateBoolLiteral(Token.NoToken, false);
+ return new Attributes("compile", new List<Expression>() { flse }, null);
}
public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {
@@ -217,10 +220,10 @@ namespace Microsoft.Dafny { public readonly string Name;
/*Frozen*/
- public readonly List<Argument> Args;
+ public readonly List<Expression> Args;
public readonly Attributes Prev;
- public Attributes(string name, [Captured] List<Argument> args, Attributes prev) {
+ public Attributes(string name, [Captured] List<Expression> args, Attributes prev) {
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(args));
Name = name;
@@ -231,9 +234,7 @@ namespace Microsoft.Dafny { public static IEnumerable<Expression> SubExpressions(Attributes attrs) {
for (; attrs != null; attrs = attrs.Prev) {
foreach (var arg in attrs.Args) {
- if (arg.E != null) {
- yield return arg.E;
- }
+ yield return arg;
}
}
}
@@ -260,7 +261,7 @@ namespace Microsoft.Dafny { for (; attrs != null; attrs = attrs.Prev) {
if (attrs.Name == nm) {
if (attrs.Args.Count == 1) {
- var arg = attrs.Args[0].E as LiteralExpr;
+ var arg = attrs.Args[0] as LiteralExpr;
if (arg != null && arg.Value is bool) {
value = (bool)arg.Value;
}
@@ -297,37 +298,13 @@ namespace Microsoft.Dafny { return false;
}
-
- public class Argument
- {
- public readonly IToken Tok;
- public readonly string S;
- public readonly Expression E;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Tok != null);
- Contract.Invariant((S == null) != (E == null));
- }
-
- public Argument(IToken tok, string s) {
- Contract.Requires(tok != null);
- Contract.Requires(s != null);
- Tok = tok;
- S = s;
- }
- public Argument(IToken tok, Expression e) {
- Contract.Requires(tok != null);
- Contract.Requires(e != null);
- Tok = tok;
- E = e;
- }
- }
}
// ------------------------------------------------------------------------------------------------------
public abstract class Type {
public static readonly BoolType Bool = new BoolType();
+ public static readonly CharType Char = new CharType();
public static readonly IntType Int = new IntType();
public static readonly RealType Real = new RealType();
@@ -400,6 +377,7 @@ namespace Microsoft.Dafny { public abstract bool Equals(Type that);
public bool IsBoolType { get { return NormalizeExpand() is BoolType; } }
+ public bool IsCharType { get { return NormalizeExpand() is CharType; } }
public bool IsIntegerType { get { return NormalizeExpand() is IntType; } }
public bool IsRealType { get { return NormalizeExpand() is RealType; } }
public bool IsSubrangeType {
@@ -607,7 +585,19 @@ namespace Microsoft.Dafny { }
}
- public class IntType : BasicType {
+ public class CharType : BasicType
+ {
+ [Pure]
+ public override string TypeName(ModuleDefinition context) {
+ return "char";
+ }
+ public override bool Equals(Type that) {
+ return that.IsCharType;
+ }
+ }
+
+ public class IntType : BasicType
+ {
[Pure]
public override string TypeName(ModuleDefinition context) {
return "int";
@@ -664,7 +654,7 @@ namespace Microsoft.Dafny { /// Constructs a(n unresolved) arrow type.
/// </summary>
public ArrowType(IToken tok, List<Type> args, Type result)
- : base(tok, ArrowType.ArrowTypeName(args.Count), Util.Snoc(args, result), null) {
+ : base(tok, ArrowTypeName(args.Count), Util.Snoc(args, result), null) {
Contract.Requires(tok != null);
Contract.Requires(args != null);
Contract.Requires(result != null);
@@ -1755,7 +1745,7 @@ namespace Microsoft.Dafny { public readonly Function Reads;
public ArrowTypeDecl(List<TypeParameter> tps, Function req, Function reads, ModuleDefinition module, Attributes attributes)
- : base(Token.NoToken, "_#Func" + (tps.Count - 1), module, tps,
+ : base(Token.NoToken, ArrowType.ArrowTypeName(tps.Count - 1), module, tps,
new List<MemberDecl> { req, reads }, attributes, null) {
Contract.Requires(tps != null && 1 <= tps.Count);
Contract.Requires(req != null);
@@ -3158,13 +3148,13 @@ namespace Microsoft.Dafny { }
public class PrintStmt : Statement {
- public readonly List<Attributes.Argument> Args;
+ public readonly List<Expression> Args;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Args));
}
- public PrintStmt(IToken tok, IToken endTok, List<Attributes.Argument> args)
+ public PrintStmt(IToken tok, IToken endTok, List<Expression> args)
: base(tok, endTok) {
Contract.Requires(tok != null);
Contract.Requires(endTok != null);
@@ -3176,9 +3166,7 @@ namespace Microsoft.Dafny { get {
foreach (var e in base.SubExpressions) { yield return e; }
foreach (var arg in Args) {
- if (arg.E != null) {
- yield return arg.E;
- }
+ yield return arg;
}
}
}
@@ -5056,6 +5044,14 @@ namespace Microsoft.Dafny { return sub.Substitute(e);
}
+ public string AsStringLiteral() {
+ var le = this as LiteralExpr;
+ if (le != null) {
+ return le.Value as string;
+ } else {
+ return null;
+ }
+ }
}
/// <summary>
@@ -5088,6 +5084,18 @@ namespace Microsoft.Dafny { }
public class LiteralExpr : Expression {
+ /// <summary>
+ /// One of the following:
+ /// * 'null' for the 'null' literal (a special case of which is the subclass StaticReceiverExpr)
+ /// * a bool for a bool literal
+ /// * a BigInteger for int literal
+ /// * a Basetypes.BigDec for a (rational) real literal
+ /// * a string for a string literal -- Note, the string is stored with all escapes as characters. For
+ /// example, the input string "hello\n" is stored in a LiteralExpr has being 7 characters long, whereas
+ /// the Dafny (and C#) length of this string is 6. This simplifies printing of the string, both when
+ /// pretty printed as a Dafny expression and when being compiled into C# code. The parser checks the
+ /// validity of the escape sequences and the verifier deals with turning them into single characters.
+ /// </summary>
public readonly object Value;
[Pure]
@@ -5111,7 +5119,6 @@ namespace Microsoft.Dafny { : base(tok) {
Contract.Requires(tok != null);
Contract.Requires(0 <= n.Sign);
-
this.Value = n;
}
@@ -5119,14 +5126,13 @@ namespace Microsoft.Dafny { : base(tok) {
Contract.Requires(0 <= n.Mantissa.Sign);
Contract.Requires(tok != null);
-
this.Value = n;
}
- public LiteralExpr(IToken tok, int n) :base(tok){
+ public LiteralExpr(IToken tok, int n)
+ :base(tok) {
Contract.Requires(tok != null);
Contract.Requires(0 <= n);
-
this.Value = new BigInteger(n);
}
@@ -5135,6 +5141,27 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
this.Value = b;
}
+
+ /// <summary>
+ /// This constructor is to be used only with the StringLiteralExpr subclass, since string literals also need
+ /// an additional field.
+ /// </summary>
+ protected LiteralExpr(IToken tok, string s)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(s != null);
+ this.Value = s;
+ }
+ }
+
+ public class StringLiteralExpr : LiteralExpr
+ {
+ public readonly bool IsVerbatim;
+ public StringLiteralExpr(IToken tok, string s, bool isVerbatim)
+ : base(tok, s) {
+ Contract.Requires(s != null);
+ IsVerbatim = isVerbatim;
+ }
}
public class DatatypeValue : Expression {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 42f8b092..c806c035 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -19,7 +19,7 @@ public class Parser { public const int _hexdigits = 3;
public const int _decimaldigits = 4;
public const int _arrayToken = 5;
- public const int _string = 6;
+ public const int _stringToken = 6;
public const int _colon = 7;
public const int _verticalbar = 8;
public const int _semi = 9;
@@ -33,7 +33,7 @@ public class Parser { public const int _closeparen = 17;
public const int _star = 18;
public const int _notIn = 19;
- public const int maxT = 130;
+ public const int maxT = 132;
const bool T = true;
const bool x = false;
@@ -50,7 +50,6 @@ readonly Expression/*!*/ dummyExpr; readonly AssignmentRhs/*!*/ dummyRhs;
readonly FrameExpression/*!*/ dummyFrameExpr;
readonly Statement/*!*/ dummyStmt;
-readonly Attributes.Argument/*!*/ dummyAttrArg;
readonly ModuleDecl theModule;
readonly BuiltIns theBuiltIns;
readonly bool theVerifyThisFile;
@@ -121,7 +120,6 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, Built dummyRhs = new ExprRhs(dummyExpr, null);
dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null);
- dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
theModule = module;
theBuiltIns = builtIns;
theVerifyThisFile = verifyThisFile;
@@ -279,15 +277,17 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { Get();
Expect(6);
{
- string parsedFile = t.filename;
- string includedFile = t.val.Substring(1, t.val.Length - 2);
- string fullPath = includedFile;
- if (!Path.IsPathRooted(includedFile)) {
- string basePath = Path.GetDirectoryName(parsedFile);
- includedFile = Path.Combine(basePath, includedFile);
- fullPath = Path.GetFullPath(includedFile);
- }
- defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
+ string parsedFile = t.filename;
+ bool isVerbatimString;
+ string includedFile = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);
+ includedFile = Util.RemoveEscaping(includedFile, isVerbatimString);
+ string fullPath = includedFile;
+ if (!Path.IsPathRooted(includedFile)) {
+ string basePath = Path.GetDirectoryName(parsedFile);
+ includedFile = Path.Combine(basePath, includedFile);
+ fullPath = Path.GetFullPath(includedFile);
+ }
+ defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
}
}
@@ -328,7 +328,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { defaultModule.TopLevelDecls.Add(trait);
break;
}
- case 32: case 33: case 36: case 47: case 48: case 49: case 50: case 51: case 67: case 68: case 69: {
+ case 32: case 33: case 36: case 47: case 48: case 49: case 50: case 51: case 69: case 70: case 71: {
ClassMemberDecl(membersDefaultClass, false);
break;
}
@@ -415,7 +415,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { module.TopLevelDecls.Add(iter);
break;
}
- case 32: case 33: case 36: case 47: case 48: case 49: case 50: case 51: case 67: case 68: case 69: {
+ case 32: case 33: case 36: case 47: case 48: case 49: case 50: case 51: case 69: case 70: case 71: {
ClassMemberDecl(namedModuleDefaultClassMembers, false);
break;
}
@@ -448,7 +448,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { }
}
if (la.kind == 9) {
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(131); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(133); Get();}
Get();
}
if (submodule == null) {
@@ -457,7 +457,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { submodule = new AliasModuleDecl(idPath, id, parent, opened);
}
- } else SynErr(132);
+ } else SynErr(134);
}
void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
@@ -470,7 +470,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 29)) {SynErr(133); Get();}
+ while (!(la.kind == 0 || la.kind == 29)) {SynErr(135); Get();}
Expect(29);
while (la.kind == 14) {
Attribute(ref attrs);
@@ -505,13 +505,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
- while (!(la.kind == 0 || la.kind == 34 || la.kind == 35)) {SynErr(134); Get();}
+ while (!(la.kind == 0 || la.kind == 34 || la.kind == 35)) {SynErr(136); Get();}
if (la.kind == 34) {
Get();
} else if (la.kind == 35) {
Get();
co = true;
- } else SynErr(135);
+ } else SynErr(137);
while (la.kind == 14) {
Attribute(ref attrs);
}
@@ -527,7 +527,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { DatatypeMemberDecl(ctors);
}
if (la.kind == 9) {
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(136); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(138); Get();}
Get();
}
if (co) {
@@ -566,9 +566,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (StartOf(3)) {
Type(out baseType);
td = new NewtypeDecl(id, id.val, module, baseType, attrs);
- } else SynErr(137);
+ } else SynErr(139);
if (la.kind == 9) {
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(138); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(140); Get();}
Get();
}
}
@@ -603,13 +603,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { Type(out ty);
td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs);
}
- } else SynErr(139);
+ } else SynErr(141);
if (td == null) {
td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
}
if (la.kind == 9) {
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(140); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(142); Get();}
Get();
}
}
@@ -637,7 +637,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 41)) {SynErr(141); Get();}
+ while (!(la.kind == 0 || la.kind == 41)) {SynErr(143); Get();}
Expect(41);
while (la.kind == 14) {
Attribute(ref attrs);
@@ -660,7 +660,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 44) {
Get();
signatureEllipsis = t;
- } else SynErr(142);
+ } else SynErr(144);
while (StartOf(5)) {
IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);
}
@@ -687,7 +687,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 31)) {SynErr(143); Get();}
+ while (!(la.kind == 0 || la.kind == 31)) {SynErr(145); Get();}
Expect(31);
while (la.kind == 14) {
Attribute(ref attrs);
@@ -725,13 +725,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { }
if (la.kind == 36) {
FieldDecl(mmod, mm);
- } else if (la.kind == 67 || la.kind == 68 || la.kind == 69) {
+ } else if (la.kind == 69 || la.kind == 70 || la.kind == 71) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (StartOf(6)) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(144);
+ } else SynErr(146);
}
void Attribute(ref Attributes attrs) {
@@ -754,7 +754,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { IToken id; IToken idPrime; ids = new List<IToken>();
Ident(out id);
ids.Add(id);
- while (la.kind == 66) {
+ while (la.kind == 68) {
IdentOrDigitsSuffix(out id, out idPrime);
ids.Add(id);
if (idPrime != null) { ids.Add(idPrime); }
@@ -773,7 +773,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { x = Token.NoToken;
y = null;
- Expect(66);
+ Expect(68);
if (la.kind == 1) {
Get();
x = t;
@@ -807,7 +807,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 12) {
Get();
x = t;
- } else SynErr(145);
+ } else SynErr(147);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -845,7 +845,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 36)) {SynErr(146); Get();}
+ while (!(la.kind == 0 || la.kind == 36)) {SynErr(148); Get();}
Expect(36);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -859,7 +859,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { FIdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(147); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(149); Get();}
Expect(9);
}
@@ -882,7 +882,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { IToken signatureEllipsis = null;
bool missingOpenParen;
- if (la.kind == 67) {
+ if (la.kind == 69) {
Get();
if (la.kind == 47) {
Get();
@@ -904,8 +904,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 44) {
Get();
signatureEllipsis = t;
- } else SynErr(148);
- } else if (la.kind == 68) {
+ } else SynErr(150);
+ } else if (la.kind == 70) {
Get();
isPredicate = true;
if (la.kind == 47) {
@@ -935,8 +935,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 44) {
Get();
signatureEllipsis = t;
- } else SynErr(149);
- } else if (la.kind == 69) {
+ } else SynErr(151);
+ } else if (la.kind == 71) {
Get();
isCoPredicate = true;
if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
@@ -962,8 +962,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 44) {
Get();
signatureEllipsis = t;
- } else SynErr(150);
- } else SynErr(151);
+ } else SynErr(152);
+ } else SynErr(153);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
while (StartOf(8)) {
FunctionSpec(reqs, reads, ens, decreases);
@@ -1018,7 +1018,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(StartOf(9))) {SynErr(152); Get();}
+ while (!(StartOf(9))) {SynErr(154); Get();}
if (la.kind == 47) {
Get();
} else if (la.kind == 48) {
@@ -1040,7 +1040,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { SemErr(t, "constructors are allowed only in classes");
}
- } else SynErr(153);
+ } else SynErr(155);
keywordToken = t;
if (isLemma) {
if (mmod.IsGhost) {
@@ -1086,7 +1086,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 44) {
Get();
signatureEllipsis = t;
- } else SynErr(154);
+ } else SynErr(156);
while (StartOf(10)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
@@ -1160,7 +1160,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { } else if (la.kind == 2) {
Get();
id = t;
- } else SynErr(155);
+ } else SynErr(157);
Expect(7);
Type(out ty);
}
@@ -1262,7 +1262,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { id = t; name = id.val;
Expect(7);
Type(out ty);
- } else SynErr(156);
+ } else SynErr(158);
if (name != null) {
identName = name;
} else {
@@ -1284,21 +1284,26 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { }
case 58: {
Get();
- tok = t; ty = new NatType();
+ tok = t; ty = new CharType();
break;
}
case 59: {
Get();
- tok = t; ty = new IntType();
+ tok = t; ty = new NatType();
break;
}
case 60: {
Get();
- tok = t; ty = new RealType();
+ tok = t; ty = new IntType();
break;
}
case 61: {
Get();
+ tok = t; ty = new RealType();
+ break;
+ }
+ case 62: {
+ Get();
tok = t; gt = new List<Type/*!*/>();
if (la.kind == 45) {
GenericInstantiation(gt);
@@ -1310,7 +1315,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { break;
}
- case 62: {
+ case 63: {
Get();
tok = t; gt = new List<Type/*!*/>();
if (la.kind == 45) {
@@ -1323,7 +1328,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { break;
}
- case 63: {
+ case 64: {
Get();
tok = t; gt = new List<Type/*!*/>();
if (la.kind == 45) {
@@ -1336,7 +1341,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { break;
}
- case 64: {
+ case 65: {
+ Get();
+ tok = t; ty = new UserDefinedType(tok, tok.val, new List<Type>(), new List<IToken>());
+ break;
+ }
+ case 66: {
Get();
tok = t; gt = new List<Type/*!*/>();
if (la.kind == 45) {
@@ -1377,11 +1387,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) { break;
}
- case 1: case 5: case 65: {
+ case 1: case 5: case 67: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(157); break;
+ default: SynErr(159); break;
}
if (la.kind == 11) {
Type t2;
@@ -1418,7 +1428,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(12))) {SynErr(158); Get();}
+ while (!(StartOf(12))) {SynErr(160); Get();}
if (la.kind == 12) {
Get();
while (IsAttribute()) {
@@ -1433,7 +1443,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(159); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(161); Get();}
Expect(9);
} else if (la.kind == 52) {
Get();
@@ -1449,7 +1459,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(160); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(162); Get();}
Expect(9);
} else if (StartOf(14)) {
if (la.kind == 53) {
@@ -1463,7 +1473,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { if (la.kind == 13) {
Get();
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(161); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(163); Get();}
Expect(9);
if (isYield) {
yieldReq.Add(new MaybeFreeExpression(e, isFree));
@@ -1477,7 +1487,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Attribute(ref ensAttrs);
}
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(162); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(164); Get();}
Expect(9);
if (isYield) {
yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
@@ -1485,16 +1495,16 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
- } else SynErr(163);
+ } else SynErr(165);
} else if (la.kind == 55) {
Get();
while (IsAttribute()) {
Attribute(ref decrAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(164); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(166); Get();}
Expect(9);
- } else SynErr(165);
+ } else SynErr(167);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -1516,7 +1526,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(16))) {SynErr(166); Get();}
+ while (!(StartOf(16))) {SynErr(168); Get();}
if (la.kind == 52) {
Get();
while (IsAttribute()) {
@@ -1531,7 +1541,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(167); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(169); Get();}
Expect(9);
} else if (la.kind == 13 || la.kind == 53 || la.kind == 54) {
if (la.kind == 53) {
@@ -1541,7 +1551,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 13) {
Get();
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(168); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(170); Get();}
Expect(9);
req.Add(new MaybeFreeExpression(e, isFree));
} else if (la.kind == 54) {
@@ -1550,19 +1560,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Attribute(ref ensAttrs);
}
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(169); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(171); Get();}
Expect(9);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(170);
+ } else SynErr(172);
} else if (la.kind == 55) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(171); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(173); Get();}
Expect(9);
- } else SynErr(172);
+ } else SynErr(174);
}
void FrameExpression(out FrameExpression/*!*/ fe) {
@@ -1575,18 +1585,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(17)) {
Expression(out e, false, false);
feTok = e.tok;
- if (la.kind == 70) {
+ if (la.kind == 72) {
Get();
Ident(out id);
fieldName = id.val; feTok = id;
}
fe = new FrameExpression(feTok, e, fieldName);
- } else if (la.kind == 70) {
+ } else if (la.kind == 72) {
Get();
Ident(out id);
fieldName = id.val;
fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName);
- } else SynErr(173);
+ } else SynErr(175);
}
void DecreasesList(List<Expression/*!*/> decreases, bool allowWildcard) {
@@ -1629,7 +1639,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Type> gt;
List<IToken> path;
- if (la.kind == 65) {
+ if (la.kind == 67) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 5) {
@@ -1645,7 +1655,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out tok);
gt = new List<Type>();
path = new List<IToken>();
- while (la.kind == 66) {
+ while (la.kind == 68) {
path.Add(tok);
Get();
Ident(out tok);
@@ -1654,7 +1664,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(174);
+ } else SynErr(176);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1663,10 +1673,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 13) {
- while (!(la.kind == 0 || la.kind == 13)) {SynErr(175); Get();}
+ while (!(la.kind == 0 || la.kind == 13)) {SynErr(177); Get();}
Get();
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(176); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(178); Get();}
Expect(9);
reqs.Add(e);
} else if (la.kind == 12) {
@@ -1680,12 +1690,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(177); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(179); Get();}
Expect(9);
} else if (la.kind == 54) {
Get();
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(178); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(180); Get();}
Expect(9);
ens.Add(e);
} else if (la.kind == 55) {
@@ -1696,9 +1706,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(179); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(181); Get();}
Expect(9);
- } else SynErr(180);
+ } else SynErr(182);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1717,7 +1727,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo fe = new FrameExpression(t, new WildcardExpr(t), null);
} else if (StartOf(13)) {
FrameExpression(out fe);
- } else SynErr(181);
+ } else SynErr(183);
}
void LambdaSpec(out Expression req, List<FrameExpression> reads) {
@@ -1749,7 +1759,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new WildcardExpr(t);
} else if (StartOf(17)) {
Expression(out e, false, false);
- } else SynErr(182);
+ } else SynErr(184);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1766,26 +1776,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(19))) {SynErr(183); Get();}
+ while (!(StartOf(19))) {SynErr(185); Get();}
switch (la.kind) {
case 14: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
s = bs;
break;
}
- case 87: {
+ case 89: {
AssertStmt(out s);
break;
}
- case 77: {
+ case 79: {
AssumeStmt(out s);
break;
}
- case 88: {
+ case 90: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 3: case 4: case 8: case 16: case 59: case 60: case 117: case 118: case 119: case 120: case 121: case 122: {
+ case 1: case 2: case 3: case 4: case 6: case 8: case 16: case 60: case 61: case 119: case 120: case 121: case 122: case 123: case 124: {
UpdateStmt(out s);
break;
}
@@ -1793,31 +1803,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s);
break;
}
- case 81: {
+ case 83: {
IfStmt(out s);
break;
}
- case 84: {
+ case 86: {
WhileStmt(out s);
break;
}
- case 86: {
+ case 88: {
MatchStmt(out s);
break;
}
- case 89: case 90: {
+ case 91: case 92: {
ForallStmt(out s);
break;
}
- case 92: {
+ case 94: {
CalcStmt(out s);
break;
}
- case 91: {
+ case 93: {
ModifyStmt(out s);
break;
}
- case 71: {
+ case 73: {
Get();
x = t;
NoUSIdent(out id);
@@ -1826,24 +1836,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 72: {
+ case 74: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
NoUSIdent(out id);
label = id.val;
- } else if (la.kind == 9 || la.kind == 72) {
- while (la.kind == 72) {
+ } else if (la.kind == 9 || la.kind == 74) {
+ while (la.kind == 74) {
Get();
breakCount++;
}
- } else SynErr(184);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(185); Get();}
+ } else SynErr(186);
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(187); Get();}
Expect(9);
s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount);
break;
}
- case 56: case 75: {
+ case 56: case 77: {
ReturnStmt(out s);
break;
}
@@ -1851,7 +1861,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo SkeletonStmt(out s);
break;
}
- default: SynErr(186); break;
+ default: SynErr(188); break;
}
}
@@ -1860,7 +1870,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e = dummyExpr; Attributes attrs = null;
IToken dotdotdot = null;
- Expect(87);
+ Expect(89);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -1870,7 +1880,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 44) {
Get();
dotdotdot = t;
- } else SynErr(187);
+ } else SynErr(189);
Expect(9);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -1885,7 +1895,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e = dummyExpr; Attributes attrs = null;
IToken dotdotdot = null;
- Expect(77);
+ Expect(79);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -1895,7 +1905,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 44) {
Get();
dotdotdot = t;
- } else SynErr(188);
+ } else SynErr(190);
Expect(9);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -1906,10 +1916,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void PrintStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
- List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression arg;
+ List<Expression> args = new List<Expression>();
- Expect(88);
+ Expect(90);
x = t;
AttributeArg(out arg, false);
args.Add(arg);
@@ -1940,14 +1950,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(9);
endTok = t; rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 37 || la.kind == 74 || la.kind == 76) {
+ } else if (la.kind == 37 || la.kind == 76 || la.kind == 78) {
lhss.Add(e); lhs0 = e;
while (la.kind == 37) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 74) {
+ if (la.kind == 76) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1957,21 +1967,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 76) {
+ } else if (la.kind == 78) {
Get();
x = t;
- if (la.kind == 77) {
+ if (la.kind == 79) {
Get();
suchThatAssume = t;
}
Expression(out suchThat, false, true);
- } else SynErr(189);
+ } else SynErr(191);
Expect(9);
endTok = t;
} else if (la.kind == 7) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(190);
+ } else SynErr(192);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
} else {
@@ -2014,8 +2024,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d); d.Attributes = attrs; attrs = null;
}
- if (la.kind == 74 || la.kind == 76) {
- if (la.kind == 74) {
+ if (la.kind == 76 || la.kind == 78) {
+ if (la.kind == 76) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -2030,7 +2040,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else {
Get();
assignTok = t;
- if (la.kind == 77) {
+ if (la.kind == 79) {
Get();
suchThatAssume = t;
}
@@ -2070,7 +2080,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(81);
+ Expect(83);
x = t;
if (IsAlternative()) {
AlternativeBlock(out alternatives, out endTok);
@@ -2084,15 +2094,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
BlockStmt(out thn, out bodyStart, out bodyEnd);
endTok = thn.EndTok;
- if (la.kind == 82) {
+ if (la.kind == 84) {
Get();
- if (la.kind == 81) {
+ if (la.kind == 83) {
IfStmt(out s);
els = s; endTok = s.EndTok;
} else if (la.kind == 14) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs; endTok = bs.EndTok;
- } else SynErr(191);
+ } else SynErr(193);
}
if (guardEllipsis != null) {
ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);
@@ -2100,7 +2110,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ifStmt = new IfStmt(x, endTok, guard, thn, els);
}
- } else SynErr(192);
+ } else SynErr(194);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -2116,7 +2126,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(84);
+ Expect(86);
x = t;
if (IsLoopSpecOrAlternative()) {
LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
@@ -2137,7 +2147,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 44) {
Get();
bodyEllipsis = t; endTok = t;
- } else SynErr(193);
+ } else SynErr(195);
if (guardEllipsis != null || bodyEllipsis != null) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -2153,7 +2163,7 @@ 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(194);
+ } else SynErr(196);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -2162,14 +2172,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
bool usesOptionalBrace = false;
- Expect(86);
+ Expect(88);
x = t;
Expression(out e, true, true);
if (la.kind == 14) {
Get();
usesOptionalBrace = true;
}
- while (la.kind == 83) {
+ while (la.kind == 85) {
CaseStatement(out c);
cases.Add(c);
}
@@ -2177,7 +2187,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(15);
} else if (StartOf(22)) {
if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
- } else SynErr(195);
+ } else SynErr(197);
s = new MatchStmt(x, t, e, cases, usesOptionalBrace);
}
@@ -2195,15 +2205,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd;
IToken tok = Token.NoToken;
- if (la.kind == 89) {
+ if (la.kind == 91) {
Get();
x = t; tok = x;
- } else if (la.kind == 90) {
+ } else if (la.kind == 92) {
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(196);
+ } else SynErr(198);
if (la.kind == 16) {
Get();
usesOptionalParen = true;
@@ -2221,7 +2231,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(17);
} else if (StartOf(23)) {
if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
- } else SynErr(197);
+ } else SynErr(199);
while (la.kind == 53 || la.kind == 54) {
isFree = false;
if (la.kind == 53) {
@@ -2262,7 +2272,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken opTok;
IToken danglingOperator = null;
- Expect(92);
+ Expect(94);
x = t;
if (StartOf(24)) {
CalcOp(out opTok, out calcOp);
@@ -2315,7 +2325,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt body = null; IToken bodyStart;
IToken ellipsisToken = null;
- Expect(91);
+ Expect(93);
tok = t;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -2337,10 +2347,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 14) {
BlockStmt(out body, out bodyStart, out endTok);
} else if (la.kind == 9) {
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(198); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(200); Get();}
Get();
endTok = t;
- } else SynErr(199);
+ } else SynErr(201);
s = new ModifyStmt(tok, endTok, mod, attrs, body);
if (ellipsisToken != null) {
s = new SkeletonStatement(s, ellipsisToken, null);
@@ -2354,13 +2364,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssignmentRhs r;
bool isYield = false;
- if (la.kind == 75) {
+ if (la.kind == 77) {
Get();
returnTok = t;
} else if (la.kind == 56) {
Get();
returnTok = t; isYield = true;
- } else SynErr(200);
+ } else SynErr(202);
if (StartOf(26)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
@@ -2386,7 +2396,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e;
Expect(44);
dotdotdot = t;
- if (la.kind == 73) {
+ if (la.kind == 75) {
Get();
names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
Ident(out tok);
@@ -2396,7 +2406,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out tok);
names.Add(tok);
}
- Expect(74);
+ Expect(76);
Expression(out e, false, true);
exprs.Add(e);
while (la.kind == 37) {
@@ -2423,21 +2433,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = dummyRhs; // to please compiler
Attributes attrs = null;
- if (la.kind == 78) {
+ if (la.kind == 80) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 16 || la.kind == 66 || la.kind == 79) {
- if (la.kind == 79) {
+ if (la.kind == 16 || la.kind == 68 || la.kind == 81) {
+ if (la.kind == 81) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(80);
+ Expect(82);
var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
} else {
x = null; args = new List<Expression/*!*/>();
- if (la.kind == 66) {
+ if (la.kind == 68) {
Get();
Ident(out x);
}
@@ -2462,7 +2472,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(17)) {
Expression(out e, false, true);
r = new ExprRhs(e);
- } else SynErr(201);
+ } else SynErr(203);
while (la.kind == 14) {
Attribute(ref attrs);
}
@@ -2474,17 +2484,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) {
DottedIdentifiersAndFunction(out e, false, false);
- while (la.kind == 66 || la.kind == 79) {
+ while (la.kind == 68 || la.kind == 81) {
Suffix(ref e);
}
ApplySuffix(ref e);
} else if (StartOf(27)) {
ConstAtomExpression(out e, false, false);
Suffix(ref e);
- while (la.kind == 66 || la.kind == 79) {
+ while (la.kind == 68 || la.kind == 81) {
Suffix(ref e);
}
- } else SynErr(202);
+ } else SynErr(204);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -2505,7 +2515,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Statement> body;
Expect(14);
- while (la.kind == 83) {
+ while (la.kind == 85) {
Get();
x = t;
Expression(out e, true, false);
@@ -2533,7 +2543,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(17)) {
Expression(out ee, true, true);
e = ee;
- } else SynErr(203);
+ } else SynErr(205);
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2544,22 +2554,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null;
while (StartOf(28)) {
- if (la.kind == 53 || la.kind == 85) {
+ if (la.kind == 53 || la.kind == 87) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(204); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(206); Get();}
Expect(9);
invariants.Add(invariant);
} else if (la.kind == 55) {
- while (!(la.kind == 0 || la.kind == 55)) {SynErr(205); Get();}
+ while (!(la.kind == 0 || la.kind == 55)) {SynErr(207); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(206); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(208); Get();}
Expect(9);
} else {
- while (!(la.kind == 0 || la.kind == 52)) {SynErr(207); Get();}
+ while (!(la.kind == 0 || la.kind == 52)) {SynErr(209); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -2574,7 +2584,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 9)) {SynErr(208); Get();}
+ while (!(la.kind == 0 || la.kind == 9)) {SynErr(210); Get();}
Expect(9);
}
}
@@ -2582,12 +2592,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo 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 == 53 || la.kind == 85)) {SynErr(209); Get();}
+ while (!(la.kind == 0 || la.kind == 53 || la.kind == 87)) {SynErr(211); Get();}
if (la.kind == 53) {
Get();
isFree = true;
}
- Expect(85);
+ Expect(87);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -2602,7 +2612,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(83);
+ Expect(85);
x = t;
Ident(out id);
if (la.kind == 16) {
@@ -2623,15 +2633,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo c = new MatchCaseStmt(x, id.val, arguments, body);
}
- void AttributeArg(out Attributes.Argument arg, bool allowSemi) {
- Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg;
- if (la.kind == 6) {
- Get();
- arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2));
- } else if (StartOf(17)) {
- Expression(out e, allowSemi, true);
- arg = new Attributes.Argument(t, e);
- } else SynErr(210);
+ void AttributeArg(out Expression arg, bool allowSemi) {
+ Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyExpr;
+ Expression(out e, allowSemi, true);
+ arg = e;
}
void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {
@@ -2665,11 +2670,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 40: {
Get();
x = t; binOp = BinaryExpr.Opcode.Eq;
- if (la.kind == 93) {
+ if (la.kind == 95) {
Get();
- Expect(79);
+ Expect(81);
Expression(out k, true, true);
- Expect(80);
+ Expect(82);
}
break;
}
@@ -2683,52 +2688,52 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; binOp = BinaryExpr.Opcode.Gt;
break;
}
- case 94: {
+ case 96: {
Get();
x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 95: {
+ case 97: {
Get();
x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
- case 96: {
+ case 98: {
Get();
x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
- case 97: {
+ case 99: {
Get();
x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
- case 98: {
+ case 100: {
Get();
x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 99: {
+ case 101: {
Get();
x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
- case 100: case 101: {
+ case 102: case 103: {
EquivOp();
x = t; binOp = BinaryExpr.Opcode.Iff;
break;
}
- case 102: case 103: {
+ case 104: case 105: {
ImpliesOp();
x = t; binOp = BinaryExpr.Opcode.Imp;
break;
}
- case 104: case 105: {
+ case 106: case 107: {
ExpliesOp();
x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(211); break;
+ default: SynErr(212); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -2747,7 +2752,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Token x = la;
IToken endTok = x;
- while (la.kind == 14 || la.kind == 92) {
+ while (la.kind == 14 || la.kind == 94) {
if (la.kind == 14) {
BlockStmt(out block, out bodyStart, out bodyEnd);
endTok = block.EndTok; subhints.Add(block);
@@ -2761,14 +2766,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 100) {
- Get();
- } else if (la.kind == 101) {
- Get();
- } else SynErr(212);
- }
-
- void ImpliesOp() {
if (la.kind == 102) {
Get();
} else if (la.kind == 103) {
@@ -2776,7 +2773,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else SynErr(213);
}
- void ExpliesOp() {
+ void ImpliesOp() {
if (la.kind == 104) {
Get();
} else if (la.kind == 105) {
@@ -2784,10 +2781,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else SynErr(214);
}
+ void ExpliesOp() {
+ if (la.kind == 106) {
+ Get();
+ } else if (la.kind == 107) {
+ Get();
+ } else SynErr(215);
+ }
+
void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpliesExpression(out e0, allowSemi, allowLambda);
- while (la.kind == 100 || la.kind == 101) {
+ while (la.kind == 102 || la.kind == 103) {
EquivOp();
x = t;
ImpliesExpliesExpression(out e1, allowSemi, allowLambda);
@@ -2799,7 +2804,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, allowLambda);
if (StartOf(29)) {
- if (la.kind == 102 || la.kind == 103) {
+ if (la.kind == 104 || la.kind == 105) {
ImpliesOp();
x = t;
ImpliesExpression(out e1, allowSemi, allowLambda);
@@ -2809,7 +2814,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
LogicalExpression(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
- while (la.kind == 104 || la.kind == 105) {
+ while (la.kind == 106 || la.kind == 107) {
ExpliesOp();
x = t;
LogicalExpression(out e1, allowSemi, allowLambda);
@@ -2823,12 +2828,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, allowLambda);
if (StartOf(30)) {
- if (la.kind == 106 || la.kind == 107) {
+ if (la.kind == 108 || la.kind == 109) {
AndOp();
x = t;
RelationalExpression(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 106 || la.kind == 107) {
+ while (la.kind == 108 || la.kind == 109) {
AndOp();
x = t;
RelationalExpression(out e1, allowSemi, allowLambda);
@@ -2839,7 +2844,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
RelationalExpression(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 108 || la.kind == 109) {
+ while (la.kind == 110 || la.kind == 111) {
OrOp();
x = t;
RelationalExpression(out e1, allowSemi, allowLambda);
@@ -2852,7 +2857,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression e0, bool allowSemi, bool allowLambda) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0, allowSemi, allowLambda);
- if (la.kind == 102 || la.kind == 103) {
+ if (la.kind == 104 || la.kind == 105) {
ImpliesOp();
x = t;
ImpliesExpression(out e1, allowSemi, allowLambda);
@@ -2962,25 +2967,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 106) {
+ if (la.kind == 108) {
Get();
- } else if (la.kind == 107) {
+ } else if (la.kind == 109) {
Get();
- } else SynErr(215);
+ } else SynErr(216);
}
void OrOp() {
- if (la.kind == 108) {
+ if (la.kind == 110) {
Get();
- } else if (la.kind == 109) {
+ } else if (la.kind == 111) {
Get();
- } else SynErr(216);
+ } else SynErr(217);
}
void Term(out Expression e0, bool allowSemi, bool allowLambda) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0, allowSemi, allowLambda);
- while (la.kind == 112 || la.kind == 113) {
+ while (la.kind == 114 || la.kind == 115) {
AddOp(out x, out op);
Factor(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2997,11 +3002,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 40: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
- if (la.kind == 93) {
+ if (la.kind == 95) {
Get();
- Expect(79);
+ Expect(81);
Expression(out k, true, true);
- Expect(80);
+ Expect(82);
}
break;
}
@@ -3015,28 +3020,28 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 94: {
+ case 96: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 95: {
+ case 97: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 96: {
+ case 98: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
- if (la.kind == 93) {
+ if (la.kind == 95) {
Get();
- Expect(79);
+ Expect(81);
Expression(out k, true, true);
- Expect(80);
+ Expect(82);
}
break;
}
- case 110: {
+ case 112: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
@@ -3046,10 +3051,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 111: {
+ case 113: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 111) {
+ if (la.kind == 113) {
Get();
y = t;
}
@@ -3064,29 +3069,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
- case 97: {
+ case 99: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 98: {
+ case 100: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 99: {
+ case 101: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(217); break;
+ default: SynErr(218); break;
}
}
void Factor(out Expression e0, bool allowSemi, bool allowLambda) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0, allowSemi, allowLambda);
- while (la.kind == 18 || la.kind == 114 || la.kind == 115) {
+ while (la.kind == 18 || la.kind == 116 || la.kind == 117) {
MulOp(out x, out op);
UnaryExpression(out e1, allowSemi, allowLambda);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -3095,81 +3100,81 @@ 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 == 112) {
+ if (la.kind == 114) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 113) {
+ } else if (la.kind == 115) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(218);
+ } else SynErr(219);
}
void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 113: {
+ case 115: {
Get();
x = t;
UnaryExpression(out e, allowSemi, allowLambda);
e = new NegationExpression(x, e);
break;
}
- case 111: case 116: {
+ case 113: case 118: {
NegOp();
x = t;
UnaryExpression(out e, allowSemi, allowLambda);
e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e);
break;
}
- case 32: case 36: case 61: case 71: case 77: case 81: case 86: case 87: case 89: case 92: case 125: case 126: case 127: {
+ case 32: case 36: case 62: case 73: case 79: case 83: case 88: case 89: case 91: case 94: case 127: case 128: case 129: {
EndlessExpression(out e, allowSemi, allowLambda);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e, allowSemi, allowLambda);
- while (la.kind == 66 || la.kind == 79) {
+ while (la.kind == 68 || la.kind == 81) {
Suffix(ref e);
}
ApplySuffix(ref e);
break;
}
- case 14: case 79: {
+ case 14: case 81: {
DisplayExpr(out e);
- while (la.kind == 66 || la.kind == 79) {
+ while (la.kind == 68 || la.kind == 81) {
Suffix(ref e);
}
break;
}
- case 62: {
+ case 63: {
MultiSetExpr(out e);
- while (la.kind == 66 || la.kind == 79) {
+ while (la.kind == 68 || la.kind == 81) {
Suffix(ref e);
}
break;
}
- case 64: {
+ case 66: {
Get();
x = t;
- if (la.kind == 79) {
+ if (la.kind == 81) {
MapDisplayExpr(x, out e);
- while (la.kind == 66 || la.kind == 79) {
+ while (la.kind == 68 || la.kind == 81) {
Suffix(ref e);
}
} else if (la.kind == 1) {
MapComprehensionExpr(x, out e, allowSemi);
} else if (StartOf(32)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(219);
+ } else SynErr(220);
break;
}
- case 2: case 3: case 4: case 8: case 16: case 59: case 60: case 117: case 118: case 119: case 120: case 121: case 122: {
+ case 2: case 3: case 4: case 6: case 8: case 16: case 60: case 61: case 119: case 120: case 121: case 122: case 123: case 124: {
ConstAtomExpression(out e, allowSemi, allowLambda);
- while (la.kind == 66 || la.kind == 79) {
+ while (la.kind == 68 || la.kind == 81) {
Suffix(ref e);
}
break;
}
- default: SynErr(220); break;
+ default: SynErr(221); break;
}
}
@@ -3178,21 +3183,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 18) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 114) {
+ } else if (la.kind == 116) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 115) {
+ } else if (la.kind == 117) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(221);
+ } else SynErr(222);
}
void NegOp() {
- if (la.kind == 111) {
+ if (la.kind == 113) {
Get();
- } else if (la.kind == 116) {
+ } else if (la.kind == 118) {
Get();
- } else SynErr(222);
+ } else SynErr(223);
}
void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3202,30 +3207,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
switch (la.kind) {
- case 81: {
+ case 83: {
Get();
x = t;
Expression(out e, true, true);
- Expect(123);
+ Expect(125);
Expression(out e0, true, true);
- Expect(82);
+ Expect(84);
Expression(out e1, allowSemi, allowLambda);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 86: {
+ case 88: {
MatchExpression(out e, allowSemi, allowLambda);
break;
}
- case 89: case 125: case 126: case 127: {
+ case 91: case 127: case 128: case 129: {
QuantifierGuts(out e, allowSemi, allowLambda);
break;
}
- case 61: {
+ case 62: {
ComprehensionExpr(out e, allowSemi, allowLambda);
break;
}
- case 77: case 87: case 92: {
+ case 79: case 89: case 94: {
StmtInExpr(out s);
Expression(out e, allowSemi, allowLambda);
e = new StmtExpr(s.Tok, s, e);
@@ -3235,11 +3240,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LetExpr(out e, allowSemi, allowLambda);
break;
}
- case 71: {
+ case 73: {
NamedExpr(out e, allowSemi, allowLambda);
break;
}
- default: SynErr(223); break;
+ default: SynErr(224); break;
}
}
@@ -3252,20 +3257,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id);
idents.Add(id);
- while (la.kind == 66) {
+ while (la.kind == 68) {
IdentOrDigitsSuffix(out id, out idPrime);
idents.Add(id);
if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
}
- if (la.kind == 16 || la.kind == 93) {
+ if (la.kind == 16 || la.kind == 95) {
args = new List<Expression>();
- if (la.kind == 93) {
+ if (la.kind == 95) {
Get();
id.val = id.val + "#"; Expression k;
- Expect(79);
+ Expect(81);
Expression(out k, true, true);
- Expect(80);
+ Expect(82);
args.Add(k);
}
Expect(16);
@@ -3310,7 +3315,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 66) {
+ if (la.kind == 68) {
IdentOrDigitsSuffix(out id, out x);
if (x != null) {
// process id as a Suffix in its own right
@@ -3318,14 +3323,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo id = x; // move to the next Suffix
}
- if (la.kind == 16 || la.kind == 93) {
+ if (la.kind == 16 || la.kind == 95) {
args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 93) {
+ if (la.kind == 95) {
Get();
id.val = id.val + "#"; Expression k;
- Expect(79);
+ Expect(81);
Expression(out k, true, true);
- Expect(80);
+ Expect(82);
args.Add(k);
}
Expect(16);
@@ -3337,24 +3342,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 == 79) {
+ } else if (la.kind == 81) {
Get();
x = t;
if (StartOf(17)) {
Expression(out ee, true, true);
e0 = ee;
- if (la.kind == 124) {
+ if (la.kind == 126) {
Get();
anyDots = true;
if (StartOf(17)) {
Expression(out ee, true, true);
e1 = ee;
}
- } else if (la.kind == 74) {
+ } else if (la.kind == 76) {
Get();
Expression(out ee, true, true);
e1 = ee;
- } else if (la.kind == 7 || la.kind == 80) {
+ } else if (la.kind == 7 || la.kind == 82) {
while (la.kind == 7) {
Get();
if (multipleLengths == null) {
@@ -3370,7 +3375,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- } else if (la.kind == 37 || la.kind == 80) {
+ } else if (la.kind == 37 || la.kind == 82) {
while (la.kind == 37) {
Get();
Expression(out ee, true, true);
@@ -3381,15 +3386,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(224);
- } else if (la.kind == 124) {
+ } else SynErr(225);
+ } else if (la.kind == 126) {
Get();
anyDots = true;
if (StartOf(17)) {
Expression(out ee, true, true);
e1 = ee;
}
- } else SynErr(225);
+ } else SynErr(226);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -3429,8 +3434,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- Expect(80);
- } else SynErr(226);
+ Expect(82);
+ } else SynErr(227);
ApplySuffix(ref e);
}
@@ -3459,15 +3464,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SetDisplayExpr(x, elements);
Expect(15);
- } else if (la.kind == 79) {
+ } else if (la.kind == 81) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(17)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(80);
- } else SynErr(227);
+ Expect(82);
+ } else SynErr(228);
}
void MultiSetExpr(out Expression e) {
@@ -3475,7 +3480,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(62);
+ Expect(63);
x = t;
if (la.kind == 14) {
Get();
@@ -3493,7 +3498,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(17);
} else if (StartOf(32)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(228);
+ } else SynErr(229);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -3501,12 +3506,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
e = dummyExpr;
- Expect(79);
+ Expect(81);
if (StartOf(17)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(mapToken, elements);
- Expect(80);
+ Expect(82);
}
void MapComprehensionExpr(IToken mapToken, out Expression e, bool allowSemi) {
@@ -3534,17 +3539,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr; Type toType = null;
switch (la.kind) {
- case 117: {
+ case 119: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 118: {
+ case 120: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 119: {
+ case 121: {
Get();
e = new LiteralExpr(t);
break;
@@ -3559,12 +3564,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, d);
break;
}
- case 120: {
+ case 6: {
+ Get();
+ bool isVerbatimString;
+ string s = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);
+ e = new StringLiteralExpr(t, s, isVerbatimString);
+
+ break;
+ }
+ case 122: {
Get();
e = new ThisExpr(t);
break;
}
- case 121: {
+ case 123: {
Get();
x = t;
Expect(16);
@@ -3573,7 +3586,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e);
break;
}
- case 122: {
+ case 124: {
Get();
x = t;
Expect(16);
@@ -3590,8 +3603,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(8);
break;
}
- case 59: case 60: {
- if (la.kind == 59) {
+ case 60: case 61: {
+ if (la.kind == 60) {
Get();
x = t; toType = new IntType();
} else {
@@ -3608,7 +3621,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ParensExpression(out e, allowSemi, allowLambda);
break;
}
- default: SynErr(229); break;
+ default: SynErr(230); break;
}
}
@@ -3633,7 +3646,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo n = BigInteger.Zero;
}
- } else SynErr(230);
+ } else SynErr(231);
}
void Dec(out Basetypes.BigDec d) {
@@ -3742,7 +3755,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 11) {
Get();
oneShot = true;
- } else SynErr(231);
+ } else SynErr(232);
}
void OptTypedExpr(out Expression e, out Type tt, bool allowSemi) {
@@ -3758,24 +3771,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d, true, true);
- Expect(74);
+ Expect(76);
Expression(out r, true, true);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 37) {
Get();
Expression(out d, true, true);
- Expect(74);
+ Expect(76);
Expression(out r, true, true);
elements.Add(new ExpressionPair(d,r));
}
}
void QSep() {
- if (la.kind == 128) {
+ if (la.kind == 130) {
Get();
- } else if (la.kind == 129) {
+ } else if (la.kind == 131) {
Get();
- } else SynErr(232);
+ } else SynErr(233);
}
void MatchExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3783,14 +3796,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
bool usesOptionalBrace = false;
- Expect(86);
+ Expect(88);
x = t;
Expression(out e, allowSemi, true);
if (la.kind == 14) {
Get();
usesOptionalBrace = true;
}
- while (la.kind == 83) {
+ while (la.kind == 85) {
CaseExpression(out c, allowSemi, usesOptionalBrace || allowLambda);
cases.Add(c);
}
@@ -3798,7 +3811,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(15);
} else if (StartOf(32)) {
if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
- } else SynErr(233);
+ } else SynErr(234);
e = new MatchExpr(x, e, cases, usesOptionalBrace);
}
@@ -3810,13 +3823,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range;
Expression/*!*/ body;
- if (la.kind == 89 || la.kind == 125) {
+ if (la.kind == 91 || la.kind == 127) {
Forall();
x = t; univ = true;
- } else if (la.kind == 126 || la.kind == 127) {
+ } else if (la.kind == 128 || la.kind == 129) {
Exists();
x = t;
- } else SynErr(234);
+ } else SynErr(235);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi, allowLambda);
@@ -3836,7 +3849,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range;
Expression body = null;
- Expect(61);
+ Expect(62);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -3847,7 +3860,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(8);
Expression(out range, allowSemi, allowLambda);
- if (la.kind == 128 || la.kind == 129) {
+ if (la.kind == 130 || la.kind == 131) {
QSep();
Expression(out body, allowSemi, allowLambda);
}
@@ -3858,13 +3871,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void StmtInExpr(out Statement s) {
s = dummyStmt;
- if (la.kind == 87) {
+ if (la.kind == 89) {
AssertStmt(out s);
- } else if (la.kind == 77) {
+ } else if (la.kind == 79) {
AssumeStmt(out s);
- } else if (la.kind == 92) {
+ } else if (la.kind == 94) {
CalcStmt(out s);
- } else SynErr(235);
+ } else SynErr(236);
}
void LetExpr(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3893,9 +3906,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo letLHSs.Add(pat);
}
- if (la.kind == 74) {
+ if (la.kind == 76) {
Get();
- } else if (la.kind == 76) {
+ } else if (la.kind == 78) {
Get();
exact = false;
foreach (var lhs in letLHSs) {
@@ -3904,7 +3917,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- } else SynErr(236);
+ } else SynErr(237);
Expression(out e, false, true);
letRHSs.Add(e);
while (la.kind == 37) {
@@ -3922,7 +3935,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
Expression expr;
- Expect(71);
+ Expect(73);
x = t;
NoUSIdent(out d);
Expect(7);
@@ -3955,7 +3968,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
pat = new CasePattern(bv.tok, bv);
- } else SynErr(237);
+ } else SynErr(238);
if (pat == null) {
pat = new CasePattern(t, "_ParseError", new List<CasePattern>());
}
@@ -3968,7 +3981,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(83);
+ Expect(85);
x = t;
Ident(out id);
if (la.kind == 16) {
@@ -3988,30 +4001,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void Forall() {
- if (la.kind == 89) {
+ if (la.kind == 91) {
Get();
- } else if (la.kind == 125) {
+ } else if (la.kind == 127) {
Get();
- } else SynErr(238);
+ } else SynErr(239);
}
void Exists() {
- if (la.kind == 126) {
+ if (la.kind == 128) {
Get();
- } else if (la.kind == 127) {
+ } else if (la.kind == 129) {
Get();
- } else SynErr(239);
+ } else SynErr(240);
}
void AttributeBody(ref Attributes attrs) {
string aName;
- List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
- Attributes.Argument/*!*/ aArg;
+ List<Expression> aArgs = new List<Expression>();
+ Expression aArg;
Expect(7);
Expect(1);
aName = t.val;
- if (StartOf(33)) {
+ if (StartOf(17)) {
AttributeArg(out aArg, true);
aArgs.Add(aArg);
while (la.kind == 37) {
@@ -4036,40 +4049,39 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
static readonly bool[,]/*!*/ set = {
- {T,T,T,T, T,x,x,x, T,T,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, T,x,T,T, T,x,x,x, x,T,x,x, T,x,x,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, 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,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,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,x,T,T, 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, x,x,x,x, x,x,x,x, T,T,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,T,x,x, x,T,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,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,T,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, x,T,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, 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, 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,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,T, x,x,x,x, T,T,T,T, T,x,x,x, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, x,T,x,T, T,T,T,T, x,x,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, 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,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, 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,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, 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,T,T,x, x,T,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, 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,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, 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, 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, T,x,x,x, x,x,T,x, 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,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,T,T, x,T,x,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,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,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, T,x,x,x, x,x,T,x, 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,x,x, T,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, T,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,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,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, 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,T,T,T, T,x,x,x, T,x,x,x, x,x,T,x, 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,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,T,T, x,T,x,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, T,x,x,x, x,x,T,x, T,x,T,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,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,T,T, x,T,x,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,x,x,x, x,x,T,x, 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,x,x, T,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, T,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, T,x,x,x, x,x,T,x, T,x,T,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, T,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,T,T, x,T,x,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, T,x,x,x, x,x,T,x, T,x,T,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,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,T,T, x,T,x,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, T,x,x,x, x,x,T,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,x,x, T,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,T, T,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, T,x,x,x, T,x,x,x, x,x,T,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,x,x, T,x,x,x, x,x,x,x, x,T,T,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,T, T,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,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, T,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, T,x,x,x, T,x,x,x, x,x,T,x, 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,x,x, T,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,T,T, x,T,x,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, T,x,x,x, x,x,T,x, T,x,T,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,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,T,T, x,T,x,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, 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,x,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,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,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, 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,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,T, 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,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},
- {T,T,T,T, T,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,T, T,x,x,x, x,x,T,T, T,T,T,T, T,x,T,T, T,T,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,x,x,x, T,T,x,x},
- {x,T,T,T, T,x,T,x, T,x,x,x, x,x,T,x, 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,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,T,T, x,T,x,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,T,x, T,T,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, T,x,T,T, T,x,x,x, x,T,x,x, T,x,x,T, T,T,T,T, T,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,T, x,x,x,T, 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,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,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,x,T,T, 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, x,x,x,x, x,x,x,x, T,T,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,T,x,x, x,T,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,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, x,T,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, 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, 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,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,T, x,x,x,x, T,T,T,T, T,x,x,x, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,x,T,T, x,T,x,x, x,T,x,T, T,T,T,T, x,x,T,T, 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, 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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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, 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,T,T,x, x,T,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, 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,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, 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, 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,T,x, T,x,x,x, x,x,T,x, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,T, x,T,x,T, x,x,x,x, T,T,x,T, x,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,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,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,T,T,T, T,x,T,x, T,x,x,x, x,x,T,x, 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,x,x, 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,T,T,x, x,T,x,T, x,x,x,T, x,x,T,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,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,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, 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,T,T,T, T,x,T,x, T,x,x,x, x,x,T,x, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, x,T,x,T, x,x,x,x, T,T,x,T, x,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,T,x, T,x,x,x, x,x,T,x, T,x,T,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, T,T,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,T, x,T,x,T, x,x,x,x, T,T,x,T, x,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,T,x, T,x,x,x, x,x,T,x, 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,x,x, 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,T,T,x, x,T,x,T, x,x,x,T, x,x,T,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,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,T,x, T,x,x,x, x,x,T,x, T,x,T,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, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, x,T,x,T, x,x,x,x, T,T,x,T, x,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,T,x, T,x,x,x, x,x,T,x, T,x,T,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, T,T,T,T, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, x,T,x,T, x,x,x,x, T,T,x,T, x,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,T,x, T,x,x,x, x,x,T,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,x,x, 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,T,T,x, x,T,x,T, x,x,x,T, x,T,T,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,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,T,x, T,x,x,x, x,x,T,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,x,x, T,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,T, x,x,x,T, x,T,T,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,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, T,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,T,x, T,x,x,x, x,x,T,x, 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,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,T, x,T,x,T, x,x,x,x, T,T,x,T, x,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,T,x, T,x,x,x, x,x,T,x, T,x,T,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, T,T,T,T, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,T, T,T,x,T, x,x,x,x, T,T,x,T, x,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,T,x, 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,x,x, 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,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,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,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, 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,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,T, 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,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},
+ {T,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,x, T,x,x,x, x,T,x,T, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, T,T,x,x, x,x,x,x, T,T,T,T, T,T,T,x, T,T,T,T, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,x,T, T,T,T,T, T,T,T,x, x,x,T,T, x,x}
};
} // end Parser
@@ -4100,7 +4112,7 @@ public class Errors { case 3: s = "hexdigits expected"; break;
case 4: s = "decimaldigits expected"; break;
case 5: s = "arrayToken expected"; break;
- case 6: s = "string expected"; break;
+ case 6: s = "stringToken expected"; break;
case 7: s = "colon expected"; break;
case 8: s = "verticalbar expected"; break;
case 9: s = "semi expected"; break;
@@ -4152,188 +4164,189 @@ public class Errors { case 55: s = "\"decreases\" expected"; break;
case 56: s = "\"yield\" expected"; break;
case 57: s = "\"bool\" expected"; break;
- case 58: s = "\"nat\" expected"; break;
- case 59: s = "\"int\" expected"; break;
- case 60: s = "\"real\" expected"; break;
- case 61: s = "\"set\" expected"; break;
- case 62: s = "\"multiset\" expected"; break;
- case 63: s = "\"seq\" expected"; break;
- case 64: s = "\"map\" expected"; break;
- case 65: s = "\"object\" expected"; break;
- case 66: s = "\".\" expected"; break;
- case 67: s = "\"function\" expected"; break;
- case 68: s = "\"predicate\" expected"; break;
- case 69: s = "\"copredicate\" expected"; break;
- case 70: s = "\"`\" expected"; break;
- case 71: s = "\"label\" expected"; break;
- case 72: s = "\"break\" expected"; break;
- case 73: s = "\"where\" expected"; break;
- case 74: s = "\":=\" expected"; break;
- case 75: s = "\"return\" expected"; break;
- case 76: s = "\":|\" expected"; break;
- case 77: s = "\"assume\" expected"; break;
- case 78: s = "\"new\" expected"; break;
- case 79: s = "\"[\" expected"; break;
- case 80: s = "\"]\" expected"; break;
- case 81: s = "\"if\" expected"; break;
- case 82: s = "\"else\" expected"; break;
- case 83: s = "\"case\" expected"; break;
- case 84: s = "\"while\" expected"; break;
- case 85: s = "\"invariant\" expected"; break;
- case 86: s = "\"match\" expected"; break;
- case 87: s = "\"assert\" expected"; break;
- case 88: s = "\"print\" expected"; break;
- case 89: s = "\"forall\" expected"; break;
- case 90: s = "\"parallel\" expected"; break;
- case 91: s = "\"modify\" expected"; break;
- case 92: s = "\"calc\" expected"; break;
- case 93: s = "\"#\" expected"; break;
- case 94: s = "\"<=\" expected"; break;
- case 95: s = "\">=\" expected"; break;
- case 96: s = "\"!=\" expected"; break;
- case 97: s = "\"\\u2260\" expected"; break;
- case 98: s = "\"\\u2264\" expected"; break;
- case 99: s = "\"\\u2265\" expected"; break;
- case 100: s = "\"<==>\" expected"; break;
- case 101: s = "\"\\u21d4\" expected"; break;
- case 102: s = "\"==>\" expected"; break;
- case 103: s = "\"\\u21d2\" expected"; break;
- case 104: s = "\"<==\" expected"; break;
- case 105: s = "\"\\u21d0\" expected"; break;
- case 106: s = "\"&&\" expected"; break;
- case 107: s = "\"\\u2227\" expected"; break;
- case 108: s = "\"||\" expected"; break;
- case 109: s = "\"\\u2228\" expected"; break;
- case 110: s = "\"in\" expected"; break;
- case 111: s = "\"!\" expected"; break;
- case 112: s = "\"+\" expected"; break;
- case 113: s = "\"-\" expected"; break;
- case 114: s = "\"/\" expected"; break;
- case 115: s = "\"%\" expected"; break;
- case 116: s = "\"\\u00ac\" expected"; break;
- case 117: s = "\"false\" expected"; break;
- case 118: s = "\"true\" expected"; break;
- case 119: s = "\"null\" expected"; break;
- case 120: s = "\"this\" expected"; break;
- case 121: s = "\"fresh\" expected"; break;
- case 122: s = "\"old\" expected"; break;
- case 123: s = "\"then\" expected"; break;
- case 124: s = "\"..\" expected"; break;
- case 125: s = "\"\\u2200\" expected"; break;
- case 126: s = "\"exists\" expected"; break;
- case 127: s = "\"\\u2203\" expected"; break;
- case 128: s = "\"::\" expected"; break;
- case 129: s = "\"\\u2022\" expected"; break;
- case 130: s = "??? expected"; break;
- case 131: s = "this symbol not expected in SubModuleDecl"; break;
- case 132: s = "invalid SubModuleDecl"; break;
- case 133: s = "this symbol not expected in ClassDecl"; break;
- case 134: s = "this symbol not expected in DatatypeDecl"; break;
- case 135: s = "invalid DatatypeDecl"; break;
+ case 58: s = "\"char\" expected"; break;
+ case 59: s = "\"nat\" expected"; break;
+ case 60: s = "\"int\" expected"; break;
+ case 61: s = "\"real\" expected"; break;
+ case 62: s = "\"set\" expected"; break;
+ case 63: s = "\"multiset\" expected"; break;
+ case 64: s = "\"seq\" expected"; break;
+ case 65: s = "\"string\" expected"; break;
+ case 66: s = "\"map\" expected"; break;
+ case 67: s = "\"object\" expected"; break;
+ case 68: s = "\".\" expected"; break;
+ case 69: s = "\"function\" expected"; break;
+ case 70: s = "\"predicate\" expected"; break;
+ case 71: s = "\"copredicate\" expected"; break;
+ case 72: s = "\"`\" expected"; break;
+ case 73: s = "\"label\" expected"; break;
+ case 74: s = "\"break\" expected"; break;
+ case 75: s = "\"where\" expected"; break;
+ case 76: s = "\":=\" expected"; break;
+ case 77: s = "\"return\" expected"; break;
+ case 78: s = "\":|\" expected"; break;
+ case 79: s = "\"assume\" expected"; break;
+ case 80: s = "\"new\" expected"; break;
+ case 81: s = "\"[\" expected"; break;
+ case 82: s = "\"]\" expected"; break;
+ case 83: s = "\"if\" expected"; break;
+ case 84: s = "\"else\" expected"; break;
+ case 85: s = "\"case\" expected"; break;
+ case 86: s = "\"while\" expected"; break;
+ case 87: s = "\"invariant\" expected"; break;
+ case 88: s = "\"match\" expected"; break;
+ case 89: s = "\"assert\" expected"; break;
+ case 90: s = "\"print\" expected"; break;
+ case 91: s = "\"forall\" expected"; break;
+ case 92: s = "\"parallel\" expected"; break;
+ case 93: s = "\"modify\" expected"; break;
+ case 94: s = "\"calc\" expected"; break;
+ case 95: s = "\"#\" expected"; break;
+ case 96: s = "\"<=\" expected"; break;
+ case 97: s = "\">=\" expected"; break;
+ case 98: s = "\"!=\" expected"; break;
+ case 99: s = "\"\\u2260\" expected"; break;
+ case 100: s = "\"\\u2264\" expected"; break;
+ case 101: s = "\"\\u2265\" expected"; break;
+ case 102: s = "\"<==>\" expected"; break;
+ case 103: s = "\"\\u21d4\" expected"; break;
+ case 104: s = "\"==>\" expected"; break;
+ case 105: s = "\"\\u21d2\" expected"; break;
+ case 106: s = "\"<==\" expected"; break;
+ case 107: s = "\"\\u21d0\" expected"; break;
+ case 108: s = "\"&&\" expected"; break;
+ case 109: s = "\"\\u2227\" expected"; break;
+ case 110: s = "\"||\" expected"; break;
+ case 111: s = "\"\\u2228\" expected"; break;
+ case 112: s = "\"in\" expected"; break;
+ case 113: s = "\"!\" expected"; break;
+ case 114: s = "\"+\" expected"; break;
+ case 115: s = "\"-\" expected"; break;
+ case 116: s = "\"/\" expected"; break;
+ case 117: s = "\"%\" expected"; break;
+ case 118: s = "\"\\u00ac\" expected"; break;
+ case 119: s = "\"false\" expected"; break;
+ case 120: s = "\"true\" expected"; break;
+ case 121: s = "\"null\" expected"; break;
+ case 122: s = "\"this\" expected"; break;
+ case 123: s = "\"fresh\" expected"; break;
+ case 124: s = "\"old\" expected"; break;
+ case 125: s = "\"then\" expected"; break;
+ case 126: s = "\"..\" expected"; break;
+ case 127: s = "\"\\u2200\" expected"; break;
+ case 128: s = "\"exists\" expected"; break;
+ case 129: s = "\"\\u2203\" expected"; break;
+ case 130: s = "\"::\" expected"; break;
+ case 131: s = "\"\\u2022\" expected"; break;
+ case 132: s = "??? expected"; break;
+ case 133: s = "this symbol not expected in SubModuleDecl"; break;
+ case 134: s = "invalid SubModuleDecl"; break;
+ case 135: s = "this symbol not expected in ClassDecl"; break;
case 136: s = "this symbol not expected in DatatypeDecl"; break;
- case 137: s = "invalid NewtypeDecl"; break;
- case 138: s = "this symbol not expected in NewtypeDecl"; break;
- case 139: s = "invalid OtherTypeDecl"; break;
- case 140: s = "this symbol not expected in OtherTypeDecl"; break;
- case 141: s = "this symbol not expected in IteratorDecl"; break;
- case 142: s = "invalid IteratorDecl"; break;
- case 143: s = "this symbol not expected in TraitDecl"; break;
- case 144: s = "invalid ClassMemberDecl"; break;
- case 145: s = "invalid IdentOrDigitsSuffix"; break;
- case 146: s = "this symbol not expected in FieldDecl"; break;
- case 147: s = "this symbol not expected in FieldDecl"; break;
- case 148: s = "invalid FunctionDecl"; break;
- case 149: s = "invalid FunctionDecl"; break;
+ case 137: s = "invalid DatatypeDecl"; break;
+ case 138: s = "this symbol not expected in DatatypeDecl"; break;
+ case 139: s = "invalid NewtypeDecl"; break;
+ case 140: s = "this symbol not expected in NewtypeDecl"; break;
+ case 141: s = "invalid OtherTypeDecl"; break;
+ case 142: s = "this symbol not expected in OtherTypeDecl"; break;
+ case 143: s = "this symbol not expected in IteratorDecl"; break;
+ case 144: s = "invalid IteratorDecl"; break;
+ case 145: s = "this symbol not expected in TraitDecl"; break;
+ case 146: s = "invalid ClassMemberDecl"; break;
+ case 147: s = "invalid IdentOrDigitsSuffix"; break;
+ case 148: s = "this symbol not expected in FieldDecl"; break;
+ case 149: s = "this symbol not expected in FieldDecl"; break;
case 150: s = "invalid FunctionDecl"; break;
case 151: s = "invalid FunctionDecl"; break;
- case 152: s = "this symbol not expected in MethodDecl"; break;
- case 153: s = "invalid MethodDecl"; break;
- case 154: s = "invalid MethodDecl"; break;
- case 155: s = "invalid FIdentType"; break;
- case 156: s = "invalid TypeIdentOptional"; break;
- case 157: s = "invalid TypeAndToken"; break;
- case 158: s = "this symbol not expected in IteratorSpec"; break;
- case 159: s = "this symbol not expected in IteratorSpec"; break;
+ case 152: s = "invalid FunctionDecl"; break;
+ case 153: s = "invalid FunctionDecl"; break;
+ case 154: s = "this symbol not expected in MethodDecl"; break;
+ case 155: s = "invalid MethodDecl"; break;
+ case 156: s = "invalid MethodDecl"; break;
+ case 157: s = "invalid FIdentType"; break;
+ case 158: s = "invalid TypeIdentOptional"; break;
+ case 159: s = "invalid TypeAndToken"; break;
case 160: s = "this symbol not expected in IteratorSpec"; break;
case 161: s = "this symbol not expected in IteratorSpec"; break;
case 162: s = "this symbol not expected in IteratorSpec"; break;
- case 163: s = "invalid IteratorSpec"; break;
+ case 163: s = "this symbol not expected in IteratorSpec"; break;
case 164: s = "this symbol not expected in IteratorSpec"; break;
case 165: s = "invalid IteratorSpec"; break;
- case 166: s = "this symbol not expected in MethodSpec"; break;
- case 167: s = "this symbol not expected in MethodSpec"; break;
+ case 166: s = "this symbol not expected in IteratorSpec"; break;
+ case 167: s = "invalid IteratorSpec"; break;
case 168: s = "this symbol not expected in MethodSpec"; break;
case 169: s = "this symbol not expected in MethodSpec"; break;
- case 170: s = "invalid MethodSpec"; break;
+ case 170: s = "this symbol not expected in MethodSpec"; break;
case 171: s = "this symbol not expected in MethodSpec"; break;
case 172: s = "invalid MethodSpec"; break;
- case 173: s = "invalid FrameExpression"; break;
- case 174: s = "invalid ReferenceType"; break;
- case 175: s = "this symbol not expected in FunctionSpec"; break;
- case 176: s = "this symbol not expected in FunctionSpec"; break;
+ case 173: s = "this symbol not expected in MethodSpec"; break;
+ case 174: s = "invalid MethodSpec"; break;
+ case 175: s = "invalid FrameExpression"; break;
+ case 176: s = "invalid ReferenceType"; break;
case 177: s = "this symbol not expected in FunctionSpec"; break;
case 178: s = "this symbol not expected in FunctionSpec"; break;
case 179: s = "this symbol not expected in FunctionSpec"; break;
- case 180: s = "invalid FunctionSpec"; break;
- case 181: s = "invalid PossiblyWildFrameExpression"; break;
- case 182: s = "invalid PossiblyWildExpression"; break;
- case 183: s = "this symbol not expected in OneStmt"; break;
- case 184: s = "invalid OneStmt"; break;
+ case 180: s = "this symbol not expected in FunctionSpec"; break;
+ case 181: s = "this symbol not expected in FunctionSpec"; break;
+ case 182: s = "invalid FunctionSpec"; break;
+ case 183: s = "invalid PossiblyWildFrameExpression"; break;
+ case 184: s = "invalid PossiblyWildExpression"; break;
case 185: s = "this symbol not expected in OneStmt"; break;
case 186: s = "invalid OneStmt"; break;
- case 187: s = "invalid AssertStmt"; break;
- case 188: s = "invalid AssumeStmt"; break;
- case 189: s = "invalid UpdateStmt"; break;
- case 190: s = "invalid UpdateStmt"; break;
- case 191: s = "invalid IfStmt"; break;
- case 192: s = "invalid IfStmt"; break;
- case 193: s = "invalid WhileStmt"; break;
- case 194: s = "invalid WhileStmt"; break;
- case 195: s = "invalid MatchStmt"; break;
- case 196: s = "invalid ForallStmt"; break;
- case 197: s = "invalid ForallStmt"; break;
- case 198: s = "this symbol not expected in ModifyStmt"; break;
- case 199: s = "invalid ModifyStmt"; break;
- case 200: s = "invalid ReturnStmt"; break;
- case 201: s = "invalid Rhs"; break;
- case 202: s = "invalid Lhs"; break;
- case 203: s = "invalid Guard"; break;
- case 204: s = "this symbol not expected in LoopSpec"; break;
- case 205: s = "this symbol not expected in LoopSpec"; break;
+ case 187: s = "this symbol not expected in OneStmt"; break;
+ case 188: s = "invalid OneStmt"; break;
+ case 189: s = "invalid AssertStmt"; break;
+ case 190: s = "invalid AssumeStmt"; break;
+ case 191: s = "invalid UpdateStmt"; break;
+ case 192: s = "invalid UpdateStmt"; break;
+ case 193: s = "invalid IfStmt"; break;
+ case 194: s = "invalid IfStmt"; break;
+ case 195: s = "invalid WhileStmt"; break;
+ case 196: s = "invalid WhileStmt"; break;
+ case 197: s = "invalid MatchStmt"; break;
+ case 198: s = "invalid ForallStmt"; break;
+ case 199: s = "invalid ForallStmt"; break;
+ case 200: s = "this symbol not expected in ModifyStmt"; break;
+ case 201: s = "invalid ModifyStmt"; break;
+ case 202: s = "invalid ReturnStmt"; break;
+ case 203: s = "invalid Rhs"; break;
+ case 204: s = "invalid Lhs"; break;
+ case 205: s = "invalid Guard"; break;
case 206: s = "this symbol not expected in LoopSpec"; break;
case 207: s = "this symbol not expected in LoopSpec"; break;
case 208: s = "this symbol not expected in LoopSpec"; break;
- case 209: s = "this symbol not expected in Invariant"; break;
- case 210: s = "invalid AttributeArg"; break;
- case 211: s = "invalid CalcOp"; break;
- case 212: s = "invalid EquivOp"; break;
- case 213: s = "invalid ImpliesOp"; break;
- case 214: s = "invalid ExpliesOp"; break;
- case 215: s = "invalid AndOp"; break;
- case 216: s = "invalid OrOp"; break;
- case 217: s = "invalid RelOp"; break;
- case 218: s = "invalid AddOp"; break;
- case 219: s = "invalid UnaryExpression"; break;
+ case 209: s = "this symbol not expected in LoopSpec"; break;
+ case 210: s = "this symbol not expected in LoopSpec"; break;
+ case 211: s = "this symbol not expected in Invariant"; break;
+ case 212: s = "invalid CalcOp"; break;
+ case 213: s = "invalid EquivOp"; break;
+ case 214: s = "invalid ImpliesOp"; break;
+ case 215: s = "invalid ExpliesOp"; break;
+ case 216: s = "invalid AndOp"; break;
+ case 217: s = "invalid OrOp"; break;
+ case 218: s = "invalid RelOp"; break;
+ case 219: s = "invalid AddOp"; break;
case 220: s = "invalid UnaryExpression"; break;
- case 221: s = "invalid MulOp"; break;
- case 222: s = "invalid NegOp"; break;
- case 223: s = "invalid EndlessExpression"; break;
- case 224: s = "invalid Suffix"; break;
+ case 221: s = "invalid UnaryExpression"; break;
+ case 222: s = "invalid MulOp"; break;
+ case 223: s = "invalid NegOp"; break;
+ case 224: s = "invalid EndlessExpression"; break;
case 225: s = "invalid Suffix"; break;
case 226: s = "invalid Suffix"; break;
- case 227: s = "invalid DisplayExpr"; break;
- case 228: s = "invalid MultiSetExpr"; break;
- case 229: s = "invalid ConstAtomExpression"; break;
- case 230: s = "invalid Nat"; break;
- case 231: s = "invalid LambdaArrow"; break;
- case 232: s = "invalid QSep"; break;
- case 233: s = "invalid MatchExpression"; break;
- case 234: s = "invalid QuantifierGuts"; break;
- case 235: s = "invalid StmtInExpr"; break;
- case 236: s = "invalid LetExpr"; break;
- case 237: s = "invalid CasePattern"; break;
- case 238: s = "invalid Forall"; break;
- case 239: s = "invalid Exists"; break;
+ case 227: s = "invalid Suffix"; break;
+ case 228: s = "invalid DisplayExpr"; break;
+ case 229: s = "invalid MultiSetExpr"; break;
+ case 230: s = "invalid ConstAtomExpression"; break;
+ case 231: s = "invalid Nat"; break;
+ case 232: s = "invalid LambdaArrow"; break;
+ case 233: s = "invalid QSep"; break;
+ case 234: s = "invalid MatchExpression"; break;
+ case 235: s = "invalid QuantifierGuts"; break;
+ case 236: s = "invalid StmtInExpr"; break;
+ case 237: s = "invalid LetExpr"; break;
+ case 238: s = "invalid CasePattern"; break;
+ case 239: s = "invalid Forall"; break;
+ case 240: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 6ec05a50..5eba44ee 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -403,19 +403,14 @@ namespace Microsoft.Dafny { }
}
- public void PrintAttributeArgs(List<Attributes.Argument> args, bool isFollowedBySemicolon) {
+ public void PrintAttributeArgs(List<Expression> args, bool isFollowedBySemicolon) {
Contract.Requires(args != null);
string prefix = " ";
- foreach (Attributes.Argument arg in args) {
+ foreach (var arg in args) {
Contract.Assert(arg != null);
wr.Write(prefix);
prefix = ", ";
- if (arg.S != null) {
- wr.Write("\"{0}\"", arg.S);
- } else {
- Contract.Assert( arg.E != null);
- PrintExpression(arg.E, isFollowedBySemicolon);
- }
+ PrintExpression(arg, isFollowedBySemicolon);
}
}
@@ -1219,6 +1214,9 @@ namespace Microsoft.Dafny { wr.Write("null");
} else if (e.Value is bool) {
wr.Write((bool)e.Value ? "true" : "false");
+ } else if (e.Value is string) {
+ var str = (StringLiteralExpr)e;
+ wr.Write("{0}\"{1}\"", str.IsVerbatim ? "@" : "", (string)e.Value);
} else if (e.Value is Basetypes.BigDec) {
Basetypes.BigDec dec = (Basetypes.BigDec)e.Value;
wr.Write((dec.Mantissa >= 0) ? "" : "-");
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 17867100..43333f22 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -444,6 +444,8 @@ namespace Microsoft.Dafny if (prev is BoolType) {
return next is BoolType;
+ } else if (prev is CharType) {
+ return next is CharType;
} else if (prev is IntType) {
if (next is IntType) {
return (prev is NatType) == (next is NatType);
@@ -1071,7 +1073,7 @@ namespace Microsoft.Dafny var e = refinementCloner.CloneExpr(oldAssume.Expr);
var attrs = refinementCloner.MergeAttributes(oldAssume.Attributes, skel.Attributes);
body.Add(new AssertStmt(new Translator.ForceCheckToken(skel.Tok), new Translator.ForceCheckToken(skel.EndTok),
- e, new Attributes("prependAssertToken", new List<Attributes.Argument>(), attrs)));
+ e, new Attributes("prependAssertToken", new List<Expression>(), attrs)));
ReportAdditionalInformation(c.ConditionEllipsis, "assume->assert: " + Printer.ExprToString(e), 3);
i++; j++;
}
@@ -1589,7 +1591,7 @@ namespace Microsoft.Dafny if (moreAttrs == null) {
return CloneAttributes(prevAttrs);
} else {
- return new Attributes(moreAttrs.Name, moreAttrs.Args.ConvertAll(CloneAttrArg), MergeAttributes(prevAttrs, moreAttrs.Prev));
+ return new Attributes(moreAttrs.Name, moreAttrs.Args.ConvertAll(CloneExpr), MergeAttributes(prevAttrs, moreAttrs.Prev));
}
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 82d774fc..b7eadc13 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3123,15 +3123,17 @@ namespace Microsoft.Dafny }
}
- void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, ResolveOpts opts, bool allowGhosts) {
+ void ResolveAttributeArgs(List<Expression> args, ResolveOpts opts, bool allowGhosts) {
Contract.Requires(args != null);
- foreach (Attributes.Argument aa in args) {
- Contract.Assert(aa != null);
- if (aa.E != null) {
- ResolveExpression(aa.E, opts);
- if (!allowGhosts) {
- CheckIsNonGhost(aa.E);
- }
+ foreach (var arg in args) {
+ Contract.Assert(arg != null);
+ int prevErrors = ErrorCount;
+ ResolveExpression(arg, opts);
+ if (!allowGhosts) {
+ CheckIsNonGhost(arg);
+ }
+ if (prevErrors == ErrorCount) {
+ CheckTypeInference(arg);
}
}
}
@@ -3962,6 +3964,8 @@ namespace Microsoft.Dafny if (a is BoolType) {
return b is BoolType;
+ } else if (a is CharType) {
+ return b is CharType;
} else if (a is IntType) {
return b is IntType;
} else if (a is RealType) {
@@ -6187,6 +6191,9 @@ namespace Microsoft.Dafny e.Type = new OperationTypeProxy(false, true, false, false);
} else if (e.Value is bool) {
e.Type = Type.Bool;
+ } else if (e.Value is string) {
+ e.Type = new UserDefinedType(e.tok, "string", new List<Type>(), new List<IToken>());
+ ResolveType(e.tok, e.Type, opts.codeContext, ResolveTypeOptionEnum.DontInfer, null);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal type
}
@@ -6864,7 +6871,7 @@ namespace Microsoft.Dafny scope.PopMarker();
expr.Type = new SetType(e.Term.Type);
- if (opts.IsGhost && (e.Term.Type.IsRefType || e.Term.Type is BoolType)) {
+ if (opts.IsGhost && (e.Term.Type.IsRefType || e.Term.Type.IsBoolType) || e.Term.Type.IsCharType) {
// ok, term type is finite and we're in a ghost context
} else {
needFiniteBoundsChecks.Add(e);
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 3f4f57b8..6921522c 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -488,8 +488,7 @@ namespace Microsoft.Dafny fWithBody.tok = newToken;
// Annotate the new function so we remember that we introduced it
- List<Attributes.Argument/*!*/>new_args = new List<Attributes.Argument/*!*/>();
- fWithBody.Attributes = new Attributes("opaque_full", new_args, fWithBody.Attributes);
+ fWithBody.Attributes = new Attributes("opaque_full", new List<Expression>(), fWithBody.Attributes);
// Create a lemma to allow the user to selectively reveal the function's body
// That is, given:
@@ -530,14 +529,12 @@ namespace Microsoft.Dafny if (f.Formals.Count > 0) {
// Build an explicit trigger for the forall, so Z3 doesn't get confused
Expression trigger = func_builder(f);
- List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Attributes.Argument/*!*/ anArg;
- anArg = new Attributes.Argument(f.tok, trigger);
- args.Add(anArg);
+ List<Expression> args = new List<Expression>();
+ args.Add(trigger);
Attributes attrs = new Attributes("trigger", args, null);
// Also specify that this is a type quantifier
- attrs = new Attributes("typeQuantifier", new List<Attributes.Argument>(), attrs);
+ attrs = new Attributes("typeQuantifier", new List<Expression>(), attrs);
newEnsures = new MaybeFreeExpression(new ForallExpr(f.tok, typeVars, boundVars, null, requiresImpliesOldEqualsNew, attrs));
} else {
@@ -548,8 +545,7 @@ namespace Microsoft.Dafny newEnsuresList.Add(newEnsures);
// Add an axiom attribute so that the compiler won't complain about the lemma's lack of a body
- List<Attributes.Argument> argList = new List<Attributes.Argument>();
- Attributes lemma_attrs = new Attributes("axiom", argList, null);
+ Attributes lemma_attrs = new Attributes("axiom", new List<Expression>(), null);
var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.IsStatic, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null), newEnsuresList,
@@ -593,7 +589,7 @@ namespace Microsoft.Dafny protected void needsLayerQuantifier(Lemma lem, Function fn) {
var origForall = lem.Ens[0].E as ForallExpr;
if (origForall != null && fn.IsRecursive) {
- var newAttrib = new Attributes("layerQuantifier", new List<Attributes.Argument>(), origForall.Attributes);
+ var newAttrib = new Attributes("layerQuantifier", new List<Expression>(), origForall.Attributes);
var newForall = new ForallExpr(origForall.tok, origForall.TypeArgs, origForall.BoundVars, origForall.Range, origForall.Term, newAttrib);
newForall.Type = Type.Bool;
lem.Ens[0] = new MaybeFreeExpression(newForall);
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index c21f58df..b9ace9e1 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 = 130;
- const int noSym = 130;
+ const int maxT = 132;
+ const int noSym = 132;
[ContractInvariantMethod]
@@ -255,45 +255,46 @@ 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] = 24;
- for (int i = 34; i <= 34; ++i) start[i] = 11;
- start[97] = 25;
- start[48] = 26;
- start[58] = 64;
- start[124] = 65;
- start[59] = 13;
- start[61] = 66;
- start[45] = 67;
- start[123] = 16;
- start[125] = 17;
- start[40] = 18;
- start[41] = 19;
- start[42] = 20;
- start[33] = 68;
- start[44] = 33;
- start[46] = 69;
- start[60] = 70;
- start[62] = 71;
- start[96] = 35;
- start[91] = 38;
- start[93] = 39;
- start[35] = 40;
- start[8800] = 43;
- start[8804] = 44;
- start[8805] = 45;
- start[8660] = 47;
- start[8658] = 49;
- start[8656] = 50;
- start[38] = 51;
- start[8743] = 53;
- start[8744] = 55;
- start[43] = 56;
- start[47] = 57;
- start[37] = 58;
- start[172] = 59;
- start[8704] = 60;
- start[8707] = 61;
- start[8226] = 63;
+ for (int i = 49; i <= 57; ++i) start[i] = 30;
+ start[97] = 31;
+ start[48] = 32;
+ start[34] = 11;
+ start[64] = 16;
+ start[58] = 72;
+ start[124] = 73;
+ start[59] = 19;
+ start[61] = 74;
+ start[45] = 75;
+ start[123] = 22;
+ start[125] = 23;
+ start[40] = 24;
+ start[41] = 25;
+ start[42] = 26;
+ start[33] = 76;
+ start[44] = 41;
+ start[46] = 77;
+ start[60] = 78;
+ start[62] = 79;
+ start[96] = 43;
+ start[91] = 46;
+ start[93] = 47;
+ start[35] = 48;
+ start[8800] = 51;
+ start[8804] = 52;
+ start[8805] = 53;
+ start[8660] = 55;
+ start[8658] = 57;
+ start[8656] = 58;
+ start[38] = 59;
+ start[8743] = 61;
+ start[8744] = 63;
+ start[43] = 64;
+ start[47] = 65;
+ start[37] = 66;
+ start[172] = 67;
+ start[8704] = 68;
+ start[8707] = 69;
+ start[8226] = 71;
start[Buffer.EOF] = -1;
}
@@ -529,44 +530,46 @@ public class Scanner { case "decreases": t.kind = 55; break;
case "yield": t.kind = 56; break;
case "bool": t.kind = 57; break;
- case "nat": t.kind = 58; break;
- case "int": t.kind = 59; break;
- case "real": t.kind = 60; break;
- case "set": t.kind = 61; break;
- case "multiset": t.kind = 62; break;
- case "seq": t.kind = 63; break;
- case "map": t.kind = 64; break;
- case "object": t.kind = 65; break;
- case "function": t.kind = 67; break;
- case "predicate": t.kind = 68; break;
- case "copredicate": t.kind = 69; break;
- case "label": t.kind = 71; break;
- case "break": t.kind = 72; break;
- case "where": t.kind = 73; break;
- case "return": t.kind = 75; break;
- case "assume": t.kind = 77; break;
- case "new": t.kind = 78; break;
- case "if": t.kind = 81; break;
- case "else": t.kind = 82; break;
- case "case": t.kind = 83; break;
- case "while": t.kind = 84; break;
- case "invariant": t.kind = 85; break;
- case "match": t.kind = 86; break;
- case "assert": t.kind = 87; break;
- case "print": t.kind = 88; break;
- case "forall": t.kind = 89; break;
- case "parallel": t.kind = 90; break;
- case "modify": t.kind = 91; break;
- case "calc": t.kind = 92; break;
- case "in": t.kind = 110; break;
- case "false": t.kind = 117; break;
- case "true": t.kind = 118; break;
- case "null": t.kind = 119; break;
- case "this": t.kind = 120; break;
- case "fresh": t.kind = 121; break;
- case "old": t.kind = 122; break;
- case "then": t.kind = 123; break;
- case "exists": t.kind = 126; break;
+ case "char": t.kind = 58; break;
+ case "nat": t.kind = 59; break;
+ case "int": t.kind = 60; break;
+ case "real": t.kind = 61; break;
+ case "set": t.kind = 62; break;
+ case "multiset": t.kind = 63; break;
+ case "seq": t.kind = 64; break;
+ case "string": t.kind = 65; break;
+ case "map": t.kind = 66; break;
+ case "object": t.kind = 67; break;
+ case "function": t.kind = 69; break;
+ case "predicate": t.kind = 70; break;
+ case "copredicate": t.kind = 71; break;
+ case "label": t.kind = 73; break;
+ case "break": t.kind = 74; break;
+ case "where": t.kind = 75; break;
+ case "return": t.kind = 77; break;
+ case "assume": t.kind = 79; break;
+ case "new": t.kind = 80; break;
+ case "if": t.kind = 83; break;
+ case "else": t.kind = 84; break;
+ case "case": t.kind = 85; break;
+ case "while": t.kind = 86; break;
+ case "invariant": t.kind = 87; break;
+ case "match": t.kind = 88; break;
+ case "assert": t.kind = 89; break;
+ case "print": t.kind = 90; break;
+ case "forall": t.kind = 91; break;
+ case "parallel": t.kind = 92; break;
+ case "modify": t.kind = 93; break;
+ case "calc": t.kind = 94; break;
+ case "in": t.kind = 112; break;
+ case "false": t.kind = 119; break;
+ case "true": t.kind = 120; break;
+ case "null": t.kind = 121; break;
+ case "this": t.kind = 122; break;
+ case "fresh": t.kind = 123; break;
+ case "old": t.kind = 124; break;
+ case "then": t.kind = 125; break;
+ case "exists": t.kind = 128; break;
default: break;
}
}
@@ -639,198 +642,226 @@ public class Scanner { if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
else {t.kind = 4; break;}
case 11:
- if (ch == '"') {AddCh(); goto case 12;}
- else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 11;}
+ if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 11;}
+ else if (ch == '"') {AddCh(); goto case 18;}
+ else if (ch == 92) {AddCh(); goto case 34;}
else {goto case 0;}
case 12:
- {t.kind = 6; break;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 13;}
+ else {goto case 0;}
case 13:
- {t.kind = 9; break;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 14;}
+ else {goto case 0;}
case 14:
- {t.kind = 10; break;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 15;}
+ else {goto case 0;}
case 15:
- {t.kind = 11; break;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 11;}
+ else {goto case 0;}
case 16:
- {t.kind = 14; break;}
+ if (ch == '"') {AddCh(); goto case 17;}
+ else {goto case 0;}
case 17:
- {t.kind = 15; break;}
+ if (ch <= '!' || ch >= '#' && ch <= 65535) {AddCh(); goto case 17;}
+ else if (ch == '"') {AddCh(); goto case 35;}
+ else {goto case 0;}
case 18:
- {t.kind = 16; break;}
+ {t.kind = 6; break;}
case 19:
- {t.kind = 17; break;}
+ {t.kind = 9; break;}
case 20:
- {t.kind = 18; break;}
+ {t.kind = 10; break;}
case 21:
- if (ch == 'n') {AddCh(); goto case 22;}
- else {goto case 0;}
+ {t.kind = 11; break;}
case 22:
- if (ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {apx++; AddCh(); goto case 23;}
- else {goto case 0;}
+ {t.kind = 14; break;}
case 23:
+ {t.kind = 15; break;}
+ case 24:
+ {t.kind = 16; break;}
+ case 25:
+ {t.kind = 17; break;}
+ case 26:
+ {t.kind = 18; break;}
+ case 27:
+ if (ch == 'n') {AddCh(); goto case 28;}
+ else {goto case 0;}
+ case 28:
+ if (ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {apx++; AddCh(); goto case 29;}
+ else {goto case 0;}
+ case 29:
{
tlen -= apx;
SetScannerBehindT();
t.kind = 19; break;}
- case 24:
+ case 30:
recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
else if (ch == '.') {AddCh(); goto case 9;}
else {t.kind = 2; break;}
- case 25:
+ case 31:
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 28;}
+ else if (ch == 'r') {AddCh(); goto case 36;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 26:
+ case 32:
recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
else if (ch == 'x') {AddCh(); goto case 7;}
else if (ch == '.') {AddCh(); goto case 9;}
else {t.kind = 2; break;}
- case 27:
+ case 33:
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 27;}
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 33;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 28:
+ case 34:
+ if (ch == '"' || ch == 39 || ch == '0' || ch == 92 || ch == 'n' || ch == 'r' || ch == 't') {AddCh(); goto case 11;}
+ else if (ch == 'u') {AddCh(); goto case 12;}
+ else {goto case 0;}
+ case 35:
+ recEnd = pos; recKind = 6;
+ if (ch == '"') {AddCh(); goto case 17;}
+ else {t.kind = 6; break;}
+ case 36:
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 29;}
+ else if (ch == 'r') {AddCh(); goto case 37;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 29:
+ case 37:
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 30;}
+ else if (ch == 'a') {AddCh(); goto case 38;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 30:
+ case 38:
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 31;}
+ else if (ch == 'y') {AddCh(); goto case 39;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 31:
+ case 39:
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 32;}
+ else if (ch >= '1' && ch <= '9') {AddCh(); goto case 40;}
else {t.kind = 5; break;}
- case 32:
+ case 40:
recEnd = pos; recKind = 5;
- if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 27;}
- else if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;}
+ if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 33;}
+ else if (ch >= '0' && ch <= '9') {AddCh(); goto case 40;}
else {t.kind = 5; break;}
- case 33:
- {t.kind = 37; break;}
- case 34:
- {t.kind = 44; break;}
- case 35:
- {t.kind = 70; break;}
- case 36:
- {t.kind = 74; break;}
- case 37:
- {t.kind = 76; break;}
- case 38:
- {t.kind = 79; break;}
- case 39:
- {t.kind = 80; break;}
- case 40:
- {t.kind = 93; break;}
case 41:
- {t.kind = 95; break;}
+ {t.kind = 37; break;}
case 42:
- {t.kind = 96; break;}
+ {t.kind = 44; break;}
case 43:
- {t.kind = 97; break;}
+ {t.kind = 72; break;}
case 44:
- {t.kind = 98; break;}
+ {t.kind = 76; break;}
case 45:
- {t.kind = 99; break;}
+ {t.kind = 78; break;}
case 46:
- {t.kind = 100; break;}
+ {t.kind = 81; break;}
case 47:
- {t.kind = 101; break;}
+ {t.kind = 82; break;}
case 48:
- {t.kind = 102; break;}
+ {t.kind = 95; break;}
case 49:
- {t.kind = 103; break;}
+ {t.kind = 97; break;}
case 50:
- {t.kind = 105; break;}
+ {t.kind = 98; break;}
case 51:
- if (ch == '&') {AddCh(); goto case 52;}
- else {goto case 0;}
+ {t.kind = 99; break;}
case 52:
- {t.kind = 106; break;}
+ {t.kind = 100; break;}
case 53:
- {t.kind = 107; break;}
+ {t.kind = 101; break;}
case 54:
- {t.kind = 108; break;}
+ {t.kind = 102; break;}
case 55:
- {t.kind = 109; break;}
+ {t.kind = 103; break;}
case 56:
- {t.kind = 112; break;}
+ {t.kind = 104; break;}
case 57:
- {t.kind = 114; break;}
+ {t.kind = 105; break;}
case 58:
- {t.kind = 115; break;}
+ {t.kind = 107; break;}
case 59:
- {t.kind = 116; break;}
+ if (ch == '&') {AddCh(); goto case 60;}
+ else {goto case 0;}
case 60:
- {t.kind = 125; break;}
+ {t.kind = 108; break;}
case 61:
- {t.kind = 127; break;}
+ {t.kind = 109; break;}
case 62:
- {t.kind = 128; break;}
+ {t.kind = 110; break;}
case 63:
- {t.kind = 129; break;}
+ {t.kind = 111; break;}
case 64:
+ {t.kind = 114; break;}
+ case 65:
+ {t.kind = 116; break;}
+ case 66:
+ {t.kind = 117; break;}
+ case 67:
+ {t.kind = 118; break;}
+ case 68:
+ {t.kind = 127; break;}
+ case 69:
+ {t.kind = 129; break;}
+ case 70:
+ {t.kind = 130; break;}
+ case 71:
+ {t.kind = 131; break;}
+ case 72:
recEnd = pos; recKind = 7;
- if (ch == '=') {AddCh(); goto case 36;}
- else if (ch == '|') {AddCh(); goto case 37;}
- else if (ch == ':') {AddCh(); goto case 62;}
+ if (ch == '=') {AddCh(); goto case 44;}
+ else if (ch == '|') {AddCh(); goto case 45;}
+ else if (ch == ':') {AddCh(); goto case 70;}
else {t.kind = 7; break;}
- case 65:
+ case 73:
recEnd = pos; recKind = 8;
- if (ch == '|') {AddCh(); goto case 54;}
+ if (ch == '|') {AddCh(); goto case 62;}
else {t.kind = 8; break;}
- case 66:
+ case 74:
recEnd = pos; recKind = 26;
- if (ch == '>') {AddCh(); goto case 14;}
- else if (ch == '=') {AddCh(); goto case 72;}
+ if (ch == '>') {AddCh(); goto case 20;}
+ else if (ch == '=') {AddCh(); goto case 80;}
else {t.kind = 26; break;}
- case 67:
+ case 75:
+ recEnd = pos; recKind = 115;
+ if (ch == '>') {AddCh(); goto case 21;}
+ else {t.kind = 115; break;}
+ case 76:
recEnd = pos; recKind = 113;
- if (ch == '>') {AddCh(); goto case 15;}
+ if (ch == 'i') {AddCh(); goto case 27;}
+ else if (ch == '=') {AddCh(); goto case 50;}
else {t.kind = 113; break;}
- case 68:
- recEnd = pos; recKind = 111;
- if (ch == 'i') {AddCh(); goto case 21;}
- else if (ch == '=') {AddCh(); goto case 42;}
- else {t.kind = 111; break;}
- case 69:
- recEnd = pos; recKind = 66;
- if (ch == '.') {AddCh(); goto case 73;}
- else {t.kind = 66; break;}
- case 70:
+ case 77:
+ recEnd = pos; recKind = 68;
+ if (ch == '.') {AddCh(); goto case 81;}
+ else {t.kind = 68; break;}
+ case 78:
recEnd = pos; recKind = 45;
- if (ch == '=') {AddCh(); goto case 74;}
+ if (ch == '=') {AddCh(); goto case 82;}
else {t.kind = 45; break;}
- case 71:
+ case 79:
recEnd = pos; recKind = 46;
- if (ch == '=') {AddCh(); goto case 41;}
+ if (ch == '=') {AddCh(); goto case 49;}
else {t.kind = 46; break;}
- case 72:
+ case 80:
recEnd = pos; recKind = 40;
- if (ch == '>') {AddCh(); goto case 48;}
+ if (ch == '>') {AddCh(); goto case 56;}
else {t.kind = 40; break;}
- case 73:
- recEnd = pos; recKind = 124;
- if (ch == '.') {AddCh(); goto case 34;}
- else {t.kind = 124; break;}
- case 74:
- recEnd = pos; recKind = 94;
- if (ch == '=') {AddCh(); goto case 75;}
- else {t.kind = 94; break;}
- case 75:
- recEnd = pos; recKind = 104;
- if (ch == '>') {AddCh(); goto case 46;}
- else {t.kind = 104; break;}
+ case 81:
+ recEnd = pos; recKind = 126;
+ if (ch == '.') {AddCh(); goto case 42;}
+ else {t.kind = 126; break;}
+ case 82:
+ recEnd = pos; recKind = 96;
+ if (ch == '=') {AddCh(); goto case 83;}
+ else {t.kind = 96; break;}
+ case 83:
+ recEnd = pos; recKind = 106;
+ if (ch == '>') {AddCh(); goto case 54;}
+ else {t.kind = 106; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index bfd748a2..59a1abaa 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -53,6 +53,7 @@ namespace Microsoft.Dafny { public string UniqueIdPrefix { get; set; }
internal class PredefinedDecls {
+ public readonly Bpl.Type CharType;
public readonly Bpl.Type RefType;
public readonly Bpl.Type BoxType;
public readonly Bpl.Type TickType;
@@ -77,6 +78,7 @@ namespace Microsoft.Dafny { private readonly Bpl.Constant allocField;
[ContractInvariantMethod]
void ObjectInvariant() {
+ Contract.Invariant(CharType != null);
Contract.Invariant(RefType != null);
Contract.Invariant(BoxType != null);
Contract.Invariant(TickType != null);
@@ -144,7 +146,7 @@ namespace Microsoft.Dafny { return new Bpl.IdentifierExpr(tok, allocField);
}
- public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
+ public PredefinedDecls(Bpl.TypeCtorDecl charType, Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor,
Bpl.Function arrayLength, Bpl.Function realTrunc, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.TypeCtorDecl tyType, Bpl.TypeCtorDecl tyTagType,
@@ -152,6 +154,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl handleType, Bpl.TypeCtorDecl layerType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField) {
#region Non-null preconditions on parameters
+ Contract.Requires(charType != null);
Contract.Requires(refType != null);
Contract.Requires(boxType != null);
Contract.Requires(tickType != null);
@@ -172,6 +175,7 @@ namespace Microsoft.Dafny { Contract.Requires(tyTagType != null);
#endregion
+ this.CharType = new Bpl.CtorType(Token.NoToken, charType, new List<Bpl.Type>());
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new List<Bpl.Type>());
this.RefType = refT;
this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new List<Bpl.Type>());
@@ -205,6 +209,7 @@ namespace Microsoft.Dafny { return null;
}
+ Bpl.TypeCtorDecl charType = null;
Bpl.TypeCtorDecl refType = null;
Bpl.TypeSynonymDecl setTypeCtor = null;
Bpl.TypeSynonymDecl multiSetTypeCtor = null;
@@ -246,6 +251,8 @@ namespace Microsoft.Dafny { layerType = dt;
} else if (dt.Name == "DtCtorId") {
dtCtorId = dt;
+ } else if (dt.Name == "char") {
+ charType = dt;
} else if (dt.Name == "ref") {
refType = dt;
} else if (dt.Name == "NameFamily") {
@@ -314,6 +321,8 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type LayerType");
} else if (dtCtorId == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DtCtorId");
+ } else if (charType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type char");
} else if (refType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ref");
} else if (boxType == null) {
@@ -325,7 +334,7 @@ namespace Microsoft.Dafny { } else if (allocField == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
} else {
- return new PredefinedDecls(refType, boxType, tickType,
+ return new PredefinedDecls(charType, refType, boxType, tickType,
setTypeCtor, multiSetTypeCtor, mapTypeCtor,
arrayLength, realTrunc, seqTypeCtor, fieldNameType,
tyType, tyTagType,
@@ -379,6 +388,8 @@ namespace Microsoft.Dafny { AddTypeDecl((OpaqueTypeDecl)d);
} else if (d is NewtypeDecl) {
AddTypeDecl((NewtypeDecl)d);
+ } else if (d is TypeSynonymDecl) {
+ // do nothing, just bypass type synonyms in the translation
} else if (d is DatatypeDecl) {
AddDatatype((DatatypeDecl)d);
} else if (d is ArrowTypeDecl) {
@@ -6517,6 +6528,8 @@ namespace Microsoft.Dafny { if (type is BoolType) {
return Bpl.Type.Bool;
+ } else if (type is CharType) {
+ return predef.CharType;
} else if (type is IntType) {
return Bpl.Type.Int;
} else if (type is RealType) {
@@ -6779,10 +6792,8 @@ namespace Microsoft.Dafny { } else if (stmt is PrintStmt) {
AddComment(builder, stmt, "print statement");
PrintStmt s = (PrintStmt)stmt;
- foreach (Attributes.Argument arg in s.Args) {
- if (arg.E != null) {
- TrStmt_CheckWellformed(arg.E, builder, locals, etran, false);
- }
+ foreach (var arg in s.Args) {
+ TrStmt_CheckWellformed(arg, builder, locals, etran, false);
}
} else if (stmt is BreakStmt) {
@@ -7353,6 +7364,8 @@ namespace Microsoft.Dafny { lit.Type = Type.Bool; // resolve here
yield return lit;
yield break; // there are no more possible witnesses for booleans
+ } else if (xType is CharType) {
+ // TODO: something could be done for character literals
} else if (xType.IsRefType) {
var lit = new LiteralExpr(x.tok); // null
lit.Type = xType;
@@ -8761,6 +8774,8 @@ namespace Microsoft.Dafny { u = u.NormalizeExpand();
if (t is BoolType) {
return u is BoolType;
+ } else if (t is CharType) {
+ return u is CharType;
} else if (t.IsNumericBased(Type.NumericPersuation.Int)) {
// we can allow different kinds of int-based types
return u.IsNumericBased(Type.NumericPersuation.Int);
@@ -8822,6 +8837,10 @@ namespace Microsoft.Dafny { eq = Bpl.Expr.Iff(e0, e1);
less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
atmost = Bpl.Expr.Imp(e0, e1);
+ } else if (ty0 is CharType) {
+ eq = Bpl.Expr.Eq(e0, e1);
+ less = Bpl.Expr.False;
+ atmost = eq; // less || eq
} else if (ty0.IsNumericBased(Type.NumericPersuation.Int) || ty0 is SeqType || ty0.IsDatatype) {
Bpl.Expr b0, b1;
if (ty0.IsNumericBased(Type.NumericPersuation.Int)) {
@@ -8948,6 +8967,8 @@ namespace Microsoft.Dafny { TypeToTy(((MapType)type).Range));
} else if (type is BoolType) {
return new Bpl.IdentifierExpr(Token.NoToken, "TBool", predef.Ty);
+ } else if (type is CharType) {
+ return new Bpl.IdentifierExpr(Token.NoToken, "TChar", predef.Ty);
} else if (type is RealType) {
return new Bpl.IdentifierExpr(Token.NoToken, "TReal", predef.Ty);
} else if (type is NatType) {
@@ -10174,6 +10195,15 @@ namespace Microsoft.Dafny { return predef.Null;
} else if (e.Value is bool) {
return translator.Lit(new Bpl.LiteralExpr(e.tok, (bool)e.Value));
+ } else if (e.Value is string) {
+ var str = (StringLiteralExpr)e;
+ Bpl.Expr seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
+ foreach (char ch in Util.UnescapedCharacters((string)e.Value, str.IsVerbatim)) {
+ var rawElement = translator.FunctionCall(expr.tok, BuiltinFunction.CharFromInt, null, Bpl.Expr.Literal((int)ch));
+ Bpl.Expr elt = BoxIfNecessary(expr.tok, rawElement, Type.Char);
+ seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, seq, elt);
+ }
+ return translator.Lit(seq, translator.TrType(new SeqType(Type.Char)));
} 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) {
@@ -10233,9 +10263,10 @@ namespace Microsoft.Dafny { } else if (expr is SeqDisplayExpr) {
SeqDisplayExpr e = (SeqDisplayExpr)expr;
+ // Note: a LiteralExpr(string) is really another kind of SeqDisplayExpr
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
bool isLit = true;
- foreach (Expression ee in e.Elements) {
+ foreach (Expression ee in e.Elements) {
var rawElement = TrExpr(ee);
isLit = isLit && translator.IsLit(rawElement);
Bpl.Expr elt = BoxIfNecessary(expr.tok, rawElement, ee.Type);
@@ -10842,11 +10873,7 @@ namespace Microsoft.Dafny { if (aa.Name == "trigger") {
List<Bpl.Expr> tt = new List<Bpl.Expr>();
foreach (var arg in aa.Args) {
- if (arg.E == null) {
- Console.WriteLine("Warning: string argument to 'trigger' attribute ignored");
- } else {
- tt.Add(bodyEtran.TrExpr(arg.E));
- }
+ tt.Add(bodyEtran.TrExpr(arg));
}
tr = new Bpl.Trigger(expr.tok, true, tt, tr);
}
@@ -11273,13 +11300,15 @@ namespace Microsoft.Dafny { continue;
}
List<object> parms = new List<object>();
- foreach (Attributes.Argument arg in attrs.Args) {
- if (arg.E != null) {
- var e = TrExpr(arg.E);
+ foreach (var arg in attrs.Args) {
+ var s = arg.AsStringLiteral();
+ if (s != null) {
+ // pass string literals down to Boogie as string literals, not as their expression translation
+ parms.Add(s);
+ } else {
+ var e = TrExpr(arg);
e = translator.RemoveLit(e);
parms.Add(e);
- } else {
- parms.Add(cce.NonNull(arg.S));
}
}
kv = new Bpl.QKeyValue(Token.NoToken, attrs.Name, parms, kv);
@@ -11325,6 +11354,7 @@ namespace Microsoft.Dafny { LitInt,
LitReal,
LayerSucc,
+ CharFromInt,
Is, IsBox,
IsAlloc, IsAllocBox,
@@ -11477,6 +11507,11 @@ namespace Microsoft.Dafny { Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$LS", predef.LayerType, args);
+ case BuiltinFunction.CharFromInt:
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "char#FromInt", predef.CharType, args);
+
case BuiltinFunction.Is:
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
@@ -12308,7 +12343,7 @@ namespace Microsoft.Dafny { // Handle {:induction false}
if (a.Args.Count == 1) {
- var arg = a.Args[0].E as LiteralExpr;
+ var arg = a.Args[0] as LiteralExpr;
if (arg != null && arg.Value is bool && !(bool)arg.Value) {
if (CommandLineOptions.Clo.Trace) {
Console.Write("Suppressing automatic induction for: ");
@@ -12324,7 +12359,7 @@ namespace Microsoft.Dafny { // check that all attribute arguments refer to bound variables; otherwise, go to default_form
var argsAsVars = new List<VarType>();
foreach (var arg in a.Args) {
- var theArg = arg.E.Resolved;
+ var theArg = arg.Resolved;
if (theArg is ThisExpr) {
foreach (var bv in boundVars) {
if (bv is ThisSurrogate) {
@@ -13453,18 +13488,16 @@ namespace Microsoft.Dafny { public Attributes SubstAttributes(Attributes attrs) {
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
if (attrs != null) {
- List<Attributes.Argument> newArgs = new List<Attributes.Argument>(); // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes
+ var newArgs = new List<Expression>(); // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes
bool anyArgSubst = false;
- foreach (Attributes.Argument arg in attrs.Args) {
- Attributes.Argument newArg = arg;
- if (arg.E != null) {
- Expression newE = Substitute(arg.E);
- if (newE != arg.E) {
- newArg = new Attributes.Argument(arg.Tok, newE);
- anyArgSubst = true;
- }
+ foreach (var arg in attrs.Args) {
+ var argToBeAdded = arg;
+ var substArg = Substitute(arg);
+ if (substArg != arg) {
+ argToBeAdded = substArg;
+ anyArgSubst = true;
}
- newArgs.Add(newArg);
+ newArgs.Add(argToBeAdded);
}
if (!anyArgSubst) {
newArgs = attrs.Args;
diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index 61004ddd..d2377a76 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -2,6 +2,7 @@ using System.Collections.Generic;
using System.Linq;
using System.Text;
+using System.Diagnostics.Contracts;
using Microsoft.Boogie;
@@ -66,5 +67,99 @@ namespace Microsoft.Dafny { return res;
}
+ /// <summary>
+ /// For "S" returns S and false.
+ /// For @"S" return S and true.
+ /// Assumes that s has one of these forms.
+ /// </summary>
+ public static string RemoveParsedStringQuotes(string s, out bool isVerbatimString) {
+ Contract.Requires(s != null);
+ var len = s.Length;
+ if (s[0] == '@') {
+ isVerbatimString = true;
+ return s.Substring(2, len - 3);
+ } else {
+ isVerbatimString = false;
+ return s.Substring(1, len - 2);
+ }
+ }
+ /// <summary>
+ /// Replaced any escaped characters in s by the actual character that the escaping represents.
+ /// Assumes s to be a well-parsed string.
+ /// </summary>
+ public static string RemoveEscaping(string s, bool isVerbatimString) {
+ Contract.Requires(s != null);
+ var sb = new StringBuilder();
+ UnescapedCharacters(s, isVerbatimString).Iter(ch => sb.Append(ch));
+ return sb.ToString();
+ }
+ /// <summary>
+ /// Returns the characters of the well-parsed string p, replacing any
+ /// escaped characters by the actual characters.
+ /// </summary>
+ public static IEnumerable<char> UnescapedCharacters(string p, bool isVerbatimString) {
+ Contract.Requires(p != null);
+ if (isVerbatimString) {
+ var skipNext = false;
+ foreach (var ch in p) {
+ if (skipNext) {
+ skipNext = false;
+ } else {
+ yield return ch;
+ if (ch == '"') {
+ skipNext = true;
+ }
+ }
+ }
+ } else {
+ var i = 0;
+ while (i < p.Length) {
+ char special = ' '; // ' ' indicates not special
+ if (p[i] == '\\') {
+ switch (p[i + 1]) {
+ case '\'': special = '\''; break;
+ case '\"': special = '\"'; break;
+ case '\\': special = '\\'; break;
+ case '\0': special = '\0'; break;
+ case 'n': special = '\n'; break;
+ case 'r': special = '\r'; break;
+ case 't': special = '\t'; break;
+ case 'u':
+ int ch = HexValue(p[i + 1]);
+ ch = 16 * ch + HexValue(p[i + 2]);
+ ch = 16 * ch + HexValue(p[i + 3]);
+ ch = 16 * ch + HexValue(p[i + 4]);
+ yield return (char)ch;
+ i += 5;
+ continue;
+ default:
+ break;
+ }
+ }
+ if (special != ' ') {
+ yield return special;
+ i += 2;
+ } else {
+ yield return p[i];
+ i++;
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// Converts a hexadecimal digit to an integer.
+ /// Assumes ch does represent a hexadecimal digit; alphabetic digits can be in either case.
+ /// </summary>
+ public static int HexValue(char ch) {
+ if ('a' <= ch && ch <= 'f') {
+ return ch - 'a' + 10;
+ } else if ('A' <= ch && ch <= 'F') {
+ return ch - 'A' + 10;
+ } else {
+ return ch - '0';
+ }
+ }
+
}
}
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index f54d5184..f3c6fc4e 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -283,8 +283,9 @@ namespace DafnyLanguage case "break":
case "calc":
case "case":
+ case "char":
case "class":
- case "trait":
+ case "trait":
case "extends":
case "codatatype":
case "colemma":
@@ -336,6 +337,7 @@ namespace DafnyLanguage case "seq":
case "set":
case "static":
+ case "string":
case "then":
case "this":
case "true":
diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy index 11df8efe..9e1b511e 100644 --- a/Test/cloudmake/CloudMake-CachedBuilds.dfy +++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy @@ -247,7 +247,6 @@ abstract module M0 { type Path(==)
function Loc(cmd: string, deps: set<Path>, exp: string): Path
- type string(==)
type Artifact
type Identifier
diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy index 9463d8bc..815352f6 100644 --- a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy +++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy @@ -334,7 +334,6 @@ datatype Primitive = primCreatePath | primExec datatype Reason = rCompatibility | rValidity | rInconsistentCache
datatype Path = OpaquePath(int) | TransparentPath(int)
-type string(==)
type Artifact
type Identifier
diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy index a4f327ff..07cae317 100644 --- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy +++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy @@ -153,7 +153,6 @@ abstract module M0 { type Path(==)
function Loc(cmd: string, deps: set<Path>, exp: string): Path
- type string(==)
type Artifact
type Identifier
@@ -778,7 +777,6 @@ module M3 refines M2 { a
}
- datatype string = stringCons(int)
datatype Artifact = ArtifactCons(int)
datatype Identifier = IdentifierCons(int)
diff --git a/Test/dafny0/Strings.dfy b/Test/dafny0/Strings.dfy new file mode 100644 index 00000000..54764662 --- /dev/null +++ b/Test/dafny0/Strings.dfy @@ -0,0 +1,57 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%2.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Char(a: char, s: string, i: int) returns (b: char)
+{
+ var ch: char;
+ if a == ch {
+ b := ch;
+ } else if 0 <= i < |s| {
+ b := s[i];
+ }
+}
+
+// An attribute parameter that is a string literal is passed down
+// to Boogie as a string literal.
+method {:MyAttribute "hello", "hi" + "there", 57} AttrTest()
+{
+}
+
+method M(a: char, b: char) returns (s: string, t: seq<char>)
+ ensures |s| == 3 ==> t == [a, b, b];
+{
+ s := s + [a, b, b] + s;
+ t := s;
+ s := t[0..|s|];
+}
+
+method Main()
+{
+ var ch: char;
+ var s, t := M(ch, ch);
+ print "ch = ", ch, "\n";
+ print "The string is: " + s + "\n";
+ var x, y, z := Escapes();
+ print "Escape X: ", x, "\n";
+ print "Escape Y: ", y, "\n";
+ print "Escape Z: ", z, "\n";
+}
+
+method GimmieAChar(s: string) returns (ch: char)
+{
+ if s == "" {
+ ch := "tn"[1];
+ assert ch == "nt"[0];
+ } else {
+ var i :| 0 <= i < |s|; // if guard guarantees such an i exists
+ ch := s[i];
+ }
+}
+
+method Escapes() returns (x: string, y: string, z: string)
+{
+ x := "I say \"hello\" \\ you say \'good bye'";
+ y := @"I say ""hello"" \ you say 'good bye'";
+ assert x == y;
+ z := "There needs to be \u0052\u0026\u0044\n\tYes, sir";
+}
diff --git a/Test/dafny0/Strings.dfy.expect b/Test/dafny0/Strings.dfy.expect new file mode 100644 index 00000000..56bffd98 --- /dev/null +++ b/Test/dafny0/Strings.dfy.expect @@ -0,0 +1,11 @@ +
+Dafny program verifier finished with 12 verified, 0 errors
+Program compiled successfully
+Running...
+
+ch = D +The string is: DDD +Escape X: I say "hello" \ you say 'good bye' +Escape Y: I say "hello" \ you say 'good bye' +Escape Z: There needs to be R&D + Yes, sir diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index ab794e2f..656fdb06 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -45,8 +45,8 @@ "old" "forall" "exists" "new" "calc" "modify" "in" "this" "fresh"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '(
- "bool" "int" "nat" "real"
- "set" "multiset" "seq" "map"
+ "bool" "char" "int" "nat" "real"
+ "set" "multiset" "seq" "string" "map"
"object" "array" "array2" "array3")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index dc0d18c7..0b9348ea 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -6,7 +6,7 @@ \lstdefinelanguage{dafny}{
morekeywords={class,datatype,codatatype,newtype,type,iterator,trait,extends,
- bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map,
+ bool,char,nat,int,real,object,set,multiset,seq,string,map,array,array2,array3,
function,predicate,copredicate,
ghost,var,static,refines,
method,lemma,constructor,colemma,
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index 92c0b079..a98d1e2f 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -13,7 +13,7 @@ syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while syntax keyword dafnyStatement assume assert return yield new print break label where calc modify syntax keyword dafnyKeyword var ghost returns yields null static this refines include -syntax keyword dafnyType bool nat int real seq set multiset object array array2 array3 map +syntax keyword dafnyType bool char nat int real set multiset seq string map object array array2 array3 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh syntax keyword dafnyBoolean true false |