New parser and pretty-printer for BIR expressions and programs

[pablobuiras]

We need this for debugging Scam-V (in particular, to inspect the generated stuff) without going insane. It's also nice for usability/user-interface reasons in case we find a counterexample and want to show it to the user.

[totorigolo]

Linking a04c369 for information: this is already a pretty-printer for BIR.

Features:

• Simplification of verbose constructs (e.g. BExp_BinExp BIExp_Or is written as BExp_Or).
• Different representation of if-then-else statements, simplifying reading the expression when either the condition or the then expression are very long.
• Consistent breaking (new lines) of long expressions, because the default printer isn't aware of the structure of printed expressions.
• Highlighting of types, facilitating debugging when the expression isn't well-typed.
• Highlighting of all strings, facilitating reading labels and variable names.
• Gathering of nested binary expressions of the same type on the same level.
• Rainbow parenthesis, i.e. matching pairs of parenthesis are printed in the same color.

Pretty-printers:

  val pretty_printers = [
    ("HOL_string", ``str: string``, hol_string_printer),
    ("bir_immtype_t", ``bit: bir_immtype_t``, bir_immtype_t_printer),
    ("bir_imm_t", ``bir_imm: bir_imm_t``, bir_imm_printer),
    ("bir_exp_t", ``bir_exp_t: bir_exp_t``, bir_exp_printer)
]

BUT the pretty-printed expression isn't parsable, that a current limitation.

[pablobuiras]

Yes, also there are no infix operators.