All extra expression definitions should follow a naming scheme

[andreaslindner]

This refers mainly to the bir_and_exp, bir_imp_exp, and similar.

[totorigolo]

What naming scheme do you suggest then? :slightly_smiling_face:

[andreaslindner]

The one that is already used, like for MSB and friends. But maybe it's less consistent than I remember. Let's do this together. Maybe imp also suggests something different than one would expect. But let's talk about this in person.

[didriklundberg]

Can someone explain what is the purpose of "normalizing" by using the bir_exp_and abbreviation in the bir_wp_comp_wps_iter_step2 function? None of the other expression shorthands are used.

I see it was added in commit ba74154.

In general, I would like to see a clearly formulated idea of how to consistently use these abbreviations.

[totorigolo]

Can someone explain what is the purpose of "normalizing" by using the bir_exp_and abbreviation in the bir_wp_comp_wps_iter_step2 function?

Just a guess: I think that this is only to simplify both reading the huge generated WP expression and the if statement that is modified in the commit you linked.

Regarding readability of huge BIR expressions, I would like to remind that bir_ppLib provides a convenient pretty-printer. Furthermore, (I think that) all pretty-printers in HOL4 should be "parsable" in quotations (to be able to copy-paste printed terms), which bir_ppLib currently isn't. Then, to solve this problem, we could introduce a bir_ppTheory with the same shorthands that bir_ppLib uses*. Those definitions could then replace the current bir_and_exp, bir_imp_exp and similar.

---

* I think that this is currently impossible because of variable arity (aka. the nesting feature: see last code block of Parse.add_user_printer.html) currently used in the pretty-printer, but I also think that solutions exist (e.g. use lists instead of varargs, or just remove the nesting feature).