| products/sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: coq-src-description.txt Sprache: TextUntersuchung Coq© |
|
||||||
|
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 ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.23Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
