Consistently use `set_` prefix.

The MR closes #24 (closed).

• Consistently set_ prefixes (instead of collection_).
• Rename the Collection type class into Set_. Likewise, SimpleCollection is called SemiSet, and FinCollection is called FinSet, and CollectionMonad is called MonadSet.
• Rename collections.v and fin_collections.v into sets.v and fin_sets.v, respectively.
• Rename set A := A → Prop (theories/set.v) into propset, and likewise bset into boolset.
• Consistently prefer X_to_Y for conversion functions, e.g. list_to_map instead of the former map_of_list.

Sed script uses

This MR is the result of the following sed script. It only had one bug, it wrongly replaced Vector.of_list into Vector.set_of_list. Note that I'm not using \b all the time because I also wanted to fix up lemma names.

sed '
s/SimpleCollection/SemiSet/g;
s/FinCollection/FinSet/g;
s/CollectionMonad/MonadSet/g;
s/Collection/Set\_/g;
s/collection\_simple/set\_semi\_set/g;
s/fin\_collection/fin\_set/g;
s/collection\_monad\_simple/monad\_set\_semi\_set/g;
s/collection\_equiv/set\_equiv/g;
s/\bbset/boolset/g;
s/mkBSet/BoolSet/g;
s/mkSet/PropSet/g;
s/set\_equivalence/set\_equiv\_equivalence/g;
s/collection\_subseteq/set\_subseteq/g;
s/collection\_disjoint/set\_disjoint/g;
s/collection\_fold/set\_fold/g;
s/collection\_map/set\_map/g;
s/collection\_size/set\_size/g;
s/collection\_filter/set\_filter/g;
s/collection\_guard/set\_guard/g;
s/collection\_choose/set\_choose/g;
s/collection\_ind/set\_ind/g;
s/collection\_wf/set\_wf/g;
s/map\_to\_collection/map\_to\_set/g;
s/map\_of\_collection/set\_to\_map/g;
s/map\_of\_list/list\_to\_map/g;
s/map\_of\_to_list/list\_to\_map\_to\_list/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/\bof\_list/list\_to\_set/g;
s/\bof\_option/option\_to\_set/g;
s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
s/seq\_set/set\_seq/g;
s/collections/sets/g;
s/collection/set/g;
s/to\_gmap/gset\_to\_gmap/g;
s/of\_bools/bools\_to\_natset/g;
s/to_bools/natset\_to\_bools/g;
' -i $(find -name "*.v")

Impact on dependencies

I have patches for Iris, lambdarust, Iron, fri-coq and iris-examples. The amount of renaming that had to be done was fairly minimal, and was mostly done automatically using the above sed script.

• Iris: 42 lines changed
• Iris-examples: 8 lines changed
• Iron: no changes needed
• Lambdarust: 17 lines changed
• Fri-coq: 83 lines changed (mostly changing set into propset by hand)

A potential issue: there is also theories/set.v which contains:

Record set (A : Type) : Type := mkSet { set_car : A → Prop }.

And shows that this thing is a collection. This is going to cause some potential clashes.

Since we barely use this construction, I would be in favor of renaming it into something else.

Note that we also have theories/bset for Boolean set (i.e. bset A := A → bool. Maybe something following that line?

mentioned in issue #24 (closed)

changed the description

Yeah, we could use pset (for Prop set).

Hmm, I just noticed we already have Pset for set of positives... Using pset may be confusing.

added 35 commits

• 310686e9...17f8c792 - 33 commits from branch master
• 17ab3cd6 - Consistently use `set_` prefix.
• f3c0d3fd - Better names for convertion functions from `gset` and `coPset`.

Compare with previous version

marked the checklist item Rename Collection type class Any suggestions? as completed

marked the checklist item Rename collections.v and fin_collections.v as completed

marked the checklist item Figure out what to do with theories/set.v as completed

I have updated this MR and the description. All issues appear to be resolved.

@jjourdan @jung Could you review?

unmarked as a Work In Progress

changed the description

mentioned in merge request !44 (merged)

As I already said several times, I do not have a strong opinion on this. The developments I care about will all be ported by you. I am just worried about how annoying this gets for all the other users -- I am not convinced it's worth the pain, but I will leave that decision to you.

Fri-coq: 83 lines changed (mostly changing set into propset by hand)

That seems like a lot, in particular if it had to happen manually.

But still, please do check that I have not introduced any new oddities, or have introduced renamings that you absolutely disagree with.

added 2 commits

• ba314f45 - Consistently use `set_` prefix.
• a3ac6324 - Better names for convertion functions from `gset` and `coPset`.

Compare with previous version

changed the description

Update: I updated the constructors of propset and boolset to become PropSet and BoolSet respectively (used to be mkSet and mkBSet).

added 6 commits

• a3ac6324...fba969b6 - 4 commits from branch master
• 4f8ff968 - Consistently use `set_` prefix.
• f5da0c1a - Better names for convertion functions from `gset` and `coPset`.

Compare with previous version

added 13 commits

• f5da0c1a...22d4a0cd - 10 commits from branch master
• b7e31ce2 - Consistently use `set` and `map` names.
• 31e0d1f6 - Better names for convertion functions from `gset` and `coPset`.
• 6f5a8ecb - Rename `of_bools`/`to_bools` into `bools_to_natset`/`natset_to_bools`.

Compare with previous version

changed the description

resolved all discussions

added 1 commit

• e823cff6 - Comment about `Set_`.

Compare with previous version

resolved all discussions

Ok, I'm going to merge this. Once !45 (merged) is also merged, and I have ported the dependencies I have access to, I will add an entry to the CHANGELOG with the sed script.

resolved all discussions

mentioned in issue #25 (closed)

merged

mentioned in commit 2cf0cd35

Added the sed script to the CHANGELOG: https://gitlab.mpi-sws.org/iris/stdpp/blob/master/CHANGELOG.md#std-master