search

draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

Address issue #300 by improving Constr.pp_constr, making Constr.t printing more readability #307

Closed gltrost closed 3 years ago

gltrost commented 3 years ago

There are several problems currently with printing Constr.t-values. Some of these issues are

  1. Escaped special characters like \n and \\
  2. Indentation issues
  3. Coloring special-words and values like let and in when printing
  4. Empty parens () => ... which don't need to be shown.
  5. Unreadable syntax like ITE instead of if ... then ... else

This branch attempts to address or fix all of these issues, mainly by adding changes to Constr.pp_constr.

With these changes, reading Constr.t statements with flags like show="precond-internal" will be much easier.

gltrost commented 3 years ago

I mark this as "approved," because my suggestions are just suggestions. Greg, make whichever of my suggested changes you like, and then feel free to merge.

My comments pertain to constraint.ml:

  • Line 50 et al: maybe change rem to rm, since rm is a common abbreviation for remove?
  • Line 250: maybe change form to fmt, since fmt is an established abbreviation for formatter arguments? Also, in the print_expr_list and to_color functions, maybe also use fmt instead of ch for the formatter arguments? (I can't quite figure out what ch is supposed to stand for...)
  • Line 250: For what it's worth, I'm a fan of using t as the argument name for the constraint. The word cons usually means something else in functional programming.
  • Line 256: you can use punning here: write goal_to_string ~colorful g instead of goal_to_string ~colorful:colorful g.
  • Line 273: can you use to_color here instead of manually adding the escape tags?
  • Line 282: can you delete this line?

Other comments:

  • I would print the goal names as yellow instead of red. Red is usually used to signal errors in terminal output.
  • For the pp_constr function, I'd probably make the first argument a named argument ~colorful. Then in the constraint.mli file it is easier to understand what it's for.

Otherwise, looks good! I like how simple you get this stuff boiled down to.

I like all of these recommendations. I'll get them added and will then merge. Thanks!