summaryrefslogtreecommitdiff
path: root/Dafny/parser.frame
blob: de0ba1fbd7eef9a322c00697336171d0dc03d9f8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103

using Microsoft.Contracts;

namespace Microsoft.-->namespace {

public class Parser {
-->constants
	const bool T = true;
	const bool x = false;
	const int minErrDist = 2;
	
	static Token/*!*/ token;			// last recognized token
	static Token/*!*/ t;				// lookahead token
	static int errDist = minErrDist;

	-->declarations

	static void Error(int n) {
		if (errDist >= minErrDist) Errors.SynErr(n, t.filename, t.line, t.col);
		errDist = 0;
	}
	
	public static void SemErr(string! msg) {
		if (errDist >= minErrDist) Errors.SemErr(token.filename, token.line, token.col, msg);
		errDist = 0;
	}

	public static void SemErr(Token! tok, string! msg) {
		if (errDist >= minErrDist) Errors.SemErr(tok.filename, tok.line, tok.col, msg);
		errDist = 0;
	}

	static void Get() {
		for (;;) {
			token = t;
			t = Scanner.Scan();
			if (t.kind<=maxT) {errDist++; return;}
-->pragmas
			t = token;
		}
	}
	
	static void Expect(int n) {
		if (t.kind==n) Get(); else Error(n);
	}
	
	static bool StartOf(int s) {
		return set[s, t.kind];
	}
	
	static void ExpectWeak(int n, int follow) {
		if (t.kind == n) Get();
		else {
			Error(n);
			while (!StartOf(follow)) Get();
		}
	}
	
	static bool WeakSeparator(int n, int syFol, int repFol) {
		bool[] s = new bool[maxT+1];
		if (t.kind == n) {Get(); return true;}
		else if (StartOf(repFol)) return false;
		else {
			for (int i=0; i <= maxT; i++) {
				s[i] = set[syFol, i] || set[repFol, i] || set[0, i];
			}
			Error(n);
			while (!s[t.kind]) Get();
			return StartOf(syFol);
		}
	}
	
-->productions

	public static void Parse() {
		Errors.SynErr = new ErrorProc(SynErr);
		t = new Token();
		Get();
-->parseRoot
	}

	[Microsoft.Contracts.Verify(false)]
	static void SynErr(int n, string filename, int line, int col) {
		Errors.count++;
		System.Console.Write("{0}({1},{2}): syntax error: ", filename, line, col);
		string s;
		switch (n) {
-->errors
			default: s = "error " + n; break;
		}
		System.Console.WriteLine(s);
	}

	static bool[,]! set = {
-->initialization
	};

	[Microsoft.Contracts.Verify(false)]
	static Parser() {}
} // end Parser

} // end namespace
$$$