blob: b3d49b7e56f7e9029890349692f9d89336a49f35 (
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
Coq main source components (in link order)
------------------------------------------
clib : Basic files in lib/, such as util.ml
lib : Other files in lib/
kernel
library
pretyping
interp
proofs
printing
parsing
tactics
toplevel
Special components
------------------
intf :
Contains mli-only interfaces, many of them providing a.s.t.
used for dialog bewteen coq components. Ex: Constrexpr.constr_expr
produced by parsing and transformed by interp.
grammar :
Camlp5 syntax extensions. The file grammar/grammar.cma is used
to pre-process .ml4 files containing EXTEND constructions,
either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND.
This grammar.cma incorporates many files from other directories
(mainly parsing/), plus some specific files in grammar/.
The other syntax extension grammar/q_constr.cmo is a addition to
grammar.cma with a constr PATTERN quotation.
Hierarchy of A.S.T.
-------------------
*** Terms ***
... ...
| /\
parsing | | printing
| |
V |
Constrexpr.constr_expr
| /\
constrintern | | constrextern
(in interp) | | (in interp)
globalization | |
V |
Glob_term.glob_constr
| /\
pretyping | | detyping
| | (in pretyping)
V |
Term.constr
| /\
safe_typing | |
(validation | |
by kernel) |______|
*** Patterns ***
|
| parsing
V
constr_pattern_expr = constr_expr
|
| Constrintern.interp_constr_pattern (in interp)
| reverse way in Constrextern
V
Pattern.constr_pattern
|
---> used for instance by Matching.matches (in pretyping)
*** Notations ***
Notation_term.notation_constr
Conversion from/to glob_constr in Notation_ops
TODO...
*** Tactics ***
|
| parsing
V
Tacexpr.raw_tactic_expr
|
| Tacinterp.intern_pure_tactic (?)
V
Tacexpr.glob_tactic_expr
|
| Tacinterp.eval_tactic (?)
V
Proof_type.tactic
TODO: check with Hugo
*** Vernac expressions ***
Vernacexpr.vernac_expr, produced by parsing, used in Vernacentries and Vernac
|
