| author | lcp |
| Tue, 09 Nov 1993 11:02:01 +0100 | |
| changeset 96 | 91e8875e9c45 |
| parent 0 | a5a9c433f639 |
| child 819 | 8928f1c44d80 |
| permissions | -rwxr-xr-x |
| clasohm@0 | 1 |
#! /bin/sh |
| clasohm@0 | 2 |
# |
| clasohm@0 | 3 |
#expandshort - shell script to expand shorthand goal commands |
| clasohm@0 | 4 |
# ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
| clasohm@0 | 5 |
# rewrite_goals_tac on 1-element lists |
| clasohm@0 | 6 |
# |
| clasohm@0 | 7 |
# Usage: |
| clasohm@0 | 8 |
# expandshort FILE1 ... FILEn |
| clasohm@0 | 9 |
# |
| clasohm@0 | 10 |
# leaves previous versions as XXX~~ |
| clasohm@0 | 11 |
# |
| clasohm@0 | 12 |
for f in $* |
| clasohm@0 | 13 |
do |
| clasohm@0 | 14 |
echo Expanding shorthands in $f. \ Backup file is $f~~ |
| clasohm@0 | 15 |
mv $f $f~~; sed -e ' |
| lcp@96 | 16 |
s/^ba \([0-9]*\);/by (assume_tac \1);/ |
| lcp@96 | 17 |
s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/ |
| lcp@96 | 18 |
s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/ |
| lcp@96 | 19 |
s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/ |
| lcp@96 | 20 |
s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/ |
| lcp@96 | 21 |
s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/ |
| lcp@96 | 22 |
s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/ |
| lcp@96 | 23 |
s/^bw \([^;]*\);/by (rewtac \1);/ |
| lcp@96 | 24 |
s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/ |
| clasohm@0 | 25 |
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g |
| clasohm@0 | 26 |
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g |
| clasohm@0 | 27 |
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g |
| clasohm@0 | 28 |
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g |
| clasohm@0 | 29 |
' $f~~ > $f |
| clasohm@0 | 30 |
done |
| clasohm@0 | 31 |
echo Finished. |