Consistently use `set_` prefix.
The MR closes #24 (closed).
- Consistently
set_
prefixes (instead ofcollection_
). - Rename the
Collection
type class intoSet_
. Likewise,SimpleCollection
is calledSemiSet
, andFinCollection
is calledFinSet
, andCollectionMonad
is calledMonadSet
. - Rename
collections.v
andfin_collections.v
intosets.v
andfin_sets.v
, respectively. - Rename
set A := A → Prop
(theories/set.v
) intopropset
, and likewisebset
intoboolset
. - Consistently prefer
X_to_Y
for conversion functions, e.g.list_to_map
instead of the formermap_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
intopropset
by hand)
Edited by Robbert Krebbers