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