New tool why3pp (pretty print)
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}
- 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
Mlw_printer
, which formats aPtree
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 branchptree_parser_pp
that is part of this MR.