Nikola Katić (Aug 03 2022 at 07:55): Nikola Katić (Aug 03 2022 at 07:55):Yesterday I've asked more basic question, but on a similar note.
If the goal is to translate Gallina's expression to the corresponding expression of a deep embedding of some language being modeled, e.g.
let <some_id> := <some_val> in <expression> -----> Let <identifier> <assign_exp> <body_exp>
What is the most easiest way to achieve that? Can Ltac extract the real name of <some_id> (e.g. in the form of string or nat)?
Definitely the problem here is the recursive nature of Let expression.
I've read some of Reflection but that offers way more complex features than I need (and can comprehend at this stage of learning Coq).
Gaëtan Gilbert (Aug 03 2022 at 08:13):use metacoq?
Enrico Tassi (Aug 03 2022 at 08:29):You can also use Coq-Elpi,
From elpi Require Import elpi.
Elpi Command let_name.
Elpi Accumulate lp:{{
pred extract-let-name i:term, o:string.
extract-let-name (let N _ _ _) ID :- coq.name->id N ID.
extract-let-name T _ :- coq.error "not a let:" {coq.term->string T}.
main [trm T] :- extract-let-name T ID, coq.say ID.
}}.
Elpi Typecheck.
Elpi Export let_name.
let_name (let x := 3 in _).
let_name (let y := 3 in _).
let_name (bool).
I suggest you look at the reification example, it does something close to what you need in the quote predicate.
If you have troubles doing so, feel free to write a message in the Elpi stream.
Nikola Katić (Aug 03 2022 at 08:40):Thanks immensely! I think I'll give both plugins a try .
Last updated: Oct 03 2023 at 20:01 UTC