diff options
| -rw-r--r-- | Source/Dafny/Compiler.cs | 8 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 96 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 116 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 540 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 79 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 213 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 191 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 129 | ||||
| -rw-r--r-- | Test/dafny0/Parallel.dfy | 84 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 2 | ||||
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/syntax/dafny.vim | 2 |
14 files changed, 962 insertions, 504 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index e531e2c5..47f5a98a 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -696,6 +696,9 @@ namespace Microsoft.Dafny { CheckHasNoAssumes(t);
}
CheckHasNoAssumes(s.GivenBody);
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ CheckHasNoAssumes(s.Body);
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
foreach (MatchCaseStmt mc in s.Cases) {
@@ -890,6 +893,11 @@ namespace Microsoft.Dafny { wr.WriteLine("}");
}
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ Error("parallel statements are not yet supported by the Dafny compiler; stay tuned");
+ // TODO
+
} else if (stmt is ForeachStmt) {
ForeachStmt s = (ForeachStmt)stmt;
// List<Pair<TType,RhsType>> pendingUpdates = new List<Pair<TType,RhsType>>();
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 77eb3dbf..0092b4d9 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -19,7 +19,7 @@ static BuiltIns theBuiltIns; static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
-static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
+static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
static int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
@@ -632,6 +632,7 @@ OneStmt<out Statement/*!*/ s> | WhileStmt<out s>
| MatchStmt<out s>
| ForeachStmt<out s>
+ | ParallelStmt<out s>
| "label" (. x = t; .)
Ident<out id> ":"
OneStmt<out s> (. s.Labels = new LabelNode(x, id.val, s.Labels); .)
@@ -868,15 +869,16 @@ MatchStmt<out Statement/*!*/ s> .
CaseStatement<out MatchCaseStmt/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
- IToken/*!*/ x, id, arg;
+ IToken/*!*/ x, id;
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
.)
"case" (. x = t; .)
Ident<out id>
[ "("
- Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
- { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
+ IdentTypeOptional<out bv> (. arguments.Add(bv); .)
+ { "," IdentTypeOptional<out bv> (. arguments.Add(bv); .)
}
")" ]
"=>"
@@ -934,6 +936,31 @@ PrintStmt<out Statement/*!*/ s> }
";" (. s = new PrintStmt(x, args); .)
.
+
+ParallelStmt<out Statement/*!*/ s>
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
+ IToken/*!*/ x;
+ List<BoundVar/*!*/> bvars;
+ Attributes attrs;
+ Expression range;
+ var ens = new List<MaybeFreeExpression/*!*/>();
+ bool isFree;
+ Expression/*!*/ e;
+ Statement/*!*/ block;
+ IToken bodyStart, bodyEnd;
+ .)
+ "parallel" (. x = t; .)
+ "("
+ QuantifierDomain<out bvars, out attrs, out range>
+ ")"
+ { (. isFree = false; .)
+ [ "free" (. isFree = true; .)
+ ]
+ "ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
+ }
+ BlockStmt<out block, out bodyStart, out bodyEnd>
+ (. s = new ParallelStmt(x, bvars, attrs, range, ens, block); .)
+ .
/*------------------------------------------------------------------------*/
Expression<out Expression/*!*/ e>
=
@@ -1230,15 +1257,16 @@ MatchExpression<out Expression/*!*/ e> (. e = new MatchExpr(x, e, cases); .)
.
CaseExpression<out MatchCaseExpr/*!*/ c>
-= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
+= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
Expression/*!*/ body;
.)
"case" (. x = t; .)
Ident<out id>
[ "("
- Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
- { "," Ident<out arg> (. arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy())); .)
+ IdentTypeOptional<out bv> (. arguments.Add(bv); .)
+ { "," IdentTypeOptional<out bv> (. arguments.Add(bv); .)
}
")" ]
"=>"
@@ -1320,36 +1348,46 @@ Suffix<ref Expression/*!*/ e> QuantifierGuts<out Expression/*!*/ q>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
bool univ = false;
- BoundVar/*!*/ bv;
- List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
- Attributes attrs = null;
- Triggers trigs = null;
- Expression range = null;
+ List<BoundVar/*!*/> bvars;
+ Attributes attrs;
+ Expression range;
Expression/*!*/ body;
.)
( Forall (. x = t; univ = true; .)
| Exists (. x = t; .)
)
- IdentTypeOptional<out bv> (. bvars.Add(bv); .)
- { ","
- IdentTypeOptional<out bv> (. bvars.Add(bv); .)
- }
- { AttributeOrTrigger<ref attrs, ref trigs> }
- [ "|"
- Expression<out range>
- ]
+ QuantifierDomain<out bvars, out attrs, out range>
QSep
Expression<out body>
(. if (univ) {
- q = new ForallExpr(x, bvars, range, body, trigs, attrs);
+ q = new ForallExpr(x, bvars, range, body, attrs);
} else {
- q = new ExistsExpr(x, bvars, range, body, trigs, attrs);
+ q = new ExistsExpr(x, bvars, range, body, attrs);
}
.)
.
+
Forall = "forall" | '\u2200'.
Exists = "exists" | '\u2203'.
QSep = "::" | '\u2022'.
+
+QuantifierDomain<.out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range.>
+= (.
+ bvars = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
+ attrs = null;
+ range = null;
+ .)
+ IdentTypeOptional<out bv> (. bvars.Add(bv); .)
+ { ","
+ IdentTypeOptional<out bv> (. bvars.Add(bv); .)
+ }
+ { Attribute<ref attrs> }
+ [ "|"
+ Expression<out range>
+ ]
+ .
+
ComprehensionExpr<out Expression/*!*/ q>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
IToken/*!*/ x = Token.NoToken;
@@ -1397,20 +1435,10 @@ AttributeBody<ref Attributes attrs> .
AttributeArg<out Attributes.Argument/*!*/ arg>
= (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg; .)
- ( string (. arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); .)
- | Expression<out e> (. arg = new Attributes.Argument(e); .)
+ ( string (. arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); .)
+ | Expression<out e> (. arg = new Attributes.Argument(t, e); .)
)
.
-AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
-= (. List<Expression/*!*/> es = new List<Expression/*!*/>();
- .)
- "{"
- ( AttributeBody<ref attrs>
- | (. es = new List<Expression/*!*/>(); .)
- Expressions<es> (. trigs = new Triggers(es, trigs); .)
- )
- "}"
- .
/*------------------------------------------------------------------------*/
Idents<.List<string/*!*/>/*!*/ ids.>
= (. IToken/*!*/ id; .)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 1a0c97de..d9d5c486 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -102,19 +102,25 @@ namespace Microsoft.Dafny { }
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(string s) {
+ public Argument(IToken tok, string s) {
+ Contract.Requires(tok != null);
Contract.Requires(s != null);
+ Tok = tok;
S = s;
}
- public Argument(Expression e) {
+ public Argument(IToken tok, Expression e) {
+ Contract.Requires(tok != null);
Contract.Requires(e != null);
+ Tok = tok;
E = e;
}
}
@@ -1781,7 +1787,82 @@ namespace Microsoft.Dafny { }
}
- public class MatchStmt : Statement {
+ public class ParallelStmt : Statement
+ {
+ public readonly List<BoundVar/*!*/> BoundVars;
+ public readonly Attributes Attributes;
+ public readonly Expression/*!*/ Range;
+ public readonly List<MaybeFreeExpression/*!*/>/*!*/ Ens;
+ public readonly Statement Body; // used only until resolution; afterwards, use BodyAssign
+
+ public List<ComprehensionExpr.BoundedPool> Bounds; // initialized and filled in by resolver
+ // invariant: if successfully resolved, Bounds.Count == BoundVars.Count;
+
+ /// <summary>
+ /// Assign means there are no ensures clauses and the body consists of one update statement,
+ /// either to an object field or to an array.
+ /// Call means there are no ensures clauses and the body consists of a single call to a (presumably
+ /// ghost, but non-ghost is also allowed) method with no out-parameters and an empty modifies
+ /// clause.
+ /// Proof means there is at least one ensures clause, and the body consists of any (presumably ghost,
+ /// but non-ghost is also allowed) code without side effects on variables (including fields and array
+ /// elements) declared outside the body itself.
+ /// Notes:
+ /// * More kinds may be allowed in the future.
+ /// * One could also allow Call to call non-ghost methods without side effects. However, that
+ /// would seem pointless in the program, so they are disallowed (to avoid any confusion that
+ /// such use of the parallel statement might actually have a point).
+ /// * One could allow Proof even without ensures clauses that "export" what was learned.
+ /// However, that might give the false impression that the body is nevertheless exported.
+ /// </summary>
+ public enum ParBodyKind { Assign, Call, Proof }
+ public ParBodyKind Kind; // filled in during resolution
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(BoundVars != null);
+ Contract.Invariant(Range != null);
+ Contract.Invariant(Ens != null);
+ Contract.Invariant(Body != null);
+ }
+
+ public ParallelStmt(IToken tok, List<BoundVar> boundVars, Attributes attrs, Expression range, List<MaybeFreeExpression/*!*/>/*!*/ ens, Statement body)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(boundVars));
+ Contract.Requires(range != null);
+ Contract.Requires(cce.NonNullElements(ens));
+ Contract.Requires(body != null);
+ this.BoundVars = boundVars;
+ this.Attributes = attrs;
+ this.Range = range;
+ this.Ens = ens;
+ this.Body = body;
+ }
+
+ public Statement S0 {
+ get {
+ // dig into Body to find a single statement
+ Statement s = this.Body;
+ while (true) {
+ var block = s as BlockStmt;
+ if (block != null && block.Body.Count == 1) {
+ s = block.Body[0];
+ } else {
+ var conc = s as ConcreteSyntaxStatement;
+ if (conc != null && conc.ResolvedStatements.Count == 1) {
+ s = conc.ResolvedStatements[0];
+ } else {
+ return s;
+ }
+ }
+ }
+ }
+ }
+ }
+
+ public class MatchStmt : Statement
+ {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Source != null);
@@ -2593,37 +2674,18 @@ namespace Microsoft.Dafny { }
public abstract class QuantifierExpr : ComprehensionExpr {
- public readonly Triggers Trigs;
-
- public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Triggers trigs, Attributes attrs)
+ public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Attributes attrs)
: base(tok, bvars, range, term, attrs) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(bvars));
Contract.Requires(term != null);
-
- this.Trigs = trigs;
}
public abstract Expression/*!*/ LogicalBody();
}
- public class Triggers {
- public readonly List<Expression/*!*/>/*!*/ Terms;
- public readonly Triggers Prev;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(Terms));
- }
-
- public Triggers(List<Expression/*!*/>/*!*/ terms, Triggers prev) {
- Contract.Requires(cce.NonNullElements(terms));
- this.Terms = terms;
- this.Prev = prev;
- }
- }
-
public class ForallExpr : QuantifierExpr {
- public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)
- : base(tok, bvars, range, term, trig, attrs) {
+ public ForallExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Attributes attrs)
+ : base(tok, bvars, range, term, attrs) {
Contract.Requires(cce.NonNullElements(bvars));
Contract.Requires(tok != null);
Contract.Requires(term != null);
@@ -2640,8 +2702,8 @@ namespace Microsoft.Dafny { }
public class ExistsExpr : QuantifierExpr {
- public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Triggers trig, Attributes attrs)
- : base(tok, bvars, range, term, trig, attrs) {
+ public ExistsExpr(IToken tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression term, Attributes attrs)
+ : base(tok, bvars, range, term, attrs) {
Contract.Requires(cce.NonNullElements(bvars));
Contract.Requires(tok != null);
Contract.Requires(term != null);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index ed0e285b..483217e5 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -18,12 +18,12 @@ public class Parser { public const int _digits = 2;
public const int _arrayToken = 3;
public const int _string = 4;
- public const int maxT = 104;
+ public const int maxT = 105;
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -36,7 +36,7 @@ static BuiltIns theBuiltIns; static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
-static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
+static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
static int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
@@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -182,7 +182,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -375,7 +375,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
- } else SynErr(105);
+ } else SynErr(106);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -490,7 +490,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! } else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(106);
+ } else SynErr(107);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
if (mmod.IsGhost) {
@@ -728,7 +728,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! ReferenceType(out tok, out ty);
break;
}
- default: SynErr(107); break;
+ default: SynErr(108); break;
}
}
@@ -779,12 +779,12 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
Expect(17);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(108);
+ } else SynErr(109);
} else if (la.kind == 32) {
Get();
DecreasesList(decreases, false);
Expect(17);
- } else SynErr(109);
+ } else SynErr(110);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -874,7 +874,7 @@ List<Expression/*!*/>/*!*/ decreases) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(110);
+ } else SynErr(111);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -906,7 +906,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
DecreasesList(decreases, false);
Expect(17);
- } else SynErr(111);
+ } else SynErr(112);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -925,7 +925,7 @@ List<Expression/*!*/>/*!*/ decreases) { fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(6)) {
FrameExpression(out fe);
- } else SynErr(112);
+ } else SynErr(113);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -936,7 +936,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new WildcardExpr(t);
} else if (StartOf(6)) {
Expression(out e);
- } else SynErr(113);
+ } else SynErr(114);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -969,7 +969,7 @@ List<Expression/*!*/>/*!*/ decreases) { PrintStmt(out s);
break;
}
- case 1: case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
+ case 1: case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
UpdateStmt(out s);
break;
}
@@ -993,6 +993,10 @@ List<Expression/*!*/>/*!*/ decreases) { ForeachStmt(out s);
break;
}
+ case 67: {
+ ParallelStmt(out s);
+ break;
+ }
case 46: {
Get();
x = t;
@@ -1013,7 +1017,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
breakCount++;
}
- } else SynErr(114);
+ } else SynErr(115);
Expect(17);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
@@ -1022,7 +1026,7 @@ List<Expression/*!*/>/*!*/ decreases) { ReturnStmt(out s);
break;
}
- default: SynErr(115); break;
+ default: SynErr(116); break;
}
}
@@ -1093,7 +1097,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 22) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(116);
+ } else SynErr(117);
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1166,13 +1170,13 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(117);
+ } else SynErr(118);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(118);
+ } else SynErr(119);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1198,7 +1202,7 @@ List<Expression/*!*/>/*!*/ decreases) { LoopSpec(out invariants, out decreases, out mod);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives);
- } else SynErr(119);
+ } else SynErr(120);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1265,6 +1269,38 @@ List<Expression/*!*/>/*!*/ decreases) { }
+ void ParallelStmt(out Statement/*!*/ s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null);
+ IToken/*!*/ x;
+ List<BoundVar/*!*/> bvars;
+ Attributes attrs;
+ Expression range;
+ var ens = new List<MaybeFreeExpression/*!*/>();
+ bool isFree;
+ Expression/*!*/ e;
+ Statement/*!*/ block;
+ IToken bodyStart, bodyEnd;
+
+ Expect(67);
+ x = t;
+ Expect(33);
+ QuantifierDomain(out bvars, out attrs, out range);
+ Expect(34);
+ while (la.kind == 29 || la.kind == 31) {
+ isFree = false;
+ if (la.kind == 29) {
+ Get();
+ isFree = true;
+ }
+ Expect(31);
+ Expression(out e);
+ Expect(17);
+ ens.Add(new MaybeFreeExpression(e, isFree));
+ }
+ BlockStmt(out block, out bodyStart, out bodyEnd);
+ s = new ParallelStmt(x, bvars, attrs, range, ens, block);
+ }
+
void ReturnStmt(out Statement/*!*/ s) {
IToken returnTok = null;
List<AssignmentRhs> rhss = null;
@@ -1335,7 +1371,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(6)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(120);
+ } else SynErr(121);
}
void Lhs(out Expression e) {
@@ -1352,7 +1388,7 @@ List<Expression/*!*/>/*!*/ decreases) { while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
- } else SynErr(121);
+ } else SynErr(122);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1375,7 +1411,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(6)) {
Expression(out ee);
e = ee;
- } else SynErr(122);
+ } else SynErr(123);
Expect(34);
}
@@ -1440,8 +1476,9 @@ List<Expression/*!*/>/*!*/ decreases) { void CaseStatement(out MatchCaseStmt/*!*/ c) {
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
- IToken/*!*/ x, id, arg;
+ IToken/*!*/ x, id;
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
Expect(57);
@@ -1449,12 +1486,12 @@ List<Expression/*!*/>/*!*/ decreases) { Ident(out id);
if (la.kind == 33) {
Get();
- Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ IdentTypeOptional(out bv);
+ arguments.Add(bv);
while (la.kind == 19) {
Get();
- Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ IdentTypeOptional(out bv);
+ arguments.Add(bv);
}
Expect(34);
}
@@ -1469,17 +1506,39 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg;
if (la.kind == 4) {
Get();
- arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2));
+ arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2));
} else if (StartOf(6)) {
Expression(out e);
- arg = new Attributes.Argument(e);
- } else SynErr(123);
+ arg = new Attributes.Argument(t, e);
+ } else SynErr(124);
+ }
+
+ void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
+ bvars = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
+ attrs = null;
+ range = null;
+
+ IdentTypeOptional(out bv);
+ bvars.Add(bv);
+ while (la.kind == 19) {
+ Get();
+ IdentTypeOptional(out bv);
+ bvars.Add(bv);
+ }
+ while (la.kind == 7) {
+ Attribute(ref attrs);
+ }
+ if (la.kind == 16) {
+ Get();
+ Expression(out range);
+ }
}
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 67 || la.kind == 68) {
+ while (la.kind == 68 || la.kind == 69) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1490,7 +1549,7 @@ List<Expression/*!*/>/*!*/ decreases) { void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 69 || la.kind == 70) {
+ if (la.kind == 70 || la.kind == 71) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1499,23 +1558,23 @@ List<Expression/*!*/>/*!*/ decreases) { }
void EquivOp() {
- if (la.kind == 67) {
+ if (la.kind == 68) {
Get();
- } else if (la.kind == 68) {
+ } else if (la.kind == 69) {
Get();
- } else SynErr(124);
+ } else SynErr(125);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (la.kind == 71 || la.kind == 72) {
+ if (la.kind == 72 || la.kind == 73) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 71 || la.kind == 72) {
+ while (la.kind == 72 || la.kind == 73) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1526,7 +1585,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 73 || la.kind == 74) {
+ while (la.kind == 74 || la.kind == 75) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1537,11 +1596,11 @@ List<Expression/*!*/>/*!*/ decreases) { }
void ImpliesOp() {
- if (la.kind == 69) {
+ if (la.kind == 70) {
Get();
- } else if (la.kind == 70) {
+ } else if (la.kind == 71) {
Get();
- } else SynErr(125);
+ } else SynErr(126);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1635,25 +1694,25 @@ List<Expression/*!*/>/*!*/ decreases) { }
void AndOp() {
- if (la.kind == 71) {
+ if (la.kind == 72) {
Get();
- } else if (la.kind == 72) {
+ } else if (la.kind == 73) {
Get();
- } else SynErr(126);
+ } else SynErr(127);
}
void OrOp() {
- if (la.kind == 73) {
+ if (la.kind == 74) {
Get();
- } else if (la.kind == 74) {
+ } else if (la.kind == 75) {
Get();
- } else SynErr(127);
+ } else SynErr(128);
}
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 84 || la.kind == 85) {
+ while (la.kind == 85 || la.kind == 86) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1666,7 +1725,7 @@ List<Expression/*!*/>/*!*/ decreases) { IToken y;
switch (la.kind) {
- case 75: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
@@ -1681,22 +1740,22 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 76: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 77: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 78: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 79: {
+ case 80: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
@@ -1706,7 +1765,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 80: {
+ case 81: {
Get();
x = t; y = Token.NoToken;
if (la.kind == 63) {
@@ -1724,29 +1783,29 @@ List<Expression/*!*/>/*!*/ decreases) { break;
}
- case 81: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(128); break;
+ default: SynErr(129); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 44 || la.kind == 86 || la.kind == 87) {
+ while (la.kind == 44 || la.kind == 87 || la.kind == 88) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1755,33 +1814,33 @@ List<Expression/*!*/>/*!*/ decreases) { 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 == 84) {
+ if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 85) {
+ } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(129);
+ } else SynErr(130);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 85: {
+ case 86: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 80: case 88: {
+ case 81: case 89: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 38: case 55: case 61: case 98: case 99: case 100: case 101: {
+ case 38: case 55: case 61: case 99: case 100: case 101: case 102: {
EndlessExpression(out e);
break;
}
@@ -1800,14 +1859,14 @@ List<Expression/*!*/>/*!*/ decreases) { MultiSetExpr(out e);
break;
}
- case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
+ case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
ConstAtomExpression(out e);
while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
break;
}
- default: SynErr(130); break;
+ default: SynErr(131); break;
}
}
@@ -1816,21 +1875,21 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 44) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 86) {
+ } else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 87) {
+ } else if (la.kind == 88) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(131);
+ } else SynErr(132);
}
void NegOp() {
- if (la.kind == 80) {
+ if (la.kind == 81) {
Get();
- } else if (la.kind == 88) {
+ } else if (la.kind == 89) {
Get();
- } else SynErr(132);
+ } else SynErr(133);
}
void EndlessExpression(out Expression e) {
@@ -1842,7 +1901,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
x = t;
Expression(out e);
- Expect(96);
+ Expect(97);
Expression(out e0);
Expect(56);
Expression(out e1);
@@ -1853,7 +1912,7 @@ List<Expression/*!*/>/*!*/ decreases) { QuantifierGuts(out e);
} else if (la.kind == 38) {
ComprehensionExpr(out e);
- } else SynErr(133);
+ } else SynErr(134);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1904,7 +1963,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (StartOf(6)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 97) {
+ if (la.kind == 98) {
Get();
anyDots = true;
if (StartOf(6)) {
@@ -1926,15 +1985,15 @@ List<Expression/*!*/>/*!*/ decreases) { multipleIndices.Add(ee);
}
- } else SynErr(134);
- } else if (la.kind == 97) {
+ } else SynErr(135);
+ } else if (la.kind == 98) {
Get();
anyDots = true;
if (StartOf(6)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(135);
+ } else SynErr(136);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -1958,7 +2017,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(52);
- } else SynErr(136);
+ } else SynErr(137);
}
void DisplayExpr(out Expression e) {
@@ -1982,7 +2041,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
e = new SeqDisplayExpr(x, elements);
Expect(52);
- } else SynErr(137);
+ } else SynErr(138);
}
void MultiSetExpr(out Expression e) {
@@ -2008,7 +2067,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(34);
} else if (StartOf(16)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(138);
+ } else SynErr(139);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2017,17 +2076,17 @@ List<Expression/*!*/>/*!*/ decreases) { e = dummyExpr;
switch (la.kind) {
- case 89: {
+ case 90: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 90: {
+ case 91: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 91: {
+ case 92: {
Get();
e = new LiteralExpr(t);
break;
@@ -2037,12 +2096,12 @@ List<Expression/*!*/>/*!*/ decreases) { e = new LiteralExpr(t, n);
break;
}
- case 92: {
+ case 93: {
Get();
e = new ThisExpr(t);
break;
}
- case 93: {
+ case 94: {
Get();
x = t;
Expect(33);
@@ -2051,7 +2110,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new FreshExpr(x, e);
break;
}
- case 94: {
+ case 95: {
Get();
x = t;
Expect(33);
@@ -2060,7 +2119,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new AllocatedExpr(x, e);
break;
}
- case 95: {
+ case 96: {
Get();
x = t;
Expect(33);
@@ -2085,7 +2144,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(34);
break;
}
- default: SynErr(139); break;
+ default: SynErr(140); break;
}
}
@@ -2117,40 +2176,25 @@ List<Expression/*!*/>/*!*/ decreases) { void QuantifierGuts(out Expression/*!*/ q) {
Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
bool univ = false;
- BoundVar/*!*/ bv;
- List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
- Attributes attrs = null;
- Triggers trigs = null;
- Expression range = null;
+ List<BoundVar/*!*/> bvars;
+ Attributes attrs;
+ Expression range;
Expression/*!*/ body;
- if (la.kind == 98 || la.kind == 99) {
+ if (la.kind == 99 || la.kind == 100) {
Forall();
x = t; univ = true;
- } else if (la.kind == 100 || la.kind == 101) {
+ } else if (la.kind == 101 || la.kind == 102) {
Exists();
x = t;
- } else SynErr(140);
- IdentTypeOptional(out bv);
- bvars.Add(bv);
- while (la.kind == 19) {
- Get();
- IdentTypeOptional(out bv);
- bvars.Add(bv);
- }
- while (la.kind == 7) {
- AttributeOrTrigger(ref attrs, ref trigs);
- }
- if (la.kind == 16) {
- Get();
- Expression(out range);
- }
+ } else SynErr(141);
+ QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
if (univ) {
- q = new ForallExpr(x, bvars, range, body, trigs, attrs);
+ q = new ForallExpr(x, bvars, range, body, attrs);
} else {
- q = new ExistsExpr(x, bvars, range, body, trigs, attrs);
+ q = new ExistsExpr(x, bvars, range, body, attrs);
}
}
@@ -2174,7 +2218,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(16);
Expression(out range);
- if (la.kind == 102 || la.kind == 103) {
+ if (la.kind == 103 || la.kind == 104) {
QSep();
Expression(out body);
}
@@ -2184,8 +2228,9 @@ List<Expression/*!*/>/*!*/ decreases) { }
void CaseExpression(out MatchCaseExpr/*!*/ c) {
- Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
+ Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
+ BoundVar/*!*/ bv;
Expression/*!*/ body;
Expect(57);
@@ -2193,12 +2238,12 @@ List<Expression/*!*/>/*!*/ decreases) { Ident(out id);
if (la.kind == 33) {
Get();
- Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ IdentTypeOptional(out bv);
+ arguments.Add(bv);
while (la.kind == 19) {
Get();
- Ident(out arg);
- arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
+ IdentTypeOptional(out bv);
+ arguments.Add(bv);
}
Expect(34);
}
@@ -2208,39 +2253,25 @@ List<Expression/*!*/>/*!*/ decreases) { }
void Forall() {
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
- } else if (la.kind == 99) {
+ } else if (la.kind == 100) {
Get();
- } else SynErr(141);
+ } else SynErr(142);
}
void Exists() {
- if (la.kind == 100) {
+ if (la.kind == 101) {
Get();
- } else if (la.kind == 101) {
+ } else if (la.kind == 102) {
Get();
- } else SynErr(142);
- }
-
- void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
- List<Expression/*!*/> es = new List<Expression/*!*/>();
-
- Expect(7);
- if (la.kind == 22) {
- AttributeBody(ref attrs);
- } else if (StartOf(6)) {
- es = new List<Expression/*!*/>();
- Expressions(es);
- trigs = new Triggers(es, trigs);
} else SynErr(143);
- Expect(8);
}
void QSep() {
- if (la.kind == 102) {
+ if (la.kind == 103) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 104) {
Get();
} else SynErr(144);
}
@@ -2269,32 +2300,32 @@ List<Expression/*!*/>/*!*/ decreases) { public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
static readonly bool[,]/*!*/ set = {
- {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,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,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, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,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,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,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,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,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,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,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,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, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
- {x,x,x,x, x,x,x,T, T,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,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
- {x,T,T,x, T,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,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,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,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, 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,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,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,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,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,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,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,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,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,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x, x,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,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,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, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T, T,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,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,T,T,x, x,x,x,T, T,x,x},
+ {x,T,T,x, T,x,x,T, 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,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}
};
} // end Parser
@@ -2303,20 +2334,18 @@ List<Expression/*!*/>/*!*/ decreases) { public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
-
- public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+ public virtual void SynErr(string filename, int line, int col, string msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
-
- string GetSyntaxErrorString(int n) {
+ }
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2386,88 +2415,88 @@ public class Errors { case 64: s = "\"assert\" expected"; break;
case 65: s = "\"assume\" expected"; break;
case 66: s = "\"print\" expected"; break;
- case 67: s = "\"<==>\" expected"; break;
- case 68: s = "\"\\u21d4\" expected"; break;
- case 69: s = "\"==>\" expected"; break;
- case 70: s = "\"\\u21d2\" expected"; break;
- case 71: s = "\"&&\" expected"; break;
- case 72: s = "\"\\u2227\" expected"; break;
- case 73: s = "\"||\" expected"; break;
- case 74: s = "\"\\u2228\" expected"; break;
- case 75: s = "\"==\" expected"; break;
- case 76: s = "\"<=\" expected"; break;
- case 77: s = "\">=\" expected"; break;
- case 78: s = "\"!=\" expected"; break;
- case 79: s = "\"!!\" expected"; break;
- case 80: s = "\"!\" expected"; break;
- case 81: s = "\"\\u2260\" expected"; break;
- case 82: s = "\"\\u2264\" expected"; break;
- case 83: s = "\"\\u2265\" expected"; break;
- case 84: s = "\"+\" expected"; break;
- case 85: s = "\"-\" expected"; break;
- case 86: s = "\"/\" expected"; break;
- case 87: s = "\"%\" expected"; break;
- case 88: s = "\"\\u00ac\" expected"; break;
- case 89: s = "\"false\" expected"; break;
- case 90: s = "\"true\" expected"; break;
- case 91: s = "\"null\" expected"; break;
- case 92: s = "\"this\" expected"; break;
- case 93: s = "\"fresh\" expected"; break;
- case 94: s = "\"allocated\" expected"; break;
- case 95: s = "\"old\" expected"; break;
- case 96: s = "\"then\" expected"; break;
- case 97: s = "\"..\" expected"; break;
- case 98: s = "\"forall\" expected"; break;
- case 99: s = "\"\\u2200\" expected"; break;
- case 100: s = "\"exists\" expected"; break;
- case 101: s = "\"\\u2203\" expected"; break;
- case 102: s = "\"::\" expected"; break;
- case 103: s = "\"\\u2022\" expected"; break;
- case 104: s = "??? expected"; break;
- case 105: s = "invalid ClassMemberDecl"; break;
- case 106: s = "invalid MethodDecl"; break;
- case 107: s = "invalid TypeAndToken"; break;
- case 108: s = "invalid MethodSpec"; break;
+ case 67: s = "\"parallel\" expected"; break;
+ case 68: s = "\"<==>\" expected"; break;
+ case 69: s = "\"\\u21d4\" expected"; break;
+ case 70: s = "\"==>\" expected"; break;
+ case 71: s = "\"\\u21d2\" expected"; break;
+ case 72: s = "\"&&\" expected"; break;
+ case 73: s = "\"\\u2227\" expected"; break;
+ case 74: s = "\"||\" expected"; break;
+ case 75: s = "\"\\u2228\" expected"; break;
+ case 76: s = "\"==\" expected"; break;
+ case 77: s = "\"<=\" expected"; break;
+ case 78: s = "\">=\" expected"; break;
+ case 79: s = "\"!=\" expected"; break;
+ case 80: s = "\"!!\" expected"; break;
+ case 81: s = "\"!\" expected"; break;
+ case 82: s = "\"\\u2260\" expected"; break;
+ case 83: s = "\"\\u2264\" expected"; break;
+ case 84: s = "\"\\u2265\" expected"; break;
+ case 85: s = "\"+\" expected"; break;
+ case 86: s = "\"-\" expected"; break;
+ case 87: s = "\"/\" expected"; break;
+ case 88: s = "\"%\" expected"; break;
+ case 89: s = "\"\\u00ac\" expected"; break;
+ case 90: s = "\"false\" expected"; break;
+ case 91: s = "\"true\" expected"; break;
+ case 92: s = "\"null\" expected"; break;
+ case 93: s = "\"this\" expected"; break;
+ case 94: s = "\"fresh\" expected"; break;
+ case 95: s = "\"allocated\" expected"; break;
+ case 96: s = "\"old\" expected"; break;
+ case 97: s = "\"then\" expected"; break;
+ case 98: s = "\"..\" expected"; break;
+ case 99: s = "\"forall\" expected"; break;
+ case 100: s = "\"\\u2200\" expected"; break;
+ case 101: s = "\"exists\" expected"; break;
+ case 102: s = "\"\\u2203\" expected"; break;
+ case 103: s = "\"::\" expected"; break;
+ case 104: s = "\"\\u2022\" expected"; break;
+ case 105: s = "??? expected"; break;
+ case 106: s = "invalid ClassMemberDecl"; break;
+ case 107: s = "invalid MethodDecl"; break;
+ case 108: s = "invalid TypeAndToken"; break;
case 109: s = "invalid MethodSpec"; break;
- case 110: s = "invalid ReferenceType"; break;
- case 111: s = "invalid FunctionSpec"; break;
- case 112: s = "invalid PossiblyWildFrameExpression"; break;
- case 113: s = "invalid PossiblyWildExpression"; break;
- case 114: s = "invalid OneStmt"; break;
+ case 110: s = "invalid MethodSpec"; break;
+ case 111: s = "invalid ReferenceType"; break;
+ case 112: s = "invalid FunctionSpec"; break;
+ case 113: s = "invalid PossiblyWildFrameExpression"; break;
+ case 114: s = "invalid PossiblyWildExpression"; break;
case 115: s = "invalid OneStmt"; break;
- case 116: s = "invalid UpdateStmt"; break;
- case 117: s = "invalid IfStmt"; break;
+ case 116: s = "invalid OneStmt"; break;
+ case 117: s = "invalid UpdateStmt"; break;
case 118: s = "invalid IfStmt"; break;
- case 119: s = "invalid WhileStmt"; break;
- case 120: s = "invalid Rhs"; break;
- case 121: s = "invalid Lhs"; break;
- case 122: s = "invalid Guard"; break;
- case 123: s = "invalid AttributeArg"; break;
- case 124: s = "invalid EquivOp"; break;
- case 125: s = "invalid ImpliesOp"; break;
- case 126: s = "invalid AndOp"; break;
- case 127: s = "invalid OrOp"; break;
- case 128: s = "invalid RelOp"; break;
- case 129: s = "invalid AddOp"; break;
- case 130: s = "invalid UnaryExpression"; break;
- case 131: s = "invalid MulOp"; break;
- case 132: s = "invalid NegOp"; break;
- case 133: s = "invalid EndlessExpression"; break;
- case 134: s = "invalid Suffix"; break;
+ case 119: s = "invalid IfStmt"; break;
+ case 120: s = "invalid WhileStmt"; break;
+ case 121: s = "invalid Rhs"; break;
+ case 122: s = "invalid Lhs"; break;
+ case 123: s = "invalid Guard"; break;
+ case 124: s = "invalid AttributeArg"; break;
+ case 125: s = "invalid EquivOp"; break;
+ case 126: s = "invalid ImpliesOp"; break;
+ case 127: s = "invalid AndOp"; break;
+ case 128: s = "invalid OrOp"; break;
+ case 129: s = "invalid RelOp"; break;
+ case 130: s = "invalid AddOp"; break;
+ case 131: s = "invalid UnaryExpression"; break;
+ case 132: s = "invalid MulOp"; break;
+ case 133: s = "invalid NegOp"; break;
+ case 134: s = "invalid EndlessExpression"; break;
case 135: s = "invalid Suffix"; break;
case 136: s = "invalid Suffix"; break;
- case 137: s = "invalid DisplayExpr"; break;
- case 138: s = "invalid MultiSetExpr"; break;
- case 139: s = "invalid ConstAtomExpression"; break;
- case 140: s = "invalid QuantifierGuts"; break;
- case 141: s = "invalid Forall"; break;
- case 142: s = "invalid Exists"; break;
- case 143: s = "invalid AttributeOrTrigger"; break;
+ case 137: s = "invalid Suffix"; break;
+ case 138: s = "invalid DisplayExpr"; break;
+ case 139: s = "invalid MultiSetExpr"; break;
+ case 140: s = "invalid ConstAtomExpression"; break;
+ case 141: s = "invalid QuantifierGuts"; break;
+ case 142: s = "invalid Forall"; break;
+ case 143: s = "invalid Exists"; break;
case 144: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2475,9 +2504,8 @@ public class Errors { Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
-
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 97324ef9..f9f1eca0 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -36,9 +36,9 @@ namespace Microsoft.Dafny { if (module.IsDefaultModule) {
PrintTopLevelDecls(module.TopLevelDecls, 0);
} else {
- wr.Write("module ");
+ wr.Write("module");
PrintAttributes(module.Attributes);
- wr.Write("{0} ", module.Name);
+ wr.Write(" {0} ", module.Name);
if (module.Imports.Count != 0) {
string sep = "imports ";
foreach (string imp in module.Imports) {
@@ -127,15 +127,18 @@ namespace Microsoft.Dafny { }
}
+ /// <summary>
+ /// Prints no space before "kind", but does print a space before "attrs" and "name".
+ /// </summary>
void PrintClassMethodHelper(string kind, Attributes attrs, string name, List<TypeParameter> typeArgs) {
Contract.Requires(kind != null);
Contract.Requires(name != null);
Contract.Requires(typeArgs != null);
if (kind.Length != 0) {
- wr.Write("{0} ", kind);
+ wr.Write(kind);
}
PrintAttributes(attrs);
- wr.Write(name);
+ wr.Write(" {0}", name);
if (typeArgs.Count != 0) {
wr.Write("<");
string sep = "";
@@ -152,7 +155,7 @@ namespace Microsoft.Dafny { Contract.Requires(dt != null);
Indent(indent);
PrintClassMethodHelper("datatype", dt.Attributes, dt.Name, dt.TypeArgs);
- wr.Write(" = ");
+ wr.Write(" =");
string sep = "";
foreach (DatatypeCtor ctor in dt.Ctors) {
wr.Write(sep);
@@ -160,18 +163,21 @@ namespace Microsoft.Dafny { if (ctor.Formals.Count != 0) {
PrintFormals(ctor.Formals);
}
- sep = " | ";
+ sep = " |";
}
wr.WriteLine(";");
}
+ /// <summary>
+ /// Prints a space before each attribute.
+ /// </summary>
public void PrintAttributes(Attributes a) {
if (a != null) {
PrintAttributes(a.Prev);
- wr.Write("{{:{0}", a.Name);
+ wr.Write(" {{:{0}", a.Name);
PrintAttributeArgs(a.Args);
- wr.Write("} ");
+ wr.Write("}");
}
}
@@ -197,9 +203,9 @@ namespace Microsoft.Dafny { if (field.IsGhost) {
wr.Write("ghost ");
}
- wr.Write("var ");
+ wr.Write("var");
PrintAttributes(field.Attributes);
- wr.Write("{0}: ", field.Name);
+ wr.Write(" {0}: ", field.Name);
PrintType(field.Type);
wr.WriteLine(";");
}
@@ -454,7 +460,6 @@ namespace Microsoft.Dafny { } else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
- wr.Write("call ");
if (s.Lhs.Count != 0) {
string sep = "";
foreach (IdentifierExpr v in s.Lhs) {
@@ -557,6 +562,19 @@ namespace Microsoft.Dafny { Indent(indent);
wr.Write("}");
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ wr.Write("parallel (");
+ PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);
+ if (s.Ens.Count == 0) {
+ wr.Write(") ");
+ } else {
+ wr.WriteLine(")");
+ PrintSpec("ensures", s.Ens, indent + IndentAmount);
+ Indent(indent);
+ }
+ PrintStatement(s.Body, indent);
+
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
wr.Write("match ");
@@ -1022,21 +1040,8 @@ namespace Microsoft.Dafny { bool parensNeeded = !isRightmost;
if (parensNeeded) { wr.Write("("); }
wr.Write(e is ForallExpr ? "forall " : "exists ");
- string sep = "";
- foreach (BoundVar bv in e.BoundVars) {
- wr.Write("{0}{1}", sep, bv.Name);
- sep = ", ";
- PrintType(": ", bv.Type);
- }
- wr.Write(" ");
- PrintAttributes(e.Attributes);
- PrintTriggers(e.Trigs);
- if (e.Range != null) {
- wr.Write("| ");
- PrintExpression(e.Range);
- wr.Write(" ");
- }
- wr.Write(":: ");
+ PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range);
+ wr.Write(" :: ");
if (0 <= indent) {
int ind = indent + IndentAmount;
wr.WriteLine();
@@ -1058,9 +1063,8 @@ namespace Microsoft.Dafny { sep = ", ";
PrintType(": ", bv.Type);
}
- wr.Write(" ");
PrintAttributes(e.Attributes);
- wr.Write("| ");
+ wr.Write(" | ");
PrintExpression(e.Range);
if (!e.TermIsImplicit) {
wr.Write(" :: ");
@@ -1108,13 +1112,18 @@ namespace Microsoft.Dafny { }
}
- void PrintTriggers(Triggers trigs) {
- if (trigs != null) {
- PrintTriggers(trigs.Prev);
-
- wr.Write("{ ");
- PrintExpressionList(trigs.Terms);
- wr.Write(" } ");
+ private void PrintQuantifierDomain(List<BoundVar> boundVars, Attributes attrs, Expression range) {
+ Contract.Requires(boundVars != null);
+ string sep = "";
+ foreach (BoundVar bv in boundVars) {
+ wr.Write("{0}{1}", sep, bv.Name);
+ sep = ", ";
+ PrintType(": ", bv.Type);
+ }
+ PrintAttributes(attrs);
+ if (range != null) {
+ wr.Write(" | ");
+ PrintExpression(range);
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 54a3de3b..ca173dbc 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -584,15 +584,6 @@ namespace Microsoft.Dafny { }
}
- void ResolveTriggers(Triggers trigs, bool twoState) {
- // order does not matter for resolution, so resolve them in reverse order
- for (; trigs != null; trigs = trigs.Prev) {
- foreach (Expression e in trigs.Terms) {
- ResolveExpression(e, twoState);
- }
- }
- }
-
void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {
Contract.Requires(tparams != null);
@@ -1529,6 +1520,79 @@ namespace Microsoft.Dafny { scope.PopMarker();
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+
+ int prevErrorCount = ErrorCount;
+ scope.PushMarker();
+ foreach (BoundVar v in s.BoundVars) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate bound-variable name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type);
+ }
+ if (s.Range != null) {
+ ResolveExpression(s.Range, true);
+ Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(s.Range.Type, Type.Bool)) {
+ Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type);
+ }
+ }
+ foreach (var ens in s.Ens) {
+ ResolveExpression(ens.E, true);
+ Contract.Assert(ens.E.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(ens.E.Type, Type.Bool)) {
+ Error(ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);
+ }
+ }
+ // Since the range and postconditions are more likely to infer the types of the bound variables, resolve them
+ // first (above) and only then resolve the attributes (below).
+ ResolveAttributes(s.Attributes, true);
+
+ bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == ErrorCount && UsesSpecFeatures(s.Range));
+ if (!bodyMustBeSpecOnly && prevErrorCount == ErrorCount) {
+ var missingBounds = new List<BoundVar>();
+ s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, missingBounds);
+ if (missingBounds.Count != 0) {
+ bodyMustBeSpecOnly = true;
+ }
+ }
+ s.IsGhost = bodyMustBeSpecOnly;
+ ResolveStatement(s.Body, bodyMustBeSpecOnly, method);
+ scope.PopMarker();
+
+ if (prevErrorCount == ErrorCount) {
+ // check for supported kinds
+ if (s.Ens.Count == 0) {
+ // The supported kinds are Assign and Call. See if it's one of them.
+ Statement s0 = s.S0;
+ if (s0 is AssignStmt) {
+ var lhs = ((AssignStmt)s0).Lhs.Resolved;
+ if (lhs is IdentifierExpr) {
+ Error(s0, "a parallel statement must not update local variables declared outside the parallel body");
+ } else if (lhs is FieldSelectExpr) {
+ // cool
+ } else if (lhs is SeqSelectExpr && ((SeqSelectExpr)lhs).SelectOne) {
+ // cool
+ } else if (lhs is MultiSelectExpr) {
+ // cool
+ } else {
+ Error(s0, "unexpected or disallowed assignment LHS in parallel statement");
+ }
+ s.Kind = ParallelStmt.ParBodyKind.Assign;
+ } else if (s0 is CallStmt) {
+ CheckNoForeignUpdates(s0);
+ s.Kind = ParallelStmt.ParBodyKind.Call;
+ } else {
+ Error(s, "the body of an ensures-less parallel statement must be one assignment statement or one call statement");
+ }
+ } else {
+ // The only supported kind with ensures clauses is Proof. See if that's what the body really is.
+ CheckNoForeignUpdates(s.Body);
+ s.Kind = ParallelStmt.ParBodyKind.Proof;
+ }
+ }
+
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
bool bodyIsSpecOnly = specContextOnly;
@@ -1649,23 +1713,19 @@ namespace Microsoft.Dafny { var tr = (TypeRhs)rhs;
ResolveTypeRhs(tr, s, specContextOnly, method);
isEffectful = tr.InitCall != null;
- }
- else if (rhs is HavocRhs) {
+ } else if (rhs is HavocRhs) {
isEffectful = false;
- }
- else {
+ } else {
var er = (ExprRhs)rhs;
if (er.Expr is IdentifierSequence) {
var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);
isEffectful = cRhs != null;
callRhs = callRhs ?? cRhs;
- }
- else if (er.Expr is FunctionCallExpr) {
+ } else if (er.Expr is FunctionCallExpr) {
var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);
isEffectful = cRhs != null;
callRhs = callRhs ?? cRhs;
- }
- else {
+ } else {
ResolveExpression(er.Expr, true);
isEffectful = false;
}
@@ -1681,8 +1741,7 @@ namespace Microsoft.Dafny { if (ie != null) {
if (lhsNameSet.ContainsKey(ie.Name)) {
Error(s, "Duplicate variable in left-hand side of {1} statement: {0}", ie.Name, callRhs != null ? "call" : "assignment");
- }
- else {
+ } else {
lhsNameSet.Add(ie.Name, null);
}
}
@@ -1992,6 +2051,115 @@ namespace Microsoft.Dafny { }
}
+ public void CheckNoForeignUpdates(Statement stmt) {
+ Contract.Requires(stmt != null);
+ if (stmt is PredicateStmt) {
+ // cool
+ } else if (stmt is PrintStmt) {
+ Error(stmt, "print statement is not allowed inside a parallel statement");
+ } else if (stmt is BreakStmt) {
+ // TODO: this case can be checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack
+ } else if (stmt is ReturnStmt) {
+ Error(stmt, "return statement is not allowed inside a parallel statement");
+ } else if (stmt is ConcreteSyntaxStatement) {
+ var s = (ConcreteSyntaxStatement)stmt;
+ foreach (var ss in s.ResolvedStatements) {
+ CheckNoForeignUpdates(ss);
+ }
+ } else if (stmt is AssignStmt) {
+ var s = (AssignStmt)stmt;
+ var idExpr = s.Lhs as IdentifierExpr;
+ if (idExpr != null) {
+ if (scope.ContainsDecl(idExpr.Var)) {
+ Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");
+ }
+ } else {
+ Error(stmt, "the body of the enclosing parallel statement may not updated heap locations");
+ }
+ } else if (stmt is VarDecl) {
+ // cool
+ } else if (stmt is CallStmt) {
+ var s = (CallStmt)stmt;
+ foreach (var lhs in s.Lhs) {
+ var idExpr = lhs as IdentifierExpr;
+ if (idExpr != null) {
+ if (scope.ContainsDecl(idExpr.Var)) {
+ Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");
+ }
+ } else {
+ Error(stmt, "the body of the enclosing parallel statement may not updated heap locations");
+ }
+ }
+ if (s.Method.Mod.Count != 0) {
+ Error(s, "in the body of a parallel statement, every method called must have an empty modifies list");
+ }
+
+ } else if (stmt is BlockStmt) {
+ var s = (BlockStmt)stmt;
+ scope.PushMarker();
+ foreach (var ss in s.Body) {
+ CheckNoForeignUpdates(ss);
+ }
+ scope.PopMarker();
+
+ } else if (stmt is IfStmt) {
+ var s = (IfStmt)stmt;
+ CheckNoForeignUpdates(s.Thn);
+ if (s.Els != null) {
+ CheckNoForeignUpdates(s.Els);
+ }
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ foreach (var alt in s.Alternatives) {
+ foreach (var ss in alt.Body) {
+ CheckNoForeignUpdates(ss);
+ }
+ }
+
+ } else if (stmt is WhileStmt) {
+ WhileStmt s = (WhileStmt)stmt;
+ CheckNoForeignUpdates(s.Body);
+
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ foreach (var alt in s.Alternatives) {
+ foreach (var ss in alt.Body) {
+ CheckNoForeignUpdates(ss);
+ }
+ }
+
+ } else if (stmt is ForeachStmt) {
+ Error(stmt, "foreach statement not allowed in body of parallel statement");
+
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ switch (s.Kind) {
+ case ParallelStmt.ParBodyKind.Assign:
+ Error(stmt, "a parallel statement with heap updates is not allowed inside the body of another parallel statement");
+ break;
+ case ParallelStmt.ParBodyKind.Call:
+ case ParallelStmt.ParBodyKind.Proof:
+ // these are fine, since they don't update any non-local state
+ break;
+ default:
+ Contract.Assert(false); // unexpected kind
+ break;
+ }
+
+ } else if (stmt is MatchStmt) {
+ var s = (MatchStmt)stmt;
+ foreach (var kase in s.Cases) {
+ foreach (var ss in kase.Body) {
+ CheckNoForeignUpdates(ss);
+ }
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException();
+ }
+ }
+
Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, Method method) {
Contract.Requires(rr != null);
Contract.Requires(stmt != null);
@@ -2603,9 +2771,8 @@ namespace Microsoft.Dafny { Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);
}
// Since the body is more likely to infer the types of the bound variables, resolve it
- // first (above) and only then resolve the attributes and triggers (below).
+ // first (above) and only then resolve the attributes (below).
ResolveAttributes(e.Attributes, twoState);
- ResolveTriggers(e.Trigs, twoState);
scope.PopMarker();
expr.Type = Type.Bool;
@@ -3850,5 +4017,9 @@ namespace Microsoft.Dafny { Contract.Requires(name != null);
return Find(name, false);
}
+
+ public bool ContainsDecl(Thing t) {
+ return things.Exists(thing => thing == t);
+ }
}
}
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index b23cdb25..ae887c47 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,17 +31,15 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
- [ContractInvariantMethod]
- void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);
- }
-
-// [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
+[ContractInvariantMethod]
+void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);}
+ [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -53,12 +51,12 @@ public class Buffer { buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -75,14 +73,14 @@ public class Buffer { }
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -102,7 +100,7 @@ public class Buffer { Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -141,7 +139,7 @@ public class Buffer { }
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -211,24 +209,23 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 104;
- const int noSym = 104;
-
-
- [ContractInvariantMethod]
- void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
- }
-
+ const int maxT = 105;
+ const int noSym = 105;
+
+
+[ContractInvariantMethod]
+void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+}
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -239,13 +236,13 @@ public class Scanner { Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -293,9 +290,9 @@ public class Scanner { start[Buffer.EOF] = -1;
}
-
-// [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
+
+ [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -305,14 +302,15 @@ public class Scanner { Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
+
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
-// [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
+
+ [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -321,9 +319,10 @@ public class Scanner { buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
+
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -344,11 +343,11 @@ public class Scanner { Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -359,7 +358,7 @@ public class Scanner { }
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -367,9 +366,9 @@ public class Scanner { // // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -419,7 +418,7 @@ public class Scanner { return;
}
-
+
}
}
@@ -531,16 +530,17 @@ public class Scanner { case "assert": t.kind = 64; break;
case "assume": t.kind = 65; break;
case "print": t.kind = 66; break;
- case "false": t.kind = 89; break;
- case "true": t.kind = 90; break;
- case "null": t.kind = 91; break;
- case "this": t.kind = 92; break;
- case "fresh": t.kind = 93; break;
- case "allocated": t.kind = 94; break;
- case "old": t.kind = 95; break;
- case "then": t.kind = 96; break;
- case "forall": t.kind = 98; break;
- case "exists": t.kind = 100; break;
+ case "parallel": t.kind = 67; break;
+ case "false": t.kind = 90; break;
+ case "true": t.kind = 91; break;
+ case "null": t.kind = 92; break;
+ case "this": t.kind = 93; break;
+ case "fresh": t.kind = 94; break;
+ case "allocated": t.kind = 95; break;
+ case "old": t.kind = 96; break;
+ case "then": t.kind = 97; break;
+ case "forall": t.kind = 99; break;
+ case "exists": t.kind = 101; break;
default: break;
}
}
@@ -557,13 +557,10 @@ public class Scanner { t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) {
- Contract.Assert(start[ch] != null);
- state = (int) start[ch];
- }
+ if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -669,56 +666,56 @@ public class Scanner { if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
case 30:
- {t.kind = 67; break;}
- case 31:
{t.kind = 68; break;}
- case 32:
+ case 31:
{t.kind = 69; break;}
- case 33:
+ case 32:
{t.kind = 70; break;}
+ case 33:
+ {t.kind = 71; break;}
case 34:
if (ch == '&') {AddCh(); goto case 35;}
else {goto case 0;}
case 35:
- {t.kind = 71; break;}
- case 36:
{t.kind = 72; break;}
- case 37:
+ case 36:
{t.kind = 73; break;}
- case 38:
+ case 37:
{t.kind = 74; break;}
+ case 38:
+ {t.kind = 75; break;}
case 39:
- {t.kind = 77; break;}
- case 40:
{t.kind = 78; break;}
- case 41:
+ case 40:
{t.kind = 79; break;}
+ case 41:
+ {t.kind = 80; break;}
case 42:
- {t.kind = 81; break;}
- case 43:
{t.kind = 82; break;}
- case 44:
+ case 43:
{t.kind = 83; break;}
- case 45:
+ case 44:
{t.kind = 84; break;}
- case 46:
+ case 45:
{t.kind = 85; break;}
- case 47:
+ case 46:
{t.kind = 86; break;}
- case 48:
+ case 47:
{t.kind = 87; break;}
- case 49:
+ case 48:
{t.kind = 88; break;}
+ case 49:
+ {t.kind = 89; break;}
case 50:
- {t.kind = 97; break;}
+ {t.kind = 98; break;}
case 51:
- {t.kind = 99; break;}
+ {t.kind = 100; break;}
case 52:
- {t.kind = 101; break;}
- case 53:
{t.kind = 102; break;}
- case 54:
+ case 53:
{t.kind = 103; break;}
+ case 54:
+ {t.kind = 104; break;}
case 55:
recEnd = pos; recKind = 15;
if (ch == '>') {AddCh(); goto case 28;}
@@ -746,31 +743,31 @@ public class Scanner { if (ch == '.') {AddCh(); goto case 50;}
else {t.kind = 53; break;}
case 61:
- recEnd = pos; recKind = 80;
+ recEnd = pos; recKind = 81;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
- else {t.kind = 80; break;}
+ else {t.kind = 81; break;}
case 62:
- recEnd = pos; recKind = 75;
+ recEnd = pos; recKind = 76;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 75; break;}
+ else {t.kind = 76; break;}
case 63:
- recEnd = pos; recKind = 76;
+ recEnd = pos; recKind = 77;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 76; break;}
+ else {t.kind = 77; break;}
}
t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -791,7 +788,7 @@ public class Scanner { }
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 3647efa6..3be3cd82 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1069,7 +1069,7 @@ namespace Microsoft.Dafny { stmts = builder.Collect(m.tok);
}
- QKeyValue kv = etran.TrAttributes(m.Attributes);
+ QKeyValue kv = etran.TrAttributes(m.Attributes, null);
Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
typeParams, inParams, outParams,
@@ -3121,7 +3121,7 @@ namespace Microsoft.Dafny { foreach (var lhs in s.Lhss) {
lhss.Add(lhs.Resolved);
}
- bool rhssCanAffectPreviouslyKnownExpressions = !s.Rhss.TrueForAll(rhs => !rhs.CanAffectPreviouslyKnownExpressions);
+ bool rhssCanAffectPreviouslyKnownExpressions = s.Rhss.Exists(rhs => rhs.CanAffectPreviouslyKnownExpressions);
List<AssignToLhs> lhsBuilder;
List<Bpl.IdentifierExpr> bLhss;
ProcessLhss(lhss, rhssCanAffectPreviouslyKnownExpressions, builder, locals, etran, out lhsBuilder, out bLhss);
@@ -3356,6 +3356,79 @@ namespace Microsoft.Dafny { builder.Add(CaptureState(stmt.Tok));
+ } else if (stmt is ParallelStmt) {
+ AddComment(builder, stmt, "parallel statement");
+ var s = (ParallelStmt)stmt;
+ if (s.Kind == ParallelStmt.ParBodyKind.Assign) {
+
+ // Given:
+ // parallel (x,y | Range(x,y)) {
+ // (a) E(x,y) . f := G(x,y);
+ // (b) A(x,y) [ I0(x,y), I1(x,y), ... ] := G(x,y);
+ // }
+ // translate into:
+ // if (*) {
+ // // check definedness of Range
+ // var x,y;
+ // havoc x,y;
+ // CheckWellDefined( Range );
+ // assume Range;
+ // // check definedness of the other expressions
+ // (a)
+ // CheckWellDefined( E );
+ // assert Tr(E) != null;
+ // check that E.f is in the modifies frame;
+ // CheckWellDefined( G );
+ // check nat restrictions for the RHS
+ // (b)
+ // CheckWellDefined( A );
+ // assert Tr(A) != null;
+ // CheckWellDefined( I0 );
+ // assert 0 <= Tr(I0) && Tr(I0) < Tr(A).Length0;
+ // CheckWellDefined( I1 );
+ // assert 0 <= Tr(I0) && Tr(I0) < Tr(A).Length1;
+ // ...
+ // check that A[I0,I1,...] is in the modifies frame;
+ // CheckWellDefined( G );
+ // check nat restrictions for the RHS
+ // // check for duplicate LHSs
+ // var x', y';
+ // havoc x', y';
+ // assume Range[x,y := x',y'];
+ // assume !(x == x' && y == y');
+ // (a)
+ // assert E(x,y) != E(x',y');
+ // (b)
+ // assert !( I0(x,y)==I0(x',y') && I1(x,y)==I1(x',y') && ... );
+ //
+ // assume false;
+ //
+ // } else {
+ // var oldHeap := $Heap;
+ // havoc $Heap;
+ // assume $HeapSucc(oldHeap, $Heap);
+ // (a)
+ // assume (forall<alpha> o: ref, F: Field alpha ::
+ // $Heap[o,F] = oldHeap[o,F] ||
+ // (exists x,y :: Range(x,y) && o == E(x,y) && F = f));
+ // assume (forall x,y :: Range ==> $Heap[ E[$Heap:=oldHeap], F] == G[$Heap:=oldHeap]);
+ // (b)
+ // assume (forall<alpha> o: ref, F: Field alpha ::
+ // $Heap[o,F] = oldHeap[o,F] ||
+ // (exists x,y :: Range(x,y) && o == A(x,y) && F = Index(I0,I1,...)));
+ // assume (forall x,y :: Range ==> $Heap[ A[$Heap:=oldHeap], Index(I0,I1,...)] == G[$Heap:=oldHeap]);
+ // }
+
+ // TODO: do the above
+
+ } else if (s.Kind == ParallelStmt.ParBodyKind.Call) {
+ // TODO: call forall
+ } else if (s.Kind == ParallelStmt.ParBodyKind.Proof) {
+ // TODO
+ } else {
+ Contract.Assert(false); // unexpected kind
+ }
+
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);
@@ -4169,6 +4242,9 @@ namespace Microsoft.Dafny { }
}
+ /// <summary>
+ /// "lhs" is expected to be a resolved form of an expression, i.e., not a conrete-syntax expression.
+ /// </summary>
void TrAssignment(IToken tok, Expression lhs, AssignmentRhs rhs,
Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran)
{
@@ -4184,7 +4260,7 @@ namespace Microsoft.Dafny { List<AssignToLhs> lhsBuilder;
List<Bpl.IdentifierExpr> bLhss;
- var lhss = new List<Expression>() { lhs.Resolved };
+ var lhss = new List<Expression>() { lhs };
ProcessLhss(lhss, rhs.CanAffectPreviouslyKnownExpressions, builder, locals, etran,
out lhsBuilder, out bLhss);
Contract.Assert(lhsBuilder.Count == 1 && bLhss.Count == 1); // guaranteed by postcondition of ProcessLhss
@@ -5059,14 +5135,20 @@ namespace Microsoft.Dafny { QuantifierExpr e = (QuantifierExpr)expr;
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);
- Bpl.QKeyValue kv = TrAttributes(e.Attributes);
+ Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");
Bpl.Trigger tr = null;
- for (Triggers trigs = e.Trigs; trigs != null; trigs = trigs.Prev) {
- Bpl.ExprSeq tt = new Bpl.ExprSeq();
- foreach (Expression term in trigs.Terms) {
- tt.Add(TrExpr(term));
+ for (Attributes aa = e.Attributes; aa != null; aa = aa.Prev) {
+ if (aa.Name == "trigger") {
+ Bpl.ExprSeq tt = new Bpl.ExprSeq();
+ foreach (var arg in aa.Args) {
+ if (arg.E == null) {
+ Console.WriteLine("Warning: string argument to 'trigger' attribute ignored");
+ } else {
+ tt.Add(TrExpr(arg.E));
+ }
+ }
+ tr = new Bpl.Trigger(expr.tok, true, tt, tr);
}
- tr = new Bpl.Trigger(expr.tok, true, tt, tr);
}
var antecedent = typeAntecedent;
if (e.Range != null) {
@@ -5086,7 +5168,7 @@ namespace Microsoft.Dafny { // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))".
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);
- Bpl.QKeyValue kv = TrAttributes(e.Attributes);
+ Bpl.QKeyValue kv = TrAttributes(e.Attributes, null);
var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$y#" + translator.otherTmpVarCount, predef.BoxType));
translator.otherTmpVarCount++;
@@ -5373,9 +5455,10 @@ namespace Microsoft.Dafny { return Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType)), Bpl.Expr.Literal(0));
}
- public Bpl.QKeyValue TrAttributes(Attributes attrs) {
+ public Bpl.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) {
Bpl.QKeyValue kv = null;
- while (attrs != null) {
+ for ( ; attrs != null; attrs = attrs.Prev) {
+ if (attrs.Name == skipThisAttribute) { continue; }
List<object> parms = new List<object>();
foreach (Attributes.Argument arg in attrs.Args) {
if (arg.E != null) {
@@ -5385,7 +5468,6 @@ namespace Microsoft.Dafny { }
}
kv = new Bpl.QKeyValue(Token.NoToken, attrs.Name, parms, kv);
- attrs = attrs.Prev;
}
return kv;
}
@@ -6455,12 +6537,11 @@ namespace Microsoft.Dafny { }
} else if (e is QuantifierExpr) {
var q = (QuantifierExpr)e;
- Triggers newTrigs = SubstTriggers(q.Trigs, receiverReplacement, substMap);
- if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes || newTrigs != q.Trigs) {
+ if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {
if (expr is ForallExpr) {
- newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
+ newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);
} else {
- newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newTrigs, newAttrs);
+ newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);
}
}
} else {
@@ -6517,18 +6598,6 @@ namespace Microsoft.Dafny { }
}
- static Triggers SubstTriggers(Triggers trigs, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
- if (trigs != null) {
- List<Expression> terms = SubstituteExprList(trigs.Terms, receiverReplacement, substMap);
- Triggers prev = SubstTriggers(trigs.Prev, receiverReplacement, substMap);
- if (terms != trigs.Terms || prev != trigs.Prev) {
- return new Triggers(terms, prev);
- }
- }
- return trigs;
- }
-
static Attributes SubstAttributes(Attributes attrs, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
if (attrs != null) {
@@ -6539,7 +6608,7 @@ namespace Microsoft.Dafny { if (arg.E != null) {
Expression newE = Substitute(arg.E, receiverReplacement, substMap);
if (newE != arg.E) {
- newArg = new Attributes.Argument(newE);
+ newArg = new Attributes.Argument(arg.Tok, newE);
anyArgSubst = true;
}
}
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy new file mode 100644 index 00000000..0928c070 --- /dev/null +++ b/Test/dafny0/Parallel.dfy @@ -0,0 +1,84 @@ +/*
+method ParallelStatement_Syntax()
+{
+ parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {
+ a[i] := a[(i + 1) % a.Length] + 3;
+ }
+
+ parallel (o | o in spine) {
+ o.f := o.f + Repr;
+ }
+
+ parallel (x, y | x in S && 0 <= y+x < 100) {
+ Lemma(x, y);
+ }
+
+ parallel (p | 0 <= p)
+ ensures F(p) <= Sum(p) * (p-1) + 100;
+ {
+ assert G(p);
+ ghost var t;
+ if (p % 2 == 0) {
+ assert G(p) == F(p+2);
+ t := p*p;
+ } else {
+ assume H(p, 20) < 100; // don't know how to justify this
+ t := p;
+ }
+ PowerLemma(p, t);
+ t := t + 1;
+ PowerLemma(p, t);
+ }
+}
+*/
+
+class C {
+ var f: set<object>;
+}
+
+method ParallelStatement_Resolve(
+ a: array<int>,
+ spine: set<C>,
+ Repr: set<object>,
+ S: set<int>
+ )
+ requires a != null;
+ modifies a, spine;
+{
+ parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {
+ a[i] := a[(i + 1) % a.Length] + 3;
+ }
+
+ parallel (o | o in spine) {
+ o.f := o.f + Repr;
+ }
+
+ parallel (x, y | x in S && 0 <= y+x < 100) {
+ Lemma(x, y);
+ }
+
+ parallel (p | 0 <= p)
+ ensures F(p) <= Sum(p) * (p-1) + 100;
+ {
+ assert 0 <= G(p);
+ ghost var t;
+ if (p % 2 == 0) {
+ assert G(p) == F(p+2);
+ t := p*p;
+ } else {
+ assume H(p, 20) < 100; // don't know how to justify this
+ t := p;
+ }
+ PowerLemma(p, t);
+ t := t + 1;
+ PowerLemma(p, t);
+ }
+}
+
+method Lemma(x: int, y: int)
+ghost method PowerLemma(x: int, y: int)
+
+function F(x: int): int
+function G(x: int): int
+function H(x: int, y: int): int
+function Sum(x: int): int
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index e352ad70..98006cca 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -37,7 +37,7 @@ )) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
"assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print"
- "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "allocated"
+ "old" "forall" "exists" "new" "foreach" "parallel" "in" "this" "fresh" "allocated"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
)
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index df0f22ee..8fc8bf4e 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -20,7 +20,7 @@ namespace Demo "assert", "assume", "new", "this", "object", "refines", "replaces", "by",
"unlimited", "module", "imports",
"if", "then", "else", "while", "invariant",
- "break", "label", "return", "foreach", "havoc", "print",
+ "break", "label", "return", "foreach", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
"function", "free",
@@ -287,6 +287,7 @@ namespace Demo | "label"
| "return"
| "foreach"
+ | "parallel"
| "havoc"
| "print"
| "returns"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 619f5f8d..5e61d2d6 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -272,6 +272,7 @@ namespace DafnyLanguage case "null":
case "object":
case "old":
+ case "parallel":
case "print":
case "reads":
case "refines":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index ebcd7fb6..809c6fc4 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -13,7 +13,7 @@ % expressions
match,case,false,true,null,old,fresh,allocated,choose,this,
% statements
- assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,foreach,
+ assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,foreach,parallel,
},
literate=%
{:}{$\colon$}1
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index e26227ed..4014e427 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -8,7 +8,7 @@ syntax case match syntax keyword dafnyFunction function method constructor syntax keyword dafnyTypeDef class datatype syntax keyword dafnyConditional if then else match case -syntax keyword dafnyRepeat foreach while +syntax keyword dafnyRepeat foreach while parallel syntax keyword dafnyStatement havoc assume assert return new print break label syntax keyword dafnyKeyword var ghost returns null static this refines replaces by syntax keyword dafnyType bool nat int seq set object array array2 array3 |