Skip to content
  • Robbert Krebbers's avatar
    Changes in preparation of the C type system and C front-end language · 3503a91f
    Robbert Krebbers authored
    Major changes:
    * Make void a base type, and include a proper void base value. This is necessary
      because expressions (free, functions without return value) can yield a void.
      We now also allow void casts conforming to the C standard.
    * Various missing lemmas about typing, weakening, decidability, ...
    * The operations "free" and "alloc" now operate on l-values instead of r-values.
      This removes some duplication.
    * Improve notations of expressions and statements. Change the presence of the
      operators conforming to the C standard.
    Small changes:
    * Use the classes "Typed" and "TypeCheck" for validity of indexes in memory.
      This gives more uniform notations.
    * New tactic "typed_inversion" performs inversion on an inductive predicate
      of type "Typed" and folds the premises.
    * Remove a horrible hack in the definitions of the classes "FMap", "MBind",
      "OMap", "Alter" that was used to let "simpl" behave better. Instead, we have
      defined a tactic "csimpl" that folds the results after performing an
      ordinary "simpl".
    * Fast operation to remove duplicates from lists using hashsets.
    * Make various type constructors (mainly finite map implementations) universe
      polymorphic by packing them into an inductive. This way, the whole C syntax
      can live in type, avoiding the need for (slow) universe checks.