diff options
Diffstat (limited to 'Source/Dafny/Parser.cs')
| -rw-r--r-- | Source/Dafny/Parser.cs | 94 |
1 files changed, 53 insertions, 41 deletions
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index c3648310..41fc89c5 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -25,7 +25,7 @@ public class Parser { const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -144,10 +144,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);
}
@@ -160,15 +160,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 {
@@ -192,7 +192,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -788,7 +788,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else SynErr(110);
} else if (la.kind == 32) {
Get();
- Expressions(decreases);
+ DecreasesList(decreases, false);
Expect(17);
} else SynErr(111);
}
@@ -818,14 +818,24 @@ List<Expression/*!*/>/*!*/ decreases) { fe = new FrameExpression(e, fieldName);
}
- void Expressions(List<Expression/*!*/>/*!*/ args) {
- Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
- Expression(out e);
- args.Add(e);
+ void DecreasesList(List<Expression/*!*/> decreases, bool allowWildcard) {
+ Expression/*!*/ e;
+ PossiblyWildExpression(out e);
+ if (!allowWildcard && e is WildcardExpr) {
+ SemErr(e.tok, "'decreases *' is only allowed on loops");
+ } else {
+ decreases.Add(e);
+ }
+
while (la.kind == 19) {
Get();
- Expression(out e);
- args.Add(e);
+ PossiblyWildExpression(out e);
+ if (!allowWildcard && e is WildcardExpr) {
+ SemErr(e.tok, "'decreases *' is only allowed on loops");
+ } else {
+ decreases.Add(e);
+ }
+
}
}
@@ -900,7 +910,7 @@ List<Expression/*!*/>/*!*/ decreases) { ens.Add(e);
} else if (la.kind == 32) {
Get();
- Expressions(decreases);
+ DecreasesList(decreases, false);
Expect(17);
} else SynErr(113);
}
@@ -1333,6 +1343,17 @@ List<Expression/*!*/>/*!*/ decreases) { } else SynErr(123);
}
+ void Expressions(List<Expression/*!*/>/*!*/ args) {
+ Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
+ Expression(out e);
+ args.Add(e);
+ while (la.kind == 19) {
+ Get();
+ Expression(out e);
+ args.Add(e);
+ }
+ }
+
void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
Expect(33);
@@ -1385,13 +1406,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(17);
} else {
Get();
- PossiblyWildExpression(out e);
- decreases.Add(e);
- while (la.kind == 19) {
- Get();
- PossiblyWildExpression(out e);
- decreases.Add(e);
- }
+ DecreasesList(decreases, true);
Expect(17);
}
}
@@ -2164,13 +2179,13 @@ 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,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},
@@ -2197,20 +2212,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;
@@ -2362,7 +2375,7 @@ public class Errors { default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2370,9 +2383,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++;
}
|