Skip to content

WIP: don't tie bi.weakestpre to program_logic.language (small canonical structure approach)

Ralf Jung requested to merge ci/ralf/bi-language into master

This is another attempt to fix #408 (closed), this time by adding a new canonical structure for just the val and expr types (so that we can define the Wp notation based on that).

This seems to mostly work. I first tried to keep the val and expr fields in language, but that does not work since then bi.weakestpre.expr LANG (where LANG: language) simplifies to program_logic.language.expr LANG (reducing the coercion away), and subsequently canonical structure search fails.

So instead I embed pre_language as a field into language, which seems to work rather well -- except for one strange failure in proph_erasure that I could not figure out.

Edited by Ralf Jung

Merge request reports