findpostulates

#!/bin/sh

if [[ $1 = "-h" ]] || [[ $1 = "--help" ]]
then
    echo "Usage: $0"
    echo
    echo "Shows every postulate used in the Agda files present in the directory"
    echo "except for HIT-related postulates, universe levels and the univalence"
    echo "axiom."
    exit 0
fi

if ! command -v awk &>/dev/null
then
    echo "You need awk to run this script"
    exit 1
fi

# Only use tput if it’s installed

TPUT="tput"

if ! tput -V &>/dev/null
then
    TPUT=":"
fi

for i in $(git ls-files) $(git ls-files -o --exclude-standard)
do
    if [[ $i =~ tutorial/* ]] ||
       [[ $i =~ "core/lib/types/HIT_README.txt" ]] || [[ $i =~ findpostulates ]] ||
       [[ $i =~ old/* ]] ||
       [[ $i =~ test/* ]] ||
       [[ $i =~ theorems/stash/* ]]
    then
        continue
    fi

    result=$(awk '/^\s*postulate/\
                    {if ($0 !~ /Demo$/ &&\
                         $0 !~ /HIT$/ &&\
                         $0 !~ /Universe levels$/ &&\
                         $0 !~ /Coinduction$/ &&\
                         $0 !~ /Univalence axiom$/)\
                      {print; getline; print}}' $i)

    if [[ $result != "" ]]
    then
        $TPUT setaf 5
        echo $i:
        $TPUT setaf 7
        echo "$result"
        echo
    fi
done