0
|
1 |
#! /bin/sh
|
819
|
2 |
# $Id$
|
|
3 |
#Shell script to expand shorthand goal commands
|
0
|
4 |
# ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
|
|
5 |
# rewrite_goals_tac on 1-element lists
|
1445
|
6 |
# ALSO expands tabs, since they are now forbidden in strings.
|
0
|
7 |
#
|
|
8 |
# Usage:
|
|
9 |
# expandshort FILE1 ... FILEn
|
|
10 |
#
|
819
|
11 |
#Renames old versions of the files as FILE1~~ ... FILEn~~
|
0
|
12 |
#
|
|
13 |
for f in $*
|
|
14 |
do
|
|
15 |
echo Expanding shorthands in $f. \ Backup file is $f~~
|
2232
|
16 |
if [ ! -s $f ]; then echo "File $f is EMPTY!!"; exit 1; fi
|
0
|
17 |
mv $f $f~~; sed -e '
|
2062
|
18 |
s/\<by(/by (/
|
|
19 |
s/\<ba \([0-9][0-9]*\);/by (assume_tac \1);/
|
|
20 |
s/\<br \([^;]*\) \([0-9][0-9]*\);/by (rtac \1 \2);/
|
|
21 |
s/\<brs \([^;]*\) \([0-9][0-9]*\);/by (resolve_tac \1 \2);/
|
|
22 |
s/\<bd \([^;]*\) \([0-9][0-9]*\);/by (dtac \1 \2);/
|
|
23 |
s/\<bds \([^;]*\) \([0-9][0-9]*\);/by (dresolve_tac \1 \2);/
|
|
24 |
s/\<be \([^;]*\) \([0-9][0-9]*\);/by (etac \1 \2);/
|
|
25 |
s/\<bes \([^;]*\) \([0-9][0-9]*\);/by (eresolve_tac \1 \2);/
|
|
26 |
s/\<bw \([^;]*\);/by (rewtac \1);/
|
|
27 |
s/\<bws \([^;]*\);/by (rewrite_goals_tac \1);/
|
2232
|
28 |
s/\<auto *()/by (Auto_tac())/
|
0
|
29 |
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
|
|
30 |
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
|
|
31 |
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
|
|
32 |
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
|
2041
|
33 |
s/rtac *(\([a-zA-Z0-9_]*\) *RS *ssubst) */stac \1 /g
|
1445
|
34 |
' $f~~ | expand > $f
|
0
|
35 |
done
|
|
36 |
echo Finished.
|