aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/coq-src-description.txt
blob: fe896d31600f56674138a03b47b04397b9293efd (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
111
112
113
114
115
116
117
118
119
120
121
122

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

highparsing :

 Files in parsing/ that cannot be linked too early.
 Contains the grammar rules g_*.ml4

hightactics :

 Files in tactics/ that cannot be linked too early.
 These are the .ml4 files that uses the EXTEND possibilities
 provided by grammar.cma, for instance eauto.ml4.


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 :

 Camlp4 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