expandshort
author lcp
Thu, 15 Dec 1994 11:08:22 +0100
changeset 790 4c10e8532d43
parent 96 91e8875e9c45
permissions -rwxr-xr-x
qconverse_qconverse, qconverse_prod: renamed from qconverse_of_qconverse, qconverse_of_prod
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
#! /bin/sh
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
#expandshort - shell script to expand shorthand goal commands
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
#  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
#     rewrite_goals_tac on 1-element lists
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
# Usage:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
#    expandshort FILE1 ... FILEn
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
#  leaves previous versions as XXX~~
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
for f in $*
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
do
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
echo Expanding shorthands in $f. \ Backup file is $f~~
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
mv $f $f~~; sed -e '
96
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    16
s/^ba \([0-9]*\);/by (assume_tac \1);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    17
s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    18
s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    19
s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    20
s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    21
s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    22
s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    23
s/^bw \([^;]*\);/by (rewtac \1);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    24
s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
' $f~~ > $f
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
done
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
echo Finished.