src/Tools/expandshort
author paulson
Fri, 19 Jan 1996 16:00:22 +0100
changeset 1445 887e9816eea4
parent 819 8928f1c44d80
child 1567 02bbdc811ae7
permissions -rwxr-xr-x
Now expands TABS as well
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
#! /bin/sh
819
8928f1c44d80 Added comments and Id: marker.
lcp
parents: 96
diff changeset
     2
# $Id$
8928f1c44d80 Added comments and Id: marker.
lcp
parents: 96
diff changeset
     3
#Shell script to expand shorthand goal commands
0
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
1445
887e9816eea4 Now expands TABS as well
paulson
parents: 819
diff changeset
     6
#  ALSO expands tabs, since they are now forbidden in strings.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
# Usage:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
#    expandshort FILE1 ... FILEn
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
#
819
8928f1c44d80 Added comments and Id: marker.
lcp
parents: 96
diff changeset
    11
#Renames old versions of the files as FILE1~~ ... FILEn~~
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
#
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
for f in $*
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
do
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
echo Expanding shorthands in $f. \ Backup file is $f~~
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
mv $f $f~~; sed -e '
96
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    17
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
    18
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
    19
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
    20
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
    21
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
    22
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
    23
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
    24
s/^bw \([^;]*\);/by (rewtac \1);/
91e8875e9c45 now forbids semicolons in the body of br, etc. No longer
lcp
parents: 0
diff changeset
    25
s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
1445
887e9816eea4 Now expands TABS as well
paulson
parents: 819
diff changeset
    30
' $f~~ | expand > $f
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
done
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
echo Finished.