#! /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.