Define `fill` in terms of a `foldl` over `fill_item`.
This has some advantages:
-
Evaluation contexts behave like a proper "Huet's zipper", and thus:
- We no longer need to reverse the list of evaluation context items in the
reshape_expr
tactic. - The
fill
function becomes tail-recursive.
- We no longer need to reverse the list of evaluation context items in the
-
It gives rise to more definitional equalities in simulation proofs using binary logical relations proofs.
In the case of binary logical relations, we simulate an expressions in some ambient context, i.e.
fill K e
. Now, whenever we reshapee
by turning it intofill K' e'
, we end up withfill K (fill K' e')
. In order to use the rules for the expression that is being simulated, we need to turnfill K (fill K' e')
intofill K'' e'
for someK'
. In case of the oldfoldr
-based approach, we had to rewrite using the lemmafill_app
to achieve that. However, in case of the oldfoldl
-basedfill
, we have thatfill K (fill K' e')
is definitionally equal tofill (K' ++ K) e'
provided thatK'
consists of a bunch ofcons
es (which is always the case, since we obtainedK'
by reshapinge
).
Note that this change hardly affected heap_lang
. Only the proof of
atomic_correct
broke. I fixed this by proving a more general lemma
ectxi_language_atomic
about ectxi
-languages, which should have been there
in the first place.