expandshort
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16 ago)
changeset 0 a5a9c433f639
child 96 91e8875e9c45
permissions -rwxr-xr-x
Initial revision
clasohm@0
     1
#! /bin/sh
clasohm@0
     2
#
clasohm@0
     3
#expandshort - shell script to expand shorthand goal commands
clasohm@0
     4
#  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
clasohm@0
     5
#     rewrite_goals_tac on 1-element lists
clasohm@0
     6
#
clasohm@0
     7
# Usage:
clasohm@0
     8
#    expandshort FILE1 ... FILEn
clasohm@0
     9
#
clasohm@0
    10
#  leaves previous versions as XXX~~
clasohm@0
    11
#
clasohm@0
    12
for f in $*
clasohm@0
    13
do
clasohm@0
    14
echo Expanding shorthands in $f. \ Backup file is $f~~
clasohm@0
    15
mv $f $f~~; sed -e '
clasohm@0
    16
s/^ba \([0-9]*\); *$/by (assume_tac \1);/
clasohm@0
    17
s/^br \(.*\) \([0-9]*\); *$/by (rtac \1 \2);/
clasohm@0
    18
s/^brs \(.*\) \([0-9]*\); *$/by (resolve_tac \1 \2);/
clasohm@0
    19
s/^bd \(.*\) \([0-9]*\); *$/by (dtac \1 \2);/
clasohm@0
    20
s/^bds \(.*\) \([0-9]*\); *$/by (dresolve_tac \1 \2);/
clasohm@0
    21
s/^be \(.*\) \([0-9]*\); *$/by (etac \1 \2);/
clasohm@0
    22
s/^bes \(.*\) \([0-9]*\); *$/by (eresolve_tac \1 \2);/
clasohm@0
    23
s/^bw \(.*\); *$/by (rewtac \1);/
clasohm@0
    24
s/^bws \(.*\); *$/by (rewrite_goals_tac \1);/
clasohm@0
    25
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
clasohm@0
    26
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
clasohm@0
    27
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
clasohm@0
    28
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
clasohm@0
    29
' $f~~ > $f
clasohm@0
    30
done
clasohm@0
    31
echo Finished.