Peter Gao (Dec 01 2022 at 05:06): Peter Gao (Dec 01 2022 at 05:06):Hello all. I'm interested in this comment here: https://github.com/coq/coq/issues/9039#issuecomment-821842114
However, as dumb as it sounds, I do not know how to get started -- for example, where in the code base are the reduction strategies implemented? What about specific tactics like simpl? Thanks!
Andres Erbsen (Dec 01 2022 at 05:30):I think the suggestion there is still valid, but now it might actually be easier to try out an Ltac2 implementation using Ltac2.Constr.Unsafe first. This API is quite similar to the Coq internal representation and a prototype based on it could serve as a stepping stone for an OCaml implementation. OTOH It's possible that you'll run into missing functionality in Ltac2.
Peter Gao (Dec 01 2022 at 05:54):Andres Erbsen said:
I think the suggestion there is still valid, but now it might actually be easier to try out an Ltac2 implementation using Ltac2.Constr.Unsafe first. This API is quite similar to the Coq internal representation and a prototype based on it could serve as a stepping stone for an OCaml implementation. OTOH It's possible that you'll run into missing functionality in Ltac2.
Thanks for the suggestion! I still want to see how the reduction strategies and tactics are implemented in the current Coq core first, as a reference point. Any idea on where they are in the repository? (or better yet, how to find specific implementations in general? The Standard Library didn't seem to help...)
Gaëtan Gilbert (Dec 01 2022 at 08:56):In that issue Jason says
the reduction strategies (match, fix, delta, beta, iota, zeta
but I would call these reduction flags (parsed by https://github.com/coq/coq/blob/e9f7e871638e0a0c48ceb2a21fdc9a4962d1d28f/plugins/ltac/g_tactic.mlg#L336 but the main type after parsing phases is https://github.com/coq/coq/blob/e9f7e871638e0a0c48ceb2a21fdc9a4962d1d28f/kernel/cClosure.mli#L25)
What I call reduction strategies is rather lazy cbv cbn vm_compute simpl etc
they get dispatched here https://github.com/coq/coq/blob/e9f7e871638e0a0c48ceb2a21fdc9a4962d1d28f/tactics/redexpr.ml#L238
from there use your editor's jump to definition to find the implementations
Last updated: Oct 12 2024 at 12:01 UTC