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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
/* v * Copyright INRIA, CNRS and contributors */
/* <O___,, * (see version control and CREDITS file for authors & dates) */
/* \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)).
// The distinction between nopipeblock and block is needed because we only want
// to require escaping within alternative blocks, so that e.g. `first [ x | y ]`
// can be written without escaping the `|`.
top: blocks EOF;
blocks: block ((whitespace)? block)*;
block: pipe | nopipeblock;
nopipeblock: atomic | escaped | hole | alternative | repeat | curlies;
alternative: LALT (WHITESPACE)? altblocks (WHITESPACE)? RBRACE;
altblocks: altblock ((WHITESPACE)? altsep (WHITESPACE)? altblock)+;
altblock: nopipeblock ((whitespace)? nopipeblock)*;
repeat: LGROUP (ATOM | PIPE)? WHITESPACE blocks (WHITESPACE)? RBRACE;
curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
pipe: PIPE;
altsep: PIPE;
whitespace: WHITESPACE;
escaped: ESCAPED;
atomic: ATOM (SUB)?;
hole: ID (SUB)?;
LALT: '{|';
LGROUP: '{+' | '{*' | '{?';
LBRACE: '{';
RBRACE: '}';
// todo: need a cleaner way to escape the 3-character strings here
ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{' |
'%|-' | '%|->' | '%||' | '%|||' | '%||||'; // for SSR
PIPE: '|';
ATOM: '@' | '_' | ~[@_{}| ]+;
ID: '@' ('_'? [a-zA-Z0-9])+;
SUB: '_' '_' [a-zA-Z0-9]+;
WHITESPACE: ' '+;
|
