Use extracted Lambda Box definitions and s-expression serializers

[4ever2]

Use $\lambda_\square$ s-expression serializer extracted from Peregrine. Also updates agda2lambox to use the new AST format and includes serializers for the Peregrine configuration object.

I moved the definition of $\lambda_\square$ from agda2lambox to the lambdabox library. We can change this if you prefer to keep the files here or include the extracted files in this repo too.

Other changes:

• Switches off the constructors as blocks transformations as we have a verified pass performing this in Peregrine.
• Fixes printing of unicode in the generated Rocq files

[flupe]

Sorry for not replying earlier, that is very cool, thanks!
I will take a closer look once we're past the deadline.

I think I'd prefer the Agda2Lambox.Compile.Target and GADT for LamBox syntax (that depends on Target) to remain on this repo, as they are very much tied to this backend. But I can take care of that later.

Don't you think we can actually fully remove the --blocks option? Now that it's enabled on the Peregrine side?

Anyways, thanks a lot.

[4ever2]

Don't you think we can actually fully remove the --blocks option? Now that it's enabled on the Peregrine side?

I don't see any reason to keep it.

[4ever2]

I'll rebase the PR later.
I agree it makes sense to keep Target here, though I would argue that some of the base definitions that don't depend (like kernames) on it make sense to have in the other repository so that there is a clean interface for the extracted code.

Would that work for you?