equal
deleted
inserted
replaced
|
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. |