Best way to obtain constrs free from de Bruijn indices?

Developing plugins
1

I need to “resolve” de Bruijn indices in constrs to their names to get better machine-readable representations.

Is there a better way to do this than recursively traversing constr and constructing and querying an ad-hoc environment (map) that resolves indices to names? (Example of this approach.) It seems to me this is a bit fragile to changes in Coq, and I was hoping someone might know about convenience functions to avoid brittle code for this case.

Take as an example

iff_refl: forall A : Prop, A <-> A

Here is what the constr looks like as a SerAPI sexp:

(Prod((binder_name(Name(Id A)))(binder_relevance Relevant))(Sort Prop)
 (App(Const((Constant(MPfile(DirPath((Id Logic)(Id Init)(Id Coq))))
 (Id iff))(Instance())))((Rel 1)(Rel 1))))

And here is one representation that would be an improvement:

(Prod((binder_name(Name(Id A)))(binder_relevance Relevant))(Sort Prop)
 (App(Const((Constant(MPfile(DirPath((Id Logic)(Id Init)(Id Coq))))
 (Id iff))(Instance())))((Id A)(Id A))))

Variable name capture is not really an issue for my purposes.

2

You got to be careful when transforming de Bruijn to named as many things including conversion won’t preserve the translation well.

That being said, I don’t see any other way than to define a new data type and an OCaml function doing the usual translation to the named-style term type.

3

you could use detyping with all the pretty printing options turned off maybe

Gaëtan Gilbert

4

Thanks, using detyping gave me something quite close to what I wanted:

((v(GProd(Name(Id A))Explicit((v(GSort GProp))(loc()))
((v(GApp((v(GRef(ConstRef(Constant(MPfile(DirPath((Id Logic)(Id Init)(Id Coq))))(Id iff)))()))(loc()))
(((v(GVar(Id A)))(loc()))((v(GVar(Id A)))(loc())))))(loc()))))(loc()))

However, due (I believe) to SerAPI serialization enhancements, a bunch of (loc()) show up. While this is not a big issue, is there a simple way to remove them @ejgallego? I tried setting the omit_loc boolean, but no difference.

5

(loc ()) means that the “detyping” process couldn’t manage to produce a loc on the AST, so the loc is empty; this is not specific to SerAPI but the way Coq works.

omit_loc will erase the locs but not the attribute holding them. You can try omit_atts , however I do recommend you handle them as they are really part of the AST meta-data.

1 Like