blob: a889ebda7bf9b5600cb8fe2879da7801f5f1da23 (
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
|
/************************************************************************/
/* * 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 | meta | hole | repeat | curlies;
repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE;
curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
whitespace: WHITESPACE;
meta: METACHAR;
atomic: ATOM (SUB)?;
hole: ID (SUB)?;
LGROUP: '{' [+*?];
LBRACE: '{';
RBRACE: '}';
METACHAR: '%' [|(){}];
ATOM: '@' | '_' | ~[@_{} ]+;
ID: '@' ('_'? [a-zA-Z0-9])+;
SUB: '_' '_' [a-zA-Z0-9]+;
WHITESPACE: ' '+;
|
