#!/bin/bash

shopt -s nullglob

me="$0"
SRCDIR=$1
#printf "$SRCDIR\n"  >&2
FILES=`echo $SRCDIR/*.spec`

gnugrep=/bin/grep
gnused=/bin/sed

case $OSTYPE in
        linux*)
                #printf "running on Linux\n" >&2
                ;;
        darwin*)
                #printf "running on macOS\n" >&2
                gnugrep=/usr/local/bin/ggrep
                gnused=/usr/local/bin/gsed
                ;;
        *)
                printf "running on untested $OSTYPE\n" >&2
esac


# find lemma names
LEMMAS=`$gnugrep -oPhw 'lemma \K\w+' $FILES | sort -u`

AXIOMATICS=`$gnugrep -oPhw 'axiomatic \K\w+' $FILES | sort -u`

AXIOMS=`$gnugrep -oPhw 'axiom \K\w+' $FILES | sort -u`

INDUCTIVES=`$gnugrep -oPhw 'inductive \K\w+' $FILES | sort -u`

PREDICATES=`$gnugrep -h -A1 -w predicate $FILES | $gnugrep -v predicate | $gnugrep -ve -- | $gnugrep -ve '^$' | $gnugrep -oP '^\s+\K\w+' | sort -u`

FUNCTIONS=`$gnugrep -Pzohe '(?:logic[\wℤ𝔹\s\*]+)\s*\b\K[a-zA-Z_]\w*' $FILES | tr '\0' '\n' | sort -u`


RAWNAMES="$LEMMAS $AXIOMATICS $AXIOMS $INDUCTIVES $PREDICATES $FUNCTIONS"

NAMES=`echo $RAWNAMES | tr " " "\n" | sort -u | tr "\n" " "`


printf "\n%% This file has been automatically generated by $me\n"
printf "%% `date`\n\n"

for name in $NAMES; do
    printf '\\newcommand{\\';
    command=`echo $name | $gnused 's/_//g'`;
    printf "$command}{\\mbox{\\inl{$name}}";
    printf '\\xspace}\n';
done

printf '\n'
