1. 20 Feb, 2019 1 commit
    • Robbert Krebbers's avatar
      Consistently use `set` and `map` names. · b7e31ce2
      Robbert Krebbers authored
      Get rid of using `Collection` and favor `set` everywhere. Also, prefer conversion
      functions that are called `X_to_Y`.
      The following sed script performs most of the renaming, with the exception of:
      - `set`, which has been renamed into `propset`. I couldn't do this rename
        using `sed` since it's too context sensitive.
      - There was a spurious rename of `Vec.of_list`, which I correctly manually.
      - Updating some section names and comments.
      sed '
      ' -i $(find -name "*.v")
  2. 29 Jan, 2019 1 commit
  3. 17 Sep, 2017 1 commit
    • Robbert Krebbers's avatar
      Set Hint Mode for all classes in `base.v`. · 7d7c9871
      Robbert Krebbers authored
      This provides significant robustness against looping type class search.
      As a consequence, at many places throughout the library we had to add
      additional typing information to lemmas. This was to be expected, since
      most of the old lemmas were ambiguous. For example:
        Section fin_collection.
          Context `{FinCollection A C}.
          size_singleton (x : A) : size {[ x ]} = 1.
      In this case, the lemma does not tell us which `FinCollection` with
      elements `A` we are talking about. So, `{[ x ]}` could not only refer to
      the singleton operation of the `FinCollection A C` in the section, but
      also to any other `FinCollection` in the development. To make this lemma
      unambigious, it should be written as:
        Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
      In similar spirit, lemmas like the one below were also ambiguous:
        Lemma lookup_alter_None {A} (f : A → A) m i j :
          alter f i m !! j = None  m !! j = None.
      It is not clear which finite map implementation we are talking about.
      To make this lemma unambigious, it should be written as:
        Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
          alter f i m !! j = None  m !! j = None.
      That is, we have to specify the type of `m`.
  4. 08 Sep, 2017 1 commit
  5. 15 Mar, 2017 1 commit
  6. 31 Jan, 2017 3 commits
  7. 20 Sep, 2016 1 commit
  8. 24 Feb, 2016 1 commit
    • Robbert Krebbers's avatar
      Rewrite set_unfold using type classes. · 9201446c
      Robbert Krebbers authored
      It now traverses terms at most once, whereas the setoid_rewrite
      approach was travering terms many times. Also, the tactic can now
      be extended by defining type class instances.
  9. 19 Feb, 2016 1 commit
  10. 17 Feb, 2016 3 commits
  11. 16 Feb, 2016 1 commit
  12. 13 Feb, 2016 1 commit
  13. 16 Jan, 2016 1 commit
    • Robbert Krebbers's avatar
      Remove elem_of_tactic that uses intuition. · 4b4e270e
      Robbert Krebbers authored
      This one (previously solve_elem_of) was hardly used. The tactic that uses
      naive_solver (previously esolve_elem_of, now solve_elem_of) has been
      extended with flags to say which hypotheses should be cleared/kept.
  14. 12 Jan, 2016 1 commit
  15. 21 Dec, 2015 1 commit
  16. 16 Nov, 2015 1 commit
  17. 11 Nov, 2015 1 commit
  18. 15 Mar, 2015 1 commit
  19. 08 Feb, 2015 2 commits
    • Robbert Krebbers's avatar
      Update copyright headers. · 5a73c4ed
      Robbert Krebbers authored
    • 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.
  20. 16 Jun, 2014 1 commit
    • 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.
  21. 05 Jun, 2014 1 commit