Shea Levy (Oct 09 2020 at 15:13): 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.
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.
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.
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.
Pierre-Marie Pédrot (Oct 09 2020 at 15:21):People have been messing with the Ltac1 / Ltac2 FFI to do this indeed
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.
Enrico Tassi (Oct 09 2020 at 15:23):So can you sketch the code for us? ltac2:( print $t ) or something?
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
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
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
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
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
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:
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.
Pierre-Marie Pédrot (Oct 09 2020 at 15:46):So there is a library that does that already, let me find it.
Pierre-Marie Pédrot (Oct 09 2020 at 15:47):https://gitlab.mpi-sws.org/iris/string-ident is probably a good start
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
Pierre-Marie Pédrot (Oct 09 2020 at 15:49):Hm, actually what you want seems to be the other way around
Shea Levy (Oct 09 2020 at 15:49):Looks like that's going in the opposite direction?
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
Pierre-Marie Pédrot (Oct 09 2020 at 15:50):Simple but tedious.
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
Pierre-Marie Pédrot (Oct 09 2020 at 15:50):I am afraid Ltac2 is not very much battery included...
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
Pierre-Marie Pédrot (Oct 09 2020 at 15:51):Ltac2 mytac x := match Constr.Unsafe.kind x with Var => blah | _ => fail end
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?
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:
Pierre-Marie Pédrot (Oct 09 2020 at 15:53):depends exactly where you put that tactic
Pierre-Marie Pédrot (Oct 09 2020 at 15:54):Notations bind Ltac2 variables as preterms, i.e. untyped syntactic expressions
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)
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)
Pierre-Marie Pédrot (Oct 09 2020 at 15:56):Hm, I don't know how term notations handle the "x ident" part
Pierre-Marie Pédrot (Oct 09 2020 at 15:57):This might not get passed to Ltac2
Pierre-Marie Pédrot (Oct 09 2020 at 15:57):or maybe yes, I actually don't know very well
Pierre-Marie Pédrot (Oct 09 2020 at 15:57):Notations are a fairly hairy component of Coq
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
Shea Levy (Oct 09 2020 at 15:58):Thank you!
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)
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?
Pierre-Marie Pédrot (Oct 09 2020 at 16:01):This should work indeed.
Last updated: Oct 12 2024 at 11:01 UTC