• Robbert Krebbers's avatar
    Modify typing judgments to depend on a description of the types of objects in · 7f9c5994
    Robbert Krebbers authored
    memory instead of the whole memory itself.
    This has the following advantages:
    * Avoid parametrization in {addresses,pointers,pointer_bits,bits}.v
    * Make {base_values,values}.v independent of the memory, this makes better
      parallelized compilation possible.
    * Allow small memories (e.g. singletons as used in separation logic) with
      addresses to objects in another part to be typed.
    * Some proofs become easier, because the memory environments are preserved
      under many operations (insert, force, lock, unlock).
    It also as the following disadvantages:
    * At all kinds of places we now have explicit casts from memories to memory
      environments. This is kind of ugly. Note, we cannot declare memenv_of as a
      Coercion because it is non-uniform.
    * It is a bit inefficient with respect to the interpreter, because memory
      environments are finite functions instead of proper functions, so calling
      memenv_of often (which we do) is not too good.
fin_maps.v 61.4 KB