diff options
author | 2015-03-04 15:12:46 +0100 | |
---|---|---|
committer | 2015-03-04 15:22:12 +0100 | |
commit | d169ecbac96fe2a8a6a44395ad7fa83612e725c4 (patch) | |
tree | 320ae485363f28f62ff56e51ce9a6743e8658498 /tools/gallina_lexer.mll | |
parent | caf8907992fdfe655af95fa74e9c749be98c430c (diff) |
Introducing MMaps, a modernized FMaps.
NB: this is work-in-progress, there is currently only one
provided implementation (MMapWeakList).
In the same spirit as MSets w.r.t FSets, the main difference between
MMaps and former FMaps is the use of a new version of OrderedType
(see Orders.v instead of obsolete OrderedType.v).
We also try to benefit more from recent notions such as Proper.
For most function specifications, the style has changed : we now use
equations over "find" instead of "MapsTo" predicates, whenever possible
(cf. Maps in Compcert for a source of inspiration). Former specs are
now derived in FMapFacts, so this is mostly a matter of taste.
Two changes inspired by the current Maps of OCaml:
- "elements" is now "bindings"
- "map2" is now "merge" (and its function argument also receives a key).
We now use a maximal implicit argument for "empty".
Diffstat (limited to 'tools/gallina_lexer.mll')
0 files changed, 0 insertions, 0 deletions