spot  2.10.5
parseaut.hh
Go to the documentation of this file.
1 // A Bison parser, made by GNU Bison 3.7.5.
2 
3 // Skeleton interface for Bison LALR(1) parsers in C++
4 
5 // Copyright (C) 2002-2015, 2018-2021 Free Software Foundation, Inc.
6 
7 // This program is free software: you can redistribute it and/or modify
8 // it under the terms of the GNU General Public License as published by
9 // the Free Software Foundation, either version 3 of the License, or
10 // (at your option) any later version.
11 
12 // This program is distributed in the hope that it will be useful,
13 // but WITHOUT ANY WARRANTY; without even the implied warranty of
14 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 // GNU General Public License for more details.
16 
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 // As a special exception, you may create a larger work that contains
21 // part or all of the Bison parser skeleton and distribute that work
22 // under terms of your choice, so long as that work isn't itself a
23 // parser generator using the skeleton or a modified version thereof
24 // as a parser skeleton. Alternatively, if you modify or redistribute
25 // the parser skeleton itself, you may (at your option) remove this
26 // special exception, which will cause the skeleton and the resulting
27 // Bison output files to be licensed under the GNU General Public
28 // License without this special exception.
29 
30 // This special exception was added by the Free Software Foundation in
31 // version 2.2 of Bison.
32 
33 
39 // C++ LALR(1) parser skeleton written by Akim Demaille.
40 
41 // DO NOT RELY ON FEATURES THAT ARE NOT DOCUMENTED in the manual,
42 // especially those whose name start with YY_ or yy_. They are
43 // private implementation details that can be changed or removed.
44 
45 #ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED
46 # define YY_HOAYY_PARSEAUT_HH_INCLUDED
47 // "%code requires" blocks.
48 #line 33 "parseaut.yy"
49 
50 #include "config.h"
51 #include <spot/misc/common.hh>
52 #include <spot/priv/robin_hood.hh>
53 #include <string>
54 #include <cstring>
55 #include <sstream>
56 #include <unordered_map>
57 #include <algorithm>
58 #include <spot/twa/formula2bdd.hh>
59 #include <spot/parseaut/public.hh>
60 #include "spot/priv/accmap.hh"
61 #include <spot/tl/parse.hh>
62 #include <spot/twaalgos/alternation.hh>
63 
64 using namespace std::string_literals;
65 
66 #ifndef HAVE_STRVERSCMP
67 // If the libc does not have this, a version is compiled in lib/.
68 extern "C" int strverscmp(const char *s1, const char *s2);
69 #endif
70 
71 // Work around Bison not letting us write
72 // %lex-param { res.h->errors, res.fcache }
73 #define PARSE_ERROR_LIST res.h->errors, res.fcache
74 
75  inline namespace hoayy_support
76  {
77  typedef std::map<int, bdd> map_t;
78 
79  /* Cache parsed formulae. Labels on arcs are frequently identical
80  and it would be a waste of time to parse them to formula
81  over and over, and to register all their atomic_propositions in
82  the bdd_dict. Keep the bdd result around so we can reuse
83  it. */
84  typedef robin_hood::unordered_flat_map<std::string, bdd> formula_cache;
85 
86  typedef std::pair<int, std::string*> pair;
87  typedef spot::twa_graph::namer<std::string> named_tgba_t;
88 
89  // Note: because this parser is meant to be used on a stream of
90  // automata, it tries hard to recover from errors, so that we get a
91  // chance to reach the end of the current automaton in order to
92  // process the next one. Several variables below are used to keep
93  // track of various error conditions.
94  enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
95  Implicit_Labels };
96  enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
97 
98  struct result_
99  {
100  struct state_info
101  {
102  bool declared = false;
103  bool used = false;
104  spot::location used_loc;
105  };
106  spot::parsed_aut_ptr h;
107  spot::twa_ptr aut_or_ks;
109  std::string format_version;
110  spot::location format_version_loc;
111  spot::environment* env;
112  formula_cache fcache;
113  named_tgba_t* namer = nullptr;
114  spot::acc_mapper_int* acc_mapper = nullptr;
115  std::vector<int> ap;
116  std::vector<bdd> guards;
117  std::vector<bdd>::const_iterator cur_guard;
118  // If "Alias: ..." occurs before "AP: ..." in the HOA format we
119  // are in trouble because the parser would like to turn each
120  // alias into a BDD, yet the atomic proposition have not been
121  // declared yet. We solve that by using arbitrary BDD variables
122  // numbers (in fact we use the same number given in the Alias:
123  // definition) and keeping track of the highest variable number
124  // we have seen (unknown_ap_max). Once AP: is encountered,
125  // we can remap everything. If AP: is never encountered an
126  // unknown_ap_max is non-negative, then we can signal an error.
127  int unknown_ap_max = -1;
128  spot::location unknown_ap_max_location;
129  bool in_alias = false;
130  map_t dest_map;
131  std::vector<state_info> info_states; // States declared and used.
132  std::vector<std::pair<spot::location,
133  std::vector<unsigned>>> start; // Initial states;
134  std::unordered_map<std::string, bdd> alias;
135  struct prop_info
136  {
137  spot::location loc;
138  bool val;
139  operator bool() const
140  {
141  return val;
142  };
143  };
144  std::unordered_map<std::string, prop_info> props;
145  spot::location states_loc;
146  spot::location ap_loc;
147  spot::location state_label_loc;
148  spot::location accset_loc;
149  spot::acc_cond::mark_t acc_state;
150  spot::acc_cond::mark_t neg_acc_sets = {};
151  spot::acc_cond::mark_t pos_acc_sets = {};
152  int plus;
153  int minus;
154  std::vector<std::string>* state_names = nullptr;
155  std::map<unsigned, unsigned>* highlight_edges = nullptr;
156  std::map<unsigned, unsigned>* highlight_states = nullptr;
157  std::map<unsigned, unsigned> states_map;
158  std::vector<bool>* state_player = nullptr;
159  spot::location state_player_loc;
160  std::set<int> ap_set;
161  unsigned cur_state;
162  int states = -1;
163  int ap_count = -1;
164  int accset = -1;
165  bdd state_label;
166  bdd cur_label;
167  bool has_state_label = false;
168  bool ignore_more_ap = false; // Set to true after the first "AP:"
169  // line has been read.
170  bool ignore_acc = false; // Set to true in case of missing
171  // Acceptance: lines.
172  bool ignore_acc_silent = false;
173  bool ignore_more_acc = false; // Set to true after the first
174  // "Acceptance:" line has been read.
175 
176  label_style_t label_style = Mixed_Labels;
177  acc_style_t acc_style = Mixed_Acc;
178 
179  bool accept_all_needed = false;
180  bool accept_all_seen = false;
181  bool aliased_states = false;
182 
183  spot::trival universal = spot::trival::maybe();
184  spot::trival existential = spot::trival::maybe();
185  spot::trival complete = spot::trival::maybe();
186  bool trans_acc_seen = false;
187 
188  std::map<std::string, spot::location> labels;
189 
190  prop_info prop_is_true(const std::string& p)
191  {
192  auto i = props.find(p);
193  if (i == props.end())
194  return prop_info{spot::location(), false};
195  return i->second;
196  }
197 
198  prop_info prop_is_false(const std::string& p)
199  {
200  auto i = props.find(p);
201  if (i == props.end())
202  return prop_info{spot::location(), false};
203  return prop_info{i->second.loc, !i->second.val};
204  }
205 
206  ~result_()
207  {
208  delete namer;
209  delete acc_mapper;
210  }
211  };
212  }
213 
214 #line 215 "parseaut.hh"
215 
216 
217 # include <cstdlib> // std::abort
218 # include <iostream>
219 # include <stdexcept>
220 # include <string>
221 # include <vector>
222 
223 #if defined __cplusplus
224 # define YY_CPLUSPLUS __cplusplus
225 #else
226 # define YY_CPLUSPLUS 199711L
227 #endif
228 
229 // Support move semantics when possible.
230 #if 201103L <= YY_CPLUSPLUS
231 # define YY_MOVE std::move
232 # define YY_MOVE_OR_COPY move
233 # define YY_MOVE_REF(Type) Type&&
234 # define YY_RVREF(Type) Type&&
235 # define YY_COPY(Type) Type
236 #else
237 # define YY_MOVE
238 # define YY_MOVE_OR_COPY copy
239 # define YY_MOVE_REF(Type) Type&
240 # define YY_RVREF(Type) const Type&
241 # define YY_COPY(Type) const Type&
242 #endif
243 
244 // Support noexcept when possible.
245 #if 201103L <= YY_CPLUSPLUS
246 # define YY_NOEXCEPT noexcept
247 # define YY_NOTHROW
248 #else
249 # define YY_NOEXCEPT
250 # define YY_NOTHROW throw ()
251 #endif
252 
253 // Support constexpr when possible.
254 #if 201703 <= YY_CPLUSPLUS
255 # define YY_CONSTEXPR constexpr
256 #else
257 # define YY_CONSTEXPR
258 #endif
259 
260 
261 
262 #ifndef YY_ATTRIBUTE_PURE
263 # if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
264 # define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
265 # else
266 # define YY_ATTRIBUTE_PURE
267 # endif
268 #endif
269 
270 #ifndef YY_ATTRIBUTE_UNUSED
271 # if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
272 # define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
273 # else
274 # define YY_ATTRIBUTE_UNUSED
275 # endif
276 #endif
277 
278 /* Suppress unused-variable warnings by "using" E. */
279 #if ! defined lint || defined __GNUC__
280 # define YY_USE(E) ((void) (E))
281 #else
282 # define YY_USE(E) /* empty */
283 #endif
284 
285 #if defined __GNUC__ && ! defined __ICC && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
286 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
287 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
288  _Pragma ("GCC diagnostic push") \
289  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
290  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
291 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
292  _Pragma ("GCC diagnostic pop")
293 #else
294 # define YY_INITIAL_VALUE(Value) Value
295 #endif
296 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
297 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
298 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
299 #endif
300 #ifndef YY_INITIAL_VALUE
301 # define YY_INITIAL_VALUE(Value) /* Nothing. */
302 #endif
303 
304 #if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__
305 # define YY_IGNORE_USELESS_CAST_BEGIN \
306  _Pragma ("GCC diagnostic push") \
307  _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"")
308 # define YY_IGNORE_USELESS_CAST_END \
309  _Pragma ("GCC diagnostic pop")
310 #endif
311 #ifndef YY_IGNORE_USELESS_CAST_BEGIN
312 # define YY_IGNORE_USELESS_CAST_BEGIN
313 # define YY_IGNORE_USELESS_CAST_END
314 #endif
315 
316 # ifndef YY_CAST
317 # ifdef __cplusplus
318 # define YY_CAST(Type, Val) static_cast<Type> (Val)
319 # define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
320 # else
321 # define YY_CAST(Type, Val) ((Type) (Val))
322 # define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
323 # endif
324 # endif
325 # ifndef YY_NULLPTR
326 # if defined __cplusplus
327 # if 201103L <= __cplusplus
328 # define YY_NULLPTR nullptr
329 # else
330 # define YY_NULLPTR 0
331 # endif
332 # else
333 # define YY_NULLPTR ((void*)0)
334 # endif
335 # endif
336 
337 /* Debug traces. */
338 #ifndef HOAYYDEBUG
339 # if defined YYDEBUG
340 #if YYDEBUG
341 # define HOAYYDEBUG 1
342 # else
343 # define HOAYYDEBUG 0
344 # endif
345 # else /* ! defined YYDEBUG */
346 # define HOAYYDEBUG 1
347 # endif /* ! defined YYDEBUG */
348 #endif /* ! defined HOAYYDEBUG */
349 
350 namespace hoayy {
351 #line 352 "parseaut.hh"
352 
353 
354 
355 
357  class parser
358  {
359  public:
360 #ifndef HOAYYSTYPE
363  {
364 #line 205 "parseaut.yy"
365 
366  std::string* str;
367  unsigned int num;
368  int b;
370  pair* p;
371  std::list<pair>* list;
373  std::vector<unsigned>* states;
374 
375 #line 376 "parseaut.hh"
376 
377  };
378 #else
379  typedef HOAYYSTYPE semantic_type;
380 #endif
382  typedef spot::location location_type;
383 
385  struct syntax_error : std::runtime_error
386  {
387  syntax_error (const location_type& l, const std::string& m)
388  : std::runtime_error (m)
389  , location (l)
390  {}
391 
392  syntax_error (const syntax_error& s)
393  : std::runtime_error (s.what ())
394  , location (s.location)
395  {}
396 
397  ~syntax_error () YY_NOEXCEPT YY_NOTHROW;
398 
399  location_type location;
400  };
401 
403  struct token
404  {
405  enum token_kind_type
406  {
407  HOAYYEMPTY = -2,
408  ENDOFFILE = 0, // "end of file"
409  HOAYYerror = 256, // error
410  HOAYYUNDEF = 257, // "invalid token"
411  HOA = 258, // "HOA:"
412  STATES = 259, // "States:"
413  START = 260, // "Start:"
414  AP = 261, // "AP:"
415  ALIAS = 262, // "Alias:"
416  ACCEPTANCE = 263, // "Acceptance:"
417  ACCNAME = 264, // "acc-name:"
418  TOOL = 265, // "tool:"
419  NAME = 266, // "name:"
420  PROPERTIES = 267, // "properties:"
421  BODY = 268, // "--BODY--"
422  END = 269, // "--END--"
423  STATE = 270, // "State:"
424  SPOT_HIGHLIGHT_EDGES = 271, // "spot.highlight.edges:"
425  SPOT_HIGHLIGHT_STATES = 272, // "spot.highlight.states:"
426  SPOT_STATE_PLAYER = 273, // "spot.state-player:"
427  IDENTIFIER = 274, // "identifier"
428  HEADERNAME = 275, // "header name"
429  ANAME = 276, // "alias name"
430  STRING = 277, // "string"
431  INT = 278, // "integer"
432  DRA = 279, // "DRA"
433  DSA = 280, // "DSA"
434  V2 = 281, // "v2"
435  EXPLICIT = 282, // "explicit"
436  ACCPAIRS = 283, // "Acceptance-Pairs:"
437  ACCSIG = 284, // "Acc-Sig:"
438  ENDOFHEADER = 285, // "---"
439  LINEDIRECTIVE = 286, // "#line"
440  BDD = 287, // BDD
441  NEVER = 288, // "never"
442  SKIP = 289, // "skip"
443  IF = 290, // "if"
444  FI = 291, // "fi"
445  DO = 292, // "do"
446  OD = 293, // "od"
447  ARROW = 294, // "->"
448  GOTO = 295, // "goto"
449  FALSE = 296, // "false"
450  ATOMIC = 297, // "atomic"
451  ASSERT = 298, // "assert"
452  FORMULA = 299, // "boolean formula"
453  ENDAUT = 300, // "-1"
454  ENDDSTAR = 301, // "end of DSTAR automaton"
455  LBTT = 302, // "LBTT header"
456  INT_S = 303, // "state acceptance"
457  LBTT_EMPTY = 304, // "acceptance sets for empty automaton"
458  ACC = 305, // "acceptance set"
459  STATE_NUM = 306, // "state number"
460  DEST_NUM = 307 // "destination number"
461  };
463  typedef token_kind_type yytokentype;
464  };
465 
467  typedef token::yytokentype token_kind_type;
468 
470  typedef token_kind_type token_type;
471 
473  struct symbol_kind
474  {
476  {
477  YYNTOKENS = 68,
478  S_YYEMPTY = -2,
479  S_YYEOF = 0, // "end of file"
480  S_YYerror = 1, // error
481  S_YYUNDEF = 2, // "invalid token"
482  S_HOA = 3, // "HOA:"
483  S_STATES = 4, // "States:"
484  S_START = 5, // "Start:"
485  S_AP = 6, // "AP:"
486  S_ALIAS = 7, // "Alias:"
487  S_ACCEPTANCE = 8, // "Acceptance:"
488  S_ACCNAME = 9, // "acc-name:"
489  S_TOOL = 10, // "tool:"
490  S_NAME = 11, // "name:"
491  S_PROPERTIES = 12, // "properties:"
492  S_BODY = 13, // "--BODY--"
493  S_END = 14, // "--END--"
494  S_STATE = 15, // "State:"
495  S_SPOT_HIGHLIGHT_EDGES = 16, // "spot.highlight.edges:"
496  S_SPOT_HIGHLIGHT_STATES = 17, // "spot.highlight.states:"
497  S_SPOT_STATE_PLAYER = 18, // "spot.state-player:"
498  S_IDENTIFIER = 19, // "identifier"
499  S_HEADERNAME = 20, // "header name"
500  S_ANAME = 21, // "alias name"
501  S_STRING = 22, // "string"
502  S_INT = 23, // "integer"
503  S_24_ = 24, // '['
504  S_DRA = 25, // "DRA"
505  S_DSA = 26, // "DSA"
506  S_V2 = 27, // "v2"
507  S_EXPLICIT = 28, // "explicit"
508  S_ACCPAIRS = 29, // "Acceptance-Pairs:"
509  S_ACCSIG = 30, // "Acc-Sig:"
510  S_ENDOFHEADER = 31, // "---"
511  S_LINEDIRECTIVE = 32, // "#line"
512  S_BDD = 33, // BDD
513  S_34_ = 34, // '|'
514  S_35_ = 35, // '&'
515  S_36_ = 36, // '!'
516  S_NEVER = 37, // "never"
517  S_SKIP = 38, // "skip"
518  S_IF = 39, // "if"
519  S_FI = 40, // "fi"
520  S_DO = 41, // "do"
521  S_OD = 42, // "od"
522  S_ARROW = 43, // "->"
523  S_GOTO = 44, // "goto"
524  S_FALSE = 45, // "false"
525  S_ATOMIC = 46, // "atomic"
526  S_ASSERT = 47, // "assert"
527  S_FORMULA = 48, // "boolean formula"
528  S_ENDAUT = 49, // "-1"
529  S_ENDDSTAR = 50, // "end of DSTAR automaton"
530  S_LBTT = 51, // "LBTT header"
531  S_INT_S = 52, // "state acceptance"
532  S_LBTT_EMPTY = 53, // "acceptance sets for empty automaton"
533  S_ACC = 54, // "acceptance set"
534  S_STATE_NUM = 55, // "state number"
535  S_DEST_NUM = 56, // "destination number"
536  S_57_t_ = 57, // 't'
537  S_58_f_ = 58, // 'f'
538  S_59_ = 59, // '('
539  S_60_ = 60, // ')'
540  S_61_ = 61, // ']'
541  S_62_ = 62, // '{'
542  S_63_ = 63, // '}'
543  S_64_ = 64, // '+'
544  S_65_ = 65, // '-'
545  S_66_ = 66, // ';'
546  S_67_ = 67, // ':'
547  S_YYACCEPT = 68, // $accept
548  S_aut = 69, // aut
549  S_70_1 = 70, // $@1
550  S_71_aut_1 = 71, // aut-1
551  S_hoa = 72, // hoa
552  S_string_opt = 73, // string_opt
553  S_BOOLEAN = 74, // BOOLEAN
554  S_header = 75, // header
555  S_version = 76, // version
556  S_77_format_version = 77, // format-version
557  S_78_2 = 78, // $@2
558  S_aps = 79, // aps
559  S_80_3 = 80, // $@3
560  S_81_header_items = 81, // header-items
561  S_82_header_item = 82, // header-item
562  S_83_4 = 83, // $@4
563  S_84_5 = 84, // $@5
564  S_85_6 = 85, // $@6
565  S_86_7 = 86, // $@7
566  S_87_8 = 87, // $@8
567  S_88_ap_names = 88, // ap-names
568  S_89_ap_name = 89, // ap-name
569  S_90_acc_spec = 90, // acc-spec
570  S_properties = 91, // properties
571  S_92_highlight_edges = 92, // highlight-edges
572  S_93_highlight_states = 93, // highlight-states
573  S_94_state_player = 94, // state-player
574  S_95_header_spec = 95, // header-spec
575  S_96_state_conj_2 = 96, // state-conj-2
576  S_97_init_state_conj_2 = 97, // init-state-conj-2
577  S_98_label_expr = 98, // label-expr
578  S_99_acc_set = 99, // acc-set
579  S_100_acceptance_cond = 100, // acceptance-cond
580  S_body = 101, // body
581  S_102_state_num = 102, // state-num
582  S_103_checked_state_num = 103, // checked-state-num
583  S_states = 104, // states
584  S_state = 105, // state
585  S_106_state_name = 106, // state-name
586  S_label = 107, // label
587  S_108_state_label_opt = 108, // state-label_opt
588  S_109_trans_label = 109, // trans-label
589  S_110_acc_sig = 110, // acc-sig
590  S_111_acc_sets = 111, // acc-sets
591  S_112_state_acc_opt = 112, // state-acc_opt
592  S_113_trans_acc_opt = 113, // trans-acc_opt
593  S_114_labeled_edges = 114, // labeled-edges
594  S_115_some_labeled_edges = 115, // some-labeled-edges
595  S_116_incorrectly_unlabeled_edge = 116, // incorrectly-unlabeled-edge
596  S_117_labeled_edge = 117, // labeled-edge
597  S_118_state_conj_checked = 118, // state-conj-checked
598  S_119_unlabeled_edges = 119, // unlabeled-edges
599  S_120_unlabeled_edge = 120, // unlabeled-edge
600  S_121_incorrectly_labeled_edge = 121, // incorrectly-labeled-edge
601  S_dstar = 122, // dstar
602  S_dstar_type = 123, // dstar_type
603  S_dstar_header = 124, // dstar_header
604  S_dstar_sizes = 125, // dstar_sizes
605  S_dstar_state_id = 126, // dstar_state_id
606  S_sign = 127, // sign
607  S_dstar_accsigs = 128, // dstar_accsigs
608  S_dstar_state_accsig = 129, // dstar_state_accsig
609  S_dstar_transitions = 130, // dstar_transitions
610  S_dstar_states = 131, // dstar_states
611  S_never = 132, // never
612  S_133_9 = 133, // $@9
613  S_134_nc_states = 134, // nc-states
614  S_135_nc_one_ident = 135, // nc-one-ident
615  S_136_nc_ident_list = 136, // nc-ident-list
616  S_137_nc_transition_block = 137, // nc-transition-block
617  S_138_nc_state = 138, // nc-state
618  S_139_nc_transitions = 139, // nc-transitions
619  S_140_nc_formula_or_ident = 140, // nc-formula-or-ident
620  S_141_nc_formula = 141, // nc-formula
621  S_142_nc_opt_dest = 142, // nc-opt-dest
622  S_143_nc_src_dest = 143, // nc-src-dest
623  S_144_nc_transition = 144, // nc-transition
624  S_lbtt = 145, // lbtt
625  S_146_lbtt_header_states = 146, // lbtt-header-states
626  S_147_lbtt_header = 147, // lbtt-header
627  S_148_lbtt_body = 148, // lbtt-body
628  S_149_lbtt_states = 149, // lbtt-states
629  S_150_lbtt_state = 150, // lbtt-state
630  S_151_lbtt_acc = 151, // lbtt-acc
631  S_152_lbtt_guard = 152, // lbtt-guard
632  S_153_lbtt_transitions = 153 // lbtt-transitions
633  };
634  };
635 
638 
640  static const symbol_kind_type YYNTOKENS = symbol_kind::YYNTOKENS;
641 
648  template <typename Base>
649  struct basic_symbol : Base
650  {
652  typedef Base super_type;
653 
656  : value ()
657  , location ()
658  {}
659 
660 #if 201103L <= YY_CPLUSPLUS
662  basic_symbol (basic_symbol&& that)
663  : Base (std::move (that))
664  , value (std::move (that.value))
665  , location (std::move (that.location))
666  {}
667 #endif
668 
670  basic_symbol (const basic_symbol& that);
672  basic_symbol (typename Base::kind_type t,
673  YY_MOVE_REF (location_type) l);
674 
676  basic_symbol (typename Base::kind_type t,
677  YY_RVREF (semantic_type) v,
678  YY_RVREF (location_type) l);
679 
682  {
683  clear ();
684  }
685 
687  void clear () YY_NOEXCEPT
688  {
689  Base::clear ();
690  }
691 
693  std::string name () const YY_NOEXCEPT
694  {
695  return parser::symbol_name (this->kind ());
696  }
697 
699  symbol_kind_type type_get () const YY_NOEXCEPT;
700 
702  bool empty () const YY_NOEXCEPT;
703 
705  void move (basic_symbol& s);
706 
709 
711  location_type location;
712 
713  private:
714 #if YY_CPLUSPLUS < 201103L
716  basic_symbol& operator= (const basic_symbol& that);
717 #endif
718  };
719 
721  struct by_kind
722  {
725 
726 #if 201103L <= YY_CPLUSPLUS
728  by_kind (by_kind&& that);
729 #endif
730 
732  by_kind (const by_kind& that);
733 
735  typedef token_kind_type kind_type;
736 
738  by_kind (kind_type t);
739 
741  void clear () YY_NOEXCEPT;
742 
744  void move (by_kind& that);
745 
748  symbol_kind_type kind () const YY_NOEXCEPT;
749 
751  symbol_kind_type type_get () const YY_NOEXCEPT;
752 
756  };
757 
759  typedef by_kind by_type;
760 
763  {};
764 
766  parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
767  virtual ~parser ();
768 
769 #if 201103L <= YY_CPLUSPLUS
771  parser (const parser&) = delete;
773  parser& operator= (const parser&) = delete;
774 #endif
775 
778  int operator() ();
779 
782  virtual int parse ();
783 
784 #if HOAYYDEBUG
786  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
788  void set_debug_stream (std::ostream &);
789 
791  typedef int debug_level_type;
793  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
795  void set_debug_level (debug_level_type l);
796 #endif
797 
801  virtual void error (const location_type& loc, const std::string& msg);
802 
804  void error (const syntax_error& err);
805 
808  static std::string symbol_name (symbol_kind_type yysymbol);
809 
810 
811 
812  class context
813  {
814  public:
815  context (const parser& yyparser, const symbol_type& yyla);
816  const symbol_type& lookahead () const YY_NOEXCEPT { return yyla_; }
817  symbol_kind_type token () const YY_NOEXCEPT { return yyla_.kind (); }
818  const location_type& location () const YY_NOEXCEPT { return yyla_.location; }
819 
823  int expected_tokens (symbol_kind_type yyarg[], int yyargn) const;
824 
825  private:
826  const parser& yyparser_;
827  const symbol_type& yyla_;
828  };
829 
830  private:
831 #if YY_CPLUSPLUS < 201103L
833  parser (const parser&);
835  parser& operator= (const parser&);
836 #endif
837 
838 
840  typedef short state_type;
841 
843  int yy_syntax_error_arguments_ (const context& yyctx,
844  symbol_kind_type yyarg[], int yyargn) const;
845 
848  virtual std::string yysyntax_error_ (const context& yyctx) const;
852  static state_type yy_lr_goto_state_ (state_type yystate, int yysym);
853 
856  static bool yy_pact_value_is_default_ (int yyvalue);
857 
860  static bool yy_table_value_is_error_ (int yyvalue);
861 
862  static const short yypact_ninf_;
863  static const short yytable_ninf_;
864 
868  static symbol_kind_type yytranslate_ (int t);
869 
871  static std::string yytnamerr_ (const char *yystr);
872 
874  static const char* const yytname_[];
875 
876 
877  // Tables.
878  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
879  // STATE-NUM.
880  static const short yypact_[];
881 
882  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
883  // Performed when YYTABLE does not specify something else to do. Zero
884  // means the default is an error.
885  static const unsigned char yydefact_[];
886 
887  // YYPGOTO[NTERM-NUM].
888  static const short yypgoto_[];
889 
890  // YYDEFGOTO[NTERM-NUM].
891  static const short yydefgoto_[];
892 
893  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
894  // positive, shift that token. If negative, reduce the rule whose
895  // number is the opposite. If YYTABLE_NINF, syntax error.
896  static const short yytable_[];
897 
898  static const short yycheck_[];
899 
900  // YYSTOS[STATE-NUM] -- The (internal number of the) accessing
901  // symbol of state STATE-NUM.
902  static const unsigned char yystos_[];
903 
904  // YYR1[YYN] -- Symbol number of symbol that rule YYN derives.
905  static const unsigned char yyr1_[];
906 
907  // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN.
908  static const signed char yyr2_[];
909 
910 
911 #if HOAYYDEBUG
912  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
913  static const short yyrline_[];
915  virtual void yy_reduce_print_ (int r) const;
917  virtual void yy_stack_print_ () const;
918 
920  int yydebug_;
922  std::ostream* yycdebug_;
923 
927  template <typename Base>
928  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
929 #endif
930 
935  template <typename Base>
936  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
937 
938  private:
940  struct by_state
941  {
943  by_state () YY_NOEXCEPT;
944 
946  typedef state_type kind_type;
947 
949  by_state (kind_type s) YY_NOEXCEPT;
950 
952  by_state (const by_state& that) YY_NOEXCEPT;
953 
955  void clear () YY_NOEXCEPT;
956 
958  void move (by_state& that);
959 
962  symbol_kind_type kind () const YY_NOEXCEPT;
963 
966  enum { empty_state = 0 };
967 
970  state_type state;
971  };
972 
974  struct stack_symbol_type : basic_symbol<by_state>
975  {
977  typedef basic_symbol<by_state> super_type;
979  stack_symbol_type ();
981  stack_symbol_type (YY_RVREF (stack_symbol_type) that);
983  stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym);
984 #if YY_CPLUSPLUS < 201103L
987  stack_symbol_type& operator= (stack_symbol_type& that);
988 
991  stack_symbol_type& operator= (const stack_symbol_type& that);
992 #endif
993  };
994 
996  template <typename T, typename S = std::vector<T> >
997  class stack
998  {
999  public:
1000  // Hide our reversed order.
1001  typedef typename S::iterator iterator;
1002  typedef typename S::const_iterator const_iterator;
1003  typedef typename S::size_type size_type;
1004  typedef typename std::ptrdiff_t index_type;
1005 
1006  stack (size_type n = 200)
1007  : seq_ (n)
1008  {}
1009 
1010 #if 201103L <= YY_CPLUSPLUS
1012  stack (const stack&) = delete;
1014  stack& operator= (const stack&) = delete;
1015 #endif
1016 
1020  const T&
1021  operator[] (index_type i) const
1022  {
1023  return seq_[size_type (size () - 1 - i)];
1024  }
1025 
1029  T&
1030  operator[] (index_type i)
1031  {
1032  return seq_[size_type (size () - 1 - i)];
1033  }
1034 
1038  void
1039  push (YY_MOVE_REF (T) t)
1040  {
1041  seq_.push_back (T ());
1042  operator[] (0).move (t);
1043  }
1044 
1046  void
1047  pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
1048  {
1049  for (; 0 < n; --n)
1050  seq_.pop_back ();
1051  }
1052 
1054  void
1055  clear () YY_NOEXCEPT
1056  {
1057  seq_.clear ();
1058  }
1059 
1061  index_type
1062  size () const YY_NOEXCEPT
1063  {
1064  return index_type (seq_.size ());
1065  }
1066 
1068  const_iterator
1069  begin () const YY_NOEXCEPT
1070  {
1071  return seq_.begin ();
1072  }
1073 
1075  const_iterator
1076  end () const YY_NOEXCEPT
1077  {
1078  return seq_.end ();
1079  }
1080 
1082  class slice
1083  {
1084  public:
1085  slice (const stack& stack, index_type range)
1086  : stack_ (stack)
1087  , range_ (range)
1088  {}
1089 
1090  const T&
1091  operator[] (index_type i) const
1092  {
1093  return stack_[range_ - i];
1094  }
1095 
1096  private:
1097  const stack& stack_;
1098  index_type range_;
1099  };
1100 
1101  private:
1102 #if YY_CPLUSPLUS < 201103L
1104  stack (const stack&);
1106  stack& operator= (const stack&);
1107 #endif
1109  S seq_;
1110  };
1111 
1112 
1114  typedef stack<stack_symbol_type> stack_type;
1115 
1117  stack_type yystack_;
1118 
1124  void yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym);
1125 
1132  void yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym);
1133 
1135  void yypop_ (int n = 1);
1136 
1138  enum
1139  {
1140  yylast_ = 245,
1141  yynnts_ = 86,
1142  yyfinal_ = 26
1143  };
1144 
1145 
1146  // User arguments.
1147  void* scanner;
1148  result_& res;
1149  spot::location initial_loc;
1150 
1151  };
1152 
1153 
1154 } // hoayy
1155 #line 1156 "parseaut.hh"
1156 
1157 
1158 
1159 
1160 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
Definition: parseaut.hh:813
int expected_tokens(symbol_kind_type yyarg[], int yyargn) const
Present a slice of the top of a stack.
Definition: parseaut.hh:1083
A Bison parser.
Definition: parseaut.hh:358
void error(const syntax_error &err)
Report a syntax error.
token_kind_type token_type
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:470
symbol_kind::symbol_kind_type symbol_kind_type
(Internal) symbol kind.
Definition: parseaut.hh:637
std::ostream & debug_stream() const
The current debugging stream.
token::yytokentype token_kind_type
Token kind, as returned by yylex.
Definition: parseaut.hh:467
spot::location location_type
Symbol locations.
Definition: parseaut.hh:382
virtual int parse()
static std::string symbol_name(symbol_kind_type yysymbol)
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:791
virtual void error(const location_type &loc, const std::string &msg)
parser(void *scanner_yyarg, result_ &res_yyarg, spot::location initial_loc_yyarg)
Build a parser object.
An environment that describes atomic propositions.
Definition: environment.hh:33
Definition: ngraph.hh:33
A class implementing Kleene's three-valued logic.
Definition: trival.hh:34
Definition: parseaut.hh:650
Base super_type
Alias to Base.
Definition: parseaut.hh:652
basic_symbol()
Default constructor.
Definition: parseaut.hh:655
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
void clear()
Destroy contents, and record that is empty.
Definition: parseaut.hh:687
basic_symbol(const basic_symbol &that)
Copy constructor.
basic_symbol(typename Base::kind_type t, location_type &l)
Constructor for valueless symbols.
basic_symbol(typename Base::kind_type t, const semantic_type &v, const location_type &l)
Constructor for symbols with semantic value.
std::string name() const
The user-facing name of this symbol.
Definition: parseaut.hh:693
~basic_symbol()
Destroy the symbol.
Definition: parseaut.hh:681
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:722
by_kind()
Default constructor.
void clear()
Record that this symbol is empty.
by_kind(kind_type t)
Constructor from (external) token numbers.
by_kind(const by_kind &that)
Copy constructor.
token_kind_type kind_type
The symbol kind as needed by the constructor.
Definition: parseaut.hh:735
Symbol kinds.
Definition: parseaut.hh:474
symbol_kind_type
Definition: parseaut.hh:476
"External" symbols: returned by the scanner.
Definition: parseaut.hh:763
Syntax errors thrown from user actions.
Definition: parseaut.hh:386
Token kinds.
Definition: parseaut.hh:404
token_kind_type yytokentype
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:463
Definition: parseaut.hh:136
Definition: parseaut.hh:101
Definition: parseaut.hh:99
An acceptance formula.
Definition: acc.hh:487
An acceptance mark.
Definition: acc.hh:89
Definition: public.hh:93
Symbol semantic values.
Definition: parseaut.hh:363

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1