aboutsummaryrefslogtreecommitdiffhomepage
path: root/coqpp/coqpp_ast.mli
blob: 39b4d2ab34fe5a05e6d7ad2b577333337734a54c (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
34
35
36
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

type loc = {
  loc_start : Lexing.position;
  loc_end : Lexing.position;
}

type code = { code : string }

type user_symbol =
| Ulist1 of user_symbol
| Ulist1sep of user_symbol * string
| Ulist0 of user_symbol
| Ulist0sep of user_symbol * string
| Uopt of user_symbol
| Uentry of string
| Uentryl of string * int

type token_data =
| TokNone
| TokName of string

type ext_token =
| ExtTerminal of string
| ExtNonTerminal of user_symbol * token_data

type tactic_rule = {
  tac_toks : ext_token list;
  tac_body : code;
}

type level = string

type position =
| First
| Last
| Before of level
| After of level
| Level of level

type assoc =
| LeftA
| RightA
| NonA

type gram_symbol =
| GSymbString of string
| GSymbQualid of string * level option
| GSymbParen of gram_symbol list
| GSymbProd of gram_prod list

and gram_prod = {
  gprod_symbs : (string option * gram_symbol list) list;
  gprod_body : code;
}

type gram_rule = {
  grule_label : string option;
  grule_assoc : assoc option;
  grule_prods : gram_prod list;
}

type grammar_entry = {
  gentry_name : string;
  gentry_pos : position option;
  gentry_rules : gram_rule list;
}

type grammar_ext = {
  gramext_name : string;
  gramext_globals : string list;
  gramext_entries : grammar_entry list;
}

type tactic_ext = {
  tacext_name : string;
  tacext_level : int option;
  tacext_rules : tactic_rule list;
}

type node =
| Code of code
| Comment of string
| DeclarePlugin of string
| GramExt of grammar_ext
| VernacExt
| TacticExt of tactic_ext

type t = node list