expandshort

Declares the function exit_use to behave like use but fail if
errors are detected. It can be used in all Makefiles except Pure, which will
write the exception handler explicitly ("exit" will have been declared
already).

#! /bin/sh
#
#expandshort - shell script to expand shorthand goal commands
#  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
#     rewrite_goals_tac on 1-element lists
#
# Usage:
#    expandshort FILE1 ... FILEn
#
#  leaves previous versions as XXX~~
#
for f in $*
do
echo Expanding shorthands in $f. \ Backup file is $f~~
mv $f $f~~; sed -e '
s/^ba \([0-9]*\);/by (assume_tac \1);/
s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/
s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/
s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/
s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/
s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/
s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/
s/^bw \([^;]*\);/by (rewtac \1);/
s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
' $f~~ > $f
done
echo Finished.