Stream: Coq users

Topic: Translating expressions between languages

view this post on Zulip 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 I need (and can comprehend at this stage of learning Coq).

view this post on Zulip Gaëtan Gilbert (Aug 03 2022 at 08:13):

use metacoq?

view this post on Zulip 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 :->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.

view this post on Zulip Nikola Katić (Aug 03 2022 at 08:40):

Thanks immensely! I think I'll give both plugins a try .

Last updated: Jan 29 2023 at 06:02 UTC