|
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
------------------
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
Proofview.V82.tac
TODO: check with Hugo
*** Vernac expressions ***
Vernacexpr.vernac_expr, produced by parsing, used in Vernacentries and Vernac
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
