albatross.exp 23.1 KB
Newer Older
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
File "albatross.mly", line 129, characters 7-10:
Warning: the token EOF is unused.
File "albatross.mly", line 135, characters 7-19:
Warning: the token HIGHEST_PREC is unused.
File "albatross.mly", line 93, characters 7-16:
Warning: the token KWCURRENT is unused.
File "albatross.mly", line 93, characters 17-26:
Warning: the token KWCurrent is unused.
File "albatross.mly", line 94, characters 7-13:
Warning: the token KWNONE is unused.
File "albatross.mly", line 95, characters 7-18:
Warning: the token KWPrecursor is unused.
File "albatross.mly", line 95, characters 19-28:
Warning: the token KWProcess is unused.
File "albatross.mly", line 98, characters 60-68:
Warning: the token KWassert is unused.
File "albatross.mly", line 99, characters 34-41:
Warning: the token KWcheck is unused.
File "albatross.mly", line 102, characters 19-28:
Warning: the token KWfeature is unused.
File "albatross.mly", line 102, characters 34-40:
Warning: the token KWfrom is unused.
File "albatross.mly", line 104, characters 34-42:
Warning: the token KWimport is unused.
File "albatross.mly", line 105, characters 34-45:
Warning: the token KWinvariant is unused.
File "albatross.mly", line 110, characters 7-17:
Warning: the token KWredefine is unused.
File "albatross.mly", line 113, characters 7-17:
Warning: the token KWundefine is unused.
File "albatross.mly", line 114, characters 7-16:
Warning: the token KWvariant is unused.
File "albatross.mly", line 115, characters 7-14:
Warning: the token KWwhile is unused.
File "albatross.mly", line 155, characters 7-13:
Warning: the token UMINUS is unused.
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 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
Grammar has 91 nonterminal symbols, among which 2 start symbols.
Grammar has 93 terminal symbols.
Grammar has 248 productions.
nullable(use_block_opt) = true
nullable(use_block) = false
nullable(uidentifier_list) = false
nullable(type_nt) = false
nullable(type_list_min2) = false
nullable(type_list) = false
nullable(tuple_type) = false
nullable(star_type) = false
nullable(simple_type) = false
nullable(separator) = false
nullable(return_type_opt) = true
nullable(return_type) = false
nullable(require_block_opt) = true
nullable(require_block) = false
nullable(rename_list) = false
nullable(rename_item) = false
nullable(qmark_type) = false
nullable(proof_seq) = false
nullable(proof_expr_struct) = false
nullable(proof_expr) = false
nullable(proof_block) = false
nullable(proof_all_expr_inner) = false
nullable(proof_all_expr) = false
nullable(path) = false
nullable(parent_list) = false
nullable(parent) = false
nullable(optsemi) = true
nullable(optghost) = true
nullable(opt_nl) = true
nullable(operator_expr) = false
nullable(operator) = false
nullable(one_module) = false
nullable(nameopconst_info) = false
nullable(nameopconst) = false
nullable(named_feature) = false
nullable(name_sig) = false
nullable(module_list) = false
nullable(local_list) = false
nullable(local_declaration) = false
nullable(local_block) = true
nullable(list_type) = false
nullable(inherit_clause) = true
nullable(info_expr) = false
nullable(implementation_note) = false
nullable(implementation_block) = false
nullable(identifier_list) = false
nullable(header_mark) = true
nullable(formal_generic) = false
nullable(formal_arguments_opt) = true
nullable(formal_arguments_info) = false
nullable(formal_arguments) = false
nullable(file) = true
nullable(feature_implementation) = false
nullable(feature_body_opt) = true
nullable(feature_body) = false
nullable(feature_adaptation) = true
nullable(featopconst) = false
nullable(expr) = false
nullable(exp_then_part_list) = false
nullable(exp_then_part) = false
nullable(exp_inspect) = false
nullable(exp_else_part) = true
nullable(exp_conditional) = false
nullable(exp_case_list) = false
nullable(exp_case) = false
nullable(entity_list) = false
nullable(entity_group) = false
nullable(ensure_block) = false
nullable(elem_type) = false
nullable(dotted_id_list) = false
nullable(do_block) = false
nullable(decls) = true
nullable(decl) = false
nullable(create_clause) = true
nullable(constructor_list) = false
nullable(constructor) = false
nullable(compound_list) = false
nullable(compound) = false
nullable(class_name) = false
nullable(class_generics) = true
nullable(class_declaration) = false
nullable(atomic_expr) = false
nullable(ass_seq) = false
nullable(ass_req_opt) = true
nullable(ass_req) = false
nullable(ass_imp) = true
nullable(ass_feat) = false
nullable(ass_ens) = false
nullable(ass_check) = false
nullable(arrow_type) = false
nullable(actual_generics) = true
first(use_block_opt) = UIDENTIFIER NUMBER LPAREN LIDENTIFIER KWuse KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall
first(use_block) = KWuse
first(uidentifier_list) = UIDENTIFIER
first(type_nt) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET
first(type_list_min2) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET
first(type_list) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET
first(tuple_type) = LPAREN
first(star_type) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET
first(simple_type) = UIDENTIFIER LIDENTIFIER
first(separator) = SEMICOL NEWLINE
first(return_type_opt) = EXCLAM COLON
first(return_type) = EXCLAM COLON
first(require_block_opt) = KWrequire
first(require_block) = KWrequire
first(rename_list) = NUMBER LPAREN LIDENTIFIER KWtrue KWfalse
first(rename_item) = NUMBER LPAREN LIDENTIFIER KWtrue KWfalse
first(qmark_type) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET
first(proof_seq) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWrequire KWproof KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(proof_expr_struct) = KWrequire KWproof
first(proof_expr) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWrequire KWproof KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(proof_block) = KWproof
first(proof_all_expr_inner) = KWall
first(proof_all_expr) = KWall
first(path) = LIDENTIFIER
first(parent_list) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET KWghost
first(parent) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET KWghost
first(optsemi) = SEMICOL
first(optghost) = KWghost
first(opt_nl) = SEMICOL NEWLINE
first(operator_expr) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(operator) = TIMES ROPERATOR PLUS PARENOP OPERATOR NOTIN NEQV NEQ MINUS LT LE KWor KWnot KWin KWand GT GE EQV EQ DIVIDE DCOLON DBAR DARROW CARET BRACKETOP BAR
first(one_module) = LIDENTIFIER
first(nameopconst_info) = NUMBER LPAREN LIDENTIFIER KWtrue KWfalse
first(nameopconst) = NUMBER LPAREN LIDENTIFIER KWtrue KWfalse
first(named_feature) = NUMBER LPAREN LIDENTIFIER KWtrue KWfalse
first(name_sig) = NUMBER LPAREN LIDENTIFIER KWtrue KWfalse
first(module_list) = LIDENTIFIER
first(local_list) = LIDENTIFIER
first(local_declaration) = LIDENTIFIER
first(local_block) = KWlocal
first(list_type) = LBRACKET
first(inherit_clause) = KWinherit
first(info_expr) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(implementation_note) = KWnote
first(implementation_block) = KWproof KWlocal KWdo
first(identifier_list) = LIDENTIFIER
first(header_mark) = KWimmutable KWdeferred KWcase
first(formal_generic) = UIDENTIFIER
first(formal_arguments_opt) = LPAREN
first(formal_arguments_info) = LPAREN
first(formal_arguments) = LPAREN
first(file) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWuse KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall
first(feature_implementation) = KWproof KWnote KWlocal KWdo KWdeferred
first(feature_body_opt) = KWrequire KWproof KWnote KWlocal KWensure KWdo KWdeferred
first(feature_body) = KWrequire KWproof KWnote KWlocal KWensure KWdo KWdeferred
first(feature_adaptation) = KWrename
first(featopconst) = NUMBER LPAREN KWtrue KWfalse
first(expr) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(exp_then_part_list) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(exp_then_part) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(exp_inspect) = KWinspect
first(exp_else_part) = KWelse
first(exp_conditional) = KWif
first(exp_case_list) = KWcase
first(exp_case) = KWcase
first(entity_list) = LIDENTIFIER
first(entity_group) = LIDENTIFIER
first(ensure_block) = KWensure
first(elem_type) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET
first(dotted_id_list) = LIDENTIFIER
first(do_block) = KWdo
first(decls) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall
first(decl) = UIDENTIFIER NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall
first(create_clause) = KWcreate
first(constructor_list) = NUMBER LPAREN LIDENTIFIER KWtrue KWfalse
first(constructor) = NUMBER LPAREN LIDENTIFIER KWtrue KWfalse
first(compound_list) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(compound) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(class_name) = UIDENTIFIER LIDENTIFIER
first(class_generics) = LBRACKET
first(class_declaration) = KWimmutable KWdeferred KWclass KWcase
first(atomic_expr) = USCORE NUMBER LIDENTIFIER KWtrue KWfalse KWResult
first(ass_seq) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWold KWnot KWinspect KWif KWfalse KWall KWagent KWResult
first(ass_req_opt) = KWrequire
first(ass_req) = KWrequire
first(ass_imp) = KWproof KWnote KWdeferred
first(ass_feat) = KWall
first(ass_ens) = KWensure
first(ass_check) = KWproof
first(arrow_type) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET
first(actual_generics) = LBRACKET
follow(use_block_opt) = #
follow(use_block) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(uidentifier_list) = RBRACKET
follow(type_nt) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN #
follow(type_list_min2) = RPAREN RBRACKET
follow(type_list) = RPAREN RBRACKET
follow(tuple_type) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE QMARK PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrequire KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN ARROW #
follow(star_type) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE QMARK PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrequire KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN ARROW #
follow(simple_type) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE QMARK PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrequire KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN ARROW #
follow(separator) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWrequire KWproof KWold KWnote KWnot KWinspect KWif KWfalse KWensure KWdeferred KWall KWagent KWResult
follow(return_type_opt) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWrequire KWproof KWnote KWlocal KWimmutable KWfalse KWensure KWdo KWdeferred KWclass KWcase KWall ARROW #
follow(return_type) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWrequire KWproof KWnote KWlocal KWimmutable KWfalse KWensure KWdo KWdeferred KWclass KWcase KWall EQ ARROW #
follow(require_block_opt) = KWensure
follow(require_block) = KWproof KWnote KWlocal KWensure KWend KWdo KWdeferred
follow(rename_list) = KWend
follow(rename_item) = SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWfalse KWend
follow(qmark_type) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE QMARK PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrequire KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN ARROW #
follow(proof_seq) = SEMICOL NEWLINE
follow(proof_expr_struct) = SEMICOL NEWLINE
follow(proof_expr) = SEMICOL NEWLINE
follow(proof_block) = KWensure KWend
follow(proof_all_expr_inner) = SEMICOL NEWLINE
follow(proof_all_expr) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(path) = UIDENTIFIER
follow(parent_list) = KWend
follow(parent) = UIDENTIFIER SEMICOL LPAREN LIDENTIFIER LBRACKET KWghost KWend
follow(optsemi) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER LBRACKET KWtrue KWrequire KWproof KWnote KWlocal KWimmutable KWghost KWfalse KWensure KWend KWdo KWdeferred KWclass KWcase KWall #
follow(optghost) = UIDENTIFIER LPAREN LIDENTIFIER LBRACKET
follow(opt_nl) = USCORE TIMES PLUS NUMBER MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWrequire KWproof KWold KWnote KWnot KWinspect KWif KWfalse KWensure KWdeferred KWall KWagent KWResult
follow(operator_expr) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWproof KWor KWnote KWlocal KWin KWimmutable KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR #
follow(operator) = RPAREN
follow(one_module) = SEMICOL NEWLINE KWend
follow(nameopconst_info) = SEMICOL NEWLINE LPAREN KWinherit KWend EXCLAM COLON
follow(nameopconst) = SEMICOL NUMBER NEWLINE LPAREN LIDENTIFIER KWtrue KWinherit KWfalse KWend KWas EXCLAM COLON
follow(named_feature) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(name_sig) = KWas
follow(module_list) = KWend
follow(local_list) = KWproof KWdo
follow(local_declaration) = SEMICOL KWproof KWdo
follow(local_block) = KWproof KWdo
follow(list_type) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE QMARK PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrequire KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN ARROW #
follow(inherit_clause) = KWend
follow(info_expr) = UIDENTIFIER SEMICOL NUMBER NEWLINE LPAREN LIDENTIFIER KWtrue KWproof KWnote KWlocal KWimmutable KWfalse KWensure KWend KWdo KWdeferred KWclass KWcase KWall #
follow(implementation_note) = KWensure KWend
follow(implementation_block) = KWensure KWend
follow(identifier_list) = SEMICOL RPAREN KWproof KWdo COMMA COLON ASSIGN
follow(header_mark) = KWclass
follow(formal_generic) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(formal_arguments_opt) = SEMICOL NEWLINE KWrequire KWproof KWnote KWinherit KWensure KWend KWdeferred
follow(formal_arguments_info) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWrequire KWproof KWnote KWlocal KWimmutable KWfalse KWensure KWdo KWdeferred KWclass KWcase KWall EXCLAM COLON ARROW #
follow(formal_arguments) = USCORE UIDENTIFIER TIMES SEMICOL PLUS NUMBER NEWLINE MINUS LPAREN LIDENTIFIER LBRACKET LBRACE KWtrue KWsome KWrequire KWproof KWold KWnote KWnot KWlocal KWinspect KWinherit KWimmutable KWif KWfalse KWensure KWend KWdo KWdeferred KWclass KWcase KWall KWagent KWResult EXCLAM COLON ARROW #
follow(file) = #
follow(feature_implementation) = KWensure KWend
follow(feature_body_opt) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(feature_body) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWproof KWimmutable KWfalse KWdo KWdeferred KWclass KWcase KWall #
follow(feature_adaptation) = UIDENTIFIER SEMICOL LPAREN LIDENTIFIER LBRACKET KWghost KWend
follow(featopconst) = SEMICOL NUMBER NEWLINE LPAREN LIDENTIFIER KWtrue KWinherit KWfalse KWend KWas EXCLAM COLON
follow(expr) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWproof KWor KWnote KWlocal KWin KWimmutable KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR #
follow(exp_then_part_list) = KWend KWelse
follow(exp_then_part) = KWend KWelseif KWelse
follow(exp_inspect) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWproof KWor KWnote KWlocal KWin KWimmutable KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR #
follow(exp_else_part) = KWend
follow(exp_conditional) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWproof KWor KWnote KWlocal KWin KWimmutable KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR #
follow(exp_case_list) = KWend
follow(exp_case) = KWend KWcase
follow(entity_list) = SEMICOL RPAREN KWproof KWdo ASSIGN
follow(entity_group) = SEMICOL RPAREN KWproof KWdo COMMA ASSIGN
follow(ensure_block) = KWend
follow(elem_type) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE QMARK PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrequire KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN ARROW #
follow(dotted_id_list) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWproof KWor KWnote KWlocal KWin KWimmutable KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR #
follow(do_block) = KWensure KWend
follow(decls) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(decl) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(create_clause) = KWinherit KWend
follow(constructor_list) = KWinherit KWend
follow(constructor) = SEMICOL NEWLINE KWinherit KWend
follow(compound_list) = KWproof KWnote KWlocal KWensure KWend KWdo KWdeferred
follow(compound) = KWproof KWnote KWlocal KWensure KWend KWdo KWdeferred
follow(class_name) = LBRACKET KWinherit KWend KWcreate
follow(class_generics) = KWinherit KWend KWcreate
follow(class_declaration) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(atomic_expr) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWproof KWor KWnote KWlocal KWin KWimmutable KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR #
follow(ass_seq) = SEMICOL NEWLINE KWproof KWnote KWensure KWend KWdeferred
follow(ass_req_opt) = KWproof KWnote KWensure KWdeferred
follow(ass_req) = KWproof KWnote KWensure KWdeferred
follow(ass_imp) = KWensure
follow(ass_feat) = UIDENTIFIER SEMICOL NUMBER LPAREN LIDENTIFIER KWtrue KWimmutable KWfalse KWdeferred KWclass KWcase KWall #
follow(ass_ens) = KWend
follow(ass_check) = KWensure
follow(arrow_type) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN #
follow(actual_generics) = UIDENTIFIER TIMES SEMICOL RPAREN RBRACKET RBRACE QMARK PLUS NUMBER NOTIN NEWLINE NEQ MINUS LT LPAREN LIDENTIFIER LE LBRACKET KWtrue KWthen KWrequire KWrename KWproof KWor KWnote KWlocal KWin KWimmutable KWghost KWfalse KWensure KWend KWelseif KWelse KWdo KWdeferred KWclass KWcase KWas KWand KWall GT GE EQ DOT DIVIDE DCOLON DBAR DARROW COMMA COLON CARET BAR ASSIGN ARROW #
Built an LR(0) automaton with 428 states.
The grammar is not SLR(1) -- 52 states have a conflict.
Built an LR(1) automaton with 428 states.
788 shift/reduce conflicts were silently solved.
317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339
File "albatross.mly", line 166, characters 9-18:
Warning: the precedence level assigned to ASSIGN is never useful.
File "albatross.mly", line 174, characters 9-18:
Warning: the precedence level assigned to EQV is never useful.
File "albatross.mly", line 187, characters 9-18:
Warning: the precedence level assigned to HIGHEST_PREC is never useful.
File "albatross.mly", line 165, characters 9-18:
Warning: the precedence level assigned to KWghost is never useful.
File "albatross.mly", line 185, characters 9-18:
Warning: the precedence level assigned to LBRACE is never useful.
File "albatross.mly", line 174, characters 9-18:
Warning: the precedence level assigned to NEQV is never useful.
File "albatross.mly", line 181, characters 9-14:
Warning: the precedence level assigned to OPERATOR is never useful.
File "albatross.mly", line 183, characters 9-18:
Warning: the precedence level assigned to QMARK is never useful.
File "albatross.mly", line 182, characters 9-15:
Warning: the precedence level assigned to ROPERATOR is never useful.
File "albatross.mly", line 186, characters 9-18:
Warning: the precedence level assigned to UMINUS is never useful.
File "albatross.mly", line 440, characters 23-34:
Warning: this %prec declaration is never useful.
Warning: 117 states have an end-of-stream conflict.
340
File "albatross.mly", line 202, characters 2-25:
341
Warning: production file -> use_block optsemi decls is never reduced.
342
File "albatross.mly", line 203, characters 2-7:
343
Warning: production file -> decls is never reduced.
344
File "albatross.mly", line 216, characters 14-14:
345 346
Warning: production use_block_opt -> is never reduced.
Warning: in total, 3 productions are never reduced.
347
166 out of 428 states have a default reduction.
348 349 350 351 352 353
198 out of 428 states are represented.
0 out of 188 symbols keep track of their start position.
0 out of 188 symbols keep track of their end position.
130 out of 250 productions exploit shiftreduce optimization.
0 out of 428 states can peek at an error.
1201 functions before inlining, 203 functions after inlining.