author | wenzelm |
Thu, 09 Oct 1997 15:06:49 +0200 | |
changeset 3822 | a17f9b8dca93 |
parent 3329 | 7b43a1e74930 |
child 4163 | a42fc09bca25 |
permissions | -rwxr-xr-x |
3329
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
1 |
#! /usr/bin/perl -pi~~ |
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 |
|
3329
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
6 |
# [Tabs are forbidden in strings. Use "expand" or "untabify" in emacs".] |
0 | 7 |
# |
8 |
# Usage: |
|
9 |
# expandshort FILE1 ... FILEn |
|
10 |
# |
|
819 | 11 |
#Renames old versions of the files as FILE1~~ ... FILEn~~ |
0 | 12 |
# |
3329
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
13 |
s/\bby\(/by (/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
14 |
s/\bba\b *(\d+);/by (assume_tac \1);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
15 |
s/\bbr\b *([^;]*) (\d+);/by (rtac \1 \2);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
16 |
s/\bbrs\b *([^;]*) (\d+);/by (resolve_tac \1 \2);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
17 |
s/\bbd\b *([^;]*) (\d+);/by (dtac \1 \2);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
18 |
s/\bbds\b *([^;]*) (\d+);/by (dresolve_tac \1 \2);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
19 |
s/\bbe\b *([^;]*) (\d+);/by (etac \1 \2);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
20 |
s/\bbes\b *([^;]*) (\d+);/by (eresolve_tac \1 \2);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
21 |
s/\bbw\b *([^;]*);/by (rewtac \1);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
22 |
s/\bbws\b *([^;]*);/by (rewrite_goals_tac \1);/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
23 |
s/\bauto *\(\)/by (Auto_tac())/; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
24 |
s/dresolve_tac *\[(\w+)\] */dtac \1 /g; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
25 |
s/eresolve_tac *\[(\w+)\] */etac \1 /g; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
26 |
s/resolve_tac *\[(\w+)\] */rtac \1 /g; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
27 |
s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac \1\2/g; |
7b43a1e74930
Now a Perl script. No longer requires commands to be at the beginnings of
paulson
parents:
3022
diff
changeset
|
28 |
s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac \1 /g; |