SourceTreeGuide

root edited this page Oct 11, 2017 · 5 revisions

Hitchhiker's Guide to the Coq Source Tree

A bit of notation :

  • terms and types are written with the form symbol_name:path/to/sourcefile.ml or (symbol_name:type):path/to/sourcefile.ml the first time they are encountered, and can be shortened to symbol_name after.

TODO : refine notations conventions, to distinguish between terms and parameters and possibly include code as-is.

Adventures of a Vernac Command

There is two way to process strings coming from stdin. The first one is by looping over do_vernac:toplevel/toplevel.ml, and the second one by looping over parse_one_command_group:toplevel/protectedtoplevel.ml.

do_vernac reads a vernac Command from stdin through mt:lib/pp.ml4, resynch the toplevel command buffer and feeds (top_buffer.tokens:char Stream.t):toplevel/toplevel.ml to raw_do_vernac:toplevel/vernac.ml. raw_do_vernac is mainly a wrapper for vernac:toplevel/vernac.ml, which itself is a wrapper for vernac_com:toplevel/vernac.ml that automatically feeds it with the output of parse_phrase:toplevel/vernac.ml. vernac_com does a pattern matching on the parsing result to handle file loading or command timing, and then calls with_heavy_rollback:lib/states.ml with interp:toplevel/vernacentries.ml as its first parameter. interp does the big match on the vernac_expr:toplevel/vernacexpr.ml input and calls the appropriate function.

To be continued ...

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.