Backporting the legacy Coq Stream library.

[ppedrot]

This is a backward compatible fix for coq/coq#7536. This is only temporarily solving the problem by redefining the removed library, the corresponding code should be rewritten using negative coinductive types at some point.

[xavierleroy]

Thanks for the early warning and workaround. I forgot CompCert uses streams, but it does, for the input to the Menhir-generated parser. @jhjourdan needs to know about this PR.

Do I understand correctly that the new coinductive-record-based implementation of Streams breaks Menhir-generated Coq parsers? Any hints on what could cause this kind of breakage in your experience?

[ppedrot]

Do I understand correctly that the new coinductive-record-based implementation of Streams breaks Menhir-generated Coq parsers?

Actually they kind of break every development that used the legacy implementation... Luckily the use of streams in CompCert is quite limited.

Any hints on what could cause this kind of breakage in your experience?

Negative coinductive types intensionally behave quite differently from their positive equivalent. The proof needs to be changed accordingly thus, e.g. any destruct is going to fail on those streams. If the developments were written without relying on combinators like the ones of paco it's likely you'll notice that at the very first proof over streams... Not to mention some properties that now do not hold without axioms, like e.g. s = cons (hd s) (tl s).

[xavierleroy]

Thanks for the info. It's worse than I thought :-) I'll reformulate my question differently:

Is there any way to write Coq code and proofs that use Streams from the Coq stdlib and that work both with the old and the new implementation of Streams?

[xavierleroy]

Formulated differently again:

If I don't use "destruct" and a bunch of other things, and use only this and that lemma provided in the old and the new Streams modules, can I write Coq code that work with both?

[ppedrot]

If I don't use "destruct" and a bunch of other things, and use only this and that lemma provided in the old and the new Streams modules, can I write Coq code that work with both?

The Coq stream library is rather crappy, and it lacks any useful combinator. So unluckily I don't think that there is a way to make the development compatible with both in their current state...

Also, switching to negative coinductive types is a foundational change, so it's not kind of unexpected that you're going to face trouble trying to come up with a compatibility layer.

[xavierleroy]

Very clear, thank you.

For CompCert it's not a big deal, as CompCert can provide its own Streams library (like this PR does) or put strict constraints on Coq's version.

For the maintainers of Menhir's Coq output (hi @jhjourdan), being unable to produce parsers that work with both Streams implementations could be a real pain.

[jhjourdan]

Thanks for this PR.

The Menhir Coq generator needs some work in order to make it compatible with negative coinductives. But anyway, I would also like to change the way the input stream is given: Currently, it is given as a stream of dependent pairs, which requires the user-side Ocaml code of verified library to use a massive Obj.magic for building the stream. Not particularly pretty nor reassuring.

Hence, I am planning to do an update of the Coq backend for Menhir that will integrate both changes. I am however happy that @ppedrot provided this temporary patch, so that nothing is broken in the meantime.

[bollu]

@ppedrot Asking to understand terminology: What is a "negative coinductive type"? In particular, what does the "negative" mean in this context?

[ppedrot]

@bollu This is a terminology inspired by linear logic. Negative means that the normal forms of the inhabitants of such types are defined by elimination rules, namely projections. This contrast with positive types which are captured by introduction rules, i.e. constructors. The nomenclature is a bit flaky here, positive vs. negative qualification have been used for a lot of different but somewhat related concepts, so I'm not claiming any novelty here. It could also have been called co-pattern-style coinductive types or something.

[xavierleroy]

Concerning terminology: several recent PL papers use "codata" or "codatatypes" to refer to types defined by their projections, as opposed to "data" or "datatypes" which are defined by their constructors.

[xavierleroy]

Concerning Menhir-generated parsers: @jhjourdan's plan sounds good, let me know when it's ready.

[xavierleroy]

Concerning this PR: I'm OK with merging it as a temporary workaround before Menhir changes. I'll wait for coq/coq#7536 to be accepted by the Coq dev team, though.

[xavierleroy]

Since commit 998f3c5 and the work of @jhjourdan (#276), CompCert no longer uses the Stream module from Coq's standard library.