Stream: Coq users

Topic: Ident reflection in notations?


view this post on Zulip Shea Levy (Oct 09 2020 at 15:13):

If I have some notation that binds an identifier, is there any way to turn that identifier into a string on the right hand side? I acknowledge this is stretching things quite far but it would be nice to annotate a term representing a variable with a user-provided name that way.

view this post on Zulip Enrico Tassi (Oct 09 2020 at 15:17):

@Pierre-Marie Pédrot does ltac2 have an API to print a term? (applied to a variable would produce its string, and with tac-in-terms could do what @Shea Levy asks for). I have one in Elpi, but it would be silly to pull it in jut for this.

view this post on Zulip Enrico Tassi (Oct 09 2020 at 15:19):

I'd also like a way to do this, de Bruijn indexes are very hard to read.

view this post on Zulip Shea Levy (Oct 09 2020 at 15:20):

Enrico Tassi said:

Pierre-Marie Pédrot does ltac2 have an API to print a term? (applied to a variable would produce its string, and with tac-in-terms could do what Shea Levy asks for). I have one in Elpi, but it would be silly to pull it in jut for this.

Is "tac-in-terms" documented anywhere? From the name I can guess what it means but not sure how I'd actually use it.

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:21):

People have been messing with the Ltac1 / Ltac2 FFI to do this indeed

view this post on Zulip Enrico Tassi (Oct 09 2020 at 15:21):

ltac:( tactic ) is equivalent to the (proof) term generated by tactic. ltac:(exact t) is like t.

view this post on Zulip Enrico Tassi (Oct 09 2020 at 15:23):

So can you sketch the code for us? ltac2:( print $t ) or something?

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:30):

For the mentioned use-case, I think that merely matching the term using Constr.Unsafe.kind is going to give you the term structure from which you can extract the ident

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:30):

Depending on what you want to do with this exactly the remaining is quite different

view this post on Zulip Shea Levy (Oct 09 2020 at 15:32):

Pierre-Marie Pédrot said:

Depending on what you want to do with this exactly the remaining is quite different

I'd like to create a term of type Strings.String.string

view this post on Zulip Shea Levy (Oct 09 2020 at 15:35):

OK so I see ident_to_string, I'm not sure how to get a kind to match on given some term in context, and then I'm not sure how to lift that ltac2 string into a gallina string

view this post on Zulip Shea Levy (Oct 09 2020 at 15:36):

I suppose for the second one I can write a tactic to construct the string directly if all else fails. So just need to figure out how to match

view this post on Zulip Shea Levy (Oct 09 2020 at 15:37):

Ooof if there's no internal way to do it though it's going to be a 256-branch case :joy:

view this post on Zulip Shea Levy (Oct 09 2020 at 15:39):

Oh wait I'm sure there's an of_int or whatever in the coq stdlib for chars. Not so bad.

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:46):

So there is a library that does that already, let me find it.

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:47):

https://gitlab.mpi-sws.org/iris/string-ident is probably a good start

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:48):

They have to go through hoops because they want to reuse the ident as an Ltac1 ident, but just getting a Coq string should be easier

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:49):

Hm, actually what you want seems to be the other way around

view this post on Zulip Shea Levy (Oct 09 2020 at 15:49):

Looks like that's going in the opposite direction?

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:49):

Yeah, essentially you'll have to write an Ltac2 function from Ltac2 string to constr that builds the corresponding Gallina string

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:50):

Simple but tedious.

view this post on Zulip Shea Levy (Oct 09 2020 at 15:50):

Yeah, I see how to go from a string to a sequence of chars and a char to an int and I'm sure once there I can get back into a coq string, just trying to see how to get the kind out of the variable in context

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:50):

I am afraid Ltac2 is not very much battery included...

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:51):

So it'd be something like ltac2:(mytac $x) where mytac : constr -> constr and x is the constr variable you want to match on

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:51):

Ltac2 mytac x := match Constr.Unsafe.kind x with Var => blah | _ => fail end

view this post on Zulip Shea Levy (Oct 09 2020 at 15:52):

Ah OK I missed that the constr type is what I want. So I assume I can get a constr by somehow quoting my variable, and then use constr_kind, and go from there?

view this post on Zulip Shea Levy (Oct 09 2020 at 15:53):

The last question, which I will figure out by trying, is if quoting the variable on the RHS of a notation gives me the ident I used in defining the notation or the one I used when I used it :sweat_smile:

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:53):

depends exactly where you put that tactic

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:54):

Notations bind Ltac2 variables as preterms, i.e. untyped syntactic expressions

view this post on Zulip Shea Levy (Oct 09 2020 at 15:55):

Have to pause for the day but I'm going to try something like Notation "'foo' x" := ltac2(do_something_with 'x) (x ident)

view this post on Zulip Shea Levy (Oct 09 2020 at 15:56):

And hope that foo y reduces to ltac2(do_something_with 'y), not ltac2(do_something_with 'x)

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:56):

Hm, I don't know how term notations handle the "x ident" part

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:57):

This might not get passed to Ltac2

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:57):

or maybe yes, I actually don't know very well

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:57):

Notations are a fairly hairy component of Coq

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:58):

But yes, that's the general guideline. If you have trouble do not hesitate to ask back here

view this post on Zulip Shea Levy (Oct 09 2020 at 15:58):

Thank you!

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 15:59):

(Were it not for the "x ident" you would indeed get the AST of the notation argument; giving a bound variable doesn't make much sense)

view this post on Zulip Shea Levy (Oct 09 2020 at 16:00):

Hmm I guess worst case I could bind x in a lambda (of type tt or whatever) and then ltac2 inside that, right?

view this post on Zulip Pierre-Marie Pédrot (Oct 09 2020 at 16:01):

This should work indeed.


Last updated: Feb 08 2023 at 22:03 UTC