search

kth-step / HolBA

Binary analysis in HOL
Other
34 stars 21 forks source link

All extra expression definitions should follow a naming scheme #27

Open andreaslindner opened 5 years ago

andreaslindner commented 5 years ago

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

totorigolo commented 5 years ago

What naming scheme do you suggest then? :slightly_smiling_face:

andreaslindner commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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).