I was looking at the grammar files of the extraction plugins in the coq repo.
https://github.com/coq/coq/blob/master/plugins/extraction/g_extraction.mlg
There are names like: ne_global_list
, preident
, identref
, etc.
I was wondering what those names signify and where they come from.
Does anyone know?
From the context, one can guess the intention sometimes but not sure how accurate such guesses would be.
Tried grep-ing the coq repo for ne_global_list
, but could spot only usages, not definition.
Does this have something to do with camlp5?
Found an identref
in pcoq.ml:
https://github.com/coq/coq/blob/master/parsing/pcoq.ml#L315
What could ne_
stand for in ne_global_list
?
Could this be related?
https://coq.inria.fr/doc/v8.10/api/coq/Stdarg/index.html
ne_
and _list
are magic modifiers, it means nonempty list of (whatever's in the middle in this case global
)
after removing the modifiers the names are regular ocaml names like https://github.com/coq/coq/blob/50ca6d51cffb28e23a4890d7cb3b254677866f3f/parsing/pcoq.mli#L152 (but I think they have to be from open
modules, you can't qualify them)
And what does the wit_
prefix in the variable names of stdarg.ml
stand for?
argument extend uses genarg instead of entry, so when you write identref
it looks up wit_identref
What does entry mean in coq?
Have heard of custom entries in notations, but never really knew what the name 'entry' meant there.
kernel entry is unrelated to grammar entry
kernel entry is the input type of the kernel, functions to have the kernel check and add a definition / inductive / etc to the environment look like entry -> safe_env -> safe_env
(in safe_typing.mli
)
and AFAICT, a "grammar entry" is what everybody else calls nonterminal; Coq's grammar has entries/nonterminals like constr
for terms, but custom entries let you add _new_ nonterminals, while other term notations only add rules to constr
.
Last updated: Oct 13 2024 at 01:02 UTC