ltlparse.yy 4.65 KB
Newer Older
1
2
3
4
5
%{
#include <string>
#include "public.hh"
#include "ltlast/allnodes.hh"

6
extern spot::ltl::formula* result;
7
8
9
10
11
12
13
14
15

%}

%debug
%error-verbose
%union
{
  int token;
  std::string* str;
16
  spot::ltl::formula* ltl;
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
}

%{
/* Spotparse.hh and parsedecl.hh include each other recursively.
   We mut ensure that YYSTYPE is declared (by the above %union)
   before parsedecl.hh uses it. */
#include "parsedecl.hh"
using namespace spot::ltl;

// At the time of writing C++ support in Bison is quite
// new and there is still no way to pass error_list to
// the parser.  We use a global variable instead.
namespace spot
{
  namespace ltl
  {
    extern parse_error_list* error_list;
34
    extern environment* parse_environment;
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
  }
}
%}

/* Logical operators.  */
%left <token> OP_AND OP_XOR OP_OR
%left <token> OP_IMPLIES OP_EQUIV

/* LTL operators.  */
%left <token> OP_U OP_R
%nonassoc <token> OP_F OP_G
%nonassoc <token> OP_X

/* Not has the most important priority.  */
%nonassoc <token> OP_NOT

/* Grouping (parentheses).  */
%token <token> PAR_OPEN PAR_CLOSE

/* Atomic proposition.  */
%token <str> ATOMIC_PROP

/* Constants */
%token CONST_TRUE 
%token CONST_FALSE
%token END_OF_INPUT

62
%type <ltl> result ltl_formula subformula
63
64

%%
65
result:       ltl_formula END_OF_INPUT
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
              { result = $$ = $1; 
		YYACCEPT;
	      }
	    | many_errors END_OF_INPUT
              { error_list->push_back(parse_error(@1,
				      "couldn't parse anything sensible")); 
	        result = $$ = 0;
		YYABORT;
	      }
	    | END_OF_INPUT
              { error_list->push_back(parse_error(@1,
				      "empty input")); 
	        result = $$ = 0;
		YYABORT;
	      }

many_errors_diagnosed : many_errors 
              { error_list->push_back(parse_error(@1, 
				     "unexpected input ignored")); }

86
ltl_formula: subformula
87
              { $$ = $1; }
88
	    | many_errors_diagnosed subformula
89
              { $$ = $2; }
90
	    | ltl_formula many_errors_diagnosed
91
92
93
94
95
              { $$ = $1; }

many_errors: error
	    | many_errors error

96
subformula: ATOMIC_PROP
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
	      { 
		$$ = parse_environment->require(*$1); 
		if (! $$)
		  {
		    std::string s = "unknown atomic proposition `";
		    s += *$1;
		    s += "' in environment `";
		    s += parse_environment->name();
		    s += "'";
		    error_list->push_back(parse_error(@1, s));
		    delete $1; 
		    YYERROR;
		  }
		else
		  delete $1; 
	      }
113
114
115
116
	    | CONST_TRUE
              { $$ = new constant(constant::True); }
	    | CONST_FALSE
              { $$ = new constant(constant::False); }
117
	    | PAR_OPEN subformula PAR_CLOSE
118
119
120
121
122
123
	      { $$ = $2; }
	    | PAR_OPEN error PAR_CLOSE
              { error_list->push_back(parse_error(@$, 
                 "treating this parenthetical block as false")); 
	        $$ = new constant(constant::False);
	      }
124
	    | PAR_OPEN subformula many_errors PAR_CLOSE
125
126
127
128
              { error_list->push_back(parse_error(@3, 
				      "unexpected input ignored")); 
	        $$ = $2;
	      }
129
	    | OP_NOT subformula
130
	      { $$ = new unop(unop::Not, $2); }
131
            | subformula OP_AND subformula
132
	      { $$ = new multop(multop::And, $1, $3); }
133
	    | subformula OP_OR subformula
134
	      { $$ = new multop(multop::Or, $1, $3); }
135
	    | subformula OP_XOR subformula
136
	      { $$ = new binop(binop::Xor, $1, $3); }
137
	    | subformula OP_IMPLIES subformula
138
	      { $$ = new binop(binop::Implies, $1, $3); }
139
            | subformula OP_EQUIV subformula
140
	      { $$ = new binop(binop::Equiv, $1, $3); }
141
            | subformula OP_U subformula
142
	      { $$ = new binop(binop::U, $1, $3); }
143
            | subformula OP_R subformula
144
	      { $$ = new binop(binop::R, $1, $3); }
145
            | OP_F subformula
146
	      { $$ = new unop(unop::F, $2); }
147
            | OP_G subformula
148
	      { $$ = new unop(unop::G, $2); }
149
            | OP_X subformula
150
	      { $$ = new unop(unop::X, $2); }
151
//	    | subformula many_errors
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
//              { error_list->push_back(parse_error(@2, 
//		  "ignoring these unexpected trailing tokens")); 
//	        $$ = $1;
//	      }
	    
;

%%

void
yy::Parser::print_()
{
  if (looka_ == ATOMIC_PROP) 
    YYCDEBUG << " '" << *value.str << "'";
}

void
yy::Parser::error_()
{
  error_list->push_back(parse_error(location, message));
}

174
formula* result = 0;
175
176
177
178
179
180

namespace spot
{
  namespace ltl
  {
    parse_error_list* error_list;
181
    environment* parse_environment;
182

183
    formula*
184
185
    parse(const std::string& ltl_string, 
	  parse_error_list& error_list,
186
	  environment& env,
187
188
189
190
	  bool debug)
    {
      result = 0;
      ltl::error_list = &error_list;
191
      parse_environment = &env;
192
193
194
195
196
197
198
199
200
201
202
      flex_set_buffer(ltl_string.c_str());
      yy::Parser parser(debug, yy::Location());
      parser.parse();  
      return result;
    }
  }
}

// Local Variables:
// mode: c++
// End: