[dir_contents] Allow qualified traversal of directories.

[ejgallego]

This is a cherry-pick of the directory traversal parts from the Dune
PR (#1968) plus a modification to enable the qualified mode inside (include_subdirs ...)

I was uncomfortable with the misnaming done there, so this PR enables
the (include_subdirs qualified) syntax and provides a local part
to the traversal so clients [such as the Coq mode] can use it.

Note that this does introduce a bit of overhead in the tree traversal,
especially in deep trees, it should be possible to optimize if we deem
it necessary.

[rgrinberg]

(include_subdirs qualified|unqalified) Is quite useful for C/Cxx sources. Of course qualified vs. unqualified is meaningless for C, but still splitting your code into different dirs is nice

In retrospect, we should have probably made this stanza a field in the library/exectuable/coqlib stanzas, but whatever.

[rgrinberg]

It's good enough to merge. @ejgallego please don't forget to add the parsing error when coq isn't enabled as a project.

[ejgallego]

In retrospect, we should have probably made this stanza a field in the library/exectuable/coqlib stanzas, but whatever.

At first I thought that would make sense, so the qualified part was "local" to the coq stanza; on the other hand at least the recursive nature seems to have a more global scope, so I dunno.

[ejgallego]

@ejgallego please don't forget to add the parsing error when coq isn't enabled as a project.

Done, thanks! You may want to check the implementation, but I think it is OK.

[ejgallego]

Umm, actually @rgrinberg I am having trouble querying the Dune_project to see if an extension is enabled. I wanted to hook the check here:

    ; "include_subdirs",
      (let+ () = Syntax.since Stanza.syntax (1, 1)
       and+ t =
         let t = ??? in
         let enable_qualified =
           Option.is_some (Dune_project.find_extension_args t Coq.key) in
         Include_subdirs.decode ~enable_qualified
       and+ loc = loc in
       [Include_subdirs (loc, t)])

however this doesn't seem like the right place I'm afraid.

[emillon]

There's a similar code path when setting up formatting rules, you can have a look at how it works there.

[ejgallego]

Thanks @emillon , I am not sure tho that I should access the super context at parsing time, it seems somehow to complicate things too much, right?

Maybe the parsing check is too much of a trouble if the a Dune_project.t is not in scope @rgrinberg ?

[rgrinberg]

The dune project is always in scope when parsing. Otherwise, we can't parse as we don't know what extensions are enabled.

You can simply call Dune_project.get_exn () to retrieve it.

[ejgallego]

You can simply call Dune_project.get_exn () to retrieve it.

Thanks @rgrinberg , somehow I missed the type on this one.

Rebased; will merge once CI is happy.