• Robbert Krebbers's avatar
    Disambiguate Haskell-style notations for partially operators. · 45690e49
    Robbert Krebbers authored
    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.
    
    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")
    ```
    45690e49
base.v 56.9 KB