• Robbert Krebbers's avatar
    Support function pointers and use a state monad in the frontend. · b2109c25
    Robbert Krebbers authored
    Important changes in the core semantics:
    * Types extended with function types. Since function types are a special kind
      of pointer types, types now have an additional mutual part called "ptr_type".
    * Pointers extended with function pointers. Theses are just names that refer
      to an actual function in the function environment.
    * Typing environments extended to assign argument and return types to function
      names. Before we used a separate environment for these, but since the
      argument and return types are already needed to type function pointers, this
      environment would appear in pretty much every typing judgment.
    
    As a side-effect, the frontend has been rewritten entirely. The important
    changes are:
    
    * Type checking of expressions is more involved: there is a special kind of
      expression type corresponding to a function designator.
    * To handle things like block scoped extern function, more state-fullness was
      needed. To prepare for future extensions, the entire frontend now uses a
      state monad.
    b2109c25
base.v 41.7 KB