WIP: Latex export of inductive rules

This MR adds a tool to print the rules of a Why3 inductive type in LaTeX. The LaTeX code is based on the mathpartir package, and functions, variable names, and field names are configurable (have to be configured) by LaTeX commands.

Example

The following inductive definition

inductive eval_instruction (input, context, state) instruction (state, context, behaviour) =
  | eval_if_true: forall inp ctx ctx1 ctx2 sta sta1 sta2 ins1 ins2 ins3 bhv2.
    eval_instruction ({inp with under_condition=True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
    ctx1.result = True ->
    eval_instruction (inp, ctx1, sta1) ins2 (sta2, ctx2, bhv2) ->
    eval_instruction (inp, ctx, sta) (IIf ins1 ins2 ins3) (sta2, ctx2, bhv2)
  
  | eval_if_false: forall inp ctx ctx1 ctx3 sta sta1 sta3 ins1 ins2 ins3 bhv3.
    eval_instruction ({inp with under_condition=True}, ctx, sta) ins1 (sta1, ctx1, BNormal) ->
    ctx1.result = False ->
    eval_instruction (inp, ctx1, sta1) ins3 (sta3, ctx3, bhv3) ->
    eval_instruction (inp, ctx, sta) (IIf ins1 ins2 ins3) (sta3, ctx3, bhv3)
  
  | eval_if_transmit_condition: forall inp ctx ctx1 sta sta1 ins1 ins2 ins3 bhv1.
    eval_instruction ({inp with under_condition=True}, ctx, sta) ins1 (sta1, ctx1, bhv1) ->
    bhv1 <> BNormal ->
    eval_instruction (inp, ctx, sta) (IIf ins1 ins2 ins3) (sta1, ctx1, bhv1)

renders as follows (with appropriate command definitions)

Reconstruction of record updates

The LaTeX output is created from the result of the Why3 parser, the Pmodule AST. However, record updates in the source code are not retained in the Pmodule AST but converted to record constructions. These record constructions usually create more verbose LaTeX output, and the why3 latex tool can reconstruct record updates from record constructions if the the records are described on the command line. The implemented rule of thumb is that when a majority of fields have the form f=x.f then the other fields are used for creating the record update (cf. https://gitlab.inria.fr/why3/why3/blob/latex-export-inductive/doc/manpages.tex#L1147).

That’s of course a dubious hack but required to create concise LaTeX output. A better solution may be to retain the Ptree declarations in the Pmodule AST, and generate the LaTeX output based on the Ptree declarations.