This MR introduces a tool why3 pp to pretty print (portions of) mlw files, and is a continuation of !146 (closed).

• It can be used to print inductive definitions to latex, as before

  $ cat test1.mlw
  module Test
    inductive t n = Z : t 0 | S : t n -> t (n+1)
  end
  $ why3 pp --output=latex --kind=inductive test.mlw test.Test.t
  % \newcommand{\INDn}[0]{\mathsf{n}}
  % \newcommand{\INDtun}[1]{\mathsf{t}(#1)}
  \begin{mathparpagebreakable} % Test.t
    \inferrule[Z]
      {~}
      {\INDtun{0}} \\
    \inferrule[S]
      {\INDtun{\INDn}}
      {\INDtun{\INDn + 1}} \\
  \end{mathparpagebreakable}

  (Larger example in !146 (closed).)
• it contains the starting point of a formtting tool for mlw files

  $ cat test2.mlw
  module Test let f xxxxxxxxxxxxxxxxxxxxxxxxxx = let yyyyyyyyyyyyyyyyyyyy = xxxxxxxxxxxxxxxxxxxxxxxxxx + 1 in yyyyyyyyyyyyyyyyyyyy + yyyyyyyyyyyyyyyyyyyy end
  $ why3 pp --output=mlw test2.mlw
  module Test
    let f xxxxxxxxxxxxxxxxxxxxxxxxxx =
      (let yyyyyyyyyyyyyyyyyyyy = (xxxxxxxxxxxxxxxxxxxxxxxxxx + 1) in
      (yyyyyyyyyyyyyyyyyyyy + yyyyyyyyyyyyyyyyyyyy))
  end

  (This still has many rough edgees and is more of a side-effect of having module Mlw_printer, which formats a Ptree into concrete syntax)
• In comparison with !146 (closed), pretty printing is now based on the Ptree instead of the typed tree. This simplifies the printing of record creations and updates (no reconstruction required anymore), and is made possible by a commit from @rmalak's branch ptree_parser_pp that is part of this MR.