expandshort
author nipkow
Tue, 09 May 1995 22:10:08 +0200
changeset 1114 c8dfb56a7e95
parent 96 91e8875e9c45
permissions -rwxr-xr-x
Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.
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.