Best way to obtain constrs free from de Bruijn indices?

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.

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.

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

Gaëtan Gilbert

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.

(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