blob: 72ae8eb6be3c3634c357c142327eef692e3fd1fd (
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
|
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
/* * GNU Lesser General Public License Version 2.1 */
/* * (see LICENSE file for the text of the license) */
/************************************************************************/
grammar TacticNotations;
// Terminals are not visited, so we add non-terminals for each terminal that
// needs rendering (in particular whitespace (kept in output) vs. WHITESPACE
// (discarded)).
top: blocks EOF;
blocks: block ((whitespace)? block)*;
block: atomic | hole | repeat | curlies;
repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE;
curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
whitespace: WHITESPACE;
atomic: ATOM;
hole: ID;
LGROUP: '{' [+*?];
LBRACE: '{';
RBRACE: '}';
ATOM: ~[@{} ]+;
ID: '@' [a-zA-Z0-9_]+;
WHITESPACE: ' '+;
|
