Disambiguate Haskell-style notations for partially applied operators

For example, change (!! i) into (.!! x) so that !! can also be used as a prefix, as done in VST for example.

This closes issue #42 (closed).

I have used the sed script below. This script took care of nearly all uses apart from a few occurrences where a space was missing, e.g. (,foo). In this case, coqc will just fail, allowing one to patch up things manually.

The script is slightly too eager on Iris developments, where it also replaces ($ ...) introduction patterns. When porting Iris developments you thus may want to remove the line for $.

sed '
s/(= /(.= /g;
s/ =)/ =.)/g;
s/(≠ /(.≠ /g;
s/ ≠)/ ≠.)/g;
s/(≡ /(.≡ /g;
s/ ≡)/ ≡.)/g;
s/(≢ /(.≢ /g;
s/ ≢)/ ≢.)/g;
s/(∧ /(.∧ /g;
s/ ∧)/ ∧.)/g;
s/(∨ /(.∨ /g;
s/ ∨)/ ∨.)/g;
s/(↔ /(.↔ /g;
s/ ↔)/ ↔.)/g;
s/(→ /(.→ /g;
s/ →)/ →.)/g;
s/($ /(.$ /g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(, /(., /g;
s/ ,)/ ,.)/g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(∪ /(.∪ /g;
s/ ∪)/ ∪.)/g;
s/(⊎ /(.⊎ /g;
s/ ⊎)/ ⊎.)/g;
s/(∩ /(.∩ /g;
s/ ∩)/ ∩.)/g;
s/(∖ /(.∖ /g;
s/ ∖)/ ∖.)/g;
s/(⊆ /(.⊆ /g;
s/ ⊆)/ ⊆.)/g;
s/(⊈ /(.⊈ /g;
s/ ⊈)/ ⊈.)/g;
s/(⊂ /(.⊂ /g;
s/ ⊂)/ ⊂.)/g;
s/(⊄ /(.⊄ /g;
s/ ⊄)/ ⊄.)/g;
s/(∈ /(.∈ /g;
s/ ∈)/ ∈.)/g;
s/(∉ /(.∉ /g;
s/ ∉)/ ∉.)/g;
s/(≫= /(.≫= /g;
s/ ≫=)/ ≫=.)/g;
s/(!! /(.!! /g;
s/ !!)/ !!.)/g;
s/(⊑ /(.⊑ /g;
s/ ⊑)/ ⊑.)/g;
s/(⊓ /(.⊓ /g;
s/ ⊓)/ ⊓.)/g;
s/(⊔ /(.⊔ /g;
s/ ⊔)/ ⊔.)/g;
s/(:: /(.:: /g;
s/ ::)/ ::.)/g;
s/(++ /(.++ /g;
s/ ++)/ ++.)/g;
s/(≡ₚ /(.≡ₚ /g;
s/ ≡ₚ)/ ≡ₚ.)/g;
s/(≢ₚ /(.≢ₚ /g;
s/ ≢ₚ)/ ≢ₚ.)/g;
s/(::: /(.::: /g;
s/ :::)/ :::.)/g;
s/(+++ /(.+++ /g;
s/ +++)/ +++.)/g;
' -i $(find -name "*.v")

added 1 commit

• 1a77ae7e - Disambiguate Haskell-style notations for partially operators.

Compare with previous version

@wmansky I have created branch of Iris based on this MR: https://gitlab.mpi-sws.org/iris/iris/commits/robbert/stdpp_issue42 Could you test if this indeed fixes the VST issue?

@wmansky confirms this fixes the incompatibility with VST.

Waiting for @jung to review after he's back from holiday.

changed title from Disambiguate Haskell-style notations for partially operators. to Disambiguate Haskell-style notations for partially applied operators

changed the description

added 1 commit

• be3b6549 - CHANGELOG entry.

Compare with previous version

added 1 commit

• 9403b964 - CHANGELOG entry.

Compare with previous version

mentioned in merge request !97 (merged)

resolved all threads

added 9 commits

• 9403b964...b53cbe77 - 7 commits from branch master
• 45690e49 - Disambiguate Haskell-style notations for partially operators.
• 3a1f5195 - CHANGELOG entry.

Compare with previous version

mentioned in commit 9041e6d8

merged

mentioned in commit dfrumin/coq-stdpp@e179fe02

mentioned in commit dfrumin/coq-stdpp@5d7009bc

mentioned in commit dfrumin/coq-stdpp@b4893e4c

mentioned in commit 41c1305d